Diffusion afp-devel 4eef94bbdc16

merge from afp-2019
4eef94bbdc16
Actions

Tags

None

Subscribers

None

Description

merge from afp-2019

Details

Provenance

Authored on

Parents

rAFP1c0ae055c848: New entry Generic_Join
rAFPe783400723b7: merged

Branches

Unknown

Tags

Unknown

Event Timeline

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

e783400723b7 merged
Author
nipkow
Browse Repository
No Builds
No Audits
0291608f6cee adjusted to devel
Author
nipkow
Browse Repository
No Builds
No Audits
a2c03373dc20 Implement equivalence relation with unfolding for LTL Master Theorem
Author
Benedikt Seidl <benedikt.seidl@tum.de>
Browse Repository
No Builds
No Audits
db7040379c22 Proof of Restricted Master Theorem on LTL
Author
Benedikt Seidl <benedikt.seidl@tum.de>
Browse Repository
No Builds
No Audits
ef5c588d2a90 Patched some failing proofs
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
f807a036febc transfer of a few results to the main Analysis library
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
35d7fb94ba43 fixed a bunch of failing proofs
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
ea6d19f95b3c renamings
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
bdb8fdb29abb A couple of theorems transferred to the main libraries
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
6e0f3f3f40d8 Mostly qualification by Henstock_Kurzweil_Integration.
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
90d5a4d124ca Elimination of a theorem synonym
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
d874707a9cd2 proper metadata format;
Author
makarius
Browse Repository
No Builds
No Audits
28e85601e0b6 updated metadata
Author
Christian Sternagel <c.sternagel@gmail.com>
Browse Repository
No Builds
No Audits
98320942654a tuned -- no duplicates;
Author
makarius
Browse Repository
No Builds
No Audits
185d92535c7d merged
Author
makarius
Browse Repository
No Builds
No Audits
48532c37dc2a clarified session setup -- proper document variants;
Author
makarius
Browse Repository
No Builds
No Audits
addaddcb957f minor updates to Stone_Algebras and Stone_Kleene_Relation_Algebras
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
863519ae0ea9 non-overlapping diretory Examples/ICF;
Author
makarius
Browse Repository
No Builds
No Audits
273de6cb6c51 clarified session directories and theory imports;
Author
makarius
Browse Repository
No Builds
No Audits
0d068cd791af clarified session directories and theory imports;
Author
makarius
Browse Repository
No Builds
No Audits
5786f7df9dd8 clarified session directories and theory imports;
Author
makarius
Browse Repository
No Builds
No Audits
e97ee9322827 declare session directories;
Author
makarius
Browse Repository
No Builds
No Audits
8934bbd2f1c6 tuned syntax;
Author
makarius
Browse Repository
No Builds
No Audits
4dd1561aba40 clarified session directories;
Author
makarius
Browse Repository
No Builds
No Audits
d97b1078fc97 clarified session directories;
Author
makarius
Browse Repository
No Builds
No Audits
98b3857f87e4 clarified session directories;
Author
makarius
Browse Repository
No Builds
No Audits
6f26aeb7cac5 clarified session directories;
Author
makarius
Browse Repository
No Builds
No Audits
cc90f69da461 clarified session directories;
Author
makarius
Browse Repository
No Builds
No Audits
1cf4d6f4de8e non-executable source files;
Author
makarius
Browse Repository
No Builds
No Audits
838a646468c7 clarified session directories;
Author
makarius
Browse Repository
No Builds
No Audits
1fa9b1612d09 added missing session entry in ROOT file
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
a161f739abbd condensed proof by using real_asymp
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
49f30bdba77d more selective import
Author
immler
Browse Repository
No Builds
No Audits
6f6333e5bb57 O_E_S -> M_A
Author
nipkow
Browse Repository
No Builds
No Audits
515130b31ce9 Ordered_Euclidean_Space -> Multivariate_Analysis
Author
nipkow
Browse Repository
No Builds
No Audits
130a0b12717f more selective Analysis imports
Author
nipkow
Browse Repository
No Builds
No Audits
da6facaa5cc2 Implement hashing for minimal dnf of LTL formulas
Author
Benedikt Seidl <benedikt.seidl@tum.de>
Browse Repository
No Builds
No Audits
35dd623fcfc1 merged
Author
immler
Browse Repository
No Builds
No Audits
7f0e4780e5b6 Multivariate_Analysis as (tentative) canonical entry point
Author
immler
Browse Repository
No Builds
No Audits
9cbc0558e973 more selective imports
Author
immler <immler@in.tum.de>
Browse Repository
No Builds
No Audits
e2a39a672da2 tuned Analysis imports
Author
nipkow
Browse Repository
No Builds
No Audits
770bcb8c1b45 fixed imports
Author
nipkow
Browse Repository
No Builds
No Audits
15104e7c4d12 merged
Author
nipkow
Browse Repository
No Builds
No Audits
c27732cff594 more selective imports
Author
nipkow
Browse Repository
No Builds
No Audits
6f1812b8554b more selective imports
Author
nipkow
Browse Repository
No Builds
No Audits
9930bc379f7a more selective imports
Author
nipkow
Browse Repository
No Builds
No Audits
451b5fe9a693 more selective imports
Author
nipkow
Browse Repository
No Builds
No Audits
ce9f129e8a6a selective Analysis imports
Author
nipkow
Browse Repository
No Builds
No Audits
34c60acbf2ac minimized imports
Author
nipkow
Browse Repository
No Builds
No Audits
bb7599abb933 tuned imports
Author
nipkow
Browse Repository
No Builds
No Audits

Changes (648)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

admin/

metadata/

templates/

Adaptive_State_Counting

ASC_Example.thy

ASC_Sufficiency.thy

FSM_Product.thy

C2KA_DistributedSystems

Communication_C2KA.thy

Topology_C2KA.thy

Fourier_Aux1.thy

Fourier_Aux2.thy

Square_Integrable.thy

Examples_Join.thy

Generic_Join.thy

Generic_Join_Correctness.thy

Hybrid_Systems_VCs

HS_Preliminaries.thy

HS_VC_Examples.thy

HS_VC_Spartan.thy

ModalKleeneAlgebra

HS_VC_MKA_Examples_ndfun.thy

HS_VC_MKA_Examples_rel.thy

HS_VC_MKA_ndfun.thy

HS_VC_MKA_rel.thy

PredicateTransformers

HS_VC_PT_Examples.thy

Jacobson_Basic_Algebra

Group_Theory.thy

Ring_Theory.thy

LLL_Factorization/

LLL_Factorization.thy

Laplace_Transform

Laplace_Transform.thy

Laplace_Transform_Library.thy

Lerch_Lemma.thy

Piecewise_Continuous.thy

Stellar_Quorums

Stellar_Quorums.thy

Config_Morphisms.thy

Corecursive_Prop.thy

Denotational.thy

Hygge_Theory.thy

Introduction.thy

Operational.thy

StutteringDefs.thy

StutteringLemmas.thy

SymbolicPrimitive.thy

tools/

afp_check_roots.scala

Abortable_Linearizable_Modules.html

Abs_Int_ITP2012.html

Abstract-Hoare-Logics.html

Abstract-Rewriting.html

Abstract_Completeness.html

Abstract_Soundness.html

Adaptive_State_Counting.html

Affine_Arithmetic.html

Aggregation_Algebras.html

Akra_Bazzi.html

Algebraic_Numbers.html

Algebraic_VCs.html

Allen_Calculus.html

Amortized_Complexity.html

Applicative_Lifting.html

Architectural_Design_Patterns.html

ArrowImpossibilityGS.html

Auto2_Imperative_HOL.html

AutoFocus-Stream.html

Automatic_Refinement.html

AxiomaticCategoryTheory.html

BNF_Operations.html

Bell_Numbers_Spivey.html

Berlekamp_Zassenhaus.html

Bertrands_Postulate.html

BinarySearchTree.html

Binding_Syntax_Theory.html

Binomial-Heaps.html

Binomial-Queues.html

Boolean_Expression_Checkers.html

Bounded_Deducibility_Security.html

Buchi_Complementation.html

Budan_Fourier.html

Buffons_Needle.html

BytecodeLogicJmlTypes.html

C2KA_DistributedSystems.html

CAVA_Automata.html

CAVA_LTL_Modelchecker.html

CISC-Kernel.html

CakeML_Codegen.html

Call_Arity.html

Card_Equiv_Relations.html

Card_Multisets.html

Card_Number_Partitions.html

Card_Partitions.html

Case_Labeling.html

Catalan_Numbers.html

Cayley_Hamilton.html

Certification_Monads.html

Chord_Segments.html

ClockSynchInst.html

Coinductive.html

Coinductive_Languages.html

Collections.html

Comparison_Sort_Lower_Bound.html

Compiling-Exceptions-Correctly.html

Complete_Non_Orders.html

Completeness.html

ComponentDependencies.html

ConcurrentGC.html

ConcurrentIMP.html

Concurrent_Ref_Alg.html

Concurrent_Revisions.html

Consensus_Refined.html

Constructive_Cryptography.html

Constructor_Funs.html

Containers.html

Count_Complex_Roots.html

CryptoBasedCompositionalProperties.html

DFS_Framework.html

DPT-SAT-Solver.html

DataRefinementIBP.html

Datatype_Order_Generator.html

Decl_Sem_Fun_PL.html

Decreasing-Diagrams-II.html

Decreasing-Diagrams.html

Deep_Learning.html

Density_Compiler.html

Dependent_SIFUM_Refinement.html

Dependent_SIFUM_Type_Systems.html

Depth-First-Search.html

Derangements.html

Descartes_Sign_Rule.html

Dict_Construction.html

Differential_Dynamic_Logic.html

Differential_Game_Logic.html

Dijkstra_Shortest_Path.html

Diophantine_Eqns_Lin_Hom.html

Dirichlet_L.html

Dirichlet_Series.html

DiscretePricing.html

Discrete_Summation.html

DynamicArchitectures.html

Dynamic_Tables.html

E_Transcendental.html

Echelon_Form.html

EdmondsKarp_Maxflow.html

Efficient-Mergesort.html

Elliptic_Curves_Group_Law.html

Encodability_Process_Calculi.html

Epistemic_Logic.html

Ergodic_Theory.html

Error_Function.html

Euler_MacLaurin.html

Euler_Partition.html

Example-Submission.html

FOL-Fitting.html

FOL_Harrison.html

FOL_Seq_Calc1.html

Factored_Transition_System_Bounding.html

Falling_Factorial_Sum.html

FeatherweightJava.html

Featherweight_OCL.html

FileRefinement.html

Finger-Trees.html

Finite_Automata_HF.html

First_Order_Terms.html

First_Welfare_Theorem.html

Fishburn_Impossibility.html

Fisher_Yates.html

Flow_Networks.html

Floyd_Warshall.html

Flyspeck-Tame.html

FocusStreamsCaseStudies.html

Formal_SSA.html

Formula_Derivatives.html

Free-Boolean-Algebra.html

Free-Groups.html

FunWithFunctions.html

FunWithTilings.html

Functional-Automata.html

Functional_Ordered_Resolution_Prover.html

GPU_Kernel_PL.html

Game_Based_Crypto.html

Gauss-Jordan-Elim-Fun.html

Gauss_Jordan.html

General-Triangle.html

Generic_Deriving.html

Generic_Join.html

GewirthPGCProof.html

Girth_Chromatic.html

GraphMarkingIBP.html

Graph_Saturation.html

Graph_Theory.html

Groebner_Bases.html

Groebner_Macaulay.html

Gromov_Hyperbolicity.html

Group-Ring-Module.html

HOLCF-Prelude.html

HRB-Slicing.html

HereditarilyFinite.html

Hidden_Markov_Models.html

Higher_Order_Terms.html

Hoare_Time.html

HotelKeyCards.html

Hybrid_Multi_Lane_Spatial_Logic.html

Hybrid_Systems_VCs.html

IEEE_Floating_Point.html

IMP2_Binary_Heap.html

IP_Addresses.html

Imperative_Insertion_Sort.html

Impossible_Geometry.html

Incompleteness.html

Incredible_Proof_Machine.html

Inductive_Confidentiality.html

InfPathElimination.html

InformationFlowSlicing.html

InformationFlowSlicing_Inter.html

Integration.html

Iptables_Semantics.html

Irrationality_J_Hancl.html

Isabelle_Meta_Model.html

Jacobson_Basic_Algebra.html

JinjaThreads.html

JiveDataStoreModel.html

Jordan_Hoelder.html

Jordan_Normal_Form.html

KAT_and_DRA.html

Key_Agreement_Strong_Adversaries.html

Kleene_Algebra.html

Knot_Theory.html

Knuth_Morris_Pratt.html

Koenigsberg_Friendship.html

Kuratowski_Closure_Complement.html

LLL_Basis_Reduction.html

LLL_Factorization.html

LTL_Master_Theorem.html

LTL_to_DRA.html

LTL_to_GBA.html

Lam-ml-Normalization.html

LambdaAuth.html

Lambda_Free_EPO.html

Lambda_Free_KBOs.html

Lambda_Free_RPOs.html

Landau_Symbols.html

Laplace_Transform.html

Latin_Square.html

LatticeProperties.html

Launchbury.html

Lazy-Lists-II.html

Lifting_Definition_Option.html

LightweightJava.html

LinearQuantifierElim.html

Linear_Inequalities.html

Linear_Recurrences.html

Liouville_Numbers.html

List-Index.html

List-Infinite.html

List_Interleaving.html

List_Inversions.html

List_Update.html

LocalLexing.html

Localization_Ring.html

Locally-Nameless-Sigma.html

Lowe_Ontological_Argument.html

Lower_Semicontinuous.html

MFMC_Countable.html

MFOTL_Monitor.html

MSO_Regex_Equivalence.html

Markov_Models.html

Mason_Stothers.html

Matrix_Tensor.html

Max-Card-Matching.html

Median_Of_Medians_Selection.html

Minimal_SSA.html

Minkowskis_Theorem.html

Minsky_Machines.html

Modal_Logics_for_NTS.html

Modular_Assembly_Kit_Security.html

Monad_Memo_DP.html

Monad_Normalisation.html

MonoBoolTranAlgebra.html

MonoidalCategory.html

Monomorphic_Monad.html

MuchAdoAboutTwo.html

Multi_Party_Computation.html

Multirelations.html

Myhill-Nerode.html

Name_Carrying_Type_Inference.html

Nat-Interval-Logic.html

Native_Word.html

Nested_Multisets_Ordinals.html

Network_Security_Policy_Verification.html

Neumann_Morgenstern_Utility.html

No_FTL_observers.html

Noninterference_CSP.html

Noninterference_Concurrent_Composition.html

Noninterference_Generic_Unwinding.html

Noninterference_Inductive_Unwinding.html

Noninterference_Ipurge_Unwinding.html

Noninterference_Sequential_Composition.html

NormByEval.html

Nullstellensatz.html

Open_Induction.html

Optimal_BST.html

Orbit_Stabiliser.html

Order_Lattice_Props.html

Ordered_Resolution_Prover.html

Ordinals_and_Cardinals.html

Ordinary_Differential_Equations.html

POPLmark-deBruijn.html

PSemigroupsConvolution.html

Pairing_Heap.html

Paraconsistency.html

Parity_Game.html

Partial_Function_MR.html

Partial_Order_Reduction.html

Password_Authentication_Protocol.html

Perfect-Number-Thm.html

Perron_Frobenius.html

Pi_Calculus.html

Pi_Transcendental.html

Planarity_Certificates.html

Polynomial_Factorization.html

Polynomial_Interpolation.html

Polynomials.html

Pop_Refinement.html

Posix-Lexing.html

Possibilistic_Noninterference.html

Pratt_Certificate.html

Presburger-Automata.html

Prim_Dijkstra_Simple.html

Prime_Distribution_Elementary.html

Prime_Harmonic_Series.html

Prime_Number_Theorem.html

Priority_Queue_Braun.html

Priority_Search_Trees.html

Probabilistic_Noninterference.html

Probabilistic_Prime_Tests.html

Probabilistic_System_Zoo.html

Probabilistic_Timed_Automata.html

Probabilistic_While.html

Program-Conflict-Analysis.html

Projective_Geometry.html

Proof_Strategy_Language.html

Propositional_Proof_Systems.html

Prpu_Maxflow.html

PseudoHoops.html

Psi_Calculi.html

Ptolemys_Theorem.html

QR_Decomposition.html

Quaternions.html

Quick_Sort_Cost.html

RIPEMD-160-SPARK.html

Ramsey-Infinite.html

Random_BSTs.html

Random_Graph_Subgraph_Threshold.html

Randomised_BSTs.html

Randomised_Social_Choice.html

Rank_Nullity_Theorem.html

Recursion-Theory-I.html

Refine_Imperative_HOL.html

Refine_Monadic.html

RefinementReactive.html

Regex_Equivalence.html

Regular-Sets.html

Regular_Algebras.html

Relation_Algebra.html

Rep_Fin_Groups.html

Residuated_Lattices.html

Resolution_FOL.html

Rewriting_Z.html

Ribbon_Proofs.html

Robbins-Conjecture.html

Root_Balanced_Tree.html

Roy_Floyd_Warshall.html

SATSolverVerification.html

SDS_Impossibility.html

SIFUM_Type_Systems.html

Secondary_Sylow.html

Security_Protocol_Refinement.html

Selection_Heap_Sort.html

SenSocialChoice.html

Separation_Algebra.html

Separation_Logic_Imperative_HOL.html

SequentInvertibility.html

Shivers-CFA.html

ShortestPath.html

Signature_Groebner.html

Simple_Firewall.html

Smooth_Manifolds.html

Sort_Encodings.html

Source_Coding_Theorem.html

Special_Function_Bounds.html

Splay_Tree.html

Sqrt_Babylonian.html

Stable_Matching.html

Statecharts.html

Stellar_Quorums.html

Stern_Brocot.html

Stewart_Apollonius.html

Stirling_Formula.html

Stochastic_Matrices.html

Stone_Algebras.html

Stone_Kleene_Relation_Algebras.html

Stone_Relation_Algebras.html

Store_Buffer_Reduction.html

Stream-Fusion.html

Stream_Fusion_Code.html

Strong_Security.html

Sturm_Sequences.html

Sturm_Tarski.html

Stuttering_Equivalence.html

Subresultants.html

SumSquares.html

Surprise_Paradox.html

Symmetric_Polynomials.html

TESL_Language.html

Tail_Recursive_Functions.html

Tarskis_Geometry.html

Taylor_Models.html

Timed_Automata.html

TortoiseHare.html

Transcendence_Series_Hancl_Rucki.html

Transformer_Semantics.html

Transition_Systems_and_Automata.html

Transitive-Closure-II.html

Transitive-Closure.html

Tree-Automata.html

Tree_Decomposition.html

Twelvefold_Way.html

Types_Tableaus_and_Goedels_God.html

UPF_Firewall.html

Universal_Turing_Machine.html

UpDown_Scheme.html

VectorSpace.html

Verified-Prover.html

VerifyThis2018.html

Vickrey_Clarke_Groves.html

VolpanoSmith.html

WHATandWHERE_Security.html

WebAssembly.html

Weight_Balanced_Trees.html

Well_Quasi_Orders.html

Winding_Number_Eval.html

WorkerWrapper.html

Zeta_Function.html

images/

statistics.html

submitting.html

rAFP4eef94bbdc16

admin/publish

metadata/metadata

metadata/templates/base.tpl

thys/Adaptive_State_Counting/ASC/ASC_Example.thy

thys/Adaptive_State_Counting/ASC/ASC_Hoare.thy

thys/Adaptive_State_Counting/ASC/ASC_LB.thy

thys/Adaptive_State_Counting/ASC/ASC_Sufficiency.thy

thys/Adaptive_State_Counting/ASC/ASC_Suite.thy

thys/Adaptive_State_Counting/ATC/ATC.thy

thys/Adaptive_State_Counting/FSM/FSM.thy

thys/Adaptive_State_Counting/FSM/FSM_Product.thy

thys/Adaptive_State_Counting/ROOT

thys/Adaptive_State_Counting/document/root.bib

thys/Adaptive_State_Counting/document/root.tex

thys/C2KA_DistributedSystems/C2KA.thy

thys/C2KA_DistributedSystems/CKA.thy

thys/C2KA_DistributedSystems/Communication_C2KA.thy

thys/C2KA_DistributedSystems/ROOT

thys/C2KA_DistributedSystems/Stimuli.thy

thys/C2KA_DistributedSystems/Topology_C2KA.thy

thys/C2KA_DistributedSystems/document/root.bib

thys/C2KA_DistributedSystems/document/root.tex

thys/FOL_Seq_Calc1/Common.thy

thys/FOL_Seq_Calc1/ROOT

thys/FOL_Seq_Calc1/Sequent.thy

thys/FOL_Seq_Calc1/Tableau.thy

thys/FOL_Seq_Calc1/document/root.bib

thys/FOL_Seq_Calc1/document/root.tex

thys/Fourier/Confine.thy

thys/Fourier/Fourier.thy

thys/Fourier/Fourier_Aux1.thy

thys/Fourier/Fourier_Aux2.thy

thys/Fourier/Lspace.thy

thys/Fourier/Periodic.thy

thys/Fourier/ROOT

thys/Fourier/Square_Integrable.thy

thys/Fourier/document/root.tex

thys/Generic_Join/Examples_Join.thy

thys/Generic_Join/Generic_Join.thy

thys/Generic_Join/Generic_Join_Correctness.thy

thys/Generic_Join/ROOT

thys/Generic_Join/document/root.bib

thys/Generic_Join/document/root.tex

thys/Hybrid_Systems_VCs/HS_ODEs.thy

thys/Hybrid_Systems_VCs/HS_Preliminaries.thy

thys/Hybrid_Systems_VCs/HS_VC_Examples.thy

thys/Hybrid_Systems_VCs/HS_VC_Spartan.thy

thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA_Examples_ndfun.thy

thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA_Examples_rel.thy

thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA_ndfun.thy

thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA_rel.thy

thys/Hybrid_Systems_VCs/PredicateTransformers/HS_VC_PT.thy

thys/Hybrid_Systems_VCs/PredicateTransformers/HS_VC_PT_Examples.thy

thys/Hybrid_Systems_VCs/ROOT

thys/Hybrid_Systems_VCs/document/root.bib

thys/Hybrid_Systems_VCs/document/root.tex

thys/IMO2019/IMO2019_Q1.thy

thys/IMO2019/IMO2019_Q4.thy

thys/IMO2019/IMO2019_Q5.thy

thys/IMO2019/ROOT

thys/IMO2019/document/root.bib

thys/IMO2019/document/root.tex

thys/Jacobson_Basic_Algebra/Group_Theory.thy

thys/Jacobson_Basic_Algebra/ROOT

thys/Jacobson_Basic_Algebra/Ring_Theory.thy

thys/Jacobson_Basic_Algebra/Set_Theory.thy

thys/Jacobson_Basic_Algebra/document/root.bib

thys/Jacobson_Basic_Algebra/document/root.tex

thys/LLL_Factorization/LLL_Factorization.thy

thys/Laplace_Transform/Existence.thy

thys/Laplace_Transform/Laplace_Transform.thy

thys/Laplace_Transform/Laplace_Transform_Library.thy

thys/Laplace_Transform/Lerch_Lemma.thy

thys/Laplace_Transform/Piecewise_Continuous.thy

thys/Laplace_Transform/ROOT

thys/Laplace_Transform/Uniqueness.thy

thys/Laplace_Transform/document/root.bib

thys/Laplace_Transform/document/root.tex

thys/ROOTS

thys/Stellar_Quorums/ROOT

thys/Stellar_Quorums/Stellar_Quorums.thy

thys/Stellar_Quorums/document/root.bib

thys/Stellar_Quorums/document/root.tex

thys/Szpilrajn/ROOT

thys/Szpilrajn/Szpilrajn.thy

thys/Szpilrajn/document/root.bib

thys/Szpilrajn/document/root.tex

thys/TESL_Language/Config_Morphisms.thy

thys/TESL_Language/Corecursive_Prop.thy

thys/TESL_Language/Denotational.thy

thys/TESL_Language/Hygge_Theory.thy

thys/TESL_Language/Introduction.thy

thys/TESL_Language/Operational.thy

thys/TESL_Language/ROOT

thys/TESL_Language/Run.thy

thys/TESL_Language/Stuttering.thy

thys/TESL_Language/StutteringDefs.thy

thys/TESL_Language/StutteringLemmas.thy

thys/TESL_Language/SymbolicPrimitive.thy

thys/TESL_Language/TESL.thy

thys/TESL_Language/document/figures/dilating.pdf

thys/TESL_Language/document/figures/dilating.tex

thys/TESL_Language/document/figures/glue.pdf

thys/TESL_Language/document/root.bib

thys/TESL_Language/document/root.tex

tools/afp_check_roots.scala

web/about.html

web/citing.html

web/download.html

web/entries/AODV.html

web/entries/AVL-Trees.html

web/entries/AWN.html

web/entries/Abortable_Linearizable_Modules.html

web/entries/Abs_Int_ITP2012.html

web/entries/Abstract-Hoare-Logics.html

web/entries/Abstract-Rewriting.html

web/entries/Abstract_Completeness.html

web/entries/Abstract_Soundness.html

web/entries/Adaptive_State_Counting.html

web/entries/Affine_Arithmetic.html

web/entries/Aggregation_Algebras.html

web/entries/Akra_Bazzi.html

web/entries/Algebraic_Numbers.html

web/entries/Algebraic_VCs.html

web/entries/Allen_Calculus.html

web/entries/Amortized_Complexity.html

web/entries/AnselmGod.html

web/entries/Applicative_Lifting.html

web/entries/Architectural_Design_Patterns.html

web/entries/ArrowImpossibilityGS.html

web/entries/Auto2_HOL.html

web/entries/Auto2_Imperative_HOL.html

web/entries/AutoFocus-Stream.html

web/entries/Automatic_Refinement.html

web/entries/AxiomaticCategoryTheory.html

web/entries/BDD.html

web/entries/BNF_CC.html

web/entries/BNF_Operations.html

web/entries/Bell_Numbers_Spivey.html

web/entries/Berlekamp_Zassenhaus.html

web/entries/Bernoulli.html

web/entries/Bertrands_Postulate.html

web/entries/BinarySearchTree.html

web/entries/Binding_Syntax_Theory.html

web/entries/Binomial-Heaps.html

web/entries/Binomial-Queues.html

web/entries/Bondy.html

web/entries/Boolean_Expression_Checkers.html

web/entries/Bounded_Deducibility_Security.html

web/entries/Buchi_Complementation.html

web/entries/Budan_Fourier.html

web/entries/Buffons_Needle.html

web/entries/Buildings.html

web/entries/BytecodeLogicJmlTypes.html

web/entries/C2KA_DistributedSystems.html

web/entries/CAVA_Automata.html

web/entries/CAVA_LTL_Modelchecker.html

web/entries/CCS.html

web/entries/CISC-Kernel.html

web/entries/CRDT.html

web/entries/CYK.html

web/entries/CakeML.html

web/entries/CakeML_Codegen.html

web/entries/Call_Arity.html

web/entries/Card_Equiv_Relations.html

web/entries/Card_Multisets.html

web/entries/Card_Number_Partitions.html

web/entries/Card_Partitions.html

web/entries/Cartan_FP.html

web/entries/Case_Labeling.html

web/entries/Catalan_Numbers.html

web/entries/Category.html

web/entries/Category2.html

web/entries/Category3.html

web/entries/Cauchy.html

web/entries/Cayley_Hamilton.html

web/entries/Certification_Monads.html

web/entries/Chord_Segments.html

web/entries/Circus.html

web/entries/ClockSynchInst.html

web/entries/CofGroups.html

web/entries/Coinductive.html

web/entries/Coinductive_Languages.html

web/entries/Collections.html

web/entries/Comparison_Sort_Lower_Bound.html

web/entries/Compiling-Exceptions-Correctly.html

web/entries/Complete_Non_Orders.html

web/entries/Completeness.html

web/entries/Complx.html

web/entries/ComponentDependencies.html

web/entries/ConcurrentGC.html

web/entries/ConcurrentIMP.html

web/entries/Concurrent_Ref_Alg.html

web/entries/Concurrent_Revisions.html

web/entries/Consensus_Refined.html

web/entries/Constructive_Cryptography.html

web/entries/Constructor_Funs.html

web/entries/Containers.html

web/entries/CoreC++.html

web/entries/Core_DOM.html

web/entries/Count_Complex_Roots.html

web/entries/CryptHOL.html

web/entries/CryptoBasedCompositionalProperties.html

web/entries/DFS_Framework.html

web/entries/DPT-SAT-Solver.html

web/entries/DataRefinementIBP.html

web/entries/Datatype_Order_Generator.html

web/entries/Decl_Sem_Fun_PL.html

web/entries/Decreasing-Diagrams-II.html

web/entries/Decreasing-Diagrams.html

web/entries/Deep_Learning.html

web/entries/Density_Compiler.html

web/entries/Dependent_SIFUM_Refinement.html

web/entries/Dependent_SIFUM_Type_Systems.html

web/entries/Depth-First-Search.html

web/entries/Derangements.html

web/entries/Deriving.html

web/entries/Descartes_Sign_Rule.html

web/entries/Dict_Construction.html

web/entries/Differential_Dynamic_Logic.html

web/entries/Differential_Game_Logic.html

web/entries/Dijkstra_Shortest_Path.html

web/entries/Diophantine_Eqns_Lin_Hom.html

web/entries/Dirichlet_L.html

web/entries/Dirichlet_Series.html

web/entries/DiscretePricing.html

web/entries/Discrete_Summation.html

web/entries/DiskPaxos.html

web/entries/DynamicArchitectures.html

web/entries/Dynamic_Tables.html

web/entries/E_Transcendental.html

web/entries/Echelon_Form.html

web/entries/EdmondsKarp_Maxflow.html

web/entries/Efficient-Mergesort.html

web/entries/Elliptic_Curves_Group_Law.html

web/entries/Encodability_Process_Calculi.html

web/entries/Epistemic_Logic.html

web/entries/Ergodic_Theory.html

web/entries/Error_Function.html

web/entries/Euler_MacLaurin.html

web/entries/Euler_Partition.html

web/entries/Example-Submission.html

web/entries/FFT.html

web/entries/FLP.html

web/entries/FOL-Fitting.html

web/entries/FOL_Harrison.html

web/entries/FOL_Seq_Calc1.html

web/entries/Factored_Transition_System_Bounding.html

web/entries/Falling_Factorial_Sum.html

web/entries/Farkas.html

web/entries/FeatherweightJava.html

web/entries/Featherweight_OCL.html

web/entries/Fermat3_4.html

web/entries/FileRefinement.html

web/entries/FinFun.html

web/entries/Finger-Trees.html

web/entries/Finite_Automata_HF.html

web/entries/First_Order_Terms.html

web/entries/First_Welfare_Theorem.html

web/entries/Fishburn_Impossibility.html

web/entries/Fisher_Yates.html

web/entries/Flow_Networks.html

web/entries/Floyd_Warshall.html

web/entries/Flyspeck-Tame.html

web/entries/FocusStreamsCaseStudies.html

web/entries/Formal_SSA.html

web/entries/Formula_Derivatives.html

web/entries/Fourier.html

web/entries/Free-Boolean-Algebra.html

web/entries/Free-Groups.html

web/entries/FunWithFunctions.html

web/entries/FunWithTilings.html

web/entries/Functional-Automata.html

web/entries/Functional_Ordered_Resolution_Prover.html

web/entries/GPU_Kernel_PL.html

web/entries/Gabow_SCC.html

web/entries/Game_Based_Crypto.html

web/entries/Gauss-Jordan-Elim-Fun.html

web/entries/Gauss_Jordan.html

web/entries/GenClock.html

web/entries/General-Triangle.html

web/entries/Generic_Deriving.html

web/entries/Generic_Join.html

web/entries/GewirthPGCProof.html

web/entries/Girth_Chromatic.html

web/entries/GoedelGod.html

web/entries/GraphMarkingIBP.html

web/entries/Graph_Saturation.html

web/entries/Graph_Theory.html

web/entries/Green.html

web/entries/Groebner_Bases.html

web/entries/Groebner_Macaulay.html

web/entries/Gromov_Hyperbolicity.html

web/entries/Group-Ring-Module.html

web/entries/HOL-CSP.html

web/entries/HOLCF-Prelude.html

web/entries/HRB-Slicing.html

web/entries/Heard_Of.html

web/entries/HereditarilyFinite.html

web/entries/Hermite.html

web/entries/Hidden_Markov_Models.html

web/entries/Higher_Order_Terms.html

web/entries/Hoare_Time.html

web/entries/HotelKeyCards.html

web/entries/Huffman.html

web/entries/Hybrid_Multi_Lane_Spatial_Logic.html

web/entries/Hybrid_Systems_VCs.html

web/entries/HyperCTL.html

web/entries/IEEE_Floating_Point.html

web/entries/IMAP-CRDT.html

web/entries/IMO2019.html

web/entries/IMP2.html

web/entries/IMP2_Binary_Heap.html

web/entries/IP_Addresses.html

web/entries/Imperative_Insertion_Sort.html

web/entries/Impossible_Geometry.html

web/entries/Incompleteness.html

web/entries/Incredible_Proof_Machine.html

web/entries/Inductive_Confidentiality.html

web/entries/InfPathElimination.html

web/entries/InformationFlowSlicing.html

web/entries/InformationFlowSlicing_Inter.html

web/entries/Integration.html

web/entries/Iptables_Semantics.html

web/entries/Irrationality_J_Hancl.html

web/entries/Isabelle_Meta_Model.html

web/entries/Jacobson_Basic_Algebra.html

web/entries/Jinja.html

web/entries/JinjaThreads.html

web/entries/JiveDataStoreModel.html

web/entries/Jordan_Hoelder.html

web/entries/Jordan_Normal_Form.html

web/entries/KAD.html

web/entries/KAT_and_DRA.html

web/entries/KBPs.html

web/entries/KD_Tree.html

web/entries/Key_Agreement_Strong_Adversaries.html

web/entries/Kleene_Algebra.html

web/entries/Knot_Theory.html

web/entries/Knuth_Morris_Pratt.html

web/entries/Koenigsberg_Friendship.html

web/entries/Kruskal.html

web/entries/Kuratowski_Closure_Complement.html

web/entries/LLL_Basis_Reduction.html

web/entries/LLL_Factorization.html

web/entries/LOFT.html

web/entries/LTL.html

web/entries/LTL_Master_Theorem.html

web/entries/LTL_to_DRA.html

web/entries/LTL_to_GBA.html

web/entries/Lam-ml-Normalization.html

web/entries/LambdaAuth.html

web/entries/LambdaMu.html

web/entries/Lambda_Free_EPO.html

web/entries/Lambda_Free_KBOs.html

web/entries/Lambda_Free_RPOs.html

web/entries/Landau_Symbols.html

web/entries/Laplace_Transform.html

web/entries/Latin_Square.html

web/entries/LatticeProperties.html

web/entries/Launchbury.html

web/entries/Lazy-Lists-II.html

web/entries/Lazy_Case.html

web/entries/Lehmer.html

web/entries/Lifting_Definition_Option.html

web/entries/LightweightJava.html

web/entries/LinearQuantifierElim.html

web/entries/Linear_Inequalities.html

web/entries/Linear_Recurrences.html

web/entries/Liouville_Numbers.html

web/entries/List-Index.html

web/entries/List-Infinite.html

web/entries/List_Interleaving.html

web/entries/List_Inversions.html

web/entries/List_Update.html

web/entries/LocalLexing.html

web/entries/Localization_Ring.html

web/entries/Locally-Nameless-Sigma.html

web/entries/Lowe_Ontological_Argument.html

web/entries/Lower_Semicontinuous.html

web/entries/Lp.html

web/entries/MFMC_Countable.html

web/entries/MFOTL_Monitor.html

web/entries/MSO_Regex_Equivalence.html

web/entries/Markov_Models.html

web/entries/Marriage.html

web/entries/Mason_Stothers.html

web/entries/Matrix.html

web/entries/Matrix_Tensor.html

web/entries/Matroids.html

web/entries/Max-Card-Matching.html

web/entries/Median_Of_Medians_Selection.html

web/entries/Menger.html

web/entries/MiniML.html

web/entries/Minimal_SSA.html

web/entries/Minkowskis_Theorem.html

web/entries/Minsky_Machines.html

web/entries/Modal_Logics_for_NTS.html

web/entries/Modular_Assembly_Kit_Security.html

web/entries/Monad_Memo_DP.html

web/entries/Monad_Normalisation.html

web/entries/MonoBoolTranAlgebra.html

web/entries/MonoidalCategory.html

web/entries/Monomorphic_Monad.html

web/entries/MuchAdoAboutTwo.html

web/entries/Multi_Party_Computation.html

web/entries/Multirelations.html

web/entries/Myhill-Nerode.html

web/entries/Name_Carrying_Type_Inference.html

web/entries/Nat-Interval-Logic.html

web/entries/Native_Word.html

web/entries/Nested_Multisets_Ordinals.html

web/entries/Network_Security_Policy_Verification.html

web/entries/Neumann_Morgenstern_Utility.html

web/entries/No_FTL_observers.html

web/entries/Nominal2.html

web/entries/Noninterference_CSP.html

web/entries/Noninterference_Concurrent_Composition.html

web/entries/Noninterference_Generic_Unwinding.html

web/entries/Noninterference_Inductive_Unwinding.html

web/entries/Noninterference_Ipurge_Unwinding.html

web/entries/Noninterference_Sequential_Composition.html

web/entries/NormByEval.html

web/entries/Nullstellensatz.html

web/entries/Octonions.html

web/entries/OpSets.html

web/entries/Open_Induction.html

web/entries/Optics.html

web/entries/Optimal_BST.html

web/entries/Orbit_Stabiliser.html

web/entries/Order_Lattice_Props.html

web/entries/Ordered_Resolution_Prover.html

web/entries/Ordinal.html

web/entries/Ordinals_and_Cardinals.html

web/entries/Ordinary_Differential_Equations.html

web/entries/PCF.html

web/entries/PLM.html

web/entries/POPLmark-deBruijn.html

web/entries/PSemigroupsConvolution.html

web/entries/Pairing_Heap.html

web/entries/Paraconsistency.html

web/entries/Parity_Game.html

web/entries/Partial_Function_MR.html

web/entries/Partial_Order_Reduction.html

web/entries/Password_Authentication_Protocol.html

web/entries/Pell.html

web/entries/Perfect-Number-Thm.html

web/entries/Perron_Frobenius.html

web/entries/Pi_Calculus.html

web/entries/Pi_Transcendental.html

web/entries/Planarity_Certificates.html

web/entries/Polynomial_Factorization.html

web/entries/Polynomial_Interpolation.html

web/entries/Polynomials.html

web/entries/Pop_Refinement.html

web/entries/Posix-Lexing.html

web/entries/Possibilistic_Noninterference.html

web/entries/Pratt_Certificate.html

web/entries/Presburger-Automata.html

web/entries/Prim_Dijkstra_Simple.html

web/entries/Prime_Distribution_Elementary.html

web/entries/Prime_Harmonic_Series.html

web/entries/Prime_Number_Theorem.html

web/entries/Priority_Queue_Braun.html

web/entries/Priority_Search_Trees.html

web/entries/Probabilistic_Noninterference.html

web/entries/Probabilistic_Prime_Tests.html

web/entries/Probabilistic_System_Zoo.html

web/entries/Probabilistic_Timed_Automata.html

web/entries/Probabilistic_While.html

web/entries/Program-Conflict-Analysis.html

web/entries/Projective_Geometry.html

web/entries/Promela.html

web/entries/Proof_Strategy_Language.html

web/entries/PropResPI.html

web/entries/Propositional_Proof_Systems.html

web/entries/Prpu_Maxflow.html

web/entries/PseudoHoops.html

web/entries/Psi_Calculi.html

web/entries/Ptolemys_Theorem.html

web/entries/QHLProver.html

web/entries/QR_Decomposition.html

web/entries/Quantales.html

web/entries/Quaternions.html

web/entries/Quick_Sort_Cost.html

web/entries/RIPEMD-160-SPARK.html

web/entries/ROBDD.html

web/entries/RSAPSS.html

web/entries/Ramsey-Infinite.html

web/entries/Random_BSTs.html

web/entries/Random_Graph_Subgraph_Threshold.html

web/entries/Randomised_BSTs.html

web/entries/Randomised_Social_Choice.html

web/entries/Rank_Nullity_Theorem.html

web/entries/Real_Impl.html

web/entries/Recursion-Theory-I.html

web/entries/Refine_Imperative_HOL.html

web/entries/Refine_Monadic.html

web/entries/RefinementReactive.html

web/entries/Regex_Equivalence.html

web/entries/Regular-Sets.html

web/entries/Regular_Algebras.html

web/entries/Relation_Algebra.html

web/entries/Rep_Fin_Groups.html

web/entries/Residuated_Lattices.html

web/entries/Resolution_FOL.html

web/entries/Rewriting_Z.html

web/entries/Ribbon_Proofs.html

web/entries/Robbins-Conjecture.html

web/entries/Root_Balanced_Tree.html

web/entries/Routing.html

web/entries/Roy_Floyd_Warshall.html

web/entries/SATSolverVerification.html

web/entries/SDS_Impossibility.html

web/entries/SIFPL.html

web/entries/SIFUM_Type_Systems.html

web/entries/SPARCv8.html

web/entries/Safe_OCL.html

web/entries/Secondary_Sylow.html

web/entries/Security_Protocol_Refinement.html

web/entries/Selection_Heap_Sort.html

web/entries/SenSocialChoice.html

web/entries/Separata.html

web/entries/Separation_Algebra.html

web/entries/Separation_Logic_Imperative_HOL.html

web/entries/SequentInvertibility.html

web/entries/Shivers-CFA.html

web/entries/ShortestPath.html

web/entries/Show.html

web/entries/Signature_Groebner.html

web/entries/Simpl.html

web/entries/Simple_Firewall.html

web/entries/Simplex.html

web/entries/Skew_Heap.html

web/entries/Slicing.html

web/entries/Smooth_Manifolds.html

web/entries/Sort_Encodings.html

web/entries/Source_Coding_Theorem.html

web/entries/Special_Function_Bounds.html

web/entries/Splay_Tree.html

web/entries/Sqrt_Babylonian.html

web/entries/Stable_Matching.html

web/entries/Statecharts.html

web/entries/Stellar_Quorums.html

web/entries/Stern_Brocot.html

web/entries/Stewart_Apollonius.html

web/entries/Stirling_Formula.html

web/entries/Stochastic_Matrices.html

web/entries/Stone_Algebras.html

web/entries/Stone_Kleene_Relation_Algebras.html

web/entries/Stone_Relation_Algebras.html

web/entries/Store_Buffer_Reduction.html

web/entries/Stream-Fusion.html

web/entries/Stream_Fusion_Code.html

web/entries/Strong_Security.html

web/entries/Sturm_Sequences.html

web/entries/Sturm_Tarski.html

web/entries/Stuttering_Equivalence.html

web/entries/Subresultants.html

web/entries/SumSquares.html

web/entries/SuperCalc.html

web/entries/Surprise_Paradox.html

web/entries/Symmetric_Polynomials.html

web/entries/Szpilrajn.html

web/entries/TESL_Language.html

web/entries/TLA.html

web/entries/Tail_Recursive_Functions.html

web/entries/Tarskis_Geometry.html

web/entries/Taylor_Models.html

web/entries/Timed_Automata.html

web/entries/Topology.html

web/entries/TortoiseHare.html

web/entries/Transcendence_Series_Hancl_Rucki.html

web/entries/Transformer_Semantics.html

web/entries/Transition_Systems_and_Automata.html

web/entries/Transitive-Closure-II.html

web/entries/Transitive-Closure.html

web/entries/Treaps.html

web/entries/Tree-Automata.html

web/entries/Tree_Decomposition.html

web/entries/Triangle.html

web/entries/Trie.html

web/entries/Twelvefold_Way.html

web/entries/Tycon.html

web/entries/Types_Tableaus_and_Goedels_God.html

web/entries/UPF.html

web/entries/UPF_Firewall.html

web/entries/UTP.html

web/entries/Universal_Turing_Machine.html

web/entries/UpDown_Scheme.html

web/entries/Valuation.html

web/entries/VectorSpace.html

web/entries/Verified-Prover.html

web/entries/VerifyThis2018.html

web/entries/Vickrey_Clarke_Groves.html

web/entries/VolpanoSmith.html

web/entries/WHATandWHERE_Security.html

web/entries/WebAssembly.html

web/entries/Weight_Balanced_Trees.html

web/entries/Well_Quasi_Orders.html

web/entries/Winding_Number_Eval.html

web/entries/Word_Lib.html

web/entries/WorkerWrapper.html

web/entries/XML.html

web/entries/Zeta_Function.html

web/entries/pGCL.html

web/images/isabelle.png

web/index.html

web/rss.xml

web/search.html

web/statistics.html

web/submitting.html

web/topics.html

web/updating.html

web/using.html