![[Jenkins]](/jenkins/static/8e513251/images/svgs/logo.svg){kind=logo}
[EnvInject] - Loading node environment variables.
Building remotely on workermtahpc (mta_hpc) in workspace /media/data/jenkins/workspace/isabelle-all
[isabelle-all] $ hg showconfig paths.default
[isabelle-all] $ hg pull --rev default
pulling from http://isabelle.in.tum.de/repos/isabelle/
real URL is https://isabelle.in.tum.de/repos/isabelle/
[isabelle-all] $ hg update --clean --rev default
0 files updated, 0 files merged, 0 files removed, 0 files unresolved
[isabelle-all] $ hg log --rev . --template {node}
[isabelle-all] $ hg log --rev . --template {rev}
[isabelle-all] $ hg log --rev a1421c88ae0a6933f6198fdf706976b79c0f00ae --template exists\n
[isabelle-all] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(a1421c88ae0a6933f6198fdf706976b79c0f00ae)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
pulling from https://foss.heptapod.net/isa-afp/afp-devel/
[afp] $ hg update --clean --rev default
1396 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp] $ hg --config extensions.purge= clean --all
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg log --rev 6927929601bad4e0d7950272fc3bd280e26e1de8 --template exists\n
[afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(6927929601bad4e0d7950272fc3bd280e26e1de8)" --encoding UTF-8 --encodingmode replace
[isabelle-all] $ /bin/sh -xe /tmp/jenkins1278120366634153573.sh
### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle.jar) ...
### Building graph browser (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_graphbrowser.jar) ...
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_admin.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
[NOTE] Package zarith is already installed (current version is 1.12).
stack will use a sandboxed GHC it installed
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
The Glorious Glasgow Haskell Compilation System, version 8.10.7
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-15c840d48c9a/x86_64_32-linux"
Session Doc/Sledgehammer (doc)
Session AFP/Abortable_Linearizable_Modules (AFP)
Session AFP/Abstract-Hoare-Logics (AFP)
Session AFP/Ackermanns_not_PR (AFP)
Session AFP/Aristotles_Assertoric_Syllogistic (AFP)
Session AFP/Attack_Trees (AFP)
Session AFP/AxiomaticCategoryTheory (AFP)
Session AFP/Belief_Revision (AFP)
Session AFP/BinarySearchTree (AFP)
Session AFP/Binomial-Queues (AFP)
Session AFP/BytecodeLogicJmlTypes (AFP)
Session AFP/C2KA_DistributedSystems (AFP)
Session AFP/Sqrt_Babylonian (AFP)
Session AFP/ClockSynchInst (AFP)
Session AFP/Compiling-Exceptions-Correctly (AFP)
Session AFP/Complete_Non_Orders (AFP)
Session AFP/ComponentDependencies (AFP)
Session AFP/Concurrent_Revisions (AFP)
Session AFP/Constructor_Funs (AFP)
Session AFP/CryptoBasedCompositionalProperties (AFP)
Session AFP/DPT-SAT-Solver (AFP)
Session AFP/Dedekind_Real (AFP)
Session AFP/Depth-First-Search (AFP)
Session AFP/Digit_Expansions (AFP)
Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
Session AFP/Example-Submission (AFP)
Session AFP/FeatherweightJava (AFP)
Session AFP/Featherweight_OCL (AFP)
Session AFP/FileRefinement (AFP)
Session AFP/FocusStreamsCaseStudies (AFP)
Session AFP/Foundation_of_geometry (AFP)
Session AFP/Free-Boolean-Algebra (AFP)
Session AFP/Fresh_Identifiers (AFP)
Session AFP/FunWithFunctions (AFP)
Session AFP/FunWithTilings (AFP)
Session AFP/GPU_Kernel_PL (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/Generic_Deriving (AFP)
Session AFP/GewirthPGCProof (AFP)
Session AFP/Goodstein_Lambda (AFP)
Session HOL/HOL-Cardinals (timing)
Session AFP/Binding_Syntax_Theory (AFP)
Session AFP/Ordinals_and_Cardinals (AFP)
Session HOL/HOL-Hoare_Parallel (timing)
Session HOL/HOL-Library (main timing)
Session AFP/Approximation_Algorithms (AFP)
Session AFP/ArrowImpossibilityGS (AFP)
Session AFP/BNF_Operations (AFP)
Session AFP/Binomial-Heaps (AFP)
Session AFP/Boolean_Expression_Checkers (AFP)
Session AFP/Bounded_Deducibility_Security (AFP)
Session AFP/BD_Security_Compositional (AFP)
Session AFP/Card_Multisets (AFP)
Session AFP/Card_Number_Partitions (AFP)
Session AFP/Combinatorics_Words (AFP)
Session AFP/Combinatorics_Words_Graph_Lemma (AFP)
Session AFP/Completeness (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/Concurrent_Ref_Alg (AFP)
Session AFP/Conditional_Simplification (AFP)
Session AFP/Conditional_Transfer_Rule (AFP)
Session AFP/DOM_Components (AFP)
Session AFP/Shadow_SC_DOM (AFP)
Session AFP/SC_DOM_Components (AFP)
Session AFP/Decl_Sem_Fun_PL (AFP)
Session AFP/Encodability_Process_Calculi (AFP)
Session AFP/Epistemic_Logic (AFP)
Session AFP/Public_Announcement_Logic (AFP)
Session AFP/Euler_Partition (AFP)
Session AFP/FOL_Seq_Calc1 (AFP)
Session AFP/FOL_Axiomatic (AFP)
Session AFP/FOL_Harrison (AFP)
Session AFP/Factored_Transition_System_Bounding (AFP)
Session AFP/Extended_Finite_State_Machines (AFP)
Session AFP/Extended_Finite_State_Machine_Inference (AFP)
Session AFP/Finger-Trees (AFP)
Session AFP/Finite-Map-Extras (AFP)
Session AFP/Generalized_Counting_Sort (AFP)
Session AFP/Graph_Saturation (AFP)
Session AFP/Group-Ring-Module (AFP)
Session HOL/HOL-UNITY (timing)
Session HOL/HOL-Combinatorics (main timing)
Session AFP/Derangements (AFP)
Session AFP/Discrete_Summation (AFP)
Session AFP/Gauss-Jordan-Elim-Fun (AFP)
Session AFP/Graph_Theory (AFP)
Session AFP/ShortestPath (AFP)
Session HOL/HOL-Computational_Algebra (main timing)
Session AFP/Descartes_Sign_Rule (AFP)
Session HOL/HOL-Algebra (main timing)
Session AFP/Finitely_Generated_Abelian_Groups (AFP)
Session HOL/HOL-Decision_Procs (timing)
Session HOL/HOL-Quotient_Examples (timing)
Session AFP/Interpolation_Polynomials_HOL_Algebra (AFP)
Session AFP/Localization_Ring (AFP)
Session AFP/Orbit_Stabiliser (AFP)
Session AFP/Perfect-Number-Thm (AFP)
Session AFP/Secondary_Sylow (AFP)
Session AFP/Jordan_Hoelder (AFP)
Session HOL/HOL-Analysis (main timing)
Session AFP/Actuarial_Mathematics (AFP)
Session AFP/Cayley_Hamilton (AFP)
Session AFP/DynamicArchitectures (AFP)
Session AFP/Architectural_Design_Patterns (AFP)
Session AFP/Lazy-Lists-II (AFP)
Session AFP/Stream_Fusion_Code (AFP)
Session AFP/Complex_Geometry (AFP)
Session AFP/Poincare_Disc (AFP)
Session AFP/Differential_Game_Logic (AFP)
Session AFP/First_Welfare_Theorem (AFP)
Session HOL/HOL-Complex_Analysis (main timing)
Session AFP/Allen_Calculus (AFP)
Session AFP/Card_Partitions (AFP)
Session AFP/Bell_Numbers_Spivey (AFP)
Session AFP/Card_Equiv_Relations (AFP)
Session AFP/Equivalence_Relation_Enumeration (AFP)
Session AFP/Falling_Factorial_Sum (AFP)
Session AFP/Case_Labeling (AFP)
Session AFP/Dependent_SIFUM_Type_Systems (AFP)
Session AFP/Dependent_SIFUM_Refinement (AFP)
Session HOL/HOL-Homology (timing)
Session HOL/HOL-Probability (main timing)
Session AFP/Buffons_Needle (AFP)
Session AFP/Density_Compiler (AFP)
Session AFP/DiscretePricing (AFP)
Session AFP/Ergodic_Theory (AFP)
Session AFP/Gromov_Hyperbolicity (AFP)
Session AFP/Laws_of_Large_Numbers (AFP)
Session AFP/Fisher_Yates (AFP)
Session AFP/Girth_Chromatic (AFP)
Session AFP/Random_Graph_Subgraph_Threshold (AFP)
Session HOL/HOL-Probability-ex (timing)
Session AFP/Hahn_Jordan_Decomposition (AFP)
Session AFP/Markov_Models (AFP)
Session AFP/Monad_Normalisation (AFP)
Session AFP/Monomorphic_Monad (AFP)
Session AFP/Neumann_Morgenstern_Utility (AFP)
Session AFP/Probabilistic_Noninterference (AFP)
Session AFP/Probabilistic_System_Zoo (AFP)
Session AFP/Quasi_Borel_Spaces (AFP)
Session AFP/Source_Coding_Theorem (AFP)
Session AFP/Universal_Hash_Families (AFP)
Session AFP/Irrationality_J_Hancl (AFP)
Session AFP/Kuratowski_Closure_Complement (AFP)
Session AFP/Laplace_Transform (AFP)
Session AFP/Lower_Semicontinuous (AFP)
Session AFP/Minkowskis_Theorem (AFP)
Session AFP/Ptolemys_Theorem (AFP)
Session AFP/Rank_Nullity_Theorem (AFP)
Session AFP/Gauss_Jordan (AFP)
Session AFP/Echelon_Form (AFP)
Session AFP/MDP-Algorithms (AFP)
Session AFP/Tarskis_Geometry (AFP)
Session AFP/Chord_Segments (AFP)
Session AFP/Stewart_Apollonius (AFP)
Session AFP/Youngs_Inequality (AFP)
Session HOL/HOL-Nonstandard_Analysis (timing)
Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
Session HOL/HOL-Number_Theory (main timing)
Session AFP/Arith_Prog_Rel_Primes (AFP)
Session AFP/E_Transcendental (AFP)
Session AFP/Elliptic_Curves_Group_Law (AFP)
Session HOL/HOL-Data_Structures (timing)
Session AFP/Efficient-Mergesort (AFP)
Session HOL/HOL-Codegenerator_Test
Session AFP/Automatic_Refinement (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Lifting_the_Exponent (AFP)
Session AFP/Pratt_Certificate (AFP)
Session AFP/Bertrands_Postulate (AFP)
Session AFP/Prime_Harmonic_Series (AFP)
Session AFP/Liouville_Numbers (AFP)
Session AFP/Lucas_Theorem (AFP)
Session AFP/DPRM_Theorem (AFP)
Session AFP/Mason_Stothers (AFP)
Session AFP/Polynomial_Interpolation (AFP)
Session AFP/Formal_Puiseux_Series (AFP)
Session AFP/Probabilistic_Prime_Tests (AFP)
Session AFP/Rep_Fin_Groups (AFP)
Session AFP/Sturm_Sequences (AFP)
Session AFP/Safe_Distance (AFP)
Session AFP/Special_Function_Bounds (AFP)
Session AFP/Sturm_Tarski (AFP)
Session AFP/Budan_Fourier (AFP)
Session AFP/Three_Circles (AFP)
Session AFP/Winding_Number_Eval (AFP)
Session AFP/Count_Complex_Roots (AFP)
Session HOL/HOL-Corec_Examples (timing)
Session HOL/HOL-Datatype_Examples (timing)
Session AFP/Abs_Int_ITP2012 (AFP)
Session AFP/Relational-Incorrectness-Logic (AFP)
Session HOL/HOL-Imperative_HOL (timing)
Session AFP/Auto2_Imperative_HOL (AFP)
Session AFP/Imperative_Insertion_Sort (AFP)
Session HOL/HOL-Metis_Examples (timing)
Session HOL/HOL-Proofs (timing)
Session HOL/HOL-Proofs-Extraction (timing)
Session HOL/HOL-Proofs-Lambda (timing)
Session AFP/Applicative_Lifting (AFP)
Session AFP/Stern_Brocot (AFP)
Session AFP/HereditarilyFinite (AFP)
Session AFP/Isabelle_Meta_Model (AFP)
Session AFP/Stuttering_Equivalence (AFP)
Session AFP/Landau_Symbols (AFP)
Session AFP/Catalan_Numbers (AFP)
Session AFP/Error_Function (AFP)
Session AFP/Euler_MacLaurin (AFP)
Session AFP/LightweightJava (AFP)
Session AFP/LinearQuantifierElim (AFP)
Session AFP/List-Infinite (AFP)
Session AFP/Nat-Interval-Logic (AFP)
Session AFP/AutoFocus-Stream (AFP)
Session AFP/Median_Method (AFP)
Session AFP/MuchAdoAboutTwo (AFP)
Session AFP/Order_Lattice_Props (AFP)
Session AFP/POPLmark-deBruijn (AFP)
Session AFP/Pairing_Heap (AFP)
Session AFP/Password_Authentication_Protocol (AFP)
Session AFP/Prefix_Free_Code_Combinators (AFP)
Session AFP/Frequency_Moments (AFP)
Session AFP/Presburger-Automata (AFP)
Session AFP/Priority_Queue_Braun (AFP)
Session AFP/Program-Conflict-Analysis (AFP)
Session AFP/Regular-Sets (AFP)
Session AFP/Abstract-Rewriting (AFP)
Session AFP/Decreasing-Diagrams (AFP)
Session AFP/First_Order_Terms (AFP)
Session AFP/Stateful_Protocol_Composition_and_Typing (AFP)
Session AFP/Automated_Stateful_Protocol_Verification (AFP)
Session AFP/Matrix_Tensor (AFP)
Session AFP/Coinductive_Languages (AFP)
Session AFP/Finite_Automata_HF (AFP)
Session AFP/Functional-Automata (AFP)
Session AFP/Posix-Lexing (AFP)
Session AFP/ResiduatedTransitionSystem (AFP)
Session AFP/Ribbon_Proofs (AFP)
Session AFP/SATSolverVerification (AFP)
Session AFP/Selection_Heap_Sort (AFP)
Session AFP/Sort_Encodings (AFP)
Session AFP/Amortized_Complexity (AFP)
Session AFP/Dynamic_Tables (AFP)
Session AFP/Root_Balanced_Tree (AFP)
Session AFP/Closest_Pair_Points (AFP)
Session AFP/Stable_Matching (AFP)
Session AFP/Szemeredi_Regularity (AFP)
Session AFP/Roth_Arithmetic_Progressions (AFP)
Session AFP/Tail_Recursive_Functions (AFP)
Session AFP/TortoiseHare (AFP)
Session AFP/Flyspeck-Tame (AFP)
Session AFP/Twelvefold_Way (AFP)
Session AFP/Vickrey_Clarke_Groves (AFP)
Session HOL/HOL-MicroJava (timing)
Session HOL/HOL-Nitpick_Examples
Session HOL/HOL-Nominal-Examples (timing)
Session AFP/Lam-ml-Normalization (AFP)
Session AFP/SequentInvertibility (AFP)
Session HOL/HOL-Predicate_Compile_Examples (timing)
Session HOL/HOL-Quickcheck_Examples (timing)
Session AFP/Cotangent_PFD_Formula (AFP)
Session AFP/Furstenberg_Topology (AFP)
Session HOL/HOL-Real_Asymp-Manual
Session AFP/Sophomores_Dream (AFP)
Session AFP/Stirling_Formula (AFP)
Session AFP/Irrationals_From_THEBOOK (AFP)
Session HOL/HOL-SET_Protocol (timing)
Session HOL/HOL-SMT_Examples (timing)
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session AFP/Banach_Steinhaus (AFP)
Session AFP/Smooth_Manifolds (AFP)
Session AFP/Types_To_Sets_Extension (AFP)
Session HOL/HOLCF (main timing)
Session AFP/HOLCF-Prelude (AFP)
Session AFP/Stream-Fusion (AFP)
Session AFP/WorkerWrapper (AFP)
Session AFP/Consensus_Refined (AFP)
Session AFP/Hood_Melville_Queue (AFP)
Session AFP/HotelKeyCards (AFP)
Session Doc/How_to_Prove_it (no_doc)
Session AFP/Hybrid_Logic (AFP)
Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
Session AFP/IFC_Tracking (AFP)
Session AFP/IMP2_Binary_Heap (AFP)
Session AFP/IMP_Compiler (AFP)
Session Doc/Implementation (doc)
Session AFP/Impossible_Geometry (AFP)
Session AFP/Inductive_Confidentiality (AFP)
Session AFP/Inductive_Inference (AFP)
Session AFP/InfPathElimination (AFP)
Session AFP/Intro_Dest_Elim (AFP)
Session AFP/Jacobson_Basic_Algebra (AFP)
Session AFP/Grothendieck_Schemes (AFP)
Session AFP/Pluennecke_Ruzsa_Inequality (AFP)
Session AFP/JiveDataStoreModel (AFP)
Session AFP/Key_Agreement_Strong_Adversaries (AFP)
Session AFP/Kleene_Algebra (AFP)
Session AFP/Algebraic_VCs (AFP)
Session AFP/Multirelations (AFP)
Session AFP/Transformer_Semantics (AFP)
Session AFP/Regular_Algebras (AFP)
Session AFP/Relation_Algebra (AFP)
Session AFP/Relational_Paths (AFP)
Session AFP/Residuated_Lattices (AFP)
Session AFP/Knights_Tour (AFP)
Session AFP/LatticeProperties (AFP)
Session AFP/DataRefinementIBP (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Lifting_Definition_Option (AFP)
Session AFP/Comparison_Sort_Lower_Bound (AFP)
Session AFP/Dominance_CHK (AFP)
Session AFP/InformationFlowSlicing_Inter (AFP)
Session AFP/InformationFlowSlicing (AFP)
Session AFP/Regression_Test_Selection (AFP)
Session AFP/Quick_Sort_Cost (AFP)
Session AFP/Randomised_BSTs (AFP)
Session AFP/Randomised_Social_Choice (AFP)
Session AFP/Fishburn_Impossibility (AFP)
Session AFP/SDS_Impossibility (AFP)
Session AFP/List_Interleaving (AFP)
Session AFP/List_Inversions (AFP)
Session AFP/Locally-Nameless-Sigma (AFP)
Session AFP/Logging_Independent_Anonymity (AFP)
Session AFP/Lowe_Ontological_Argument (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/Median_Of_Medians_Selection (AFP)
Session AFP/Metalogic_ProofChecker (AFP)
Session AFP/Modular_Assembly_Kit_Security (AFP)
Session AFP/MonoBoolTranAlgebra (AFP)
Session AFP/Name_Carrying_Type_Inference (AFP)
Session AFP/Nash_Williams (AFP)
Session AFP/No_FTL_observers (AFP)
Session AFP/Incompleteness (AFP)
Session AFP/Surprise_Paradox (AFP)
Session AFP/Modal_Logics_for_NTS (AFP)
Session AFP/Noninterference_CSP (AFP)
Session AFP/Noninterference_Ipurge_Unwinding (AFP)
Session AFP/Noninterference_Generic_Unwinding (AFP)
Session AFP/Noninterference_Inductive_Unwinding (AFP)
Session AFP/Noninterference_Sequential_Composition (AFP)
Session AFP/Noninterference_Concurrent_Composition (AFP)
Session AFP/Open_Induction (AFP)
Session AFP/Well_Quasi_Orders (AFP)
Session AFP/Decreasing-Diagrams-II (AFP)
Session AFP/Myhill-Nerode (AFP)
Session AFP/Nested_Multisets_Ordinals (AFP)
Session AFP/Design_Theory (AFP)
Session AFP/Lambda_Free_RPOs (AFP)
Session AFP/Lambda_Free_EPO (AFP)
Session AFP/Ordered_Resolution_Prover (AFP)
Session AFP/Chandy_Lamport (AFP)
Session AFP/Saturation_Framework (AFP)
Session AFP/Saturation_Framework_Extensions (AFP)
Session AFP/Progress_Tracking (AFP)
Session AFP/PSemigroupsConvolution (AFP)
Session AFP/Package_logic (AFP)
Session AFP/Combinable_Wands (AFP)
Session AFP/Paraconsistency (AFP)
Session AFP/GaleStewart_Games (AFP)
Session AFP/Partial_Function_MR (AFP)
Session AFP/Physical_Quantities (AFP)
Session AFP/Pop_Refinement (AFP)
Session AFP/Possibilistic_Noninterference (AFP)
Session AFP/Priority_Search_Trees (AFP)
Session AFP/Prim_Dijkstra_Simple (AFP)
Session AFP/Projective_Geometry (AFP)
Session AFP/Proof_Strategy_Language (AFP)
Session AFP/Propositional_Proof_Systems (AFP)
Session AFP/Ramsey-Infinite (AFP)
Session AFP/Real_Time_Deque (AFP)
Session AFP/Recursion-Theory-I (AFP)
Session AFP/Minsky_Machines (AFP)
Session AFP/RefinementReactive (AFP)
Session AFP/Regex_Equivalence (AFP)
Session AFP/Relational_Method (AFP)
Session AFP/Resolution_FOL (AFP)
Session AFP/Robbins-Conjecture (AFP)
Session AFP/Roy_Floyd_Warshall (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/Schutz_Spacetime (AFP)
Session AFP/Security_Protocol_Refinement (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/SimplifiedOntologicalArgument (AFP)
Session AFP/Sliding_Window_Algorithm (AFP)
Session AFP/Stellar_Quorums (AFP)
Session AFP/Stone_Algebras (AFP)
Session AFP/Stone_Relation_Algebras (AFP)
Session AFP/Stone_Kleene_Relation_Algebras (AFP)
Session AFP/Aggregation_Algebras (AFP)
Session AFP/Relational_Disjoint_Set_Forests (AFP)
Session AFP/Relational_Minimum_Spanning_Trees (AFP)
Session AFP/Relational_Forests (AFP)
Session AFP/Subset_Boolean_Algebras (AFP)
Session AFP/Correctness_Algebras (AFP)
Session AFP/Store_Buffer_Reduction (AFP)
Session AFP/Strong_Security (AFP)
Session AFP/Clique_and_Monotone_Circuits (AFP)
Session AFP/Syntax_Independent_Logic (AFP)
Session AFP/Goedel_Incompleteness (AFP)
Session AFP/Goedel_HFSet_Semantic (AFP)
Session AFP/Goedel_HFSet_Semanticless (AFP)
Session AFP/Robinson_Arithmetic (AFP)
Session AFP/Combinatorics_Words_Lyndon (AFP)
Session AFP/TESL_Language (AFP)
Session AFP/Timed_Automata (AFP)
Session AFP/Probabilistic_Timed_Automata (AFP)
Session AFP/Topological_Semantics (AFP)
Session AFP/Transitive-Closure-II (AFP)
Session AFP/Tree_Decomposition (AFP)
Session Doc/Typeclass_Hierarchy (doc)
Session AFP/Types_Tableaus_and_Goedels_God (AFP)
Session AFP/UPF_Firewall (AFP)
Session AFP/Universal_Turing_Machine (AFP)
Session AFP/Van_der_Waerden (AFP)
Session AFP/Interpreter_Optimizations (AFP)
Session AFP/Verified-Prover (AFP)
Session AFP/VolpanoSmith (AFP)
Session AFP/WHATandWHERE_Security (AFP)
Session AFP/Weight_Balanced_Trees (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Interval_Arithmetic_Word32 (AFP)
Session AFP/Abstract_Completeness (AFP)
Session AFP/Abstract_Soundness (AFP)
Session AFP/FOL_Seq_Calc3 (AFP)
Session AFP/Incredible_Proof_Machine (AFP)
Session AFP/CAVA_Automata (AFP)
Session AFP/DFS_Framework (AFP)
Session AFP/Collections_Examples (AFP)
Session AFP/Containers-Benchmarks (AFP)
Session AFP/MFOTL_Monitor (AFP)
Session AFP/Generic_Join (AFP)
Session AFP/MFODL_Monitor_Optimized (AFP)
Session AFP/Formula_Derivatives (AFP)
Session AFP/MSO_Regex_Equivalence (AFP)
Session AFP/Affine_Arithmetic (AFP)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/Differential_Dynamic_Logic (AFP)
Session AFP/Hybrid_Systems_VCs (AFP)
Session AFP/Matrices_for_ODEs (AFP)
Session AFP/Taylor_Models (AFP)
Session AFP/Certification_Monads (AFP)
Session AFP/AI_Planning_Languages_Semantics (AFP)
Session AFP/Verified_SAT_Based_AI_Planning (AFP)
Session AFP/Dict_Construction (AFP)
Session AFP/Formula_Derivatives-Examples (AFP)
Session AFP/Monad_Memo_DP (AFP)
Session AFP/Hidden_Markov_Models (AFP)
Session AFP/Polynomial_Factorization (AFP)
Session AFP/Amicable_Numbers (AFP)
Session AFP/Dirichlet_Series (AFP)
Session AFP/Finite_Fields (AFP)
Session AFP/Zeta_Function (AFP)
Session AFP/Prime_Number_Theorem (AFP)
Session AFP/Prime_Distribution_Elementary (AFP)
Session AFP/Irrational_Series_Erdos_Straus (AFP)
Session AFP/Transcendence_Series_Hancl_Rucki (AFP)
Session AFP/Zeta_3_Irrational (AFP)
Session AFP/Gaussian_Integers (AFP)
Session AFP/Jordan_Normal_Form (AFP)
Session AFP/Isabelle_Marries_Dirac (AFP)
Session AFP/Knuth_Bendix_Order (AFP)
Session AFP/Functional_Ordered_Resolution_Prover (AFP)
Session AFP/Regular_Tree_Relations (AFP)
Session AFP/FO_Theory_Rewriting (AFP)
Session AFP/Rewrite_Properties_Reduction (AFP)
Session AFP/Weighted_Path_Order (AFP)
Session AFP/Multiset_Ordering_NPC (AFP)
Session AFP/Linear_Recurrences (AFP)
Session AFP/Perron_Frobenius (AFP)
Session AFP/Stochastic_Matrices (AFP)
Session AFP/Subresultants (AFP)
Session AFP/Berlekamp_Zassenhaus (AFP)
Session AFP/Algebraic_Numbers (AFP)
Session AFP/BenOr_Kozen_Reif (AFP)
Session AFP/LLL_Basis_Reduction (AFP)
Session AFP/LLL_Factorization (AFP)
Session AFP/Linear_Inequalities (AFP)
Session AFP/Linear_Programming (AFP)
Session AFP/Smith_Normal_Form (AFP)
Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP)
Session AFP/Deep_Learning (AFP)
Session AFP/Projective_Measurements (AFP)
Session AFP/Groebner_Bases (AFP)
Session AFP/Fishers_Inequality (AFP)
Session AFP/Groebner_Macaulay (AFP)
Session AFP/Nullstellensatz (AFP)
Session AFP/Signature_Groebner (AFP)
Session AFP/Lambda_Free_KBOs (AFP)
Session AFP/Symmetric_Polynomials (AFP)
Session AFP/Pi_Transcendental (AFP)
Session AFP/Power_Sum_Polynomials (AFP)
Session AFP/Hermite_Lindemann (AFP)
Session AFP/Factor_Algebraic_Polynomial (AFP)
Session AFP/Cubic_Quartic_Equations (AFP)
Session AFP/Linear_Recurrences_Solver (AFP)
Session AFP/Virtual_Substitution (AFP)
Session AFP/Complex_Bounded_Operators (AFP)
Session AFP/QR_Decomposition (AFP)
Session AFP/Van_Emde_Boas_Trees (AFP)
Session AFP/Dijkstra_Shortest_Path (AFP)
Session AFP/Koenigsberg_Friendship (AFP)
Session AFP/FOL_Seq_Calc2 (AFP)
Session AFP/Gale_Shapley (AFP)
Session AFP/HOL-ODE-Numerics (AFP)
Session AFP/HOL-ODE-ARCH-COMP (AFP)
Session AFP/HOL-ODE-Examples (AFP large)
Session AFP/Lorenz_Approximation (AFP)
Session AFP/Lorenz_C0 (AFP large)
Session AFP/Lorenz_C1 (AFP large)
Session AFP/Poincare_Bendixson (AFP)
Session AFP/Transition_Systems_and_Automata (AFP)
Session AFP/Adaptive_State_Counting (AFP)
Session AFP/Buchi_Complementation (AFP)
Session AFP/LTL_Master_Theorem (AFP)
Session AFP/LTL_Normal_Form (AFP)
Session AFP/Partial_Order_Reduction (AFP)
Session AFP/CAVA_LTL_Modelchecker (AFP)
Session AFP/Transitive-Closure (AFP)
Session AFP/Network_Security_Policy_Verification (AFP)
Session AFP/Planarity_Certificates (AFP)
Session AFP/Tree-Automata (AFP)
Session AFP/Datatype_Order_Generator (AFP)
Session AFP/Higher_Order_Terms (AFP)
Session AFP/CakeML_Codegen (AFP)
Session AFP/Old_Datatype_Show (AFP)
Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/Mersenne_Primes (AFP)
Session AFP/Separation_Logic_Imperative_HOL (AFP)
Session AFP/Sepref_Prereq (AFP)
Session AFP/Refine_Imperative_HOL (AFP)
Session AFP/Floyd_Warshall (AFP)
Session AFP/Sepref_Basic (AFP)
Session AFP/Flow_Networks (AFP)
Session AFP/EdmondsKarp_Maxflow (AFP)
Session AFP/MFMC_Countable (AFP)
Session AFP/Probabilistic_While (AFP)
Session AFP/Constructive_Cryptography (AFP)
Session AFP/Game_Based_Crypto (AFP)
Session AFP/Multi_Party_Computation (AFP)
Session AFP/Sigma_Commit_Crypto (AFP)
Session AFP/Constructive_Cryptography_CM (AFP)
Session AFP/Prpu_Maxflow (AFP)
Session AFP/Knuth_Morris_Pratt (AFP)
Session AFP/VerifyThis2018 (AFP)
Session AFP/VerifyThis2019 (AFP)
Session AFP/Simplicial_complexes_and_boolean_functions (AFP)
Session AFP/UpDown_Scheme (AFP)
Session AFP/X86_Semantics (AFP)
Session AFP/CZH_Foundations (AFP)
Session AFP/CZH_Elementary_Categories (AFP)
Session AFP/CZH_Universal_Constructions (AFP)
Session AFP/MonoidalCategory (AFP)
Session AFP/Ordinal_Partitions (AFP)
Session AFP/Wetzels_Problem (AFP)
Session AFP/Recursion-Addition (AFP)
Session AFP/Delta_System_Lemma (AFP)
Session AFP/Transitive_Models (AFP)
Session AFP/Independence_CH (AFP)
Building Linear_Inequalities ...
Linear_Inequalities: theory Linear_Inequalities.Missing_Matrix
Linear_Inequalities: theory Linear_Inequalities.Missing_VS_Connect
Linear_Inequalities: theory Linear_Inequalities.Sum_Vec_Set
Linear_Inequalities: theory Linear_Inequalities.Basis_Extension
Linear_Inequalities: theory Linear_Inequalities.Integral_Bounded_Vectors
Linear_Inequalities: theory Linear_Inequalities.Cone
Linear_Inequalities: theory Linear_Inequalities.Convex_Hull
Linear_Inequalities: theory Linear_Inequalities.Dim_Span
Linear_Inequalities: theory Linear_Inequalities.Normal_Vector
Linear_Inequalities: theory Linear_Inequalities.Fundamental_Theorem_Linear_Inequalities
Linear_Inequalities: theory Linear_Inequalities.Farkas_Lemma
Linear_Inequalities: theory Linear_Inequalities.Farkas_Minkowsky_Weyl
Linear_Inequalities: theory Linear_Inequalities.Decomposition_Theorem
Linear_Inequalities: theory Linear_Inequalities.Mixed_Integer_Solutions
Linear_Inequalities: theory Linear_Inequalities.Integer_Hull
Preparing Linear_Inequalities/document ...
Finished Linear_Inequalities/document (0:00:09 elapsed time)
Preparing Linear_Inequalities/outline ...
Finished Linear_Inequalities/outline (0:00:04 elapsed time)
Timing Linear_Inequalities (8 threads, 37.561s elapsed time, 149.247s cpu time, 4.492s GC time, factor 3.97)
Finished Linear_Inequalities (0:01:23 elapsed time, 0:03:55 cpu time, factor 2.83)
LP_Duality: theory LP_Duality.Minimum_Maximum
LP_Duality: theory LP_Duality.LP_Duality
Preparing LP_Duality/document ...
Finished LP_Duality/document (0:00:03 elapsed time)
Preparing LP_Duality/outline ...
Finished LP_Duality/outline (0:00:02 elapsed time)
Timing LP_Duality (8 threads, 4.131s elapsed time, 13.913s cpu time, 0.153s GC time, factor 3.37)
Finished LP_Duality (0:00:14 elapsed time, 0:00:23 cpu time, factor 1.68)
Presentation in "/media/data/jenkins/workspace/isabelle-all/browser_info"
Presenting document CTT/document
Presenting document FOL/document
Presenting document FOL-ex/document
Presenting document CTT/outline
Presenting document FOL-ex/outline
Presenting document FOL/outline
Presenting theory FOLP-ex.Intro
Presenting theory FOL-ex.Natural_Numbers
Presenting theory FOL-ex.Intro
Presenting theory FOLP-ex.Foundation
Presenting theory Cube.Example
Presenting theory FOL-ex.Nat_Class
Presenting theory FOL-ex.Foundation
Presenting document HOL/document
Presenting document HOL/outline
Presenting theory FOL-ex.Prolog
Presenting theory FOLP-ex.Intuitionistic
Presenting theory FOLP-ex.Classical
Presenting theory FOL-ex.Intuitionistic
Presenting theory FOLP-ex.Propositional_Int
Presenting theory FOL-ex.Propositional_Int
Presenting theory FOLP-ex.Quantifiers_Int
Presenting file "$ISABELLE_HOME/src/Provers/typedsimp.ML"
Presenting file "$ISABELLE_HOME/src/Tools/misc_legacy.ML"
Presenting file "intprover.ML"
Presenting theory FOL-ex.Quantifiers_Int
Presenting theory FOLP-ex.Propositional_Cla
Presenting theory CTT.Typechecking
Presenting theory FOLP-ex.Quantifiers_Cla
Presenting AI_Planning_Languages_Semantics ...
Presenting document AI_Planning_Languages_Semantics/document
Presenting document AI_Planning_Languages_Semantics/outline
Presenting theory AI_Planning_Languages_Semantics.Error_Monad_Add
Presenting theory CTT.Elimination
Presenting file "$ISABELLE_HOME/src/Tools/misc_legacy.ML"
Presenting file "$ISABELLE_HOME/src/Provers/splitter.ML"
Presenting file "$ISABELLE_HOME/src/Provers/hypsubst.ML"
Presenting file "$ISABELLE_HOME/src/Tools/IsaPlanner/zipper.ML"
Presenting file "$ISABELLE_HOME/src/Tools/IsaPlanner/isand.ML"
Presenting theory CTT.Equality
Presenting file "$ISABELLE_HOME/src/Tools/IsaPlanner/rw_inst.ML"
Presenting theory AI_Planning_Languages_Semantics.Option_Monad_Add
Presenting file "$ISABELLE_HOME/src/Provers/quantifier1.ML"
Presenting file "$ISABELLE_HOME/src/Tools/intuitionistic.ML"
Presenting file "$ISABELLE_HOME/src/Tools/project_rule.ML"
Presenting file "$ISABELLE_HOME/src/Tools/atomize_elim.ML"
Presenting file "intprover.ML"
Presenting theory FOL-ex.Classical
Presenting theory CTT.Synthesis
Presenting document AVL-Trees/document
Presenting document AVL-Trees/outline
Presenting theory FOL-ex.Propositional_Cla
Presenting theory FOL-ex.Quantifiers_Cla
Presenting theory AI_Planning_Languages_Semantics.SASP_Semantics
Presenting theory FOL-ex.Miniscope
Presenting theory ML_Bootstrap
Presenting theory AVL-Trees.AVL
Presenting theory AI_Planning_Languages_Semantics.SASP_Checker
Presenting theory Pure.Sessions
Presenting document AWN/document
Presenting document AWN/outline
Presenting theory AWN.TransitionSystems
Presenting theory AVL-Trees.AVL2
Presenting Abortable_Linearizable_Modules ...
Presenting document Abortable_Linearizable_Modules/document
Presenting document Abortable_Linearizable_Modules/outline
Presenting theory Abortable_Linearizable_Modules.Sequences
Presenting file "classical.ML"
Presenting Abstract-Hoare-Logics ...
Presenting document Abstract-Hoare-Logics/document
Presenting document Abstract-Hoare-Logics/outline
Presenting theory AI_Planning_Languages_Semantics.PDDL_STRIPS_Semantics
Presenting theory Abstract-Hoare-Logics.Lang
Presenting theory AWN.Invariants
Presenting theory Abstract-Hoare-Logics.Hoare
Presenting theory FOL-ex.Locale_Test1
Presenting theory FOL-ex.Locale_Test2
Presenting theory FOL-ex.Locale_Test3
Presenting theory FOL-ex.Locale_Test
Presenting Ackermanns_not_PR ...
Presenting theory Abstract-Hoare-Logics.Termi
Presenting document Ackermanns_not_PR/document
Presenting document Ackermanns_not_PR/outline
Presenting theory Abortable_Linearizable_Modules.IOA
Presenting theory Ackermanns_not_PR.Primrec
Presenting theory Abstract-Hoare-Logics.HoareTotal
Presenting document Allen_Calculus/document
Presenting document Allen_Calculus/outline
Presenting theory Allen_Calculus.xor_cal
Presenting theory Allen_Calculus.axioms
Presenting theory Abortable_Linearizable_Modules.RDR
Presenting theory AI_Planning_Languages_Semantics.PDDL_STRIPS_Checker
Presenting theory Abortable_Linearizable_Modules.SLin
Presenting theory Abstract-Hoare-Logics.PLang
Presenting theory AWN.OInvariants
Presenting theory AI_Planning_Languages_Semantics.Lifschitz_Consistency
Presenting document AnselmGod/document
Presenting document AnselmGod/outline
Presenting Approximation_Algorithms ...
Presenting document Approximation_Algorithms/document
Presenting document Approximation_Algorithms/outline
Presenting theory AnselmGod.AnselmGod
Presenting Aristotles_Assertoric_Syllogistic ...
Presenting document Aristotles_Assertoric_Syllogistic/document
Presenting document Aristotles_Assertoric_Syllogistic/outline
Presenting theory Aristotles_Assertoric_Syllogistic.AristotlesAssertoric
Presenting ArrowImpossibilityGS ...
Presenting document ArrowImpossibilityGS/document
Presenting document ArrowImpossibilityGS/outline
Presenting theory Abstract-Hoare-Logics.PHoare
Presenting theory Abortable_Linearizable_Modules.Simulations
Presenting theory ArrowImpossibilityGS.Arrow_Utility
Presenting theory Abstract-Hoare-Logics.PTermi
Presenting theory Approximation_Algorithms.Approx_VC_Hoare
Presenting theory ArrowImpossibilityGS.Arrow_Order
Presenting theory ArrowImpossibilityGS.GS
Presenting document Attack_Trees/document
Presenting document Attack_Trees/outline
Presenting theory Approximation_Algorithms.Approx_SC_Hoare
Presenting theory Attack_Trees.MC
Presenting theory Attack_Trees.AT
Presenting theory Attack_Trees.Infrastructure
Presenting theory Abstract-Hoare-Logics.PHoareTotal
Presenting theory Attack_Trees.GDPRhealthcare
Presenting document Auto2_HOL/document
Presenting document Auto2_HOL/outline
Presenting theory Approximation_Algorithms.Approx_MIS_Hoare
Presenting theory Allen_Calculus.allen
Presenting theory Abstract-Hoare-Logics.PsLang
Presenting theory Allen_Calculus.disjoint_relations
Presenting theory Allen_Calculus.jointly_exhaustive
Presenting theory Abstract-Hoare-Logics.PsHoare
Presenting theory Allen_Calculus.examples
Presenting theory Abstract-Hoare-Logics.PsTermi
Presenting theory Abortable_Linearizable_Modules.Idempotence
Presenting theory Approximation_Algorithms.Approx_LB_Hoare
Presenting theory Abortable_Linearizable_Modules.Consensus
Presenting theory Allen_Calculus.nest
Presenting Auto2_Imperative_HOL ...
Presenting document Auto2_Imperative_HOL/document
Presenting document Auto2_Imperative_HOL/outline
Presenting Automatic_Refinement ...
Presenting document Automatic_Refinement/document
Presenting document Automatic_Refinement/outline
Presenting theory Automatic_Refinement.Refine_Util_Bootstrap1
Presenting file "$ISABELLE_HOME/src/Provers/classical.ML"
Presenting file "$ISABELLE_HOME/src/Provers/blast.ML"
Presenting file "$ISABELLE_HOME/src/Provers/clasimp.ML"
Presenting file "$ISABELLE_HOME/src/Tools/eqsubst.ML"
Presenting file "$ISABELLE_HOME/src/Tools/induct.ML"
Presenting file "$ISABELLE_HOME/src/Tools/case_product.ML"
Presenting theory Automatic_Refinement.Mpat_Antiquot
Presenting document Refine_Monadic/document
Presenting document Refine_Monadic/outline
Presenting theory Refine_Monadic.Refine_Chapter
Presenting theory Auto2_Imperative_HOL.Mapping_Str
Presenting theory Automatic_Refinement.Mk_Term_Antiquot
Presenting theory Refine_Monadic.Refine_Mono_Prover
Presenting file "refine_mono_prover.ML"
Presenting theory Auto2_Imperative_HOL.Lists_Ex
Presenting theory Abstract-Hoare-Logics.PsHoareTotal
Presenting theory Auto2_Imperative_HOL.BST
Presenting theory Auto2_Imperative_HOL.Partial_Equiv_Rel
Presenting theory Refine_Monadic.Refine_Misc
Presenting document Collections/document
Presenting document Collections/outline
Presenting document Collections/userguide
Presenting theory Automatic_Refinement.Refine_Util
Presenting theory Auto2_Imperative_HOL.Union_Find
Presenting theory Automatic_Refinement.Attr_Comb
Presenting theory Automatic_Refinement.Named_Sorted_Thms
Presenting theory Refine_Monadic.RefineG_Transfer
Presenting theory Automatic_Refinement.Prio_List
Presenting theory Collections.Sorted_List_Operations
Presenting theory Auto2_Imperative_HOL.Connectivity
Presenting theory Automatic_Refinement.Tagged_Solver
Presenting theory Collections.HashCode
Presenting theory Collections.Code_Target_ICF
Presenting theory Refine_Monadic.RefineG_Domain
Presenting theory Automatic_Refinement.Anti_Unification
Presenting theory AWN.AWN_Cterms
Presenting theory Auto2_Imperative_HOL.Arrays_Ex
Presenting theory Refine_Monadic.RefineG_Recursion
Presenting theory Refine_Monadic.RefineG_Assert
Presenting theory Auto2_Imperative_HOL.Dijkstra
Presenting theory Auto2_Imperative_HOL.Interval
Presenting theory AWN.AWN_Labels
Presenting theory Auto2_Imperative_HOL.Interval_Tree
Presenting theory AWN.Inv_Cterms
Presenting theory Auto2_Imperative_HOL.Quicksort
Presenting theory AWN.AWN_SOS_Labels
Presenting theory Automatic_Refinement.Misc
Presenting theory Approximation_Algorithms.Approx_BP_Hoare
Presenting theory Auto2_Imperative_HOL.Indexed_PQueue
Presenting theory Collections.SetIterator
Presenting theory Automatic_Refinement.Foldi
Presenting theory Automatic_Refinement.Indep_Vars
Presenting theory Automatic_Refinement.Select_Solve
Presenting theory Automatic_Refinement.Mk_Record_Simp
Presenting theory Automatic_Refinement.Refine_Lib
Presenting file "Cond_Rewr_Conv.ML"
Presenting file "Revert_Abbrev.ML"
Presenting theory Automatic_Refinement.Param_Chapter
Presenting theory Approximation_Algorithms.Center_Selection
Presenting theory CAVA_Base.Statistics
Presenting theory CAVA_Base.Code_String
Presenting theory CAVA_Base.CAVA_Code_Target
Presenting theory CAVA_Base.CAVA_Base
Presenting theory CAVA_Base.Lexord_List
Presenting theory CAVA_Base.All_Of_CAVA_Base
Presenting document CAVA_Automata/document
Presenting document CAVA_Automata/outline
Presenting theory Auto2_Imperative_HOL.RBTree
Presenting theory Refine_Monadic.Refine_Basic
Presenting theory Automatic_Refinement.Relators
Presenting theory Collections.SetIteratorOperations
Presenting theory CAVA_Automata.Digraph_Basic
Presenting theory Automatic_Refinement.Param_Tool
Presenting theory CAVA_Automata.Digraph
Presenting theory Refine_Monadic.Refine_Leof
Presenting theory Refine_Monadic.Refine_Heuristics
Presenting theory Auto2_Imperative_HOL.Rect_Intersect
Presenting theory Automatic_Refinement.Param_HOL
Presenting theory Collections.Proper_Iterator
Presenting theory Automatic_Refinement.Parametricity
Presenting theory Refine_Monadic.Refine_More_Comb
Presenting theory Automatic_Refinement.Autoref_Phases
Presenting theory Automatic_Refinement.Autoref_Data
Presenting theory Automatic_Refinement.Autoref_Tagging
Presenting theory Collections.It_to_It
Presenting theory Automatic_Refinement.Autoref_Id_Ops
Presenting theory CAVA_Automata.Automata
Presenting theory Refine_Monadic.RefineG_While
Presenting file "$ISABELLE_HOME/src/Tools/misc_legacy.ML"
Presenting file "$ISABELLE_HOME/src/Tools/try.ML"
Presenting file "$ISABELLE_HOME/src/Tools/quickcheck.ML"
Presenting file "$ISABELLE_HOME/src/Tools/solve_direct.ML"
Presenting file "$ISABELLE_HOME/src/Tools/IsaPlanner/zipper.ML"
Presenting file "$ISABELLE_HOME/src/Tools/IsaPlanner/isand.ML"
Presenting file "$ISABELLE_HOME/src/Tools/IsaPlanner/rw_inst.ML"
Presenting file "$ISABELLE_HOME/src/Provers/hypsubst.ML"
Presenting file "$ISABELLE_HOME/src/Provers/splitter.ML"
Presenting file "$ISABELLE_HOME/src/Provers/classical.ML"
Presenting file "$ISABELLE_HOME/src/Provers/blast.ML"
Presenting file "$ISABELLE_HOME/src/Provers/clasimp.ML"
Presenting file "$ISABELLE_HOME/src/Tools/eqsubst.ML"
Presenting file "$ISABELLE_HOME/src/Provers/quantifier1.ML"
Presenting file "$ISABELLE_HOME/src/Tools/atomize_elim.ML"
Presenting file "$ISABELLE_HOME/src/Tools/cong_tac.ML"
Presenting file "$ISABELLE_HOME/src/Tools/intuitionistic.ML"
Presenting file "$ISABELLE_HOME/src/Tools/project_rule.ML"
Presenting file "$ISABELLE_HOME/src/Tools/subtyping.ML"
Presenting file "$ISABELLE_HOME/src/Tools/case_product.ML"
Presenting file "Tools/hologic.ML"
Presenting file "Tools/rewrite_hol_proof.ML"
Presenting file "Tools/simpdata.ML"
Presenting file "$ISABELLE_HOME/src/Tools/induct.ML"
Presenting file "$ISABELLE_HOME/src/Tools/induction.ML"
Presenting file "$ISABELLE_HOME/src/Tools/induct_tacs.ML"
Presenting file "$ISABELLE_HOME/src/Tools/coherent.ML"
Presenting file "Tools/cnf.ML"
Presenting theory Automatic_Refinement.Autoref_Fix_Rel
Presenting theory Automatic_Refinement.Autoref_Relator_Interface
Presenting theory Auto2_Imperative_HOL.SepLogic_Base
Presenting file "sep_util_base.ML"
Presenting file "assn_matcher.ML"
Presenting file "sep_steps.ML"
Presenting theory Automatic_Refinement.Autoref_Translate
Presenting theory Automatic_Refinement.Autoref_Gen_Algo
Presenting theory Automatic_Refinement.Autoref_Chapter
Presenting theory Automatic_Refinement.Autoref_Tool
Presenting theory Auto2_HOL.Auto2_Setup
Presenting file "util_base.ML"
Presenting file "util_logic.ML"
Presenting file "propertydata.ML"
Presenting file "auto2_data.ML"
Presenting file "normalize.ML"
Presenting file "proofsteps.ML"
Presenting file "auto2_state.ML"
Presenting file "logic_steps.ML"
Presenting file "auto2_outer.ML"
Presenting file "auto2_setup.ML"
Presenting theory Automatic_Refinement.Autoref_Bindings_HOL
Presenting theory Collections.SetIteratorGA
Presenting theory Automatic_Refinement.Automatic_Refinement
Presenting CAVA_LTL_Modelchecker ...
Presenting document CAVA_LTL_Modelchecker/document
Presenting document CAVA_LTL_Modelchecker/outline
Presenting theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics
Presenting theory AWN.OAWN_SOS
Presenting theory CAVA_Automata.Lasso
Presenting theory AWN.OAWN_SOS_Labels
Presenting theory CAVA_LTL_Modelchecker.NDFS_SI
Presenting theory Auto2_Imperative_HOL.SepAuto
Presenting file "sep_steps_test.ML"
Presenting theory CAVA_Automata.Simulation
Presenting theory Auto2_Imperative_HOL.GCD_Impl
Presenting theory CAVA_LTL_Modelchecker.CAVA_Abstract
Presenting theory CAVA_Automata.Step_Conv
Presenting theory CAVA_LTL_Modelchecker.BoolProgs
Presenting theory Collections.Gen_Iterator
Presenting theory Refine_Monadic.Refine_While
Presenting theory CAVA_LTL_Modelchecker.BoolProgs_Extras
Presenting theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv
Presenting theory CAVA_Automata.Stuttering_Extension
Presenting theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers
Presenting theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter
Presenting theory CAVA_LTL_Modelchecker.BoolProgs_Simple
Presenting theory Collections.Idx_Iterator
Presenting theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters
Presenting theory Collections.Iterator
Presenting theory CAVA_LTL_Modelchecker.BoolProgs_Programs
Presenting theory Refine_Monadic.Refine_Det
Presenting theory Auto2_Imperative_HOL.LinkedList
Presenting file "list_matcher_test.ML"
Presenting theory Refine_Monadic.Refine_Pfun
Presenting theory Collections.RBT_add
Presenting theory Refine_Monadic.Refine_Transfer
Presenting theory Auto2_HOL.Auto2_HOL_Extra_Setup
Presenting file "unfolding.ML"
Presenting file "induct_outer.ML"
Presenting file "extra_hol.ML"
Presenting file "auto2_hol_extra_setup.ML"
Presenting theory Collections.Dlist_add
Presenting theory Auto2_HOL.HOL_Base
Presenting theory CAVA_LTL_Modelchecker.CAVA_Impl
Presenting theory Auto2_Imperative_HOL.BST_Impl
Presenting theory CAVA_Automata.Digraph_Impl
Presenting theory Auto2_HOL.Auto2_HOL_Setup
Presenting file "auto2_hol_util_base.ML"
Presenting theory Collections.Assoc_List
Presenting theory AWN.ONode_Lifting
Presenting theory Auto2_HOL.Logic_Thms
Presenting theory Auto2_HOL.Order_Thms
Presenting file "util_arith.ML"
Presenting theory CAVA_LTL_Modelchecker.Mulog
Presenting theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS
Presenting theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker
Presenting document DFS_Framework/document
Presenting document DFS_Framework/outline
Presenting theory DFS_Framework.DFS_Framework_Misc
Presenting theory Collections.Diff_Array
Presenting theory Collections.Partial_Equivalence_Relation
Presenting theory DFS_Framework.DFS_Framework_Refine_Aux
Presenting theory Collections.ICF_Tools
Presenting theory DFS_Framework.Impl_Rev_Array_Stack
Presenting theory Collections.Ord_Code_Preproc
Presenting theory Auto2_Imperative_HOL.RBTree_Impl
Presenting theory Collections.Record_Intf
Presenting theory DFS_Framework.On_Stack
Presenting theory DFS_Framework.DFS_Chapter_Framework
Presenting theory CAVA_Automata.Automata_Impl
Presenting theory Auto2_Imperative_HOL.Arrays_Impl
Presenting theory Collections.Locale_Code
Presenting theory Collections.ICF_Spec_Base
Presenting theory CAVA_Automata.All_Of_CAVA_Automata
Presenting document Gabow_SCC/document
Presenting document Gabow_SCC/outline
Presenting theory Auto2_Imperative_HOL.Quicksort_Impl
Presenting theory Auto2_Imperative_HOL.Union_Find_Impl
Presenting theory Auto2_Imperative_HOL.Connectivity_Impl
Presenting theory Auto2_Imperative_HOL.DynamicArray
Presenting theory Auto2_Imperative_HOL.Indexed_PQueue_Impl
Presenting theory Refine_Monadic.Refine_Foreach
Presenting theory Auto2_Imperative_HOL.Dijkstra_Impl
Presenting theory Auto2_Imperative_HOL.IntervalTree_Impl
Presenting theory Refine_Monadic.Refine_Automation
Presenting theory Refine_Monadic.Autoref_Monadic
Presenting theory Refine_Monadic.Refine_Monadic
Presenting theory Refine_Monadic.Example_Chapter
Presenting theory DFS_Framework.Param_DFS
Presenting theory Gabow_SCC.Gabow_Skeleton
Presenting theory HOL.Orderings
Presenting file "$ISABELLE_HOME/src/Provers/order_procedure.ML"
Presenting file "$ISABELLE_HOME/src/Provers/order_tac.ML"
Presenting theory Refine_Monadic.Breadth_First_Search
Presenting theory AWN.OPnet_Lifting
Presenting theory Auto2_Imperative_HOL.Rect_Intersect_Impl
Presenting theory Auto2_Imperative_HOL.Sep_Examples
Presenting theory Refine_Monadic.WordRefine
Presenting theory Refine_Monadic.Examples
Presenting document LTL_to_GBA/document
Presenting document LTL_to_GBA/outline
Presenting document Promela/document
Presenting document Promela/outline
Presenting theory Promela.PromelaStatistics
Presenting theory Promela.PromelaAST
Presenting theory Auto2_HOL.Arith_Thms
Presenting file "order_test.ML"
Presenting theory Collections.MapSpec
Presenting file "nat_sub_test.ML"
Presenting theory AWN.OClosed_Lifting
Presenting theory Gabow_SCC.Gabow_SCC
Presenting theory Gabow_SCC.Find_Path
Presenting theory Auto2_HOL.Set_Thms
Presenting file "Tools/group_cancel.ML"
Presenting theory HOL.Lattices
Presenting theory Gabow_SCC.Gabow_GBG
Presenting theory DFS_Framework.DFS_Invars_Basic
Presenting theory Auto2_HOL.Lists_Thms
Presenting file "list_ac_test.ML"
Presenting theory HOL.Boolean_Algebras
Presenting file "Tools/boolean_algebra_cancel.ML"
Presenting theory Auto2_HOL.Auto2_Main
Presenting theory AWN.AWN_Invariants
Presenting theory Gabow_SCC.Gabow_Skeleton_Code
Presenting theory Gabow_SCC.Gabow_SCC_Code
Presenting theory Gabow_SCC.Find_Path_Impl
Presenting theory DFS_Framework.DFS_Invars_SCC
Presenting theory Gabow_SCC.Gabow_GBG_Code
Presenting theory Gabow_SCC.All_Of_Gabow_SCC
Presenting theory SM.SOS_Misc_Add
Presenting theory SM.SM_Datastructures
Presenting theory SM.Gen_Scheduler
Presenting theory Promela.PromelaDatastructures
Presenting theory SM.Gen_Scheduler_Refine
Presenting theory SM.SM_Syntax
Presenting theory Auto2_HOL.Auto2_Test
Presenting file "util_test.ML"
Presenting file "rewrite_test.ML"
Presenting theory DFS_Framework.General_DFS_Structure
Presenting file "matcher_test.ML"
Presenting file "normalize_test.ML"
Presenting file "logic_steps_test.ML"
Presenting file "acdata_test.ML"
Presenting theory SM.SM_Semantics
Presenting theory Promela.PromelaInvariants
Presenting theory SM.Decide_Locality
Presenting theory DFS_Framework.Tailrec_Impl
Presenting theory Collections.Robdd
Presenting theory Auto2_HOL.Pelletier
Presenting theory SM.Type_System
Presenting theory SM.SM_Finite_Reachable
Presenting theory Auto2_HOL.Primes_Ex
Presenting Collections_Examples ...
Presenting file "Tools/typedef.ML"
Presenting document Collections_Examples/document
Presenting document Collections_Examples/outline
Presenting theory Collections_Examples.Examples_Chapter
Presenting theory Collections_Examples.Collection_Autoref_Examples_Chapter
Presenting theory Collections_Examples.Succ_Graph
Presenting theory DFS_Framework.Rec_Impl
Presenting theory AWN.OAWN_Invariants
Presenting theory Collections_Examples.Coll_Test
Presenting theory SM.Pid_Scheduler
Presenting theory Collections_Examples.Simple_DFS
Presenting theory SM.Gen_Cfg_Bisim
Presenting theory Collections_Examples.ICF_Test
Presenting theory Collections_Examples.ICF_Only_Test
Presenting theory Collections.Locale_Code_Ex
Presenting theory SM.Rename_Cfg
Presenting theory SM.SM_Visible
Presenting theory Collections.DatRef
Presenting theory DFS_Framework.Simple_Impl
Presenting theory Collections_Examples.Nested_DFS
Presenting theory SM.SM_Variables
Presenting theory Collections_Examples.Combined_TwoSat
Presenting theory Collections_Examples.Collection_Autoref_Examples
Presenting theory Collections_Examples.Refine_Monadic_Examples_Chapter
Presenting theory Collections_Examples.Bfs_Impl
Presenting theory Collections_Examples.Foreach_Refine
Presenting theory Collections_Examples.Refine_Fold
Presenting theory AWN.OAWN_Convert
Presenting theory Collections_Examples.Refine_Monadic_Examples
Presenting theory DFS_Framework.Restr_Impl
Presenting theory Collections_Examples.ICF_Examples_Chapter
Presenting theory DFS_Framework.DFS_Framework
Presenting theory DFS_Framework.DFS_Chapter_Examples
Presenting theory SM.SM_Sticky
Presenting theory Collections_Examples.itp_2010
Presenting theory Collections_Examples.Exploration
Presenting theory Collections_Examples.Exploration_DFS
Presenting theory Collections_Examples.PerformanceTest
Presenting theory Collections_Examples.ICF_Examples
Presenting theory Collections_Examples.Collection_Examples
Presenting Dijkstra_Shortest_Path ...
Presenting document Dijkstra_Shortest_Path/document
Presenting document Dijkstra_Shortest_Path/outline
Presenting theory Dijkstra_Shortest_Path.Introduction
Presenting theory Dijkstra_Shortest_Path.Dijkstra_Misc
Presenting theory DFS_Framework.Cyc_Check
Presenting theory Dijkstra_Shortest_Path.Graph
Presenting theory Dijkstra_Shortest_Path.Weight
Presenting file "Tools/functor.ML"
Presenting theory LTL_to_GBA.LTL_to_GBA
Presenting theory Collections.SetAbstractionIterator
Presenting theory Collections.GenCF_Chapter
Presenting theory Collections.GenCF_Intf_Chapter
Presenting theory DFS_Framework.DFS_Find_Path
Presenting theory AWN.Qmsg_Lifting
Presenting theory Promela.Promela
Presenting theory Dijkstra_Shortest_Path.Dijkstra
Presenting theory Collections.Intf_Map
Presenting theory DFS_Framework.Reachable_Nodes
Presenting theory Dijkstra_Shortest_Path.GraphSpec
Presenting theory Promela.PromelaLTL
Presenting theory Promela.PromelaLTLConv
Presenting theory Promela.All_Of_Promela
Presenting theory Dijkstra_Shortest_Path.GraphGA
Presenting document Formal_SSA/document
Presenting document Formal_SSA/outline
Presenting theory Collections.Intf_Set
Presenting theory Dijkstra_Shortest_Path.GraphByMap
Presenting theory DFS_Framework.Feedback_Arcs
Presenting theory Collections.Intf_Hash
Presenting theory Dijkstra_Shortest_Path.HashGraphImpl
Presenting theory Formal_SSA.FormalSSA_Misc
Presenting theory Formal_SSA.Serial_Rel
Presenting theory Dijkstra_Shortest_Path.Dijkstra_Impl
Presenting theory Formal_SSA.Mapping_Exts
Presenting theory Formal_SSA.RBT_Mapping_Exts
Presenting theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet
Presenting theory Dijkstra_Shortest_Path.Test
Presenting document Minimal_SSA/document
Presenting document Minimal_SSA/outline
Presenting theory HOL.Complete_Lattices
Presenting theory Collections.Intf_Comp
Presenting theory Collections.GenCF_Gen_Chapter
Presenting theory Minimal_SSA.Irreducible
Presenting document ROBDD/document
Presenting document ROBDD/outline
Presenting theory DFS_Framework.Nested_DFS
Presenting theory ROBDD.Bool_Func
Presenting theory SM.SM_Ample_Impl
Presenting theory SM.SM_Wrapup
Presenting Refine_Imperative_HOL ...
Presenting document Refine_Imperative_HOL/document
Presenting document Refine_Imperative_HOL/outline
Presenting theory Refine_Imperative_HOL.Concl_Pres_Clarification
Presenting theory LTL_to_GBA.LTL_to_GBA_impl
Presenting theory ROBDD.Option_Helpers
Presenting theory LTL_to_GBA.All_Of_LTL_to_GBA
Presenting document BTree/document
Presenting document BTree/outline
Presenting theory Refine_Imperative_HOL.Named_Theorems_Rev
Presenting theory Refine_Imperative_HOL.Pf_Add
Presenting theory Refine_Imperative_HOL.Pf_Mono_Prover
Presenting theory Formal_SSA.Graph_path
Presenting theory Collections.Gen_Set
Presenting theory ROBDD.Abstract_Impl
Presenting theory DFS_Framework.Tarjan_LowLink
Presenting theory Refine_Imperative_HOL.PO_Normalizer
Presenting file "PO_Normalizer.ML"
Presenting theory ROBDD.Pointer_Map
Presenting theory ROBDD.Middle_Impl
Presenting theory ROBDD.Array_List
Presenting theory Refine_Imperative_HOL.Sepref_Misc
Presenting theory ROBDD.Pointer_Map_Impl
Presenting theory Refine_Imperative_HOL.Structured_Apply
Presenting theory Refine_Imperative_HOL.Term_Synth
Presenting theory ROBDD.Conc_Impl
Presenting theory Refine_Imperative_HOL.User_Smashing
Presenting theory Refine_Imperative_HOL.Sepref_Chapter_Tool
Presenting theory ROBDD.Level_Collapse
Presenting theory ROBDD.BDD_Examples
Presenting theory BTree.BTree_Height
Presenting theory ROBDD.BDD_Code
Presenting document Floyd_Warshall/document
Presenting document Floyd_Warshall/outline
Presenting theory Collections.Gen_Map
Presenting theory Refine_Imperative_HOL.Sepref_Id_Op
Presenting theory Formal_SSA.SSA_CFG
Presenting theory AWN.OClosed_Transfer
Presenting theory Collections.Gen_Map2Set
Presenting theory Collections.Gen_Comp
Presenting theory Collections.GenCF_Impl_Chapter
Presenting theory DFS_Framework.Tarjan
Presenting theory Collections.Impl_Array_Stack
Presenting theory AWN.AWN_Main
Presenting theory DFS_Framework.DFS_All_Examples
Presenting document Flow_Networks/document
Presenting document Flow_Networks/outline
Presenting theory Flow_Networks.Fofu_Abs_Base
Presenting theory Flow_Networks.Fofu_Impl_Base
Presenting theory Flow_Networks.Refine_Add_Fofu
Presenting theory Collections.Impl_List_Set
Presenting theory Collections.Array_Iterator
Presenting theory Refine_Imperative_HOL.Sepref_Basic
Presenting theory Formal_SSA.Minimality
Presenting theory Floyd_Warshall.Floyd_Warshall
Presenting theory Flow_Networks.Graph
Presenting theory Floyd_Warshall.Recursion_Combinators
Presenting theory Refine_Imperative_HOL.Sepref_Monadify
Presenting theory Flow_Networks.Network
Presenting theory Floyd_Warshall.FW_Code
Presenting EdmondsKarp_Maxflow ...
Presenting document EdmondsKarp_Maxflow/document
Presenting document EdmondsKarp_Maxflow/outline
Presenting theory Flow_Networks.Residual_Graph
Presenting theory AWN.AWN_Term_Graph
Presenting document Prpu_Maxflow/document
Presenting document Prpu_Maxflow/outline
Presenting theory Refine_Imperative_HOL.Sepref_Constraints
Presenting theory Formal_SSA.Construct_SSA
Presenting theory EdmondsKarp_Maxflow.FordFulkerson_Algo
Presenting theory Collections.Impl_List_Map
Presenting theory Flow_Networks.Augmenting_Flow
Presenting theory BTree.BTree_Set
Presenting theory Refine_Imperative_HOL.Sepref_Frame
Presenting theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
Presenting theory Flow_Networks.Augmenting_Path
Presenting theory EdmondsKarp_Maxflow.EdmondsKarp_Algo
Presenting theory BTree.BTree_Split
Presenting theory Formal_SSA.Construct_SSA_notriv
Presenting theory Flow_Networks.Ford_Fulkerson
Presenting theory Formal_SSA.SSA_Semantics
Presenting theory Formal_SSA.While_Combinator_Exts
Presenting theory Flow_Networks.Graph_Impl
Presenting theory EdmondsKarp_Maxflow.Augmenting_Path_BFS
Presenting theory BTree.Array_SBlit
Presenting theory Formal_SSA.SSA_CFG_code
Presenting theory Prpu_Maxflow.Generic_Push_Relabel
Presenting theory Prpu_Maxflow.Prpu_Common_Inst
Presenting theory Flow_Networks.Network_Impl
Presenting theory Formal_SSA.Construct_SSA_code
Presenting theory BTree.Partially_Filled_Array
Presenting theory Refine_Imperative_HOL.Sepref_Rules
Presenting theory BTree.Basic_Assn
Presenting theory BTree.BTree_Imp
Presenting theory Formal_SSA.SSA_Transfer_Rules
Presenting theory Prpu_Maxflow.Fifo_Push_Relabel
Presenting theory HOL.Ctr_Sugar
Presenting file "Tools/Ctr_Sugar/case_translation.ML"
Presenting file "Tools/Ctr_Sugar/ctr_sugar_util.ML"
Presenting file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
Presenting file "Tools/Ctr_Sugar/ctr_sugar_code.ML"
Presenting file "Tools/Ctr_Sugar/ctr_sugar.ML"
Presenting file "Tools/coinduction.ML"
Presenting theory Prpu_Maxflow.Graph_Topological_Ordering
Presenting theory Refine_Imperative_HOL.Sepref_Combinator_Setup
Presenting theory Prpu_Maxflow.Relabel_To_Front
Presenting theory EdmondsKarp_Maxflow.EdmondsKarp_Impl
Presenting theory Formal_SSA.Construct_SSA_notriv_code
Presenting theory Refine_Imperative_HOL.Sepref_Translate
Presenting theory Collections.Impl_Array_Hash_Map
Presenting theory EdmondsKarp_Maxflow.Edka_Checked_Impl
Presenting theory EdmondsKarp_Maxflow.Edka_Benchmark_Export
Presenting Knuth_Morris_Pratt ...
Presenting document Knuth_Morris_Pratt/document
Presenting document Knuth_Morris_Pratt/outline
Presenting theory Prpu_Maxflow.Prpu_Common_Impl
Presenting theory Refine_Imperative_HOL.Sepref_Definition
Presenting theory Formal_SSA.Generic_Interpretation
Presenting theory Formal_SSA.Generic_Extract
Presenting theory Flow_Networks.NetCheck
Presenting theory Formal_SSA.Disjoin_Transform
Presenting theory Knuth_Morris_Pratt.KMP
Presenting document Kruskal/document
Presenting document Kruskal/outline
Presenting theory BTree.BTree_ImpSet
Presenting document PAC_Checker/document
Presenting document PAC_Checker/outline
Presenting theory Prpu_Maxflow.Fifo_Push_Relabel_Impl
Presenting theory Formal_SSA.WhileGraphSSA
Presenting document VerifyThis2018/document
Presenting document VerifyThis2018/outline
Presenting theory BTree.Imperative_Loops
Presenting theory VerifyThis2018.Dynamic_Array
Presenting theory VerifyThis2018.DRAT_Misc
Presenting theory Kruskal.Kruskal_Misc
Presenting theory Prpu_Maxflow.Relabel_To_Front_Impl
Presenting theory Refine_Imperative_HOL.Sepref_Intf_Util
Presenting theory Prpu_Maxflow.Generated_Code_Test
Presenting document VerifyThis2019/document
Presenting document VerifyThis2019/outline
Presenting theory VerifyThis2018.Array_Map_Default
Presenting theory Kruskal.SeprefUF
Presenting theory VerifyThis2018.Synth_Definition
Presenting theory Refine_Imperative_HOL.Sepref_Tool
Presenting theory Refine_Imperative_HOL.Sepref_Chapter_Setup
Presenting theory BTree.BTree_ImpSplit
Presenting Simplicial_complexes_and_boolean_functions ...
Presenting document Simplicial_complexes_and_boolean_functions/document
Presenting document Simplicial_complexes_and_boolean_functions/outline
Presenting theory PAC_Checker.PAC_More_Poly
Presenting theory Kruskal.MinWeightBasis
Presenting theory Simplicial_complexes_and_boolean_functions.Boolean_functions
Presenting theory VerifyThis2019.Exc_Nres_Monad
Presenting theory Collections.Impl_RBT_Map
Presenting theory VerifyThis2019.VTcomp
Presenting theory VerifyThis2019.Challenge1A
Presenting theory Collections.Impl_Cfun_Set
Presenting theory PAC_Checker.Finite_Map_Multiset
Presenting theory VerifyThis2019.Challenge1B
Presenting theory Kruskal.Kruskal
Presenting theory VerifyThis2019.Challenge2A
Presenting theory VerifyThis2019.Challenge2B
Presenting theory VerifyThis2019.Parallel_Multiset_Fold
Presenting theory Kruskal.Kruskal_Refine
Presenting theory VerifyThis2019.Challenge3
Presenting Transition_Systems_and_Automata ...
Presenting document Transition_Systems_and_Automata/document
Presenting document Transition_Systems_and_Automata/outline
Presenting theory Transition_Systems_and_Automata.Basic
Presenting theory Collections.Impl_Array_Map
Presenting theory Transition_Systems_and_Automata.Sequence
Presenting theory Simplicial_complexes_and_boolean_functions.Simplicial_complex
Presenting theory Kruskal.Kruskal_Impl
Presenting theory Transition_Systems_and_Automata.Sequence_LTL
Presenting theory Collections.Impl_Bit_Set
Presenting theory Simplicial_complexes_and_boolean_functions.Bij_betw_simplicial_complex_bool_func
Presenting theory Transition_Systems_and_Automata.Sequence_Zip
Presenting theory Simplicial_complexes_and_boolean_functions.MkIfex
Presenting theory Transition_Systems_and_Automata.Maps
Presenting theory VerifyThis2018.Exc_Nres_Monad
Presenting theory Transition_Systems_and_Automata.Acceptance
Presenting theory Simplicial_complexes_and_boolean_functions.Evasive
Presenting theory Simplicial_complexes_and_boolean_functions.ListLexorder
Presenting theory VerifyThis2018.VTcomp
Presenting theory Transition_Systems_and_Automata.Degeneralization
Presenting theory Refine_Imperative_HOL.Sepref_HOL_Bindings
Presenting theory Transition_Systems_and_Automata.Transition_System
Presenting theory Transition_Systems_and_Automata.Transition_System_Extra
Presenting theory PAC_Checker.WB_Sort
Presenting theory Collections.Impl_Uv_Set
Presenting theory Transition_Systems_and_Automata.Transition_System_Construction
Presenting theory Collections.Gen_Hash
Presenting theory Collections.GenCF
Presenting theory Collections.ICF_Chapter
Presenting theory Collections.ICF_Spec_Chapter
Presenting theory VerifyThis2018.DF_System
Presenting theory PAC_Checker.More_Loops
Presenting theory VerifyThis2018.Snippets
Presenting theory Transition_Systems_and_Automata.Deterministic
Presenting theory Simplicial_complexes_and_boolean_functions.BDD
Presenting theory VerifyThis2018.Challenge1
Presenting theory Kruskal.UGraph
Presenting theory PAC_Checker.PAC_Specification
Presenting theory VerifyThis2018.Challenge1_short
Presenting theory Transition_Systems_and_Automata.DFA
Presenting theory Refine_Imperative_HOL.Sepref_Foreach
Presenting theory Refine_Imperative_HOL.Sepref_Improper
Presenting theory Refine_Imperative_HOL.Sepref
Presenting theory Refine_Imperative_HOL.Sepref_Chapter_IICF
Presenting theory Simplicial_complexes_and_boolean_functions.Binary_operations
Presenting Adaptive_State_Counting ...
Presenting document Adaptive_State_Counting/document
Presenting document Adaptive_State_Counting/outline
Presenting theory Refine_Imperative_HOL.IICF_Set
Presenting theory PAC_Checker.PAC_Map_Rel
Presenting theory Refine_Imperative_HOL.IICF_List_SetO
Presenting theory VerifyThis2018.Challenge2
Presenting theory Refine_Imperative_HOL.IICF_Multiset
Presenting theory Refine_Imperative_HOL.IICF_Prio_Bag
Presenting theory Refine_Imperative_HOL.IICF_List_Mset
Presenting theory Refine_Imperative_HOL.IICF_List_MsetO
Presenting theory Refine_Imperative_HOL.IICF_List
Presenting theory Kruskal.UGraph_Impl
Presenting theory Refine_Imperative_HOL.IICF_Abs_Heap
Presenting theory VerifyThis2018.Challenge3
Presenting Buchi_Complementation ...
Presenting document Buchi_Complementation/document
Presenting document Buchi_Complementation/outline
Presenting theory Buchi_Complementation.Alternate
Presenting theory Transition_Systems_and_Automata.Nondeterministic
Presenting theory Refine_Imperative_HOL.IICF_HOL_List
Presenting theory Refine_Imperative_HOL.IICF_Array_List
Presenting theory Transition_Systems_and_Automata.NFA
Presenting theory Transition_Systems_and_Automata.DBA
Presenting theory Buchi_Complementation.Graph
Presenting theory Collections.SetSpec
Presenting theory Transition_Systems_and_Automata.DGBA
Presenting theory PAC_Checker.PAC_Checker_Specification
Presenting theory Refine_Imperative_HOL.IICF_Impl_Heap
Presenting theory Adaptive_State_Counting.FSM
Presenting theory Refine_Imperative_HOL.IICF_Map
Presenting theory Transition_Systems_and_Automata.DBA_Combine
Presenting theory Refine_Imperative_HOL.IICF_Prio_Map
Presenting theory Transition_Systems_and_Automata.DBTA
Presenting theory Transition_Systems_and_Automata.DGBTA
Presenting theory Collections.ListSpec
Presenting theory PAC_Checker.PAC_Polynomials
Presenting theory PAC_Checker.PAC_Polynomials_Term
Presenting theory Collections.AnnotatedListSpec
Presenting theory Kruskal.Graph_Definition
Presenting theory Collections.PrioSpec
Presenting theory Transition_Systems_and_Automata.DBTA_Combine
Presenting theory Transition_Systems_and_Automata.DCA
Presenting theory Collections.PrioUniqueSpec
Presenting theory Transition_Systems_and_Automata.DGCA
Presenting theory Collections.ICF_Gen_Algo_Chapter
Presenting theory Collections.SetIteratorCollectionsGA
Presenting theory Refine_Imperative_HOL.IICF_Abs_Heapmap
Presenting theory Buchi_Complementation.Ranking
Presenting theory Transition_Systems_and_Automata.DCA_Combine
Presenting theory Refine_Imperative_HOL.IICF_Array
Presenting theory Transition_Systems_and_Automata.DRA
Presenting theory Kruskal.Graph_Definition_Aux
Presenting theory Transition_Systems_and_Automata.DRA_Combine
Presenting theory Refine_Imperative_HOL.IICF_MS_Array_List
Presenting theory Transition_Systems_and_Automata.Refine
Presenting theory Refine_Imperative_HOL.IICF_Indexed_Array_List
Presenting theory Transition_Systems_and_Automata.Acceptance_Refine
Presenting theory PAC_Checker.PAC_Polynomials_Operations
Presenting theory Adaptive_State_Counting.FSM_Product
Presenting theory PAC_Checker.PAC_Misc
Presenting theory Transition_Systems_and_Automata.Transition_System_Refine
Presenting theory Refine_Imperative_HOL.IICF_Impl_Heapmap
Presenting theory Kruskal.Graph_Definition_Impl
Presenting LTL_Master_Theorem ...
Presenting document LTL_Master_Theorem/document
Presenting document LTL_Master_Theorem/outline
Presenting theory Transition_Systems_and_Automata.DRA_Refine
Presenting theory Collections.MapGA
Presenting theory Refine_Imperative_HOL.IICF_Matrix
Presenting theory Transition_Systems_and_Automata.Implement
Presenting theory Refine_Imperative_HOL.IICF_Array_Matrix
Presenting theory Transition_Systems_and_Automata.DRA_Implement
Presenting theory Transition_Systems_and_Automata.DRA_Nodes
Presenting theory Buchi_Complementation.Complementation
Presenting theory Adaptive_State_Counting.ATC
Presenting theory LTL_Master_Theorem.Syntactic_Fragments_and_Stability
Presenting theory Refine_Imperative_HOL.IICF_Sepl_Binding
Presenting theory Refine_Imperative_HOL.IICF
Presenting theory Refine_Imperative_HOL.Sepref_Chapter_Userguides
Presenting theory PAC_Checker.PAC_Checker
Presenting theory Transition_Systems_and_Automata.DRA_Explicit
Presenting theory Refine_Imperative_HOL.Sepref_Guide_Quickstart
Presenting theory PAC_Checker.PAC_Checker_Relation
Presenting theory PAC_Checker.PAC_Assoc_Map_Rel
Presenting theory Refine_Imperative_HOL.Sepref_Guide_Reference
Presenting theory Refine_Imperative_HOL.Sepref_Guide_General_Util
Presenting theory Refine_Imperative_HOL.Sepref_ICF_Bindings
Presenting theory Transition_Systems_and_Automata.DRA_Translate
Presenting theory LTL_Master_Theorem.After
Presenting theory Refine_Imperative_HOL.Sepref_WGraph
Presenting theory Refine_Imperative_HOL.Sepref_Chapter_Examples
Presenting theory Refine_Imperative_HOL.Sepref_Graph
Presenting theory Refine_Imperative_HOL.Sepref_DFS
Presenting theory Transition_Systems_and_Automata.NBA
Presenting theory Transition_Systems_and_Automata.NGBA
Presenting theory Collections.SetGA
Presenting theory Refine_Imperative_HOL.Sepref_Dijkstra
Presenting theory Refine_Imperative_HOL.Sepref_NDFS
Presenting theory Transition_Systems_and_Automata.NBA_Combine
Presenting theory Collections.SetByMap
Presenting theory Refine_Imperative_HOL.Sepref_Minitests
Presenting theory Collections.ListGA
Presenting theory Transition_Systems_and_Automata.NBA_Graphs
Presenting theory Refine_Imperative_HOL.Worklist_Subsumption
Presenting theory Collections.SetIndex
Presenting theory Refine_Imperative_HOL.Worklist_Subsumption_Impl
Presenting theory Collections.Algos
Presenting theory Transition_Systems_and_Automata.NBA_Refine
Presenting theory Refine_Imperative_HOL.Sepref_Snip_Datatype
Presenting theory PAC_Checker.PAC_Checker_Init
Presenting theory PAC_Checker.PAC_Version
Presenting theory Refine_Imperative_HOL.Sepref_Snip_Combinator
Presenting theory Refine_Imperative_HOL.Sepref_All_Examples
Presenting theory Refine_Imperative_HOL.Sepref_Chapter_Benchmarks
Presenting theory Refine_Imperative_HOL.Heapmap_Bench
Presenting theory Refine_Imperative_HOL.Dijkstra_Benchmark
Presenting theory Refine_Imperative_HOL.NDFS_Benchmark
Presenting Partial_Order_Reduction ...
Presenting document Partial_Order_Reduction/document
Presenting document Partial_Order_Reduction/outline
Presenting theory Transition_Systems_and_Automata.NBA_Implement
Presenting theory Partial_Order_Reduction.List_Prefixes
Presenting theory Partial_Order_Reduction.List_Extensions
Presenting theory Collections.PrioByAnnotatedList
Presenting theory LTL_Master_Theorem.Advice
Presenting theory Partial_Order_Reduction.Word_Prefixes
Presenting theory Transition_Systems_and_Automata.NBA_Algorithms
Presenting theory Partial_Order_Reduction.Set_Extensions
Presenting theory Buchi_Complementation.Complementation_Implement
Presenting theory LTL_Master_Theorem.Master_Theorem
Presenting theory Partial_Order_Reduction.Basic_Extensions
Presenting theory Partial_Order_Reduction.Relation_Extensions
Presenting theory Buchi_Complementation.Formula
Presenting theory Partial_Order_Reduction.Transition_System_Extensions
Presenting theory LTL_Master_Theorem.Asymmetric_Master_Theorem
Presenting theory Transition_Systems_and_Automata.NBA_Explicit
Presenting theory Buchi_Complementation.Complementation_Final
Presenting theory Buchi_Complementation.Complementation_Build
Presenting file "code/Autool.mlb"
Presenting file "code/Prelude.sml"
Presenting file "code/Autool.sml"
Presenting Transitive-Closure ...
Presenting document Transitive-Closure/document
Presenting document Transitive-Closure/outline
Presenting theory PAC_Checker.PAC_Checker_Synthesis
Presenting theory Partial_Order_Reduction.Traces
Presenting theory PAC_Checker.PAC_Checker_MLton
Presenting document Tree-Automata/document
Presenting document Tree-Automata/outline
Presenting theory Tree-Automata.Tree
Presenting theory LTL_Master_Theorem.Restricted_Master_Theorem
Presenting theory Partial_Order_Reduction.Transition_System_Traces
Presenting theory Partial_Order_Reduction.Functions
Presenting theory Partial_Order_Reduction.ENat_Extensions
Presenting theory Transitive-Closure.Transitive_Closure_Impl
Presenting theory Partial_Order_Reduction.CCPO_Extensions
Presenting theory Transitive-Closure.Transitive_Closure_List_Impl
Presenting theory Transition_Systems_and_Automata.NBA_Translate
Presenting theory Partial_Order_Reduction.ESet_Extensions
Presenting theory Adaptive_State_Counting.ASC_LB
Presenting theory Collections.PrioUniqueByAnnotatedList
Presenting theory Transitive-Closure.RBT_Map_Set_Extension
Presenting theory Transition_Systems_and_Automata.NGBA_Graphs
Presenting theory LTL_Master_Theorem.Transition_Functions
Presenting theory Collections.ICF_Impl_Chapter
Presenting theory LTL_Master_Theorem.Quotient_Type
Presenting theory LTL_Master_Theorem.Omega_Words_Fun_Stream
Presenting theory Transitive-Closure.Transitive_Closure_RBT_Impl
Presenting theory Transition_Systems_and_Automata.NGBA_Refine
Presenting theory Collections.ListMapImpl
Presenting theory Partial_Order_Reduction.Coinductive_List_Extensions
Presenting theory Transitive-Closure.Finite_Transitive_Closure_Simprocs
Presenting AxiomaticCategoryTheory ...
Presenting document AxiomaticCategoryTheory/document
Presenting document AxiomaticCategoryTheory/outline
Presenting theory Partial_Order_Reduction.LList_Prefixes
Presenting theory Transition_Systems_and_Automata.NGBA_Implement
Presenting theory Transition_Systems_and_Automata.Degeneralization_Refine
Presenting theory Collections.ListMapImpl_Invar
Presenting theory Partial_Order_Reduction.Stuttering
Presenting theory Tree-Automata.Ta
Presenting theory Transition_Systems_and_Automata.NGBA_Algorithms
Presenting theory Collections.RBTMapImpl
Presenting theory Transition_Systems_and_Automata.NBTA
Presenting theory HOL.Inductive
Presenting file "Tools/inductive.ML"
Presenting file "Tools/Old_Datatype/old_datatype_aux.ML"
Presenting file "Tools/Old_Datatype/old_datatype_prop.ML"
Presenting file "Tools/Old_Datatype/old_datatype_data.ML"
Presenting theory Transition_Systems_and_Automata.NGBTA
Presenting file "Tools/Old_Datatype/old_rep_datatype.ML"
Presenting file "Tools/Old_Datatype/old_datatype_codegen.ML"
Presenting file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
Presenting file "Tools/Old_Datatype/old_primrec.ML"
Presenting file "Tools/BNF/bnf_lfp_rec_sugar.ML"
Presenting theory Partial_Order_Reduction.Transition_System_Interpreted_Traces
Presenting theory Transition_Systems_and_Automata.NBTA_Combine
Presenting document BNF_CC/document
Presenting document BNF_CC/outline
Presenting theory BNF_CC.Preliminaries
Presenting theory Partial_Order_Reduction.Ample_Abstract
Presenting theory AxiomaticCategoryTheory.AxiomaticCategoryTheory
Presenting theory Collections.HashMap_Impl
Presenting theory Partial_Order_Reduction.Formula
Presenting document BNF_Operations/document
Presenting theory Partial_Order_Reduction.Ample_Correctness
Presenting document BNF_Operations/outline
Presenting theory Partial_Order_Reduction.Ample_Analysis
Presenting Belief_Revision ...
Presenting document Belief_Revision/document
Presenting document Belief_Revision/outline
Presenting theory Belief_Revision.AGM_Logic
Presenting theory Collections.HashMap
Presenting theory Belief_Revision.AGM_Remainder
Presenting theory LTL_Master_Theorem.DRA_Construction
Presenting theory Belief_Revision.AGM_Contraction
Presenting theory LTL_Master_Theorem.DRA_Implementation
Presenting theory Belief_Revision.AGM_Revision
Presenting theory Collections.Trie_Impl
Presenting BinarySearchTree ...
Presenting document BinarySearchTree/document
Presenting document BinarySearchTree/outline
Presenting theory LTL_Master_Theorem.Extra_Equivalence_Relations
Presenting theory LTL_Master_Theorem.DRA_Instantiation
Presenting theory Collections.Trie2
Presenting theory LTL_Master_Theorem.Code_Export
Presenting Binomial-Queues ...
Presenting document Binomial-Queues/document
Presenting document Binomial-Queues/outline
Presenting theory BinarySearchTree.BinaryTree
Presenting theory Binomial-Queues.PQ
Presenting theory BinarySearchTree.BinaryTree_Map
Presenting theory Collections.TrieMapImpl
Presenting theory BinarySearchTree.BinaryTree_TacticStyle
Presenting document Bondy/document
Presenting document Bondy/outline
Presenting Bounded_Deducibility_Security ...
Presenting document Bounded_Deducibility_Security/document
Presenting document Bounded_Deducibility_Security/outline
Presenting theory Tree-Automata.AbsAlgo
Presenting theory Bounded_Deducibility_Security.Trivia
Presenting theory Bounded_Deducibility_Security.Filtermap
Presenting theory Bounded_Deducibility_Security.Transition_System
Presenting theory Bounded_Deducibility_Security.IO_Automaton
Presenting theory Bounded_Deducibility_Security.Abstract_BD_Security
Presenting theory Bounded_Deducibility_Security.BD_Security_TS
Presenting theory Bounded_Deducibility_Security.BD_Security_IO
Presenting theory Bounded_Deducibility_Security.BD_Security_Triggers
Presenting theory BNF_CC.Axiomatised_BNF_CC
Presenting theory Bounded_Deducibility_Security.BD_Security_Unwinding
Presenting theory Binomial-Queues.Binomial_Queue
Presenting theory Bounded_Deducibility_Security.Compositional_Reasoning
Presenting theory Bounded_Deducibility_Security.Bounded_Deducibility_Security
Presenting BD_Security_Compositional ...
Presenting document BD_Security_Compositional/document
Presenting document BD_Security_Compositional/outline
Presenting theory Collections.ArrayHashMap_Impl
Presenting theory BNF_Operations.LFP
Presenting theory Collections.ArrayHashMap
Presenting theory Collections.ArrayMapImpl
Presenting theory Collections.MapStdImpl
Presenting theory BD_Security_Compositional.Composing_Security
Presenting theory Collections.ListSetImpl
Presenting theory BD_Security_Compositional.Trivial_Security
Presenting theory Adaptive_State_Counting.ASC_Suite
Presenting theory Collections.ListSetImpl_Invar
Presenting theory Collections.ListSetImpl_NotDist
Presenting theory BD_Security_Compositional.Transporting_Security
Presenting theory Tree-Automata.Ta_impl
Presenting theory Tree-Automata.Ta_impl_codegen
Presenting document CoSMeDis/document
Presenting document CoSMeDis/outline
Presenting theory Collections.ListSetImpl_Sorted
Presenting theory HOL.Product_Type
Presenting file "Tools/split_rule.ML"
Presenting file "Tools/set_comprehension_pointfree.ML"
Presenting file "Tools/inductive_set.ML"
Presenting theory CoSMeDis.Prelim
Presenting theory Collections.RBTSetImpl
Presenting theory Binomial-Queues.PQ_Implementation
Presenting document CoCon/document
Presenting document CoCon/outline
Presenting theory Collections.HashSet
Presenting theory BNF_Operations.GFP
Presenting theory Collections.TrieSetImpl
Presenting theory HOL.Sum_Type
Presenting theory CoCon.Prelim
Presenting theory Collections.ArrayHashSet
Presenting theory Collections.ArraySetImpl
Presenting theory Collections.SetStdImpl
Presenting theory BNF_Operations.Compose
Presenting theory CoSMeDis.System_Specification
Presenting theory BNF_Operations.Kill
Presenting theory BNF_Operations.Lift
Presenting theory Collections.Fifo
Presenting theory BNF_Operations.Permute
Presenting theory Collections.BinoPrioImpl
Presenting theory BNF_CC.Composition
Presenting theory CoSMeDis.API_Network
Presenting theory Collections.SkewPrioImpl
Presenting theory BNF_Operations.N2M
Presenting theory CoSMeDis.Automation_Setup
Presenting document CoSMed/document
Presenting document CoSMed/outline
Presenting theory CoSMed.Prelim
Presenting theory Collections.FTAnnotatedListImpl
Presenting theory CoSMed.System_Specification
Presenting theory CoSMeDis.Safety_Properties
Presenting theory Collections.FTPrioImpl
Presenting theory CoSMeDis.Post_Intro
Presenting theory CoSMed.Automation_Setup
Presenting theory Collections.FTPrioUniqueImpl
Presenting theory Collections.ICF_Impl
Presenting theory CoSMed.Safety_Properties
Presenting theory CoSMed.Observation_Setup
Presenting theory CoSMed.Post_Intro
Presenting theory CoSMeDis.Post_Observation_Setup_ISSUER
Presenting theory CoSMed.Post_Value_Setup
Presenting theory CoSMeDis.Post_Unwinding_Helper_ISSUER
Presenting theory CoSMeDis.Post_Value_Setup_ISSUER
Presenting theory Collections.ICF_Refine_Monadic
Presenting theory CoSMeDis.Post_ISSUER
Presenting theory CoCon.System_Specification
Presenting theory CoSMed.Friend_Intro
Presenting theory CoCon.Automation_Setup
Presenting theory Adaptive_State_Counting.ASC_Sufficiency
Presenting theory BNF_CC.Fixpoints
Presenting theory CoSMeDis.Post_Observation_Setup_RECEIVER
Presenting theory BD_Security_Compositional.Composing_Security_Network
Presenting file "Tools/arith_data.ML"
Presenting file "$ISABELLE_HOME/src/Provers/Arith/cancel_div_mod.ML"
Presenting theory CoSMeDis.Post_Unwinding_Helper_RECEIVER
Presenting theory Collections.ICF_Autoref
Presenting theory Collections.ICF_Entrypoints_Chapter
Presenting theory Collections.Collections
Presenting theory CoSMeDis.Post_Value_Setup_RECEIVER
Presenting theory CoSMed.Friend_Value_Setup
Presenting theory BD_Security_Compositional.Independent_Secrets
Presenting BytecodeLogicJmlTypes ...
Presenting document BytecodeLogicJmlTypes/document
Presenting document BytecodeLogicJmlTypes/outline
Presenting theory CoSMeDis.Post_RECEIVER
Presenting theory CoCon.Safety_Properties
Presenting theory CoCon.Observation_Setup
Presenting theory CoCon.Paper_Intro
Presenting theory CoSMeDis.Post_COMPOSE2
Presenting theory BytecodeLogicJmlTypes.AssocLists
Presenting theory BNF_CC.Subtypes
Presenting theory BNF_CC.Quotient_Preservation
Presenting theory BNF_CC.Operation_Examples
Presenting theory CoCon.Paper_Value_Setup
Presenting theory CoSMeDis.Post_Network
Presenting theory Collections.CollectionsV1
Presenting theory Collections.Collections_Entrypoints_Chapter
Presenting theory CoSMeDis.DYNAMIC_Post_Value_Setup_ISSUER
Presenting theory CoCon.Paper_Aut_PC
Presenting theory BNF_CC.Concrete_Examples
Presenting theory CoSMed.Friend
Presenting theory CoSMed.Friend_Request_Intro
Presenting theory CoCon.Paper_Aut
Presenting C2KA_DistributedSystems ...
Presenting document C2KA_DistributedSystems/document
Presenting document C2KA_DistributedSystems/outline
Presenting theory C2KA_DistributedSystems.Stimuli
Presenting theory CoCon.Paper_All
Presenting theory CoCon.Review_Intro
Presenting theory C2KA_DistributedSystems.CKA
Presenting theory Collections.Refine_Dflt
Presenting theory C2KA_DistributedSystems.C2KA
Presenting theory C2KA_DistributedSystems.Topology_C2KA
Presenting theory C2KA_DistributedSystems.Communication_C2KA
Presenting document CISC-Kernel/document
Presenting document CISC-Kernel/outline
Presenting theory CISC-Kernel.Option_Binders
Presenting theory CISC-Kernel.List_Theorems
Presenting theory CISC-Kernel.K
Presenting file "Tools/nat_arith.ML"
Presenting theory CoCon.Review_Value_Setup
Presenting theory BytecodeLogicJmlTypes.Language
Presenting theory CoSMed.Friend_Request_Value_Setup
Presenting theory Collections.Refine_Dflt_ICF
Presenting theory CoSMeDis.DYNAMIC_Post_ISSUER
Presenting theory CISC-Kernel.SK
Presenting theory Collections.Refine_Dflt_Only_ICF
Presenting theory Collections.Userguides_Chapter
Presenting theory CoSMeDis.DYNAMIC_Post_COMPOSE2
Presenting theory Collections.Refine_Monadic_Userguide
Presenting theory CoCon.Review_RAut
Presenting theory CISC-Kernel.ISK
Presenting theory Collections.ICF_Userguide
Presenting document CRDT/document
Presenting document CRDT/outline
Presenting theory CoSMeDis.DYNAMIC_Post_Network
Presenting theory CRDT.Convergence
Presenting theory CoSMeDis.Independent_Post_Observation_Setup_ISSUER
Presenting theory CRDT.Network
Presenting theory CoSMed.Friend_Request
Presenting theory CoSMed.Traceback_Intro
Presenting theory CISC-Kernel.CISK
Presenting theory CISC-Kernel.Step_configuration
Presenting theory CoSMeDis.Independent_DYNAMIC_Post_Value_Setup_ISSUER
Presenting theory CISC-Kernel.Step_policies
Presenting theory Adaptive_State_Counting.ASC_Hoare
Presenting theory CISC-Kernel.Step
Presenting theory CRDT.Ordered_List
Presenting theory CISC-Kernel.Step_invariants
Presenting theory CISC-Kernel.Step_vpeq
Presenting theory CoSMed.Post_Visibility_Traceback
Presenting theory CISC-Kernel.Step_vpeq_locally_respects
Presenting theory CRDT.Counter
Presenting theory CISC-Kernel.Step_vpeq_weakly_step_consistent
Presenting document IMAP-CRDT/document
Presenting document IMAP-CRDT/outline
Presenting theory IMAP-CRDT.IMAP-def
Presenting theory CoCon.Review_RAut_NCPC
Presenting theory IMAP-CRDT.IMAP-proof-commute
Presenting theory CoSMed.Friend_Traceback
Presenting document CYK/document
Presenting document CYK/outline
Presenting theory IMAP-CRDT.IMAP-proof-helpers
Presenting theory Adaptive_State_Counting.ASC_Example
Presenting theory BytecodeLogicJmlTypes.Logic
Presenting document Card_Multisets/document
Presenting document Card_Multisets/outline
Presenting theory CISC-Kernel.Separation_kernel_model
Presenting file "$ISABELLE_HOME/src/Provers/Arith/fast_lin_arith.ML"
Presenting file "Tools/lin_arith.ML"
Presenting theory CISC-Kernel.Link_separation_kernel_model_to_CISK
Presenting theory Card_Multisets.Card_Multisets
Presenting Card_Partitions ...
Presenting document Card_Partitions/document
Presenting document Card_Partitions/outline
Presenting document Case_Labeling/document
Presenting document Case_Labeling/outline
Presenting theory BytecodeLogicJmlTypes.MultiStep
Presenting theory IMAP-CRDT.IMAP-proof-independent
Presenting theory Card_Partitions.Set_Partition
Presenting theory Card_Partitions.Injectivity_Solver
Presenting theory BytecodeLogicJmlTypes.Reachability
Presenting theory IMAP-CRDT.IMAP-proof
Presenting document Category/document
Presenting document Category/outline
Presenting theory Category.Cat
Presenting theory Card_Partitions.Card_Partitions
Presenting theory CoCon.Review_RAut_NCPC_PAut
Presenting document Cauchy/document
Presenting document Cauchy/outline
Presenting theory CoCon.Review_All
Presenting theory CoCon.Discussion_Intro
Presenting theory Category.SetCat
Presenting theory Cauchy.CauchysMeanTheorem
Presenting theory Cauchy.CauchySchwarz
Presenting theory Category.Functors
Presenting theory CoCon.Discussion_Value_Setup
Presenting Sqrt_Babylonian ...
Presenting document Sqrt_Babylonian/document
Presenting document Sqrt_Babylonian/outline
Presenting theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
Presenting theory Sqrt_Babylonian.Log_Impl
Presenting theory Category.HomFunctors
Presenting theory Case_Labeling.Case_Labeling
Presenting file "print_nested_cases.ML"
Presenting theory Category.NatTrans
Presenting theory Sqrt_Babylonian.NthRoot_Impl
Presenting document Real_Impl/document
Presenting document Real_Impl/outline
Presenting theory Real_Impl.Real_Impl_Auxiliary
Presenting theory Case_Labeling.Labeled_Hoare
Presenting theory Sqrt_Babylonian.Sqrt_Babylonian
Presenting file "labeled_hoare_tac.ML"
Presenting Certification_Monads ...
Presenting document Certification_Monads/document
Presenting document Certification_Monads/outline
Presenting theory Certification_Monads.Error_Syntax
Presenting theory CoSMeDis.Independent_DYNAMIC_Post_ISSUER
Presenting theory CoCon.Discussion_NCPC
Presenting theory CoCon.Discussion_All
Presenting theory CoCon.Decision_Intro
Presenting theory Certification_Monads.Error_Monad
Presenting theory Category.Yoneda
Presenting document Classes/classes
Presenting theory Certification_Monads.Check_Monad
Presenting theory Case_Labeling.Labeled_Hoare_Examples
Presenting theory Real_Impl.Prime_Product
Presenting theory Case_Labeling.Conditionals
Presenting theory CoSMeDis.Independent_Post_Observation_Setup_RECEIVER
Presenting theory CoSMeDis.Independent_Post_Value_Setup_RECEIVER
Presenting theory Classes.Setup
Presenting file "$ISABELLE_HOME/src/Doc/antiquote_setup.ML"
Presenting file "$ISABELLE_HOME/src/Doc/more_antiquote.ML"
Presenting theory Certification_Monads.Strict_Sum
Presenting theory Classes.Classes
Presenting document Clean/document
Presenting document Clean/outline
Presenting theory BytecodeLogicJmlTypes.Sound
Presenting theory CoSMeDis.Independent_Post_RECEIVER
Presenting theory Clean.Lens_Laws
Presenting theory Clean.Optics
Presenting theory Case_Labeling.Monadic_Language
Presenting file "$AFP/Case_Labeling/util.ML"
Presenting theory Case_Labeling.Case_Labeling_Examples
Presenting document ClockSynchInst/document
Presenting document ClockSynchInst/outline
Presenting theory CoCon.Decision_Value_Setup
Presenting theory Certification_Monads.Parser_Monad
Presenting theory Certification_Monads.Misc
Presenting document Codegen/codegen
Presenting theory Clean.MonadSE
Presenting theory Real_Impl.Real_Impl
Presenting theory HOL.Finite_Set
Presenting theory Clean.Seq_MonadSE
Presenting theory CoSMeDis.Independent_DYNAMIC_Post_Network
Presenting theory Codegen.Setup
Presenting file "$ISABELLE_HOME/src/Doc/antiquote_setup.ML"
Presenting file "$ISABELLE_HOME/src/Doc/more_antiquote.ML"
Presenting theory ClockSynchInst.ICAInstance
Presenting theory Codegen.Introduction
Presenting theory Codegen.Foundations
Presenting theory Codegen.Refinement
Presenting theory Clean.Symbex_MonadSE
Presenting theory Real_Impl.Real_Unique_Impl
Presenting theory CoCon.Decision_NCPC
Presenting document CofGroups/document
Presenting document CofGroups/outline
Presenting theory Codegen.Inductive_Predicate
Presenting theory Codegen.Evaluation
Presenting theory ClockSynchInst.LynchInstance
Presenting theory Codegen.Computations
Presenting theory Codegen.Adaptation
Presenting Coinductive_Languages ...
Presenting document Coinductive_Languages/document
Presenting document Coinductive_Languages/outline
Presenting theory Codegen.Further
Presenting Compiling-Exceptions-Correctly ...
Presenting document Compiling-Exceptions-Correctly/document
Presenting document Compiling-Exceptions-Correctly/outline
Presenting theory Compiling-Exceptions-Correctly.Exceptions
Presenting Complete_Non_Orders ...
Presenting document Complete_Non_Orders/document
Presenting document Complete_Non_Orders/outline
Presenting theory CofGroups.CofGroups
Presenting document Completeness/document
Presenting document Completeness/outline
Presenting theory Completeness.PermutationLemmas
Presenting theory HOL.Relation
Presenting theory Completeness.Base
Presenting theory CoCon.Decision_NCPC_Aut
Presenting theory CoCon.Decision_All
Presenting theory CoCon.Reviewer_Assignment_Intro
Presenting theory CoSMeDis.Independent_Posts_Network
Presenting theory CoSMeDis.Post_All
Presenting theory CoSMeDis.Friend_Intro
Presenting theory CoSMeDis.Friend_Observation_Setup
Presenting theory Completeness.Formula
Presenting theory Clean.Hoare_MonadSE
Presenting theory Coinductive_Languages.Coinductive_Language
Presenting theory CoSMeDis.Friend_State_Indistinguishability
Presenting theory Coinductive_Languages.Coinductive_Regular_Set
Presenting theory Completeness.Sequents
Presenting theory CoCon.Reviewer_Assignment_Value_Setup
Presenting theory Clean.Hoare_Clean
Presenting theory HOL.Transitive_Closure
Presenting file "$ISABELLE_HOME/src/Provers/trancl.ML"
Presenting theory CoSMeDis.Friend_Openness
Presenting theory Coinductive_Languages.Context_Free_Grammar
Presenting Complex_Geometry ...
Presenting document Complex_Geometry/document
Presenting document Complex_Geometry/outline
Presenting theory Complete_Non_Orders.Binary_Relations
Presenting theory Complex_Geometry.More_Transcendental
Presenting theory HOL.Wellfounded
Presenting theory Clean.Clean_Symbex
Presenting theory CoSMeDis.Friend_Value_Setup
Presenting theory Clean.Test_Clean
Presenting theory Clean.Clean_Main
Presenting theory Complex_Geometry.Canonical_Angle
Presenting theory Clean.IsPrime
Presenting theory Clean.LinearSearch
Presenting theory BytecodeLogicJmlTypes.Cachera
Presenting document Poincare_Disc/document
Presenting document Poincare_Disc/outline
Presenting theory Completeness.Tree
Presenting theory HOL.Order_Relation
Presenting theory Clean.Quicksort
Presenting theory Poincare_Disc.Hyperbolic_Functions
Presenting theory Poincare_Disc.Tarski
Presenting theory Complete_Non_Orders.Complete_Relations
Presenting theory HOL.Hilbert_Choice
Presenting file "Tools/choice_specification.ML"
Presenting theory CoSMeDis.Friend
Presenting theory Clean.Quicksort_concept
Presenting theory Clean.SquareRoot_concept
Presenting ComponentDependencies ...
Presenting document ComponentDependencies/document
Presenting document ComponentDependencies/outline
Presenting theory Poincare_Disc.Poincare_Lines
Presenting theory Complex_Geometry.More_Complex
Presenting theory CoSMeDis.Friend_Network
Presenting theory CoSMeDis.Friend_All
Presenting theory CoSMeDis.Friend_Request_Intro
Presenting theory CoCon.Reviewer_Assignment_NCPC
Presenting theory ComponentDependencies.DataDependenciesConcreteValues
Presenting theory Poincare_Disc.Poincare_Lines_Ideal_Points
Presenting theory Complete_Non_Orders.Fixed_Points
Presenting theory HOL.BNF_Wellorder_Relation
Presenting theory Complex_Geometry.Angles
Presenting theory Complex_Geometry.More_Set
Presenting theory CoSMeDis.Friend_Request_Value_Setup
Presenting theory Complete_Non_Orders.Kleene_Fixed_Point
Presenting Concurrent_Ref_Alg ...
Presenting document Concurrent_Ref_Alg/document
Presenting document Concurrent_Ref_Alg/outline
Presenting theory Complex_Geometry.Linear_Systems
Presenting theory Concurrent_Ref_Alg.Refinement_Lattice
Presenting theory Concurrent_Ref_Alg.Sequential
Presenting theory Concurrent_Ref_Alg.Parallel
Presenting theory Concurrent_Ref_Alg.Conjunction
Presenting theory ComponentDependencies.DataDependencies
Presenting theory Completeness.Completeness
Presenting theory Concurrent_Ref_Alg.CRA
Presenting theory HOL.BNF_Wellorder_Embedding
Presenting theory Completeness.Soundness
Presenting Concurrent_Revisions ...
Presenting document Concurrent_Revisions/document
Presenting document Concurrent_Revisions/outline
Presenting theory Poincare_Disc.Poincare_Distance
Presenting theory Complex_Geometry.Quadratic
Presenting theory CoSMeDis.Friend_Request
Presenting theory Concurrent_Ref_Alg.Galois_Connections
Presenting theory CoSMeDis.Friend_Request_Network
Presenting theory CoSMeDis.Friend_Request_All
Presenting theory CoSMeDis.Outer_Friend_Intro
Presenting theory CoCon.Reviewer_Assignment_NCPC_Aut
Presenting theory CoSMeDis.Outer_Friend
Presenting theory CoCon.Reviewer_Assignment_All
Presenting theory Poincare_Disc.Poincare_Circles
Presenting theory CoSMeDis.Outer_Friend_Issuer_Observation_Setup
Presenting theory Concurrent_Ref_Alg.Iteration
Presenting theory Concurrent_Revisions.Data
Presenting theory Concurrent_Ref_Alg.Conjunctive_Sequential
Presenting theory Concurrent_Ref_Alg.Infimum_Nat
Presenting theory CoSMeDis.Outer_Friend_Issuer_State_Indistinguishability
Presenting theory CoSMeDis.Outer_Friend_Issuer_Openness
Presenting theory ComponentDependencies.DataDependenciesCaseStudy
Presenting theory Poincare_Disc.Poincare_Between
Presenting theory HOL.BNF_Wellorder_Constructions
Presenting theory Concurrent_Ref_Alg.Conjunctive_Iteration
Presenting Conditional_Simplification ...
Presenting document Conditional_Simplification/document
Presenting document Conditional_Simplification/outline
Presenting theory Conditional_Simplification.CS_Tools
Presenting file "More_Tactical.ML"
Presenting theory CoCon.Traceback_Properties
Presenting theory CoCon.All_BD_Security_Instances_for_CoCon
Presenting Conditional_Transfer_Rule ...
Presenting document Conditional_Transfer_Rule/document
Presenting document Conditional_Transfer_Rule/outline
Presenting theory CoSMeDis.Outer_Friend_Issuer_Value_Setup
Presenting theory Concurrent_Ref_Alg.Rely_Quotient
Presenting Types_To_Sets_Extension ...
Presenting theory Complex_Geometry.Matrices
Presenting document Types_To_Sets_Extension/document
Presenting document Types_To_Sets_Extension/outline
Presenting theory Conditional_Simplification.IHOL_CS
Presenting file "CS_TimeIt.ML"
Presenting file "CS_Cond_Simp.ML"
Presenting theory Conditional_Simplification.Reference_Prerequisites
Presenting file "$ISABELLE_HOME/src/Doc/antiquote_setup.ML"
Presenting theory Conditional_Simplification.CS_Reference
Presenting theory Poincare_Disc.Poincare_Lines_Axis_Intersections
Presenting Consensus_Refined ...
Presenting document Consensus_Refined/document
Presenting document Consensus_Refined/outline
Presenting theory Consensus_Refined.Infra
Presenting theory Consensus_Refined.Consensus_Types
Presenting theory Consensus_Refined.Quorums
Presenting theory Consensus_Refined.Consensus_Misc
Presenting theory Consensus_Refined.Two_Steps
Presenting theory Consensus_Refined.Three_Steps
Presenting theory Poincare_Disc.Poincare_Perpendicular
Presenting theory Complex_Geometry.Unitary_Matrices
Presenting theory Poincare_Disc.Poincare
Presenting theory CoSMeDis.Outer_Friend_Issuer
Presenting theory Consensus_Refined.Refinement
Presenting theory Concurrent_Revisions.Occurrences
Presenting theory CoSMeDis.Outer_Friend_Receiver_Observation_Setup
Presenting theory Consensus_Refined.HO_Transition_System
Presenting theory Types_To_Sets_Extension.ETTS_Tools
Presenting file "More_Library.ML"
Presenting file "More_Term.ML"
Presenting file "More_Logic.ML"
Presenting file "More_Tactical.ML"
Presenting file "More_Simplifier.ML"
Presenting file "More_HOLogic.ML"
Presenting file "More_Transfer.ML"
Presenting file "ETTS_Writer.ML"
Presenting theory Consensus_Refined.Voting
Presenting theory CoSMeDis.Outer_Friend_Receiver_State_Indistinguishability
Presenting theory Consensus_Refined.Voting_Opt
Presenting theory Consensus_Refined.OneThirdRule_Defs
Presenting theory Complex_Geometry.Unitary11_Matrices
Presenting theory CoSMeDis.Outer_Friend_Receiver_Value_Setup
Presenting theory Conditional_Transfer_Rule.CTR_Tools
Presenting file "More_Library.ML"
Presenting file "More_Binding.ML"
Presenting file "More_Type.ML"
Presenting file "More_Sort.ML"
Presenting file "More_Term.ML"
Presenting file "More_Variable.ML"
Presenting file "More_Logic.ML"
Presenting file "More_Simplifier.ML"
Presenting file "More_HOLogic.ML"
Presenting file "More_Transfer.ML"
Presenting file "CTR_Utilities.ML"
Presenting theory Poincare_Disc.Poincare_Tarski
Presenting theory Conditional_Transfer_Rule.IML_UT
Presenting theory Consensus_Refined.OneThirdRule_Proofs
Presenting theory CoSMeDis.Outer_Friend_Receiver
Presenting theory Consensus_Refined.Ate_Defs
Presenting Constructor_Funs ...
Presenting document Constructor_Funs/document
Presenting document Constructor_Funs/outline
Presenting theory CoSMeDis.Outer_Friend_Network
Presenting theory CoSMeDis.Outer_Friend_All
Presenting Correctness_Algebras ...
Presenting document Correctness_Algebras/document
Presenting document Correctness_Algebras/outline
Presenting theory Correctness_Algebras.Base
Presenting theory Complex_Geometry.Hermitean_Matrices
Presenting theory Conditional_Transfer_Rule.UD
Presenting theory Constructor_Funs.Constructor_Funs
Presenting file "constructor_funs.ML"
Presenting file "UD_Consts.ML"
Presenting theory Constructor_Funs.Test_Constructor_Funs
Presenting CryptoBasedCompositionalProperties ...
Presenting document CryptoBasedCompositionalProperties/document
Presenting document CryptoBasedCompositionalProperties/outline
Presenting theory Concurrent_Revisions.Renaming
Presenting theory CryptoBasedCompositionalProperties.ListExtras
Presenting theory CryptoBasedCompositionalProperties.Secrecy_types
Presenting theory Consensus_Refined.Ate_Proofs
Presenting theory CryptoBasedCompositionalProperties.inout
Presenting theory Complex_Geometry.Elementary_Complex_Geometry
Presenting theory Correctness_Algebras.Omega_Algebras
Presenting theory Consensus_Refined.Same_Vote
Presenting theory Consensus_Refined.Observing_Quorums
Presenting theory Correctness_Algebras.Capped_Omega_Algebras
Presenting theory Concurrent_Revisions.Substitution
Presenting theory Consensus_Refined.Observing_Quorums_Opt
Presenting theory CryptoBasedCompositionalProperties.Secrecy
Presenting theory Consensus_Refined.Two_Step_Observing
Presenting theory Complex_Geometry.Homogeneous_Coordinates
Presenting theory Conditional_Transfer_Rule.CTR
Presenting file "CTR_Relators.ML"
Presenting theory Consensus_Refined.Uv_Defs
Presenting file "CTR_Foundations.ML"
Presenting file "CTR_Algorithm.ML"
Presenting file "CTR_Conversions.ML"
Presenting file "CTR_Relativization.ML"
Presenting file "CTR_Parametricity.ML"
Presenting file "CTR_Postprocessing.ML"
Presenting theory CryptoBasedCompositionalProperties.CompLocalSecrets
Presenting theory Correctness_Algebras.General_Refinement_Algebras
Presenting theory Conditional_Transfer_Rule.UD_Tests
Presenting file "UD_TEST_UNOVERLOAD_DEFINITION.ML"
Presenting theory CryptoBasedCompositionalProperties.KnowledgeKeysSecrets
Presenting theory HOL.BNF_Cardinal_Order_Relation
Presenting document DPRM_Theorem/document
Presenting document DPRM_Theorem/outline
Presenting theory Correctness_Algebras.Lattice_Ordered_Semirings
Presenting theory DPRM_Theorem.Parametric_Polynomials
Presenting theory Conditional_Transfer_Rule.CTR_Tests
Presenting file "CTR_TEST_PROCESS_RELATIVIZATION.ML"
Presenting file "CTR_TEST_PROCESS_CTR_RELATOR.ML"
Presenting theory Complex_Geometry.Moebius
Presenting theory Consensus_Refined.Uv_Proofs
Presenting theory DPRM_Theorem.Assignments
Presenting theory Conditional_Transfer_Rule.Reference_Prerequisites
Presenting file "$ISABELLE_HOME/src/Doc/antiquote_setup.ML"
Presenting theory Conditional_Transfer_Rule.CTR_Introduction
Presenting theory Consensus_Refined.BenOr_Defs
Presenting theory Conditional_Transfer_Rule.UD_Reference
Presenting theory Conditional_Transfer_Rule.CTR_Reference
Presenting document DPT-SAT-Solver/document
Presenting document DPT-SAT-Solver/outline
Presenting theory DPRM_Theorem.Diophantine_Relations
Presenting theory DPRM_Theorem.Existential_Quantifier
Presenting theory Correctness_Algebras.Boolean_Semirings
Presenting theory DPRM_Theorem.Modulo_Divisibility
Presenting theory Consensus_Refined.BenOr_Proofs
Presenting theory Complex_Geometry.Circlines
Presenting theory Consensus_Refined.MRU_Vote
Presenting theory Correctness_Algebras.Binary_Iterings
Presenting theory Consensus_Refined.MRU_Vote_Opt
Presenting theory Correctness_Algebras.Binary_Iterings_Strict
Presenting theory HOL.BNF_Cardinal_Arithmetic
Presenting theory Consensus_Refined.Three_Step_MRU
Presenting theory Complex_Geometry.Oriented_Circlines
Presenting theory Consensus_Refined.New_Algorithm_Defs
Presenting theory Correctness_Algebras.Binary_Iterings_Nonstrict
Presenting theory Concurrent_Revisions.OperationalSemantics
Presenting theory Types_To_Sets_Extension.ETTS
Presenting file "ETTS_Tactics.ML"
Presenting file "ETTS_Utilities.ML"
Presenting file "ETTS_Substitution.ML"
Presenting file "ETTS_Context.ML"
Presenting file "ETTS_Algorithm.ML"
Presenting file "ETTS_Active.ML"
Presenting file "ETTS_Lemma.ML"
Presenting file "ETTS_Lemmas.ML"
Presenting theory Complex_Geometry.Circlines_Angle
Presenting theory Correctness_Algebras.Tests
Presenting theory Correctness_Algebras.Test_Iterings
Presenting theory Types_To_Sets_Extension.ETTS_Auxiliary
Presenting theory Concurrent_Revisions.Executions
Presenting theory Correctness_Algebras.N_Semirings
Presenting theory Types_To_Sets_Extension.Manual_Prerequisites
Presenting file "$ISABELLE_HOME/src/Doc/antiquote_setup.ML"
Presenting theory DPT-SAT-Solver.DPT_SAT_Solver
Presenting file "dpt_sat_solver.ML"
Presenting theory Consensus_Refined.New_Algorithm_Proofs
Presenting theory DPT-SAT-Solver.DPT_SAT_Tests
Presenting DataRefinementIBP ...
Presenting document DataRefinementIBP/document
Presenting document DataRefinementIBP/outline
Presenting theory Correctness_Algebras.N_Semirings_Boolean
Presenting theory DataRefinementIBP.Preliminaries
Presenting theory DataRefinementIBP.Statements
Presenting theory Consensus_Refined.Paxos_Defs
Presenting theory DataRefinementIBP.Hoare
Presenting theory Correctness_Algebras.N_Semirings_Modal
Presenting theory Correctness_Algebras.Approximation
Presenting theory Complex_Geometry.Unit_Circle_Preserving_Moebius
Presenting theory DataRefinementIBP.Diagram
Presenting theory Correctness_Algebras.Recursion_Strict
Presenting theory HOL.Fun_Def_Base
Presenting file "Tools/Function/function_lib.ML"
Presenting file "Tools/Function/function_common.ML"
Presenting file "Tools/Function/function_context_tree.ML"
Presenting file "Tools/Function/sum_tree.ML"
Presenting theory DataRefinementIBP.DataRefinement
Presenting theory Consensus_Refined.Paxos_Proofs
Presenting document Datatypes/datatypes
Presenting theory Datatypes.Setup
Presenting file "$ISABELLE_HOME/src/Doc/antiquote_setup.ML"
Presenting theory Concurrent_Revisions.Determinacy
Presenting theory Types_To_Sets_Extension.ETTS_Tests
Presenting file "ETTS_TEST_AMEND_CTXT_DATA.ML"
Presenting file "ETTS_TEST_TTS_ALGORITHM.ML"
Presenting file "ETTS_TEST_TTS_REGISTER_SBTS.ML"
Presenting theory Types_To_Sets_Extension.ETTS_Introduction
Presenting theory Types_To_Sets_Extension.ETTS_Theory
Presenting document Corec/corec
Presenting theory DPRM_Theorem.Exponentiation
Presenting theory Consensus_Refined.CT_Defs
Presenting theory Types_To_Sets_Extension.ETTS_Syntax
Presenting theory Correctness_Algebras.N_Algebras
Presenting theory Types_To_Sets_Extension.ETTS_Examples
Presenting theory Types_To_Sets_Extension.ETTS_CR
Presenting theory Types_To_Sets_Extension.Introduction
Presenting theory Types_To_Sets_Extension.SML_Introduction
Presenting theory Types_To_Sets_Extension.Set_Ext
Presenting theory Complex_Geometry.Riemann_Sphere
Presenting Decl_Sem_Fun_PL ...
Presenting document Decl_Sem_Fun_PL/document
Presenting document Decl_Sem_Fun_PL/outline
Presenting theory Decl_Sem_Fun_PL.Lambda
Presenting theory Types_To_Sets_Extension.Lifting_Set_Ext
Presenting theory Decl_Sem_Fun_PL.SmallStepLam
Presenting theory Types_To_Sets_Extension.Product_Type_Ext
Presenting theory DPRM_Theorem.Alpha_Sequence
Presenting theory Datatypes.Datatypes
Presenting theory Correctness_Algebras.Recursion
Presenting theory DPRM_Theorem.Exponential_Relation
Presenting document Dedekind_Real/document
Presenting document Dedekind_Real/outline
Presenting theory Consensus_Refined.CT_Proofs
Presenting Dependent_SIFUM_Type_Systems ...
Presenting document Dependent_SIFUM_Type_Systems/document
Presenting document Dependent_SIFUM_Type_Systems/outline
Presenting theory DPRM_Theorem.Digit_Function
Presenting theory Dependent_SIFUM_Type_Systems.Preliminaries
Presenting theory Types_To_Sets_Extension.Transfer_Ext
Presenting theory DPRM_Theorem.Binomial_Coefficient
Presenting theory DPRM_Theorem.Binary_Orthogonal
Presenting theory Types_To_Sets_Extension.SML_Relations
Presenting theory DPRM_Theorem.Binary_Masking
Presenting theory Decl_Sem_Fun_PL.BigStepLam
Presenting theory Dedekind_Real.Dedekind_Real
Presenting theory DPRM_Theorem.Binary_And
Presenting Dependent_SIFUM_Refinement ...
Presenting document Dependent_SIFUM_Refinement/document
Presenting document Dependent_SIFUM_Refinement/outline
Presenting theory Decl_Sem_Fun_PL.ValuesFSet
Presenting theory DPRM_Theorem.RegisterMachineSpecification
Presenting theory Decl_Sem_Fun_PL.ValuesFSetProps
Presenting theory Correctness_Algebras.N_Omega_Algebras
Presenting theory Decl_Sem_Fun_PL.RelationalSemFSet
Presenting theory Decl_Sem_Fun_PL.DeclSemAsDenotFSet
Presenting theory Decl_Sem_Fun_PL.EquivRelationalDenotFSet
Presenting theory Dependent_SIFUM_Type_Systems.Security
Presenting theory DPRM_Theorem.RegisterMachineProperties
Presenting theory Decl_Sem_Fun_PL.ChangeEnv
Presenting theory Decl_Sem_Fun_PL.DeclSemAsNDInterpFSet
Presenting theory DPRM_Theorem.RegisterMachineSimulation
Presenting theory Decl_Sem_Fun_PL.InterTypeSystem
Presenting theory Decl_Sem_Fun_PL.Values
Presenting theory DPRM_Theorem.SingleStepRegister
Presenting theory Complex_Geometry.Chordal_Metric
Presenting theory Decl_Sem_Fun_PL.ValueProps
Presenting theory DPRM_Theorem.SingleStepState
Presenting theory Types_To_Sets_Extension.SML_Simple_Orders
Presenting theory Decl_Sem_Fun_PL.DeclSemAsDenot
Presenting Depth-First-Search ...
Presenting document Depth-First-Search/document
Presenting document Depth-First-Search/outline
Presenting theory Types_To_Sets_Extension.SML_Semigroups
Presenting theory Depth-First-Search.DFS
Presenting document Derangements/document
Presenting document Derangements/outline
Presenting theory DPRM_Theorem.MultipleStepRegister
Presenting theory Decl_Sem_Fun_PL.DenotLam5
Presenting theory Correctness_Algebras.N_Omega_Binary_Iterings
Presenting theory Types_To_Sets_Extension.SML_Monoids
Presenting theory Types_To_Sets_Extension.SML_Groups
Presenting theory Correctness_Algebras.N_Relation_Algebras
Presenting theory Types_To_Sets_Extension.SML_Semirings
Presenting theory DPRM_Theorem.MultipleStepState
Presenting theory Types_To_Sets_Extension.SML_Rings
Presenting theory Derangements.Derangements
Presenting theory Correctness_Algebras.Domain
Presenting Dict_Construction ...
Presenting document Dict_Construction/document
Presenting document Dict_Construction/outline
Presenting theory Decl_Sem_Fun_PL.EquivDenotInterTypes
Presenting theory Dict_Construction.Introduction
Presenting theory Dict_Construction.Impossibility
Presenting theory Types_To_Sets_Extension.SML_Semilattices
Presenting theory Correctness_Algebras.Domain_Iterings
Presenting theory DPRM_Theorem.MachineMasking
Presenting theory DPRM_Theorem.MachineEquations
Presenting theory Types_To_Sets_Extension.SML_Lattices
Presenting theory Correctness_Algebras.Domain_Recursion
Presenting theory Decl_Sem_Fun_PL.DenotSoundFSet
Presenting theory DPRM_Theorem.CommutationRelations
Presenting theory Types_To_Sets_Extension.SML_Complete_Lattices
Presenting theory Dependent_SIFUM_Type_Systems.Compositionality
Presenting theory Types_To_Sets_Extension.SML_Linorders
Presenting theory Correctness_Algebras.Extended_Designs
Presenting theory Decl_Sem_Fun_PL.DenotCompleteFSet
Presenting theory Dependent_SIFUM_Type_Systems.Language
Presenting theory Dependent_SIFUM_Refinement.CompositionalRefinement
Presenting theory Decl_Sem_Fun_PL.DenotCongruenceFSet
Presenting theory Decl_Sem_Fun_PL.DenotEqualitiesFSet
Presenting theory Decl_Sem_Fun_PL.Optimizer
Presenting theory Types_To_Sets_Extension.SML_Topological_Space
Presenting theory DPRM_Theorem.MultipleToSingleSteps
Presenting theory DPRM_Theorem.Equation_Setup
Presenting theory Correctness_Algebras.Relative_Domain
Presenting theory DPRM_Theorem.Register_Machine_Sums
Presenting theory Dependent_SIFUM_Refinement.Eg1
Presenting theory Types_To_Sets_Extension.SML_Topological_Space_Countability
Presenting theory DPRM_Theorem.RM_Sums_Diophantine
Presenting theory Types_To_Sets_Extension.SML_Ordered_Topological_Spaces
Presenting theory Dependent_SIFUM_Refinement.Eg1RefinementTrivial
Presenting theory Decl_Sem_Fun_PL.SystemF
Presenting theory Types_To_Sets_Extension.SML_Product_Topology
Presenting theory Types_To_Sets_Extension.SML_Conclusions
Presenting theory Dependent_SIFUM_Refinement.Eg2
Presenting theory Types_To_Sets_Extension.VS_Prerequisites
Presenting theory DPRM_Theorem.Register_Equations
Presenting theory Types_To_Sets_Extension.VS_Groups
Presenting file "Tools/BNF/bnf_util.ML"
Presenting file "Tools/BNF/bnf_tactics.ML"
Presenting file "Tools/BNF/bnf_def_tactics.ML"
Presenting file "Tools/BNF/bnf_def.ML"
Presenting theory Dependent_SIFUM_Refinement.Eg1Eg2
Presenting theory Decl_Sem_Fun_PL.MutableRef
Presenting theory Correctness_Algebras.Relative_Modal
Presenting theory Decl_Sem_Fun_PL.MutableRefProps
Presenting Digit_Expansions ...
Presenting document Digit_Expansions/document
Presenting document Digit_Expansions/outline
Presenting theory DPRM_Theorem.State_0_Equation
Presenting theory Types_To_Sets_Extension.VS_Modules
Presenting theory Correctness_Algebras.Complete_Tests
Presenting theory Correctness_Algebras.Complete_Domain
Presenting theory Digit_Expansions.Bits_Digits
Presenting theory Types_To_Sets_Extension.VS_Vector_Spaces
Presenting theory Types_To_Sets_Extension.VS_Conclusions
Presenting theory Types_To_Sets_Extension.FNDS_Introduction
Presenting theory Types_To_Sets_Extension.FNDS_Set_Ext
Presenting theory DPRM_Theorem.State_d_Equation
Presenting theory Types_To_Sets_Extension.FNDS_Definite_Description
Presenting theory Types_To_Sets_Extension.FNDS_Auxiliary
Presenting theory Digit_Expansions.Carries
Presenting theory DPRM_Theorem.State_Unique_Equations
Presenting theory DPRM_Theorem.All_State_Equations
Presenting theory DPRM_Theorem.Mask_Equations
Presenting theory Types_To_Sets_Extension.Type_Simple_Orders
Presenting theory DPRM_Theorem.Constants_Equations
Presenting theory Correctness_Algebras.Preconditions
Presenting theory DPRM_Theorem.All_Equations_Invariance
Presenting theory Digit_Expansions.Binary_Operations
Presenting Diophantine_Eqns_Lin_Hom ...
Presenting document Diophantine_Eqns_Lin_Hom/document
Presenting document Diophantine_Eqns_Lin_Hom/outline
Presenting theory DPRM_Theorem.All_Equations
Presenting theory DPRM_Theorem.Machine_Equation_Equivalence
Presenting theory Dependent_SIFUM_Refinement.Eg1Eg2RefinementSimple
Presenting theory DPRM_Theorem.DPRM
Presenting Discrete_Summation ...
Presenting document Discrete_Summation/document
Presenting document Discrete_Summation/outline
Presenting theory Types_To_Sets_Extension.Set_Simple_Orders
Presenting theory Dict_Construction.Dict_Construction
Presenting file "dict_construction_util.ML"
Presenting file "transfer_termination.ML"
Presenting file "congruences.ML"
Presenting file "side_conditions.ML"
Presenting file "class_graph.ML"
Presenting file "dict_construction.ML"
Presenting theory Discrete_Summation.Factorials
Presenting theory Types_To_Sets_Extension.Type_Semigroups
Presenting theory Diophantine_Eqns_Lin_Hom.List_Vector
Presenting theory Dict_Construction.Termination
Presenting theory Discrete_Summation.Discrete_Summation
Presenting theory Types_To_Sets_Extension.FNDS_Lifting_Set_Ext
Presenting theory Dict_Construction.Test_Dict_Construction
Presenting theory Types_To_Sets_Extension.Set_Semigroups
Presenting theory Discrete_Summation.Summation_Conversion
Presenting theory Types_To_Sets_Extension.FNDS_Conclusions
Presenting document DiskPaxos/document
Presenting document DiskPaxos/outline
Presenting theory Dict_Construction.Test_Side_Conditions
Presenting theory Discrete_Summation.Examples
Presenting document Dominance_CHK/document
Presenting document Dominance_CHK/outline
Presenting theory Dict_Construction.Test_Lazy_Case
Presenting Efficient-Mergesort ...
Presenting document Efficient-Mergesort/document
Presenting document Efficient-Mergesort/outline
Presenting theory DiskPaxos.DiskPaxos_Model
Presenting theory DiskPaxos.DiskPaxos_Inv1
Presenting theory Efficient-Mergesort.Efficient_Sort
Presenting theory Efficient-Mergesort.Mergesort_Complexity
Presenting theory DiskPaxos.DiskPaxos_Inv2
Presenting theory Efficient-Mergesort.Natural_Mergesort
Presenting document Eisbach/eisbach
Presenting theory Dominance_CHK.Cfg
Presenting theory DiskPaxos.DiskPaxos_Inv3
Presenting theory Dominance_CHK.Sorted_Less2
Presenting theory Eisbach.Base
Presenting file "$ISABELLE_HOME/src/Doc/antiquote_setup.ML"
Presenting theory Eisbach.Preface
Presenting theory Dominance_CHK.Sorted_List_Operations2
Presenting theory Diophantine_Eqns_Lin_Hom.Linear_Diophantine_Equations
Presenting theory HOL.BNF_Composition
Presenting file "Tools/BNF/bnf_comp_tactics.ML"
Presenting file "Tools/BNF/bnf_comp.ML"
Presenting theory Dominance_CHK.Dom_Semi_List
Presenting theory Eisbach.Manual
Presenting theory Correctness_Algebras.Hoare
Presenting Encodability_Process_Calculi ...
Presenting document Encodability_Process_Calculi/document
Presenting document Encodability_Process_Calculi/outline
Presenting theory Diophantine_Eqns_Lin_Hom.Sorted_Wrt
Presenting theory Dominance_CHK.Dom_Kildall
Presenting theory Diophantine_Eqns_Lin_Hom.Minimize_Wrt
Presenting theory HOL.Basic_BNFs
Presenting theory Encodability_Process_Calculi.Relations
Presenting theory Diophantine_Eqns_Lin_Hom.Simple_Algorithm
Presenting theory Encodability_Process_Calculi.ProcessCalculi
Presenting theory DiskPaxos.DiskPaxos_Inv4
Presenting theory Correctness_Algebras.Hoare_Modal
Presenting theory DiskPaxos.DiskPaxos_Inv5
Presenting theory DiskPaxos.DiskPaxos_Chosen
Presenting theory Dependent_SIFUM_Type_Systems.TypeSystem
Presenting theory Correctness_Algebras.Pre_Post
Presenting theory Correctness_Algebras.Pre_Post_Modal
Presenting theory DiskPaxos.DiskPaxos_Inv6
Presenting theory DiskPaxos.DiskPaxos_Invariant
Presenting theory Diophantine_Eqns_Lin_Hom.Algorithm
Presenting theory DiskPaxos.DiskPaxos
Presenting Euler_Partition ...
Presenting document Euler_Partition/document
Presenting document Euler_Partition/outline
Presenting theory Diophantine_Eqns_Lin_Hom.Solver_Code
Presenting Example-Submission ...
Presenting document Example-Submission/document
Presenting document Example-Submission/outline
Presenting theory Example-Submission.Submission
Presenting document FFT/document
Presenting document FFT/outline
Presenting theory Encodability_Process_Calculi.SimulationRelations
Presenting theory Euler_Partition.Euler_Partition
Presenting document FLP/document
Presenting document FLP/outline
Presenting theory FLP.Multiset
Presenting document FOL_Axiomatic/document
Presenting document FOL_Axiomatic/outline
Presenting theory Correctness_Algebras.Monotonic_Boolean_Transformers
Presenting theory FOL_Axiomatic.FOL_Axiomatic
Presenting theory Dependent_SIFUM_Type_Systems.LocallySoundModeUse
Presenting theory FLP.AsynchronousSystem
Presenting theory Encodability_Process_Calculi.Encodings
Presenting theory FOL_Axiomatic.FOL_Axiomatic_Variant
Presenting document FOL_Harrison/document
Presenting document FOL_Harrison/outline
Presenting theory Dominance_CHK.Dom_Kildall_Property
Presenting theory FLP.ListUtilities
Presenting theory Dominance_CHK.Dom_Kildall_Correct
Presenting Factored_Transition_System_Bounding ...
Presenting document Factored_Transition_System_Bounding/document
Presenting document Factored_Transition_System_Bounding/outline
Presenting theory Factored_Transition_System_Bounding.FactoredSystemLib
Presenting theory Dependent_SIFUM_Type_Systems.Example
Presenting theory Dependent_SIFUM_Type_Systems.TypeSystemTactics
Presenting theory Factored_Transition_System_Bounding.ListUtils
Presenting theory Dependent_SIFUM_Type_Systems.Example_TypeSystem
Presenting theory Factored_Transition_System_Bounding.FSSublist
Presenting theory Factored_Transition_System_Bounding.HoArithUtils
Presenting theory Correctness_Algebras.Monotonic_Boolean_Transformers_Instances
Presenting FeatherweightJava ...
Presenting document FeatherweightJava/document
Presenting document FeatherweightJava/outline
Presenting theory Dependent_SIFUM_Type_Systems.Example_Swap_Add
Presenting theory FLP.Execution
Presenting theory Factored_Transition_System_Bounding.FmapUtils
Presenting Featherweight_OCL ...
Presenting document Featherweight_OCL/annex-a
Presenting document Featherweight_OCL/document
Presenting document Featherweight_OCL/outline
Presenting theory Dependent_SIFUM_Refinement.EgHighBranchRevC
Presenting theory Featherweight_OCL.UML_Types
Presenting theory FeatherweightJava.FJDefs
Presenting document FileRefinement/document
Presenting document FileRefinement/outline
Presenting theory FileRefinement.CArrays
Presenting theory FileRefinement.ResizableArrays
Presenting theory FileRefinement.FileRefinement
Presenting document FinFun/document
Presenting document FinFun/outline
Presenting theory FeatherweightJava.FJAux
Presenting theory FLP.FLPSystem
Presenting theory FinFun.FinFun
Presenting theory FinFun.FinFunPred
Presenting Finite-Map-Extras ...
Presenting document Finite-Map-Extras/document
Presenting document Finite-Map-Extras/outline
Presenting theory Featherweight_OCL.UML_Logic
Presenting theory Finite-Map-Extras.Finite_Map_Extras
Presenting Finite_Automata_HF ...
Presenting document Finite_Automata_HF/document
Presenting document Finite_Automata_HF/outline
Presenting theory Finite_Automata_HF.Finite_Automata_HF
Presenting Fishburn_Impossibility ...
Presenting document Fishburn_Impossibility/document
Presenting document Fishburn_Impossibility/outline
Presenting theory Featherweight_OCL.UML_PropertyProfiles
Presenting theory FOL_Harrison.FOL_Harrison
Presenting document Flyspeck-Tame/document
Presenting document Flyspeck-Tame/outline
Presenting theory Featherweight_OCL.UML_Boolean
Presenting theory Featherweight_OCL.UML_Void
Presenting theory Fishburn_Impossibility.Social_Choice_Functions
Presenting theory Featherweight_OCL.UML_Integer
Presenting theory FeatherweightJava.FJSound
Presenting theory Fishburn_Impossibility.Fishburn_Impossibility
Presenting FocusStreamsCaseStudies ...
Presenting document FocusStreamsCaseStudies/document
Presenting document FocusStreamsCaseStudies/outline
Presenting theory FocusStreamsCaseStudies.ArithExtras
Presenting theory FocusStreamsCaseStudies.ListExtras
Presenting theory Featherweight_OCL.UML_Real
Presenting theory FocusStreamsCaseStudies.arith_hints
Presenting theory Featherweight_OCL.UML_String
Presenting theory FLP.FLPTheorem
Presenting theory Featherweight_OCL.UML_Pair
Presenting theory FLP.FLPExistingSystem
Presenting theory FocusStreamsCaseStudies.stream
Presenting Foundation_of_geometry ...
Presenting document Foundation_of_geometry/document
Presenting document Foundation_of_geometry/outline
Presenting theory FeatherweightJava.Execute
Presenting theory FeatherweightJava.Featherweight_Java
Presenting Free-Boolean-Algebra ...
Presenting document Free-Boolean-Algebra/document
Presenting document Free-Boolean-Algebra/outline
Presenting theory FocusStreamsCaseStudies.BitBoolTS
Presenting theory Foundation_of_geometry.Incidence
Presenting theory FocusStreamsCaseStudies.JoinSplitTime
Presenting theory FocusStreamsCaseStudies.SteamBoiler
Presenting theory FocusStreamsCaseStudies.SteamBoiler_proof
Presenting theory FocusStreamsCaseStudies.FR_types
Presenting theory FocusStreamsCaseStudies.FR
Presenting theory Featherweight_OCL.UML_Bag
Presenting theory Free-Boolean-Algebra.Free_Boolean_Algebra
Presenting document Free-Groups/document
Presenting document Free-Groups/outline
Presenting theory FocusStreamsCaseStudies.FR_proof
Presenting theory FocusStreamsCaseStudies.Gateway_types
Presenting theory FocusStreamsCaseStudies.Gateway
Presenting theory Flyspeck-Tame.ListAux
Presenting theory Flyspeck-Tame.Quasi_Order
Presenting theory Encodability_Process_Calculi.SourceTargetRelation
Presenting theory FocusStreamsCaseStudies.Gateway_proof_aux
Presenting theory Factored_Transition_System_Bounding.FactoredSystem
Presenting theory Encodability_Process_Calculi.SuccessSensitiveness
Presenting theory Free-Groups.Cancelation
Presenting theory Encodability_Process_Calculi.DivergenceReflection
Presenting theory Featherweight_OCL.UML_Set
Presenting theory FocusStreamsCaseStudies.Gateway_proof
Presenting Fresh_Identifiers ...
Presenting document Fresh_Identifiers/document
Presenting document Fresh_Identifiers/outline
Presenting theory Fresh_Identifiers.Fresh
Presenting theory Fresh_Identifiers.Fresh_Nat
Presenting theory Fresh_Identifiers.Fresh_String
Presenting theory Fresh_Identifiers.Fresh_Infinite
Presenting FunWithFunctions ...
Presenting document FunWithFunctions/document
Presenting document FunWithFunctions/outline
Presenting theory Free-Groups.Generators
Presenting theory Flyspeck-Tame.PlaneGraphIso
Presenting theory FunWithFunctions.FunWithFunctions
Presenting document FunWithTilings/document
Presenting document FunWithTilings/outline
Presenting theory Featherweight_OCL.UML_Sequence
Presenting theory Flyspeck-Tame.Rotation
Presenting theory FunWithTilings.Tilings
Presenting document Functions/functions
Presenting theory Featherweight_OCL.UML_Library
Presenting theory Functions.Functions
Presenting theory Flyspeck-Tame.Graph
Presenting document GPU_Kernel_PL/document
Presenting document GPU_Kernel_PL/outline
Presenting theory Flyspeck-Tame.IArray_Syntax
Presenting theory GPU_Kernel_PL.Misc
Presenting theory GPU_Kernel_PL.KPL_syntax
Presenting theory Flyspeck-Tame.Enumerator
Presenting theory GPU_Kernel_PL.KPL_wellformedness
Presenting theory GPU_Kernel_PL.KPL_state
Presenting theory Flyspeck-Tame.FaceDivision
Presenting theory GPU_Kernel_PL.KPL_execution_thread
Presenting theory Flyspeck-Tame.RTranCl
Presenting theory Flyspeck-Tame.Plane
Presenting theory Free-Groups.FreeGroups
Presenting theory Flyspeck-Tame.Plane1
Presenting theory GPU_Kernel_PL.KPL_execution_group
Presenting theory Factored_Transition_System_Bounding.ActionSeqProcess
Presenting theory Free-Groups.UnitGroup
Presenting theory Free-Groups.C2
Presenting theory Factored_Transition_System_Bounding.RelUtils
Presenting theory GPU_Kernel_PL.KPL_execution_kernel
Presenting theory GPU_Kernel_PL.Kernel_programming_language
Presenting document Gale_Shapley/document
Presenting document Gale_Shapley/outline
Presenting theory Flyspeck-Tame.GraphProps
Presenting theory Foundation_of_geometry.Order
Presenting theory Flyspeck-Tame.EnumeratorProps
Presenting theory Factored_Transition_System_Bounding.Dependency
Presenting theory Factored_Transition_System_Bounding.Invariants
Presenting theory Factored_Transition_System_Bounding.SetUtils
Presenting theory Free-Groups.Isomorphisms
Presenting theory HOL.BNF_Fixpoint_Base
Presenting file "Tools/BNF/bnf_fp_util_tactics.ML"
Presenting file "Tools/BNF/bnf_fp_util.ML"
Presenting file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
Presenting file "Tools/BNF/bnf_fp_def_sugar.ML"
Presenting file "Tools/BNF/bnf_fp_n2m_tactics.ML"
Presenting file "Tools/BNF/bnf_fp_n2m.ML"
Presenting file "Tools/BNF/bnf_fp_n2m_sugar.ML"
Presenting theory Free-Groups.PingPongLemma
Presenting document GenClock/document
Presenting document GenClock/outline
Presenting theory Featherweight_OCL.UML_State
Presenting theory Gale_Shapley.Gale_Shapley1
Presenting theory Encodability_Process_Calculi.OperationalCorrespondence
Presenting theory Gale_Shapley.Gale_Shapley2
Presenting General-Triangle ...
Presenting document General-Triangle/document
Presenting document General-Triangle/outline
Presenting theory General-Triangle.GeneralTriangle
Presenting Generic_Deriving ...
Presenting document Generic_Deriving/document
Presenting document Generic_Deriving/outline
Presenting theory Generic_Deriving.Tagged_Prod_Sum
Presenting theory GenClock.GenClock
Presenting theory Featherweight_OCL.UML_Contracts
Presenting document Generic_Join/document
Presenting document Generic_Join/outline
Presenting theory Featherweight_OCL.UML_Tools
Presenting theory Featherweight_OCL.UML_Main
Presenting theory Generic_Deriving.Derive
Presenting file "derive_util.ML"
Presenting file "derive_laws.ML"
Presenting file "derive_setup.ML"
Presenting theory Generic_Join.Generic_Join
Presenting theory Generic_Deriving.Derive_Datatypes
Presenting theory Generic_Deriving.Derive_Eq
Presenting theory Generic_Deriving.Derive_Encode
Presenting theory Generic_Deriving.Derive_Algebra
Presenting theory Generic_Deriving.Derive_Show
Presenting theory Generic_Deriving.Derive_Eq_Laws
Presenting theory HOL.BNF_Least_Fixpoint
Presenting file "Tools/BNF/bnf_lfp_util.ML"
Presenting file "Tools/BNF/bnf_lfp_tactics.ML"
Presenting theory Generic_Deriving.Derive_Algebra_Laws
Presenting file "Tools/BNF/bnf_lfp.ML"
Presenting file "Tools/BNF/bnf_lfp_compat.ML"
Presenting file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
Presenting file "Tools/BNF/bnf_lfp_size.ML"
Presenting file "Tools/datatype_simprocs.ML"
Presenting GewirthPGCProof ...
Presenting document GewirthPGCProof/document
Presenting document GewirthPGCProof/outline
Presenting theory HOL.Equiv_Relations
Presenting theory Encodability_Process_Calculi.FullAbstraction
Presenting theory HOL.Basic_BNF_LFPs
Presenting file "Tools/BNF/bnf_lfp_basic_sugar.ML"
Presenting theory GewirthPGCProof.CJDDLplus
Presenting file "Tools/Meson/meson.ML"
Presenting file "Tools/Meson/meson_clausify.ML"
Presenting file "Tools/Meson/meson_tactic.ML"
Presenting theory GewirthPGCProof.ExtendedDDL
Presenting theory Featherweight_OCL.Analysis_UML
Presenting theory Factored_Transition_System_Bounding.TopologicalProps
Presenting theory GewirthPGCProof.GewirthArgument
Presenting document GoedelGod/document
Presenting document GoedelGod/outline
Presenting theory GoedelGod.GoedelGod
Presenting Goodstein_Lambda ...
Presenting document Goodstein_Lambda/document
Presenting document Goodstein_Lambda/outline
Presenting theory Featherweight_OCL.Analysis_OCL
Presenting theory Goodstein_Lambda.Goodstein_Lambda
Presenting GraphMarkingIBP ...
Presenting document GraphMarkingIBP/document
Presenting document GraphMarkingIBP/outline
Presenting theory Generic_Join.Generic_Join_Correctness
Presenting theory GraphMarkingIBP.Graph
Presenting theory Flyspeck-Tame.FaceDivisionProps
Presenting theory Generic_Join.Examples_Join
Presenting Grothendieck_Schemes ...
Presenting document Grothendieck_Schemes/document
Presenting document Grothendieck_Schemes/outline
Presenting theory Grothendieck_Schemes.Set_Extras
Presenting theory GraphMarkingIBP.SetMark
Presenting theory Factored_Transition_System_Bounding.SystemAbstraction
Presenting theory Grothendieck_Schemes.Group_Extras
Presenting theory GraphMarkingIBP.StackMark
Presenting theory Grothendieck_Schemes.Topological_Space
Presenting theory Factored_Transition_System_Bounding.Acyclicity
Presenting theory Encodability_Process_Calculi.CombinedCriteria
Presenting theory GraphMarkingIBP.LinkMark
Presenting document HOL-Analysis/document
Presenting document HOL-Analysis/manual
Presenting theory Featherweight_OCL.Design_UML
Presenting theory HOL-Analysis.L2_Norm
Presenting theory Featherweight_OCL.Design_OCL
Presenting Actuarial_Mathematics ...
Presenting document Actuarial_Mathematics/document
Presenting document Actuarial_Mathematics/outline
Presenting theory HOL-Analysis.Inner_Product
Presenting theory Actuarial_Mathematics.Preliminaries
Presenting theory Factored_Transition_System_Bounding.AcycSspace
Presenting theory GraphMarkingIBP.DSWMark
Presenting Affine_Arithmetic ...
Presenting document Affine_Arithmetic/document
Presenting document Affine_Arithmetic/outline
Presenting document Taylor_Models/document
Presenting document Taylor_Models/outline
Presenting theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
Presenting theory Actuarial_Mathematics.Interest
Presenting document Akra_Bazzi/document
Presenting document Akra_Bazzi/outline
Presenting theory HOL-Analysis.Product_Vector
Presenting theory Flyspeck-Tame.Invariants
Presenting theory Affine_Arithmetic.Executable_Euclidean_Space
Presenting theory Akra_Bazzi.Akra_Bazzi_Library
Presenting theory HOL-Analysis.Euclidean_Space
Presenting theory Akra_Bazzi.Akra_Bazzi_Asymptotics
Presenting theory Taylor_Models.Polynomial_Expression
Presenting theory Flyspeck-Tame.PlaneProps
Presenting theory Flyspeck-Tame.ListSum
Presenting theory Flyspeck-Tame.Tame
Presenting theory Flyspeck-Tame.Plane1Props
Presenting theory Taylor_Models.Float_Topology
Presenting theory Flyspeck-Tame.Generator
Presenting theory Flyspeck-Tame.TameProps
Presenting theory Taylor_Models.Horner_Eval
Presenting theory Flyspeck-Tame.TameEnum
Presenting theory Affine_Arithmetic.Affine_Form
Presenting theory Taylor_Models.Polynomial_Expression_Additional
Presenting theory Taylor_Models.Taylor_Models_Misc
Presenting theory Flyspeck-Tame.ScoreProps
Presenting theory Akra_Bazzi.Akra_Bazzi_Real
Presenting theory Flyspeck-Tame.LowerBound
Presenting theory HOL-Analysis.Linear_Algebra
Presenting theory Flyspeck-Tame.GeneratorProps
Presenting theory Flyspeck-Tame.TameEnumProps
Presenting theory Grothendieck_Schemes.Comm_Ring
Presenting theory Akra_Bazzi.Akra_Bazzi
Presenting theory Flyspeck-Tame.Worklist
Presenting theory Flyspeck-Tame.Maps
Presenting theory Flyspeck-Tame.Arch
Presenting theory Flyspeck-Tame.ArchCompAux
Presenting theory Flyspeck-Tame.ArchCompProps
Presenting theory Taylor_Models.Taylor_Models
Presenting theory Flyspeck-Tame.Relative_Completeness
Presenting Closest_Pair_Points ...
Presenting document Closest_Pair_Points/document
Presenting document Closest_Pair_Points/outline
Presenting theory Akra_Bazzi.Master_Theorem
Presenting theory Akra_Bazzi.Eval_Numeral
Presenting theory Taylor_Models.Experiments
Presenting Banach_Steinhaus ...
Presenting document Banach_Steinhaus/document
Presenting document Banach_Steinhaus/outline
Presenting theory Banach_Steinhaus.Banach_Steinhaus_Missing
Presenting theory Affine_Arithmetic.Floatarith_Expression
Presenting theory Closest_Pair_Points.Common
Presenting theory HOL-Analysis.Affine
Presenting theory Banach_Steinhaus.Banach_Steinhaus
Presenting Catalan_Numbers ...
Presenting document Catalan_Numbers/document
Presenting document Catalan_Numbers/outline
Presenting theory Catalan_Numbers.Catalan_Auxiliary_Integral
Presenting theory Catalan_Numbers.Catalan_Numbers
Presenting Cayley_Hamilton ...
Presenting document Cayley_Hamilton/document
Presenting document Cayley_Hamilton/outline
Presenting theory Cayley_Hamilton.Square_Matrix
Presenting theory Cayley_Hamilton.Cayley_Hamilton
Presenting document Chord_Segments/document
Presenting document Chord_Segments/outline
Presenting theory Chord_Segments.Chord_Segments
Presenting Complex_Bounded_Operators ...
Presenting document Complex_Bounded_Operators/document
Presenting document Complex_Bounded_Operators/outline
Presenting theory Akra_Bazzi.Akra_Bazzi_Method
Presenting file "akra_bazzi.ML"
Presenting theory Complex_Bounded_Operators.Extra_General
Presenting theory Akra_Bazzi.Akra_Bazzi_Approximation
Presenting theory Complex_Bounded_Operators.Extra_Vector_Spaces
Presenting theory Affine_Arithmetic.Straight_Line_Program
Presenting theory Complex_Bounded_Operators.Extra_Ordered_Fields
Presenting theory Akra_Bazzi.Master_Theorem_Examples
Presenting document Registers/document
Presenting document Registers/outline
Presenting theory Registers.Axioms
Presenting theory Complex_Bounded_Operators.Complex_Vector_Spaces0
Presenting theory Closest_Pair_Points.Closest_Pair
Presenting theory HOL-Analysis.Convex
Presenting theory Registers.Laws
Presenting theory Registers.Axioms_Complement
Presenting theory Registers.Laws_Complement
Presenting theory Complex_Bounded_Operators.Complex_Vector_Spaces
Presenting theory Grothendieck_Schemes.Scheme
Presenting Differential_Game_Logic ...
Presenting document Differential_Game_Logic/document
Presenting document Differential_Game_Logic/outline
Presenting theory Registers.Axioms_Classical
Presenting theory Differential_Game_Logic.Lib
Presenting theory Differential_Game_Logic.Identifiers
Presenting theory Complex_Bounded_Operators.Complex_Inner_Product0
Presenting theory HOL-Analysis.Finite_Cartesian_Product
Presenting theory Differential_Game_Logic.Syntax
Presenting theory Foundation_of_geometry.Congruence
Presenting file "Tools/ATP/atp_util.ML"
Presenting file "Tools/ATP/atp_problem.ML"
Presenting file "Tools/ATP/atp_proof.ML"
Presenting file "Tools/ATP/atp_proof_redirect.ML"
Presenting file "Tools/lambda_lifting.ML"
Presenting file "Tools/monomorph.ML"
Presenting file "Tools/ATP/atp_problem_generate.ML"
Presenting theory Registers.Laws_Classical
Presenting file "Tools/ATP/atp_proof_reconstruct.ML"
Presenting theory Differential_Game_Logic.Denotational_Semantics
Presenting theory Registers.Misc
Presenting theory Differential_Game_Logic.Static_Semantics
Presenting theory Registers.Classical_Extra
Presenting document Echelon_Form/document
Presenting document Echelon_Form/outline
Presenting theory HOL-Analysis.Cartesian_Space
Presenting theory Echelon_Form.Rings2
Presenting theory Complex_Bounded_Operators.Complex_Inner_Product
Presenting theory Echelon_Form.Cayley_Hamilton_Compatible
Presenting theory Echelon_Form.Code_Cayley_Hamilton
Presenting theory Closest_Pair_Points.Closest_Pair_Alternative
Presenting document Hermite/document
Presenting document Hermite/outline
Presenting theory Complex_Bounded_Operators.Extra_Operator_Norm
Presenting theory Complex_Bounded_Operators.One_Dimensional_Spaces
Presenting theory Registers.Finite_Tensor_Product
Presenting theory Complex_Bounded_Operators.Complex_Euclidean_Space0
Presenting theory Registers.Axioms_Quantum
Presenting theory Affine_Arithmetic.Affine_Approximation
Presenting theory Differential_Game_Logic.Coincidence
Presenting theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function0
Presenting theory HOL-Analysis.Determinants
Presenting theory Hermite.Hermite
Presenting theory Echelon_Form.Echelon_Form
Presenting theory Hermite.Hermite_IArrays
Presenting Smith_Normal_Form ...
Presenting document Smith_Normal_Form/document
Presenting document Smith_Normal_Form/outline
Presenting theory Affine_Arithmetic.Counterclockwise
Presenting theory Smith_Normal_Form.Smith_Normal_Form
Presenting theory Echelon_Form.Echelon_Form_Det
Presenting theory Echelon_Form.Echelon_Form_Inverse
Presenting theory Affine_Arithmetic.Counterclockwise_Vector
Presenting theory Echelon_Form.Examples_Echelon_Form_Abstract
Presenting theory Echelon_Form.Echelon_Form_IArrays
Presenting theory Affine_Arithmetic.Counterclockwise_2D_Strict
Presenting theory Echelon_Form.Echelon_Form_Det_IArrays
Presenting theory Echelon_Form.Code_Cayley_Hamilton_IArrays
Presenting theory Echelon_Form.Echelon_Form_Inverse_IArrays
Presenting theory Echelon_Form.Examples_Echelon_Form_IArrays
Presenting Modular_arithmetic_LLL_and_HNF_algorithms ...
Presenting document Modular_arithmetic_LLL_and_HNF_algorithms/document
Presenting document Modular_arithmetic_LLL_and_HNF_algorithms/outline
Presenting theory Modular_arithmetic_LLL_and_HNF_algorithms.Matrix_Change_Row
Presenting theory Modular_arithmetic_LLL_and_HNF_algorithms.Signed_Modulo
Presenting theory Registers.Laws_Quantum
Presenting theory Registers.Quantum
Presenting theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function
Presenting theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation
Presenting theory Affine_Arithmetic.Polygon
Presenting theory Registers.Quantum_Extra
Presenting theory Registers.QHoare
Presenting theory Registers.Finite_Tensor_Product_Matrices
Presenting theory Smith_Normal_Form.Diagonal_To_Smith
Presenting theory Registers.Teleport
Presenting theory HOL-Analysis.Elementary_Topology
Presenting theory Complex_Bounded_Operators.Complex_L2
Presenting theory Differential_Game_Logic.USubst
Presenting theory Smith_Normal_Form.Mod_Type_Connect
Presenting theory Differential_Game_Logic.Ids
Presenting theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
Presenting theory Differential_Game_Logic.Axioms
Presenting theory Differential_Game_Logic.Differential_Game_Logic
Presenting First_Welfare_Theorem ...
Presenting document First_Welfare_Theorem/document
Presenting document First_Welfare_Theorem/outline
Presenting theory First_Welfare_Theorem.Syntax
Presenting theory First_Welfare_Theorem.Argmax
Presenting theory Complex_Bounded_Operators.Extra_Jordan_Normal_Form
Presenting theory First_Welfare_Theorem.Preferences
Presenting theory First_Welfare_Theorem.Utility_Functions
Presenting theory First_Welfare_Theorem.Consumers
Presenting theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann
Presenting theory First_Welfare_Theorem.Common
Presenting theory Smith_Normal_Form.SNF_Missing_Lemmas
Presenting theory First_Welfare_Theorem.Exchange_Economy
Presenting theory First_Welfare_Theorem.Private_Ownership_Economy
Presenting theory Registers.Axioms_Complement_Quantum
Presenting theory First_Welfare_Theorem.Arrow_Debreu_Model
Presenting Furstenberg_Topology ...
Presenting document Furstenberg_Topology/document
Presenting document Furstenberg_Topology/outline
Presenting theory Complex_Bounded_Operators.Cblinfun_Matrix
Presenting theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl
Presenting theory Furstenberg_Topology.Furstenberg_Topology
Presenting document Gauss_Jordan/document
Presenting document Gauss_Jordan/outline
Presenting theory Complex_Bounded_Operators.Cblinfun_Code
Presenting theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite
Presenting theory Complex_Bounded_Operators.Extra_Pretty_Code_Examples
Presenting theory Complex_Bounded_Operators.Cblinfun_Code_Examples
Presenting document Green/document
Presenting document Green/outline
Presenting theory Green.General_Utils
Presenting theory Green.Derivs
Presenting theory Smith_Normal_Form.Cauchy_Binet
Presenting theory Gauss_Jordan.Rref
Presenting theory Affine_Arithmetic.Intersection
Presenting theory Gauss_Jordan.Code_Set
Presenting theory Registers.Laws_Complement_Quantum
Presenting theory Registers.Quantum_Extra2
Presenting theory Gauss_Jordan.Code_Matrix
Presenting theory Smith_Normal_Form.Smith_Normal_Form_JNF
Presenting theory Green.Integrals
Presenting theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite_JNF
Presenting theory Affine_Arithmetic.Affine_Code
Presenting theory Affine_Arithmetic.Optimize_Integer
Presenting theory Affine_Arithmetic.Optimize_Float
Presenting theory Affine_Arithmetic.Print
Presenting theory Gauss_Jordan.Elementary_Operations
Presenting theory Affine_Arithmetic.Float_Real
Presenting theory Smith_Normal_Form.Rings2_Extended
Presenting theory Gauss_Jordan.Rank
Presenting theory Affine_Arithmetic.Ex_Affine_Approximation
Presenting theory Smith_Normal_Form.Finite_Field_Mod_Type_Connection
Presenting theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm
Presenting theory Affine_Arithmetic.Ex_Ineqs
Presenting theory Affine_Arithmetic.Ex_Inter
Presenting theory Affine_Arithmetic.Affine_Arithmetic
Presenting Gromov_Hyperbolicity ...
Presenting document Gromov_Hyperbolicity/document
Presenting document Gromov_Hyperbolicity/outline
Presenting theory Smith_Normal_Form.Admits_SNF_From_Diagonal_Iff_Bezout_Ring
Presenting theory Registers.Pure_States
Presenting theory Registers.Check_Autogenerated_Files
Presenting HOL-Analysis-ex ...
Presenting theory Gromov_Hyperbolicity.Library_Complements
Presenting file "$ISABELLE_HOME/src/Tools/Metis/metis.ML"
Presenting file "Tools/Metis/metis_generate.ML"
Presenting file "Tools/Metis/metis_reconstruct.ML"
Presenting file "Tools/Metis/metis_tactic.ML"
Presenting theory Gromov_Hyperbolicity.Eexp_Eln
Presenting theory Gromov_Hyperbolicity.Hausdorff_Distance
Presenting theory HOL-Analysis-ex.Approximations
Presenting theory HOL-Analysis-ex.Metric_Arith_Examples
Presenting HOL-Complex_Analysis ...
Presenting document HOL-Complex_Analysis/document
Presenting document HOL-Complex_Analysis/manual
Presenting theory Smith_Normal_Form.SNF_Uniqueness
Presenting theory Smith_Normal_Form.Cauchy_Binet_HOL_Analysis
Presenting theory Smith_Normal_Form.Diagonalize
Presenting theory Smith_Normal_Form.SNF_Algorithm_Two_Steps
Presenting theory HOL-Analysis.Abstract_Topology
Presenting theory Gromov_Hyperbolicity.Isometries
Presenting theory HOL-Complex_Analysis.Contour_Integration
Presenting theory Smith_Normal_Form.Diagonal_To_Smith_JNF
Presenting theory Smith_Normal_Form.SNF_Algorithm_Two_Steps_JNF
Presenting theory Gauss_Jordan.Gauss_Jordan
Presenting theory Gromov_Hyperbolicity.Metric_Completion
Presenting theory HOL-Analysis.Abstract_Topology_2
Presenting theory HOL.Transfer
Presenting file "Tools/Transfer/transfer.ML"
Presenting file "Tools/Transfer/transfer_bnf.ML"
Presenting file "Tools/BNF/bnf_fp_rec_sugar_transfer.ML"
Presenting theory Gromov_Hyperbolicity.Gromov_Hyperbolicity
Presenting theory Smith_Normal_Form.SNF_Algorithm
Presenting theory Smith_Normal_Form.SNF_Algorithm_HOL_Analysis
Presenting theory HOL-Analysis.Connected
Presenting theory HOL-Analysis.Abstract_Limits
Presenting theory HOL-Analysis.Metric_Arith
Presenting file "metric_arith.ML"
Presenting theory HOL-Complex_Analysis.Cauchy_Integral_Theorem
Presenting theory Smith_Normal_Form.Elementary_Divisor_Rings
Presenting theory Gauss_Jordan.Linear_Maps
Presenting theory HOL-Analysis.Elementary_Metric_Spaces
Presenting theory Gromov_Hyperbolicity.Morse_Gromov_Theorem
Presenting theory Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain
Presenting theory Smith_Normal_Form.Smith_Certified
Presenting theory Gauss_Jordan.Gauss_Jordan_PA
Presenting theory Smith_Normal_Form.Alternative_Proofs
Presenting document Bernoulli/document
Presenting document Bernoulli/outline
Presenting theory Bernoulli.Bernoulli
Presenting theory Gromov_Hyperbolicity.Bonk_Schramm_Extension
Presenting theory Bernoulli.Periodic_Bernpoly
Presenting theory HOL-Analysis.Elementary_Normed_Spaces
Presenting theory HOL-Complex_Analysis.Winding_Numbers
Presenting file "Tools/Lifting/lifting_util.ML"
Presenting file "Tools/Lifting/lifting_info.ML"
Presenting file "Tools/Lifting/lifting_bnf.ML"
Presenting file "Tools/Lifting/lifting_term.ML"
Presenting file "Tools/Lifting/lifting_def.ML"
Presenting file "Tools/Lifting/lifting_setup.ML"
Presenting file "Tools/Lifting/lifting_def_code_dt.ML"
Presenting theory Gauss_Jordan.Determinants2
Presenting theory Gromov_Hyperbolicity.Gromov_Boundary
Presenting theory Bernoulli.Bernoulli_FPS
Presenting theory HOL-Analysis.Norm_Arith
Presenting file "normarith.ML"
Presenting theory Gauss_Jordan.Inverse
Presenting theory Gromov_Hyperbolicity.Boundary_Extension
Presenting theory Gromov_Hyperbolicity.Busemann_Function
Presenting theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
Presenting theory Bernoulli.Bernoulli_Zeta
Presenting Euler_MacLaurin ...
Presenting document Euler_MacLaurin/document
Presenting document Euler_MacLaurin/outline
Presenting theory Gromov_Hyperbolicity.Isometries_Classification
Presenting document Lambert_W/document
Presenting document Lambert_W/outline
Presenting theory Lambert_W.Lambert_W
Presenting theory Lambert_W.Lambert_W_MacLaurin_Series
Presenting Stirling_Formula ...
Presenting document Stirling_Formula/document
Presenting document Stirling_Formula/outline
Presenting theory Green.SymmetricR2Shapes
Presenting theory Gauss_Jordan.System_Of_Equations
Presenting theory Stirling_Formula.Stirling_Formula
Presenting theory Gauss_Jordan.Code_Z2
Presenting theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness
Presenting theory Euler_MacLaurin.Euler_MacLaurin
Presenting theory HOL-Complex_Analysis.Cauchy_Integral_Formula
Presenting theory Euler_MacLaurin.Euler_MacLaurin_Landau
Presenting Clique_and_Monotone_Circuits ...
Presenting theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
Presenting document Clique_and_Monotone_Circuits/document
Presenting document Clique_and_Monotone_Circuits/outline
Presenting theory Gauss_Jordan.IArray_Addenda
Presenting theory Green.CircExample
Presenting theory Clique_and_Monotone_Circuits.Preliminaries
Presenting theory Stirling_Formula.Gamma_Asymptotics
Presenting theory Clique_and_Monotone_Circuits.Monotone_Formula
Presenting Comparison_Sort_Lower_Bound ...
Presenting document Comparison_Sort_Lower_Bound/document
Presenting document Comparison_Sort_Lower_Bound/outline
Presenting theory HOL-Analysis.Topology_Euclidean_Space
Presenting theory Gauss_Jordan.Matrix_To_IArray
Presenting theory Comparison_Sort_Lower_Bound.Linorder_Relations
Presenting theory Green.DiamExample
Presenting theory Clique_and_Monotone_Circuits.Assumptions_and_Approximations
Presenting Irrationals_From_THEBOOK ...
Presenting document Irrationals_From_THEBOOK/document
Presenting document Irrationals_From_THEBOOK/outline
Presenting theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
Presenting document Cartan_FP/document
Presenting document Cartan_FP/outline
Presenting theory Irrationals_From_THEBOOK.Irrationals_From_THEBOOK
Presenting Cotangent_PFD_Formula ...
Presenting document Cotangent_PFD_Formula/document
Presenting document Cotangent_PFD_Formula/outline
Presenting theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF
Presenting Count_Complex_Roots ...
Presenting document Count_Complex_Roots/document
Presenting document Count_Complex_Roots/outline
Presenting theory Cartan_FP.Cartan
Presenting Linear_Recurrences ...
Presenting document Linear_Recurrences/document
Presenting document Linear_Recurrences/outline
Presenting theory Gauss_Jordan.Gauss_Jordan_IArrays
Presenting theory Cotangent_PFD_Formula.Cotangent_PFD_Formula
Presenting theory Count_Complex_Roots.CC_Polynomials_Extra
Presenting Dirichlet_Series ...
Presenting document Dirichlet_Series/document
Presenting document Dirichlet_Series/outline
Presenting theory Linear_Recurrences.RatFPS
Presenting theory Dirichlet_Series.Dirichlet_Misc
Presenting theory Linear_Recurrences.Pochhammer_Polynomials
Presenting theory HOL-Complex_Analysis.Conformal_Mappings
Presenting theory Dirichlet_Series.Multiplicative_Function
Presenting theory HOL.Quotient
Presenting file "Tools/Quotient/quotient_info.ML"
Presenting file "Tools/Quotient/quotient_term.ML"
Presenting file "Tools/Quotient/quotient_type.ML"
Presenting file "Tools/Quotient/quotient_def.ML"
Presenting file "Tools/Quotient/quotient_tacs.ML"
Presenting file "Tools/BNF/bnf_lift.ML"
Presenting theory Linear_Recurrences.Linear_Recurrences_Misc
Presenting theory Gauss_Jordan.Gauss_Jordan_PA_IArrays
Presenting file "Tools/numeral.ML"
Presenting theory Clique_and_Monotone_Circuits.Clique_Large_Monotone_Circuits
Presenting document Gauss_Sums/document
Presenting document Gauss_Sums/outline
Presenting theory Dirichlet_Series.Dirichlet_Product
Presenting theory Linear_Recurrences.Partial_Fraction_Decomposition
Presenting theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces_IArrays
Presenting theory Gauss_Sums.Gauss_Sums_Auxiliary
Presenting theory HOL-Analysis.Convex_Euclidean_Space
Presenting theory Linear_Recurrences.Factorizations
Presenting theory Gauss_Sums.Periodic_Arithmetic
Presenting theory HOL.Groups_Big
Presenting theory HOL.Complete_Partial_Order
Presenting theory Gauss_Sums.Complex_Roots_Of_Unity
Presenting theory HOL-Analysis.Operator_Norm
Presenting theory Linear_Recurrences.Rational_FPS_Solver
Presenting theory Gauss_Jordan.System_Of_Equations_IArrays
Presenting theory Linear_Recurrences.Linear_Recurrences_Common
Presenting theory HOL.Partial_Function
Presenting file "Tools/Function/partial_function.ML"
Presenting theory Gauss_Sums.Finite_Fourier_Series
Presenting theory Linear_Recurrences.Linear_Homogenous_Recurrences
Presenting theory Dirichlet_Series.Dirichlet_Series
Presenting theory Gauss_Jordan.Determinants_IArrays
Presenting theory Gauss_Jordan.Inverse_IArrays
Presenting theory Linear_Recurrences.Eulerian_Polynomials
Presenting theory Gauss_Jordan.Examples_Gauss_Jordan_IArrays
Presenting theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
Presenting theory HOL-Complex_Analysis.Complex_Singularities
Presenting theory Gauss_Jordan.Code_Generation_IArrays
Presenting theory Dirichlet_Series.Moebius_Mu
Presenting theory Gauss_Jordan.Code_Generation_IArrays_SML
Presenting theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell
Presenting theory Gauss_Jordan.Code_Rational
Presenting theory Gauss_Jordan.Code_Generation_IArrays_Haskell
Presenting document Zeta_Function/document
Presenting document Zeta_Function/outline
Presenting theory Dirichlet_Series.More_Totient
Presenting theory Dirichlet_Series.Liouville_Lambda
Presenting theory HOL-Analysis.Line_Segment
Presenting theory Dirichlet_Series.Divisor_Count
Presenting theory Gauss_Sums.Ramanujan_Sums
Presenting theory Count_Complex_Roots.Extended_Sturm
Presenting theory Linear_Recurrences.Rational_FPS_Asymptotics
Presenting theory Dirichlet_Series.Arithmetic_Summatory
Presenting document Dirichlet_L/document
Presenting document Dirichlet_L/outline
Presenting theory Dirichlet_Series.Partial_Summation
Presenting theory Zeta_Function.Zeta_Library
Presenting theory HOL-Complex_Analysis.Complex_Residues
Presenting theory Dirichlet_Series.Euler_Products
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_expr.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_term.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_lit.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_proof.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_rewr.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_cls.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_common.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_cc.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_simplex.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_thy.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_heap.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_cdcl.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_core.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_clausify.ML"
Presenting file "$ISABELLE_HOME/src/Tools/Argo/argo_solver.ML"
Presenting file "Tools/Argo/argo_tactic.ML"
Presenting theory HOL-Complex_Analysis.Residue_Theorem
Presenting theory Count_Complex_Roots.Count_Line
Presenting theory Gauss_Sums.Gauss_Sums
Presenting file "Tools/prop_logic.ML"
Presenting file "Tools/sat_solver.ML"
Presenting file "Tools/sat.ML"
Presenting file "Tools/Argo/argo_sat_solver.ML"
Presenting theory Dirichlet_L.Multiplicative_Characters
Presenting theory HOL-Analysis.Extended_Real_Limits
Presenting theory Dirichlet_L.Dirichlet_Characters
Presenting theory Gauss_Sums.Polya_Vinogradov
Presenting Prime_Distribution_Elementary ...
Presenting document Prime_Distribution_Elementary/document
Presenting document Prime_Distribution_Elementary/outline
Presenting theory Zeta_Function.Zeta_Function
Presenting file "Tools/Function/function_core.ML"
Presenting file "Tools/Function/mutual.ML"
Presenting file "Tools/Function/pattern_split.ML"
Presenting file "Tools/Function/relation.ML"
Presenting file "Tools/Function/function_elims.ML"
Presenting file "Tools/Function/function.ML"
Presenting file "Tools/Function/pat_completeness.ML"
Presenting file "Tools/Function/fun.ML"
Presenting file "Tools/Function/induction_schema.ML"
Presenting file "Tools/Function/measure_functions.ML"
Presenting file "Tools/Function/lexicographic_order.ML"
Presenting file "Tools/Function/termination.ML"
Presenting file "Tools/Function/scnp_solve.ML"
Presenting file "Tools/Function/scnp_reconstruct.ML"
Presenting file "Tools/Function/fun_cases.ML"
Presenting theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
Presenting theory Count_Complex_Roots.Count_Half_Plane
Presenting theory Dirichlet_Series.Dirichlet_Series_Analysis
Presenting theory Prime_Distribution_Elementary.More_Dirichlet_Misc
Presenting theory Count_Complex_Roots.Count_Circle
Presenting theory Prime_Distribution_Elementary.Primes_Omega
Presenting file "Tools/int_arith.ML"
Presenting theory Zeta_Function.Zeta_Laurent_Expansion
Presenting theory Prime_Distribution_Elementary.Primorial
Presenting theory Dirichlet_L.Dirichlet_L_Functions
Presenting theory HOL-Complex_Analysis.Great_Picard
Presenting theory Prime_Distribution_Elementary.Lcm_Nat_Upto
Presenting theory HOL-Analysis.Summation_Tests
Presenting theory HOL.Lattices_Big
Presenting theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics
Presenting theory Prime_Distribution_Elementary.Shapiro_Tauberian
Presenting theory Zeta_Function.Hadjicostas_Chapman
Presenting theory Dirichlet_L.Dirichlet_Theorem
Presenting theory Dirichlet_Series.Dirichlet_Efficient_Code
Presenting Prime_Number_Theorem ...
Presenting document IMO2019/document
Presenting document IMO2019/outline
Presenting document Prime_Number_Theorem/document
Presenting document Prime_Number_Theorem/outline
Presenting Zeta_3_Irrational ...
Presenting document Zeta_3_Irrational/document
Presenting document Zeta_3_Irrational/outline
Presenting theory IMO2019.IMO2019_Q1
Presenting theory HOL.Euclidean_Division
Presenting theory IMO2019.IMO2019_Q4
Presenting theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
Presenting theory IMO2019.IMO2019_Q5
Presenting E_Transcendental ...
Presenting document E_Transcendental/document
Presenting document E_Transcendental/outline
Presenting theory Prime_Distribution_Elementary.Moebius_Mu_Sum
Presenting theory HOL-Analysis.Uniform_Limit
Presenting theory Count_Complex_Roots.Count_Rectangle
Presenting theory E_Transcendental.E_Transcendental
Presenting Pi_Transcendental ...
Presenting document Pi_Transcendental/document
Presenting document Pi_Transcendental/outline
Presenting theory Count_Complex_Roots.Count_Complex_Roots
Presenting theory Count_Complex_Roots.Count_Complex_Roots_Examples
Presenting Hermite_Lindemann ...
Presenting document Hermite_Lindemann/document
Presenting document Hermite_Lindemann/outline
Presenting theory HOL.Numeral_Simprocs
Presenting file "$ISABELLE_HOME/src/Provers/Arith/assoc_fold.ML"
Presenting file "$ISABELLE_HOME/src/Provers/Arith/cancel_numerals.ML"
Presenting file "$ISABELLE_HOME/src/Provers/Arith/combine_numerals.ML"
Presenting file "$ISABELLE_HOME/src/Provers/Arith/cancel_numeral_factor.ML"
Presenting file "$ISABELLE_HOME/src/Provers/Arith/extract_common_term.ML"
Presenting file "Tools/numeral_simprocs.ML"
Presenting file "Tools/nat_numeral_simprocs.ML"
Presenting theory Hermite_Lindemann.Algebraic_Integer_Divisibility
Presenting theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library
Presenting theory Prime_Distribution_Elementary.Elementary_Prime_Bounds
Presenting theory HOL-Complex_Analysis.Riemann_Mapping
Presenting theory HOL-Complex_Analysis.Complex_Analysis
Presenting document Error_Function/document
Presenting document Error_Function/outline
Presenting theory Hermite_Lindemann.More_Polynomial_HLW
Presenting theory Hermite_Lindemann.More_Min_Int_Poly
Presenting theory HOL.Semiring_Normalization
Presenting file "Tools/semiring_normalizer.ML"
Presenting theory Hermite_Lindemann.Complex_Lexorder
Presenting theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds
Presenting theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
Presenting theory Hermite_Lindemann.More_Algebraic_Numbers_HLW
Presenting theory Pi_Transcendental.Pi_Transcendental
Presenting Transcendence_Series_Hancl_Rucki ...
Presenting document Transcendence_Series_Hancl_Rucki/document
Presenting document Transcendence_Series_Hancl_Rucki/outline
Presenting theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula
Presenting theory Hermite_Lindemann.Misc_HLW
Presenting theory Error_Function.Error_Function
Presenting theory HOL.Groebner_Basis
Presenting file "Tools/groebner.ML"
Presenting theory Zeta_3_Irrational.Zeta_3_Irrational
Presenting theory Prime_Number_Theorem.Prime_Number_Theorem_Library
Presenting theory Prime_Distribution_Elementary.PNT_Consequences
Presenting Wetzels_Problem ...
Presenting document Wetzels_Problem/document
Presenting document Wetzels_Problem/outline
Presenting Winding_Number_Eval ...
Presenting document Winding_Number_Eval/document
Presenting document Winding_Number_Eval/outline
Presenting theory Transcendence_Series_Hancl_Rucki.Transcendence_Series
Presenting theory Error_Function.Error_Function_Asymptotics
Presenting document HOL-Homology/document
Presenting document HOL-Homology/manual
Presenting HOL-Probability ...
Presenting document HOL-Probability/document
Presenting document HOL-Probability/outline
Presenting theory Winding_Number_Eval.Missing_Topology
Presenting theory Wetzels_Problem.Wetzels_Problem
Presenting theory Winding_Number_Eval.Missing_Algebraic
Presenting Applicative_Lifting ...
Presenting document Applicative_Lifting/document
Presenting document Applicative_Lifting/outline
Presenting theory HOL.Set_Interval
Presenting theory Prime_Number_Theorem.Newman_Ingham_Tauberian
Presenting theory Winding_Number_Eval.Missing_Transcendental
Presenting theory Winding_Number_Eval.Missing_Analysis
Presenting theory HOL-Probability.Probability_Measure
Presenting theory HOL-Probability.Distribution_Functions
Presenting theory HOL-Analysis.Function_Topology
Presenting theory HOL-Probability.Weak_Convergence
Presenting theory Hermite_Lindemann.Hermite_Lindemann
Presenting document Stern_Brocot/document
Presenting document Stern_Brocot/outline
Presenting theory HOL-Analysis.Bounded_Linear_Function
Presenting theory HOL-Probability.Giry_Monad
Presenting theory Prime_Number_Theorem.Prime_Counting_Functions
Presenting theory Stern_Brocot.Cotree
Presenting theory Applicative_Lifting.Applicative
Presenting file "applicative.ML"
Presenting theory Applicative_Lifting.Applicative_Environment
Presenting theory Stern_Brocot.Cotree_Algebra
Presenting theory Applicative_Lifting.Applicative_Option
Presenting theory Applicative_Lifting.Applicative_Sum
Presenting theory Applicative_Lifting.Applicative_Set
Presenting theory Applicative_Lifting.Applicative_List
Presenting theory Applicative_Lifting.Applicative_DNEList
Presenting theory Applicative_Lifting.Applicative_Monoid
Presenting theory Applicative_Lifting.Applicative_Filter
Presenting theory Applicative_Lifting.Applicative_State
Presenting theory Applicative_Lifting.Applicative_Stream
Presenting theory Applicative_Lifting.Applicative_Open_State
Presenting theory Applicative_Lifting.Applicative_PMF
Presenting theory HOL-Probability.Projective_Family
Presenting theory Applicative_Lifting.Applicative_Probability_List
Presenting theory Applicative_Lifting.Applicative_Star
Presenting theory Applicative_Lifting.Applicative_Vector
Presenting theory Stern_Brocot.Stern_Brocot_Tree
Presenting theory Applicative_Lifting.Applicative_Functor
Presenting theory Applicative_Lifting.Applicative_Environment_Algebra
Presenting theory Prime_Number_Theorem.Prime_Number_Theorem
Presenting theory Applicative_Lifting.Stream_Algebra
Presenting theory Stern_Brocot.Bird_Tree
Presenting theory Applicative_Lifting.Tree_Relabelling
Presenting document Buffons_Needle/document
Presenting document Buffons_Needle/outline
Presenting theory Applicative_Lifting.Applicative_Examples
Presenting theory Applicative_Lifting.Joinable
Presenting theory Applicative_Lifting.Beta_Eta
Presenting theory Applicative_Lifting.Combinators
Presenting theory Applicative_Lifting.Idiomatic_Terms
Presenting theory Buffons_Needle.Buffons_Needle
Presenting document Deep_Learning/document
Presenting document Deep_Learning/outline
Presenting theory Applicative_Lifting.Abstract_AF
Presenting theory Applicative_Lifting.Applicative_Test
Presenting Density_Compiler ...
Presenting document Density_Compiler/document
Presenting document Density_Compiler/outline
Presenting theory HOL-Probability.Infinite_Product_Measure
Presenting theory Deep_Learning.Tensor
Presenting theory Density_Compiler.Density_Predicates
Presenting theory Prime_Number_Theorem.Mertens_Theorems
Presenting theory Deep_Learning.Tensor_Subtensor
Presenting DiscretePricing ...
Presenting document DiscretePricing/document
Presenting document DiscretePricing/outline
Presenting theory Density_Compiler.PDF_Transformations
Presenting theory Deep_Learning.Tensor_Plus
Presenting theory Deep_Learning.Tensor_Scalar_Mult
Presenting theory DiscretePricing.Generated_Subalgebra
Presenting theory Density_Compiler.PDF_Values
Presenting theory Deep_Learning.Tensor_Product
Presenting theory HOL.Presburger
Presenting file "Tools/Qelim/qelim.ML"
Presenting file "Tools/Qelim/cooper_procedure.ML"
Presenting file "Tools/Qelim/cooper.ML"
Presenting file "Tools/try0.ML"
Presenting theory Winding_Number_Eval.Cauchy_Index_Theorem
Presenting theory Deep_Learning.Tensor_Unit_Vec
Presenting theory Density_Compiler.PDF_Semantics
Presenting theory Deep_Learning.Tensor_Rank
Presenting theory HOL-Homology.Simplices
Presenting theory DiscretePricing.Filtration
Presenting theory Deep_Learning.Tensor_Matricization
Presenting theory DiscretePricing.Martingale
Presenting theory Deep_Learning.DL_Rank_CP_Rank
Presenting theory Deep_Learning.DL_Flatten_Matrix
Presenting theory HOL-Probability.Independent_Family
Presenting theory Density_Compiler.PDF_Density_Contexts
Presenting theory HOL-Probability.Convolution
Presenting theory Deep_Learning.DL_Network
Presenting theory Deep_Learning.DL_Concrete_Matrices
Presenting theory Deep_Learning.DL_Missing_Finite_Set
Presenting theory HOL-Analysis.Derivative
Presenting theory DiscretePricing.Disc_Cond_Expect
Presenting theory Density_Compiler.PDF_Compiler_Pred
Presenting theory HOL-Analysis.Cartesian_Euclidean_Space
Presenting theory Deep_Learning.DL_Deep_Model
Presenting theory Density_Compiler.PDF_Target_Semantics
Presenting theory Winding_Number_Eval.Winding_Number_Eval
Presenting theory Density_Compiler.PDF_Target_Density_Contexts
Presenting theory Winding_Number_Eval.Winding_Number_Eval_Examples
Presenting document Ergodic_Theory/document
Presenting document Ergodic_Theory/outline
Presenting theory Deep_Learning.DL_Deep_Model_Poly
Presenting theory Deep_Learning.Lebesgue_Functional
Presenting theory Deep_Learning.Lebesgue_Zero_Set
Presenting theory Deep_Learning.DL_Shallow_Model
Presenting theory HOL-Probability.Information
Presenting theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity
Presenting Laws_of_Large_Numbers ...
Presenting document Laws_of_Large_Numbers/document
Presenting document Laws_of_Large_Numbers/outline
Presenting theory Laws_of_Large_Numbers.Laws_of_Large_Numbers
Presenting theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example
Presenting theory Density_Compiler.PDF_Compiler
Presenting document Fisher_Yates/document
Presenting document Fisher_Yates/outline
Presenting document Fourier/document
Presenting document Fourier/outline
Presenting theory HOL-Homology.Homology_Groups
Presenting theory Fourier.Periodic
Presenting theory Fourier.Lspace
Presenting theory Ergodic_Theory.SG_Library_Complement
Presenting theory Fisher_Yates.Fisher_Yates
Presenting Frequency_Moments ...
Presenting document Frequency_Moments/document
Presenting document Frequency_Moments/outline
Presenting theory Fourier.Square_Integrable
Presenting theory Ergodic_Theory.ME_Library_Complement
Presenting theory Fourier.Confine
Presenting theory Fourier.Fourier_Aux2
Presenting theory Ergodic_Theory.Fekete
Presenting theory Frequency_Moments.Frequency_Moments_Preliminary_Results
Presenting theory Frequency_Moments.Frequency_Moments
Presenting theory Frequency_Moments.K_Smallest
Presenting theory Frequency_Moments.Landau_Ext
Presenting theory HOL-Probability.Distributions
Presenting theory Frequency_Moments.Probability_Ext
Presenting theory Ergodic_Theory.Asymptotic_Density
Presenting theory Frequency_Moments.Product_PMF_Ext
Presenting theory Fourier.Fourier
Presenting Girth_Chromatic ...
Presenting document Girth_Chromatic/document
Presenting document Girth_Chromatic/outline
Presenting theory Girth_Chromatic.Girth_Chromatic_Misc
Presenting theory Frequency_Moments.Frequency_Moment_0
Presenting theory Girth_Chromatic.Ugraphs
Presenting theory HOL-Probability.Characteristic_Functions
Presenting theory Frequency_Moments.Frequency_Moment_2
Presenting theory Girth_Chromatic.Girth_Chromatic
Presenting Random_Graph_Subgraph_Threshold ...
Presenting document Random_Graph_Subgraph_Threshold/document
Presenting document Random_Graph_Subgraph_Threshold/outline
Presenting theory HOL-Probability.Helly_Selection
Presenting theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
Presenting theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
Presenting theory Ergodic_Theory.Measure_Preserving_Transformations
Presenting theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
Presenting theory HOL-Probability.Sinc_Integral
Presenting theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
Presenting theory Frequency_Moments.Frequency_Moment_k
Presenting HOL-Probability-ex ...
Presenting theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
Presenting Hahn_Jordan_Decomposition ...
Presenting document Hahn_Jordan_Decomposition/document
Presenting document Hahn_Jordan_Decomposition/outline
Presenting theory Hahn_Jordan_Decomposition.Extended_Reals_Sums_Compl
Presenting theory HOL-Probability-ex.Dining_Cryptographers
Presenting theory Hahn_Jordan_Decomposition.Hahn_Jordan_Prelims
Presenting theory DiscretePricing.Infinite_Coin_Toss_Space
Presenting theory HOL-Probability.Levy
Presenting theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure
Presenting theory HOL-Probability-ex.Measure_Not_CCC
Presenting document List_Update/document
Presenting document List_Update/outline
Presenting theory List_Update.Inversion
Presenting theory HOL-Probability.Central_Limit_Theorem
Presenting theory List_Update.Swaps
Presenting theory HOL-Probability.Discrete_Topology
Presenting theory DiscretePricing.Geometric_Random_Walk
Presenting theory HOL-Homology.Brouwer_Degree
Presenting theory List_Update.On_Off
Presenting theory Hahn_Jordan_Decomposition.Hahn_Jordan_Decomposition
Presenting document Lp/document
Presenting document Lp/outline
Presenting theory List_Update.Prob_Theory
Presenting theory List_Update.Competitive_Analysis
Presenting theory List_Update.Move_to_Front
Presenting theory HOL-Analysis.Starlike
Presenting theory Lp.Functional_Spaces
Presenting file "Tools/SMT/smt_util.ML"
Presenting file "Tools/SMT/smt_failure.ML"
Presenting file "Tools/SMT/smt_config.ML"
Presenting file "Tools/SMT/smt_builtin.ML"
Presenting file "Tools/SMT/smt_datatypes.ML"
Presenting file "Tools/SMT/smt_normalize.ML"
Presenting file "Tools/SMT/smt_translate.ML"
Presenting file "Tools/SMT/smtlib.ML"
Presenting file "Tools/SMT/smtlib_interface.ML"
Presenting file "Tools/SMT/smtlib_proof.ML"
Presenting file "Tools/SMT/smtlib_isar.ML"
Presenting file "Tools/SMT/z3_proof.ML"
Presenting file "Tools/SMT/z3_isar.ML"
Presenting file "Tools/SMT/smt_solver.ML"
Presenting file "Tools/SMT/cvc4_interface.ML"
Presenting file "Tools/SMT/lethe_proof.ML"
Presenting file "Tools/SMT/lethe_isar.ML"
Presenting file "Tools/SMT/lethe_proof_parse.ML"
Presenting file "Tools/SMT/cvc4_proof_parse.ML"
Presenting file "Tools/SMT/verit_proof.ML"
Presenting file "Tools/SMT/conj_disj_perm.ML"
Presenting file "Tools/SMT/smt_replay_methods.ML"
Presenting file "Tools/SMT/smt_replay.ML"
Presenting file "Tools/SMT/smt_replay_arith.ML"
Presenting file "Tools/SMT/z3_interface.ML"
Presenting file "Tools/SMT/z3_replay_rules.ML"
Presenting file "Tools/SMT/z3_replay_methods.ML"
Presenting file "Tools/SMT/z3_replay.ML"
Presenting file "Tools/SMT/lethe_replay_methods.ML"
Presenting file "Tools/SMT/verit_replay_methods.ML"
Presenting file "Tools/SMT/verit_replay.ML"
Presenting file "Tools/SMT/smt_systems.ML"
Presenting theory List_Update.Bit_Strings
Presenting theory Ergodic_Theory.Recurrence
Presenting theory List_Update.MTF2_Effects
Presenting theory HOL-Analysis.Product_Topology
Presenting theory HOL-Probability.Probability_Mass_Function
Presenting theory Ergodic_Theory.Invariants
Presenting theory HOL-Probability.PMF_Impl
Presenting theory HOL-Analysis.T1_Spaces
Presenting theory Ergodic_Theory.Ergodicity
Presenting theory Ergodic_Theory.Shift_Operator
Presenting theory HOL-Homology.Invariance_of_Domain
Presenting document MDP-Rewards/document
Presenting document MDP-Rewards/outline
Presenting theory HOL-Homology.Homology
Presenting document MDP-Algorithms/document
Presenting document MDP-Algorithms/outline
Presenting theory MDP-Rewards.Bounded_Functions
Presenting theory List_Update.BIT
Presenting theory MDP-Algorithms.Value_Iteration
Presenting theory List_Update.Partial_Cost_Model
Presenting theory MDP-Rewards.Blinfun_Util
Presenting theory MDP-Algorithms.Policy_Iteration
Presenting theory MDP-Rewards.MDP_reward_Util
Presenting theory HOL-Probability.Fin_Map
Presenting theory List_Update.RExp_Var
Presenting theory DiscretePricing.Fair_Price
Presenting theory Ergodic_Theory.Kingman
Presenting theory HOL-Analysis.Path_Connected
Presenting theory MDP-Algorithms.Modified_Policy_Iteration
Presenting theory MDP-Algorithms.Matrix_Util
Presenting theory MDP-Algorithms.Blinfun_Matrix
Presenting theory List_Update.OPT2
Presenting theory HOL-Probability.Projective_Limit
Presenting theory List_Update.Phase_Partitioning
Presenting theory HOL-Probability.Random_Permutations
Presenting theory MDP-Rewards.MDP_cont
Presenting theory HOL-Analysis.Weierstrass_Theorems
Presenting theory Ergodic_Theory.Gouezel_Karlsson
Presenting theory Ergodic_Theory.Kohlberg_Neyman_Karlsson
Presenting theory HOL.Sledgehammer
Presenting file "Tools/ATP/system_on_tptp.ML"
Presenting file "Tools/Sledgehammer/async_manager_legacy.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_util.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_fact.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_proof_methods.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_isar_proof.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_isar_compress.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_isar_minimize.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_isar.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_atp_systems.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_prover.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_prover_smt.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_mepo.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_mash.ML"
Presenting file "Tools/Sledgehammer/sledgehammer.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_commands.ML"
Presenting file "Tools/Sledgehammer/sledgehammer_tactics.ML"
Presenting theory MDP-Rewards.MDP_disc
Presenting theory HOL.Lifting_Set
Presenting theory Ergodic_Theory.Transfer_Operator
Presenting theory HOL-Probability.SPMF
Presenting theory HOL-Analysis.Sigma_Algebra
Presenting theory MDP-Algorithms.Splitting_Methods
Presenting theory MDP-Algorithms.Algorithms
Presenting theory HOL-Probability.Product_PMF
Presenting theory HOL-Analysis.Measurable
Presenting file "measurable.ML"
Presenting theory List_Update.List_Factoring
Presenting theory MDP-Algorithms.Code_DP
Presenting theory MDP-Algorithms.Code_Mod
Presenting theory MDP-Algorithms.Code_Real_Approx_By_Float_Fix
Presenting theory MDP-Rewards.MDP_reward
Presenting theory Ergodic_Theory.Normalizing_Sequences
Presenting document MFMC_Countable/document
Presenting document MFMC_Countable/outline
Presenting document Markov_Models/document
Presenting document Markov_Models/outline
Presenting theory MFMC_Countable.MFMC_Misc
Presenting theory HOL-Probability.Hoeffding
Presenting theory MDP-Algorithms.Code_Inventory
Presenting theory MFMC_Countable.MFMC_Finite
Presenting theory Markov_Models.Markov_Models_Auxiliary
Presenting theory MDP-Algorithms.Code_Gridworld
Presenting theory MDP-Algorithms.Examples
Presenting Hidden_Markov_Models ...
Presenting document Hidden_Markov_Models/document
Presenting document Hidden_Markov_Models/outline
Presenting theory Hidden_Markov_Models.Auxiliary
Presenting theory HOL-Probability.Stream_Space
Presenting theory Hidden_Markov_Models.Hidden_Markov_Model
Presenting theory MFMC_Countable.Matrix_For_Marginals
Presenting theory HOL-Probability.Tree_Space
Presenting theory Hidden_Markov_Models.HMM_Implementation
Presenting theory Hidden_Markov_Models.HMM_Example
Presenting Probabilistic_Timed_Automata ...
Presenting document Probabilistic_Timed_Automata/document
Presenting document Probabilistic_Timed_Automata/outline
Presenting theory Probabilistic_Timed_Automata.MDP_Aux
Presenting theory Probabilistic_Timed_Automata.Finiteness
Presenting theory Probabilistic_Timed_Automata.Basic
Presenting theory Probabilistic_Timed_Automata.Sequence
Presenting theory Probabilistic_Timed_Automata.Sequence_LTL
Presenting theory Markov_Models.Discrete_Time_Markov_Chain
Presenting theory Probabilistic_Timed_Automata.Instantiate_Existentials
Presenting theory Probabilistic_Timed_Automata.More_List
Presenting theory MFMC_Countable.MFMC_Network
Presenting theory Probabilistic_Timed_Automata.Stream_More
Presenting theory Markov_Models.Trace_Space_Equals_Markov_Processes
Presenting theory HOL-Analysis.Measure_Space
Presenting theory HOL-Probability.Conditional_Expectation
Presenting theory HOL-Probability.Essential_Supremum
Presenting theory Probabilistic_Timed_Automata.Graphs
Presenting theory DiscretePricing.CRR_Model
Presenting theory List_Update.TS
Presenting theory HOL-Probability.Stopping_Time
Presenting theory HOL-Probability.Probability
Presenting Stochastic_Matrices ...
Presenting document Stochastic_Matrices/document
Presenting document Stochastic_Matrices/outline
Presenting theory HOL-Analysis.Ordered_Euclidean_Space
Presenting theory Stochastic_Matrices.Stochastic_Matrix
Presenting theory Stochastic_Matrices.Stochastic_Vector_PMF
Presenting theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models
Presenting theory Stochastic_Matrices.Eigenspace
Presenting theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius
Presenting document Median_Method/document
Presenting document Median_Method/outline
Presenting theory MFMC_Countable.MFMC_Web
Presenting theory Probabilistic_Timed_Automata.Lib
Presenting theory Median_Method.Median
Presenting Monad_Normalisation ...
Presenting document Monad_Normalisation/document
Presenting document Monad_Normalisation/outline
Presenting theory List_Update.BIT_pairwise
Presenting theory DiscretePricing.Option_Price_Examples
Presenting Monomorphic_Monad ...
Presenting document Monomorphic_Monad/document
Presenting document Monomorphic_Monad/outline
Presenting theory HOL-Analysis.Borel_Space
Presenting theory Monad_Normalisation.Monad_Normalisation
Presenting file "monad_rules.ML"
Presenting file "monad_normalisation.ML"
Presenting theory HOL.Groups_List
Presenting theory Monad_Normalisation.Monad_Normalisation_Test
Presenting Neumann_Morgenstern_Utility ...
Presenting document Neumann_Morgenstern_Utility/document
Presenting document Neumann_Morgenstern_Utility/outline
Presenting theory Neumann_Morgenstern_Utility.PMF_Composition
Presenting theory Neumann_Morgenstern_Utility.Lotteries
Presenting theory Markov_Models.Classifying_Markov_Chain_States
Presenting theory HOL.Bit_Operations
Presenting theory List_Update.BIT_2comp_on2
Presenting theory MFMC_Countable.MFMC_Reduction
Presenting theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem
Presenting theory HOL.Code_Numeral
Presenting theory Neumann_Morgenstern_Utility.Expected_Utility
Presenting Probabilistic_Noninterference ...
Presenting document Probabilistic_Noninterference/document
Presenting document Probabilistic_Noninterference/outline
Presenting theory Probabilistic_Noninterference.Interface
Presenting theory Markov_Models.Markov_Decision_Process
Presenting theory HOL-Analysis.Nonnegative_Lebesgue_Integration
Presenting theory List_Update.Comb
Presenting Probabilistic_Prime_Tests ...
Presenting document Probabilistic_Prime_Tests/document
Presenting document Probabilistic_Prime_Tests/outline
Presenting theory MFMC_Countable.MFMC_Bounded
Presenting theory Probabilistic_Prime_Tests.Legendre_Symbol
Presenting file "Tools/string_syntax.ML"
Presenting file "Tools/literal.ML"
Presenting theory Markov_Models.MDP_Reachability_Problem
Presenting theory HOL.Predicate
Presenting theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
Presenting theory HOL.Lazy_Sequence
Presenting theory HOL.Limited_Sequence
Presenting theory Probabilistic_Noninterference.Language_Semantics
Presenting theory Probabilistic_Prime_Tests.Jacobi_Symbol
Presenting theory HOL.Code_Evaluation
Presenting file "Tools/code_evaluation.ML"
Presenting file "Tools/value_command.ML"
Presenting file "Tools/reification.ML"
Presenting theory Probabilistic_Prime_Tests.Residues_Nat
Presenting theory Probabilistic_Prime_Tests.QuadRes
Presenting theory Markov_Models.Discrete_Time_Markov_Process
Presenting theory Probabilistic_Prime_Tests.Euler_Witness
Presenting theory Probabilistic_Prime_Tests.Carmichael_Numbers
Presenting theory Probabilistic_Prime_Tests.Fermat_Witness
Presenting theory HOL.Quickcheck_Random
Presenting file "Tools/Quickcheck/quickcheck_common.ML"
Presenting file "Tools/Quickcheck/random_generators.ML"
Presenting theory Probabilistic_Prime_Tests.Generalized_Primality_Test
Presenting theory Probabilistic_Prime_Tests.Fermat_Test
Presenting theory HOL.Random_Pred
Presenting theory Probabilistic_Prime_Tests.Miller_Rabin_Test
Presenting theory HOL-Analysis.Binary_Product_Measure
Presenting theory Probabilistic_Prime_Tests.Solovay_Strassen_Test
Presenting Probabilistic_System_Zoo ...
Presenting document Probabilistic_System_Zoo/document
Presenting document Probabilistic_System_Zoo/outline
Presenting document Probabilistic_System_Zoo/bnfs
Presenting document Probabilistic_System_Zoo/non_bnfs
Presenting theory Probabilistic_System_Zoo.Bool_Bounded_Set
Presenting theory HOL.Random_Sequence
Presenting theory Probabilistic_System_Zoo.Finitely_Bounded_Set_Counterexample
Presenting theory Probabilistic_System_Zoo.Nonempty_Bounded_Set
Presenting theory Monomorphic_Monad.Monomorphic_Monad
Presenting theory HOL.Quickcheck_Exhaustive
Presenting file "Tools/Quickcheck/exhaustive_generators.ML"
Presenting file "Tools/Quickcheck/abstract_generators.ML"
Presenting theory Probabilistic_Timed_Automata.PTA
Presenting theory Probabilistic_System_Zoo.Probabilistic_Hierarchy
Presenting theory Probabilistic_Noninterference.Resumption_Based
Presenting theory Probabilistic_System_Zoo.Vardi
Presenting theory Probabilistic_System_Zoo.Vardi_Counterexample
Presenting Probabilistic_While ...
Presenting document Probabilistic_While/document
Presenting document Probabilistic_While/outline
Presenting theory Markov_Models.Continuous_Time_Markov_Chain
Presenting theory Markov_Models.Markov_Models
Presenting theory Markov_Models.Example_A
Presenting theory Probabilistic_While.While_SPMF
Presenting theory Markov_Models.Example_B
Presenting theory Probabilistic_While.Bernoulli
Presenting theory HOL-Analysis.Finite_Product_Measure
Presenting theory Probabilistic_While.Geometric
Presenting theory MFMC_Countable.MFMC_Flow_Attainability
Presenting theory Probabilistic_While.Fast_Dice_Roll
Presenting theory Probabilistic_While.Resampling
Presenting document CryptHOL/document
Presenting document CryptHOL/outline
Presenting theory HOL-Analysis.Caratheodory
Presenting theory Monomorphic_Monad.Monad_Overloading
Presenting theory Markov_Models.PCTL
Presenting theory Markov_Models.PGCL
Presenting theory Probabilistic_Noninterference.Trace_Based
Presenting theory Monomorphic_Monad.Interpreter
Presenting theory Markov_Models.Crowds_Protocol
Presenting theory Monomorphic_Monad.Just_Do_It_Examples
Presenting Constructive_Cryptography ...
Presenting document Constructive_Cryptography/document
Presenting document Constructive_Cryptography/outline
Presenting theory Markov_Models.Zeroconf_Analysis
Presenting theory Markov_Models.Gossip_Broadcast
Presenting theory HOL-Analysis.Bochner_Integration
Presenting theory CryptHOL.Misc_CryptHOL
Presenting theory CryptHOL.Set_Applicative
Presenting theory Markov_Models.MDP_RP_Certification
Presenting theory CryptHOL.SPMF_Applicative
Presenting theory CryptHOL.List_Bits
Presenting theory Constructive_Cryptography.Resource
Presenting theory CryptHOL.Environment_Functor
Presenting theory Markov_Models.MDP_RP
Presenting Constructive_Cryptography_CM ...
Presenting document Constructive_Cryptography_CM/document
Presenting document Constructive_Cryptography_CM/outline
Presenting theory CryptHOL.Partial_Function_Set
Presenting theory CryptHOL.Negligible
Presenting theory Probabilistic_Noninterference.Compositionality
Presenting theory Probabilistic_Timed_Automata.PTA_Reachability
Presenting theory HOL-Analysis.Complete_Measure
Presenting theory Probabilistic_Noninterference.Syntactic_Criteria
Presenting Game_Based_Crypto ...
Presenting document Game_Based_Crypto/document
Presenting document Game_Based_Crypto/outline
Presenting theory Game_Based_Crypto.Diffie_Hellman
Presenting theory Probabilistic_Noninterference.Concrete
Presenting Multi_Party_Computation ...
Presenting document Multi_Party_Computation/document
Presenting document Multi_Party_Computation/outline
Presenting theory Multi_Party_Computation.Cyclic_Group_Ext
Presenting theory Multi_Party_Computation.Number_Theory_Aux
Presenting theory Multi_Party_Computation.Uniform_Sampling
Presenting theory Multi_Party_Computation.Semi_Honest_Def
Presenting theory Game_Based_Crypto.IND_CCA2
Presenting theory Multi_Party_Computation.OT_Functionalities
Presenting theory MFMC_Countable.MFMC_Unbounded
Presenting theory Multi_Party_Computation.ETP
Presenting theory Game_Based_Crypto.IND_CCA2_sym
Presenting theory HOL-Analysis.Regularity
Presenting theory Game_Based_Crypto.IND_CPA
Presenting theory Game_Based_Crypto.IND_CPA_PK
Presenting theory Multi_Party_Computation.ETP_OT
Presenting theory Game_Based_Crypto.IND_CPA_PK_Single
Presenting theory MFMC_Countable.Max_Flow_Min_Cut_Countable
Presenting theory CryptHOL.Resumption
Presenting theory Multi_Party_Computation.ETP_RSA_OT
Presenting theory MFMC_Countable.Rel_PMF_Characterisation
Presenting theory Game_Based_Crypto.SUF_CMA
Presenting theory Game_Based_Crypto.Pseudo_Random_Function
Presenting theory Multi_Party_Computation.Noar_Pinkas_OT
Presenting theory Game_Based_Crypto.Pseudo_Random_Permutation
Presenting theory CryptHOL.Generat
Presenting theory HOL.Predicate_Compile
Presenting file "Tools/Predicate_Compile/predicate_compile_aux.ML"
Presenting file "Tools/Predicate_Compile/predicate_compile_compilations.ML"
Presenting file "Tools/Predicate_Compile/core_data.ML"
Presenting file "Tools/Predicate_Compile/mode_inference.ML"
Presenting file "Tools/Predicate_Compile/predicate_compile_proof.ML"
Presenting file "Tools/Predicate_Compile/predicate_compile_core.ML"
Presenting file "Tools/Predicate_Compile/predicate_compile_data.ML"
Presenting file "Tools/Predicate_Compile/predicate_compile_fun.ML"
Presenting file "Tools/Predicate_Compile/predicate_compile_pred.ML"
Presenting file "Tools/Predicate_Compile/predicate_compile_specialisation.ML"
Presenting file "Tools/Predicate_Compile/predicate_compile.ML"
Presenting theory Constructive_Cryptography.Converter
Presenting theory MFMC_Countable.Rel_PMF_Characterisation_MFMC
Presenting Sigma_Commit_Crypto ...
Presenting document Sigma_Commit_Crypto/document
Presenting document Sigma_Commit_Crypto/outline
Presenting theory Game_Based_Crypto.Guessing_Many_One
Presenting theory Sigma_Commit_Crypto.Commitment_Schemes
Presenting theory Sigma_Commit_Crypto.Cyclic_Group_Ext
Presenting theory Game_Based_Crypto.Unpredictable_Function
Presenting theory Game_Based_Crypto.Security_Spec
Presenting theory Multi_Party_Computation.OT14
Presenting theory Sigma_Commit_Crypto.Discrete_Log
Presenting theory Sigma_Commit_Crypto.Number_Theory_Aux
Presenting theory HOL.Quickcheck_Narrowing
Presenting file "Tools/Quickcheck/Narrowing_Engine.hs"
Presenting file "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
Presenting file "Tools/Quickcheck/narrowing_generators.ML"
Presenting file "Tools/Quickcheck/find_unused_assms.ML"
Presenting theory HOL-Analysis.Lebesgue_Measure
Presenting theory Game_Based_Crypto.Elgamal
Presenting theory Sigma_Commit_Crypto.Uniform_Sampling
Presenting theory Multi_Party_Computation.GMW
Presenting theory Constructive_Cryptography.Converter_Rewrite
Presenting theory Constructive_Cryptography_CM.More_CC
Presenting theory HOL.Mirabelle
Presenting file "Tools/Mirabelle/mirabelle_util.ML"
Presenting file "Tools/Mirabelle/mirabelle.ML"
Presenting file "Tools/Mirabelle/mirabelle_arith.ML"
Presenting file "Tools/Mirabelle/mirabelle_metis.ML"
Presenting file "Tools/Mirabelle/mirabelle_presburger.ML"
Presenting file "Tools/Mirabelle/mirabelle_quickcheck.ML"
Presenting file "Tools/Mirabelle/mirabelle_sledgehammer_filter.ML"
Presenting file "Tools/Mirabelle/mirabelle_sledgehammer.ML"
Presenting file "Tools/Mirabelle/mirabelle_try0.ML"
Presenting theory Sigma_Commit_Crypto.Pedersen
Presenting theory HOL.Extraction
Presenting theory Constructive_Cryptography.Random_System
Presenting theory Multi_Party_Computation.Secure_Multiplication
Presenting theory Game_Based_Crypto.Hashed_Elgamal
Presenting theory Multi_Party_Computation.DH_Ext
Presenting theory Sigma_Commit_Crypto.Rivest
Presenting theory Multi_Party_Computation.Malicious_Defs
Presenting theory Constructive_Cryptography.Distinguisher
Presenting theory Game_Based_Crypto.RP_RF
Presenting theory Sigma_Commit_Crypto.Sigma_Protocols
Presenting theory Sigma_Commit_Crypto.Schnorr_Sigma_Commit
Presenting theory Game_Based_Crypto.PRF_UHF
Presenting file "Tools/record.ML"
Presenting theory Multi_Party_Computation.Malicious_OT
Presenting theory Constructive_Cryptography.Wiring
Presenting Projective_Measurements ...
Presenting document Projective_Measurements/document
Presenting document Projective_Measurements/outline
Presenting theory Sigma_Commit_Crypto.Chaum_Pedersen_Sigma_Commit
Presenting theory HOL-Analysis.Tagged_Division
Presenting theory Sigma_Commit_Crypto.Okamoto_Sigma_Commit
Presenting theory Game_Based_Crypto.PRF_IND_CPA
Presenting theory Constructive_Cryptography.Constructive_Cryptography
Presenting theory Sigma_Commit_Crypto.Xor
Presenting theory Projective_Measurements.Linear_Algebra_Complements
Presenting theory Constructive_Cryptography.System_Construction
Presenting theory Constructive_Cryptography_CM.Observe_Failure
Presenting theory Sigma_Commit_Crypto.Sigma_AND
Presenting theory Constructive_Cryptography_CM.Fold_Spmf
Presenting theory Constructive_Cryptography.One_Time_Pad
Presenting theory Sigma_Commit_Crypto.Sigma_OR
Presenting Quasi_Borel_Spaces ...
Presenting document Quasi_Borel_Spaces/document
Presenting document Quasi_Borel_Spaces/outline
Presenting theory Projective_Measurements.Projective_Measurements
Presenting theory Quasi_Borel_Spaces.StandardBorel
Presenting theory Game_Based_Crypto.PRF_UPF_IND_CCA
Presenting theory Game_Based_Crypto.Cryptographic_Constructions
Presenting theory Game_Based_Crypto.Game_Based_Crypto
Presenting theory Quasi_Borel_Spaces.QuasiBorel
Presenting theory Quasi_Borel_Spaces.Measure_QuasiBorel_Adjunction
Presenting theory Quasi_Borel_Spaces.Binary_Product_QuasiBorel
Presenting theory Quasi_Borel_Spaces.Product_QuasiBorel
Presenting theory Projective_Measurements.CHSH_Inequality
Presenting Quick_Sort_Cost ...
Presenting document Quick_Sort_Cost/document
Presenting document Quick_Sort_Cost/outline
Presenting theory Constructive_Cryptography.Message_Authentication_Code
Presenting theory Constructive_Cryptography.Secure_Channel
Presenting theory Constructive_Cryptography.Examples
Presenting document Random_BSTs/document
Presenting document Random_BSTs/outline
Presenting theory Quasi_Borel_Spaces.Binary_CoProduct_QuasiBorel
Presenting theory Quick_Sort_Cost.Randomised_Quick_Sort
Presenting theory Random_BSTs.Random_BSTs
Presenting Randomised_BSTs ...
Presenting document Randomised_BSTs/document
Presenting document Randomised_BSTs/outline
Presenting theory Quick_Sort_Cost.Quick_Sort_Average_Case
Presenting Randomised_Social_Choice ...
Presenting document Randomised_Social_Choice/document
Presenting document Randomised_Social_Choice/outline
Presenting theory CryptHOL.Generative_Probabilistic_Value
Presenting theory Game_Based_Crypto.CryptHOL_Tutorial
Presenting SDS_Impossibility ...
Presenting document SDS_Impossibility/document
Presenting document SDS_Impossibility/outline
Presenting theory Quasi_Borel_Spaces.CoProduct_QuasiBorel
Presenting theory HOL-Analysis.Henstock_Kurzweil_Integration
Presenting theory Randomised_Social_Choice.Order_Predicates
Presenting theory Randomised_BSTs.Randomised_BSTs
Presenting Roth_Arithmetic_Progressions ...
Presenting document Roth_Arithmetic_Progressions/document
Presenting document Roth_Arithmetic_Progressions/outline
Presenting theory Constructive_Cryptography_CM.Fused_Resource
Presenting theory CryptHOL.Computational_Model
Presenting theory Constructive_Cryptography_CM.State_Isomorphism
Presenting theory HOL-Analysis.Radon_Nikodym
Presenting theory Quasi_Borel_Spaces.Exponent_QuasiBorel
Presenting theory SDS_Impossibility.SDS_Impossibility
Presenting theory Randomised_Social_Choice.Preference_Profiles
Presenting document Skip_Lists/document
Presenting document Skip_Lists/outline
Presenting theory Randomised_Social_Choice.Elections
Presenting theory Randomised_Social_Choice.Lotteries
Presenting theory HOL-Analysis.Set_Integral
Presenting theory Randomised_Social_Choice.Utility_Functions
Presenting theory HOL-Analysis.Continuum_Not_Denumerable
Presenting theory Skip_Lists.Pi_pmf
Presenting theory Randomised_Social_Choice.Stochastic_Dominance
Presenting theory Roth_Arithmetic_Progressions.Roth_Arithmetic_Progressions
Presenting Source_Coding_Theorem ...
Presenting document Source_Coding_Theorem/document
Presenting document Source_Coding_Theorem/outline
Presenting theory Skip_Lists.Misc
Presenting theory Constructive_Cryptography_CM.Construction_Utility
Presenting theory Randomised_Social_Choice.SD_Efficiency
Presenting theory Source_Coding_Theorem.Source_Coding_Theorem
Presenting theory Skip_Lists.Geometric_PMF
Presenting theory CryptHOL.GPV_Expectation
Presenting document Treaps/document
Presenting document Treaps/outline
Presenting theory Quasi_Borel_Spaces.Probability_Space_QuasiBorel
Presenting theory Randomised_Social_Choice.Social_Decision_Schemes
Presenting theory Treaps.Probability_Misc
Presenting theory Treaps.Treap
Presenting theory Randomised_Social_Choice.SDS_Lowering
Presenting theory Treaps.Random_List_Permutation
Presenting theory Treaps.Treap_Sort_and_BSTs
Presenting theory Randomised_Social_Choice.Random_Dictatorship
Presenting theory Constructive_Cryptography_CM.Concrete_Security
Presenting theory Skip_Lists.Skip_List
Presenting theory Treaps.Random_Treap
Presenting Universal_Hash_Families ...
Presenting document Universal_Hash_Families/document
Presenting document Universal_Hash_Families/outline
Presenting Hybrid_Systems_VCs ...
Presenting document Hybrid_Systems_VCs/document
Presenting document Hybrid_Systems_VCs/outline
Presenting theory CryptHOL.GPV_Bisim
Presenting theory Universal_Hash_Families.Definitions
Presenting theory Universal_Hash_Families.Preliminary_Results
Presenting theory Hybrid_Systems_VCs.HS_Preliminaries
Presenting theory Randomised_Social_Choice.Random_Serial_Dictatorship
Presenting theory CryptHOL.GPV_Applicative
Presenting theory Randomised_Social_Choice.Randomised_Social_Choice
Presenting theory Universal_Hash_Families.Carter_Wegman_Hash_Family
Presenting theory CryptHOL.Cyclic_Group
Presenting theory Universal_Hash_Families.Field
Presenting document Hyperdual/document
Presenting document Hyperdual/outline
Presenting theory CryptHOL.Cyclic_Group_SPMF
Presenting theory CryptHOL.CryptHOL
Presenting Irrational_Series_Erdos_Straus ...
Presenting document Irrational_Series_Erdos_Straus/document
Presenting document Irrational_Series_Erdos_Straus/outline
Presenting theory HOL-Analysis.Homotopy
Presenting theory Constructive_Cryptography_CM.Asymptotic_Security
Presenting theory Constructive_Cryptography_CM.Key
Presenting theory Hyperdual.Hyperdual
Presenting theory Constructive_Cryptography_CM.Channel
Presenting theory Hyperdual.TwiceFieldDifferentiable
Presenting theory Hybrid_Systems_VCs.HS_ODEs
Presenting theory Hyperdual.HyperdualFunctionExtension
Presenting theory Hyperdual.LogisticFunction
Presenting theory HOL-Analysis.Homeomorphism
Presenting theory Hyperdual.AnalyticTestFunction
Presenting Irrationality_J_Hancl ...
Presenting document Irrationality_J_Hancl/document
Presenting theory Randomised_Social_Choice.Preference_Profile_Cmd
Presenting document Irrationality_J_Hancl/outline
Presenting file "preference_profiles.ML"
Presenting theory Quasi_Borel_Spaces.Monad_QuasiBorel
Presenting theory Hybrid_Systems_VCs.HS_VC_Spartan
Presenting theory Irrational_Series_Erdos_Straus.Irrational_Series_Erdos_Straus
Presenting theory Randomised_Social_Choice.QSOpt_Exact
Presenting document KD_Tree/document
Presenting document KD_Tree/outline
Presenting theory Irrationality_J_Hancl.Irrationality_J_Hancl
Presenting theory Quasi_Borel_Spaces.Pair_QuasiBorel_Measure
Presenting Kuratowski_Closure_Complement ...
Presenting document Kuratowski_Closure_Complement/document
Presenting document Kuratowski_Closure_Complement/outline
Presenting theory Hybrid_Systems_VCs.HS_VC_Examples
Presenting theory KD_Tree.KD_Tree
Presenting theory Kuratowski_Closure_Complement.KuratowskiClosureComplementTheorem
Presenting theory Quasi_Borel_Spaces.Measure_as_QuasiBorel_Measure
Presenting Laplace_Transform ...
Presenting document Laplace_Transform/document
Presenting document Laplace_Transform/outline
Presenting theory Hybrid_Systems_VCs.HS_VC_PT
Presenting theory Laplace_Transform.Laplace_Transform_Library
Presenting theory Randomised_Social_Choice.SDS_Automation
Presenting file "randomised_social_choice.ML"
Presenting file "sds_automation.ML"
Presenting Lower_Semicontinuous ...
Presenting document Lower_Semicontinuous/document
Presenting document Lower_Semicontinuous/outline
Presenting theory Laplace_Transform.Piecewise_Continuous
Presenting theory KD_Tree.Build
Presenting theory Hybrid_Systems_VCs.HS_VC_PT_Examples
Presenting theory KD_Tree.Range_Search
Presenting theory Hybrid_Systems_VCs.HS_VC_MKA
Presenting theory Constructive_Cryptography_CM.One_Time_Pad
Presenting theory Hybrid_Systems_VCs.HS_VC_KA_rel
Presenting theory Quasi_Borel_Spaces.Bayesian_Linear_Regression
Presenting theory Hybrid_Systems_VCs.HS_VC_MKA_rel
Presenting theory Lower_Semicontinuous.Lower_Semicontinuous
Presenting theory Laplace_Transform.Existence
Presenting theory KD_Tree.Nearest_Neighbors
Presenting theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
Presenting file "Tools/Nitpick/kodkod.ML"
Presenting Matrices_for_ODEs ...
Presenting file "Tools/Nitpick/kodkod_sat.ML"
Presenting file "Tools/Nitpick/nitpick_util.ML"
Presenting Minkowskis_Theorem ...
Presenting file "Tools/Nitpick/nitpick_hol.ML"
Presenting document Matrices_for_ODEs/document
Presenting document Matrices_for_ODEs/outline
Presenting document Minkowskis_Theorem/document
Presenting document Minkowskis_Theorem/outline
Presenting theory Hybrid_Systems_VCs.HS_VC_MKA_Examples_rel
Presenting file "Tools/Nitpick/nitpick_mono.ML"
Presenting file "Tools/Nitpick/nitpick_preproc.ML"
Presenting file "Tools/Nitpick/nitpick_scope.ML"
Presenting file "Tools/Nitpick/nitpick_peephole.ML"
Presenting file "Tools/Nitpick/nitpick_rep.ML"
Presenting file "Tools/Nitpick/nitpick_nut.ML"
Presenting file "Tools/Nitpick/nitpick_kodkod.ML"
Presenting file "Tools/Nitpick/nitpick_model.ML"
Presenting file "Tools/Nitpick/nitpick.ML"
Presenting file "Tools/Nitpick/nitpick_commands.ML"
Presenting file "Tools/Nitpick/nitpick_tests.ML"
Presenting document Octonions/document
Presenting document Octonions/outline
Presenting theory Hybrid_Systems_VCs.HS_VC_KA_ndfun
Presenting theory Laplace_Transform.Lerch_Lemma
Presenting theory Matrices_for_ODEs.MTX_Preliminaries
Presenting theory Octonions.Cross_Product_7
Presenting theory Minkowskis_Theorem.Minkowskis_Theorem
Presenting Ordinary_Differential_Equations ...
Presenting document Ordinary_Differential_Equations/document
Presenting document Ordinary_Differential_Equations/outline
Presenting theory Matrices_for_ODEs.MTX_Norms
Presenting theory Laplace_Transform.Uniqueness
Presenting theory Laplace_Transform.Laplace_Transform
Presenting Differential_Dynamic_Logic ...
Presenting document Differential_Dynamic_Logic/document
Presenting document Differential_Dynamic_Logic/outline
Presenting theory Differential_Dynamic_Logic.Ids
Presenting theory Hybrid_Systems_VCs.HS_VC_MKA_ndfun
Presenting theory Matrices_for_ODEs.SQ_MTX
Presenting theory Ordinary_Differential_Equations.ODE_Auxiliarities
Presenting theory Ordinary_Differential_Equations.MVT_Ex
Presenting theory Octonions.Octonions
Presenting theory Matrices_for_ODEs.MTX_Flows
Presenting theory Ordinary_Differential_Equations.Vector_Derivative_On
Presenting HOL-ODE-Numerics ...
Presenting theory Hybrid_Systems_VCs.HS_VC_MKA_Examples_ndfun
Presenting theory HOL-ODE-Numerics.GenCF_No_Comp
Presenting theory Matrices_for_ODEs.MTX_Examples
Presenting HOL-ODE-ARCH-COMP ...
Presenting theory HOL-Analysis.Complex_Analysis_Basics
Presenting theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
Presenting theory Ordinary_Differential_Equations.Interval_Integral_HK
Presenting theory Hybrid_Systems_VCs.HS_VC_KAT
Presenting theory Ordinary_Differential_Equations.Gronwall
Presenting theory HOL-ODE-Numerics.Autoref_Misc
Presenting theory Differential_Dynamic_Logic.Lib
Presenting theory HOL-ODE-Numerics.Weak_Set
Presenting theory Hybrid_Systems_VCs.HS_VC_KAT_rel
Presenting theory HOL-Analysis.Complex_Transcendental
Presenting theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
Presenting HOL-ODE-Examples ...
Presenting theory Differential_Dynamic_Logic.Syntax
Presenting theory HOL-ODE-Numerics.Enclosure_Operations
Presenting theory HOL-ODE-Examples.Examples_Integral
Presenting theory HOL-ODE-Numerics.Refine_Vector_List
Presenting theory HOL-Analysis.Harmonic_Numbers
Presenting theory HOL-ODE-Numerics.Transfer_Analysis
Presenting theory HOL-ODE-Numerics.Transfer_ODE
Presenting theory Hybrid_Systems_VCs.HS_VC_KAT_Examples_rel
Presenting theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
Presenting theory HOL-ODE-Examples.Examples_One_Step_Method
Presenting theory Ordinary_Differential_Equations.Initial_Value_Problem
Presenting theory HOL.Nunchaku
Presenting file "Tools/Nunchaku/nunchaku_util.ML"
Presenting file "Tools/Nunchaku/nunchaku_collect.ML"
Presenting file "Tools/Nunchaku/nunchaku_problem.ML"
Presenting file "Tools/Nunchaku/nunchaku_translate.ML"
Presenting file "Tools/Nunchaku/nunchaku_model.ML"
Presenting file "Tools/Nunchaku/nunchaku_reconstruct.ML"
Presenting file "Tools/Nunchaku/nunchaku_display.ML"
Presenting file "Tools/Nunchaku/nunchaku_tool.ML"
Presenting file "Tools/Nunchaku/nunchaku.ML"
Presenting file "Tools/Nunchaku/nunchaku_commands.ML"
Presenting theory Differential_Dynamic_Logic.Denotational_Semantics
Presenting theory HOL-ODE-Numerics.Refine_Hyperplane
Presenting theory HOL-ODE-Examples.Examples_Poincare_Map
Presenting theory Hybrid_Systems_VCs.HS_VC_KAT_ndfun
Presenting theory HOL-ODE-Examples.ODE_Examples
Presenting Lorenz_Approximation ...
Presenting theory Lorenz_Approximation.Result_Elements
Presenting theory HOL-ODE-Numerics.Refine_Unions
Presenting theory Differential_Dynamic_Logic.Axioms
Presenting theory HOL-Analysis.Gamma_Function
Presenting theory HOL-ODE-Numerics.Refine_Intersection
Presenting theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
Presenting theory Hybrid_Systems_VCs.HS_VC_KAT_Examples_ndfun
Presenting theory HOL-ODE-Numerics.Refine_Invar
Presenting theory Lorenz_C0.Lorenz_C0
Presenting theory Ordinary_Differential_Equations.Bounded_Linear_Operator
Presenting theory Lorenz_C1.Lorenz_C1
Presenting Poincare_Bendixson ...
Presenting document Poincare_Bendixson/document
Presenting document Poincare_Bendixson/outline
Presenting theory Poincare_Bendixson.Analysis_Misc
Presenting theory HOL-Analysis.Interval_Integral
Presenting theory Constructive_Cryptography_CM.Diffie_Hellman_CC
Presenting theory HOL-ODE-Numerics.Refine_Interval
Presenting theory Differential_Dynamic_Logic.Frechet_Correctness
Presenting theory HOL-ODE-Numerics.Refine_Info
Presenting theory Ordinary_Differential_Equations.Multivariate_Taylor
Presenting theory Poincare_Bendixson.ODE_Misc
Presenting theory HOL-Analysis.Lebesgue_Integral_Substitution
Presenting theory Lorenz_Approximation.Result_File_Coarse
Presenting theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
Presenting theory Poincare_Bendixson.Invariance
Presenting theory HOL-Analysis.Ball_Volume
Presenting theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
Presenting theory HOL-Analysis.Integral_Test
Presenting theory Poincare_Bendixson.Limit_Set
Presenting theory Differential_Dynamic_Logic.Static_Semantics
Presenting theory Poincare_Bendixson.Periodic_Orbit
Presenting theory Constructive_Cryptography_CM.DH_OTP
Presenting Prime_Harmonic_Series ...
Presenting document Prime_Harmonic_Series/document
Presenting document Prime_Harmonic_Series/outline
Presenting theory Prime_Harmonic_Series.Prime_Harmonic_Misc
Presenting theory Prime_Harmonic_Series.Squarefree_Nat
Presenting theory Prime_Harmonic_Series.Prime_Harmonic
Presenting Ptolemys_Theorem ...
Presenting document Ptolemys_Theorem/document
Presenting document Ptolemys_Theorem/outline
Presenting theory Ptolemys_Theorem.Ptolemys_Theorem
Presenting QR_Decomposition ...
Presenting document QR_Decomposition/document
Presenting document QR_Decomposition/outline
Presenting theory QR_Decomposition.Miscellaneous_QR
Presenting theory QR_Decomposition.Projections
Presenting theory HOL-Analysis.Improper_Integral
Presenting theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
Presenting theory QR_Decomposition.Gram_Schmidt
Presenting theory HOL-Analysis.Continuous_Extension
Presenting theory QR_Decomposition.QR_Decomposition
Presenting theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
Presenting theory Poincare_Bendixson.Poincare_Bendixson
Presenting theory QR_Decomposition.Least_Squares_Approximation
Presenting theory HOL-Analysis.Equivalence_Measurable_On_Borel
Presenting theory HOL-ODE-Numerics.Refine_String
Presenting theory QR_Decomposition.Examples_QR_Abstract_Float
Presenting theory QR_Decomposition.Examples_QR_Abstract_Symbolic
Presenting theory QR_Decomposition.IArray_Addenda_QR
Presenting theory Poincare_Bendixson.Affine_Arithmetic_Misc
Presenting theory HOL-ODE-Numerics.Refine_Folds
Presenting theory HOL-Analysis.Embed_Measure
Presenting theory QR_Decomposition.Matrix_To_IArray_QR
Presenting theory Poincare_Bendixson.Examples
Presenting document Quaternions/document
Presenting document Quaternions/outline
Presenting theory Lorenz_Approximation.Lorenz_Approximation
Presenting theory QR_Decomposition.Gram_Schmidt_IArrays
Presenting theory HOL-ODE-Numerics.One_Step_Method
Presenting Rank_Nullity_Theorem ...
Presenting document Rank_Nullity_Theorem/document
Presenting document Rank_Nullity_Theorem/outline
Presenting theory Rank_Nullity_Theorem.Dual_Order
Presenting theory QR_Decomposition.QR_Decomposition_IArrays
Presenting theory Quaternions.Quaternions
Presenting document Safe_Distance/document
Presenting document Safe_Distance/outline
Presenting theory QR_Decomposition.Examples_QR_IArrays_Float
Presenting theory HOL-Analysis.Brouwer_Fixpoint
Presenting theory Rank_Nullity_Theorem.Mod_Type
Presenting theory QR_Decomposition.Examples_QR_IArrays_Symbolic
Presenting theory Ordinary_Differential_Equations.Flow
Presenting theory Rank_Nullity_Theorem.Miscellaneous
Presenting theory Rank_Nullity_Theorem.Fundamental_Subspaces
Presenting theory QR_Decomposition.Generalizations2
Presenting theory Safe_Distance.Safe_Distance
Presenting theory HOL-Analysis.Fashoda_Theorem
Presenting theory Differential_Dynamic_Logic.Coincidence
Presenting theory Rank_Nullity_Theorem.Dim_Formula
Presenting Smooth_Manifolds ...
Presenting document Smooth_Manifolds/document
Presenting document Smooth_Manifolds/outline
Presenting theory HOL-Analysis.Cross3
Presenting theory Differential_Dynamic_Logic.Bound_Effect
Presenting theory Ordinary_Differential_Equations.Upper_Lower_Solution
Presenting theory HOL-Analysis.Bounded_Continuous_Function
Presenting theory HOL-ODE-Numerics.Runge_Kutta
Presenting theory QR_Decomposition.QR_Efficient
Presenting Sophomores_Dream ...
Presenting document Sophomores_Dream/document
Presenting theory HOL-Analysis.Lindelof_Spaces
Presenting document Sophomores_Dream/outline
Presenting theory HOL.BNF_Greatest_Fixpoint
Presenting file "Tools/BNF/bnf_gfp_util.ML"
Presenting file "Tools/BNF/bnf_gfp_tactics.ML"
Presenting file "Tools/BNF/bnf_gfp.ML"
Presenting file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
Presenting file "Tools/BNF/bnf_gfp_rec_sugar.ML"
Presenting theory Sophomores_Dream.Sophomores_Dream
Presenting Stewart_Apollonius ...
Presenting document Stewart_Apollonius/document
Presenting document Stewart_Apollonius/outline
Presenting theory Stewart_Apollonius.Stewart_Apollonius
Presenting Tarskis_Geometry ...
Presenting document Tarskis_Geometry/document
Presenting document Tarskis_Geometry/outline
Presenting theory Tarskis_Geometry.Metric
Presenting theory Smooth_Manifolds.Analysis_More
Presenting theory Safe_Distance.Safe_Distance_Reaction
Presenting theory Tarskis_Geometry.Miscellany
Presenting theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
Presenting theory Safe_Distance.Evaluation
Presenting document Triangle/document
Presenting document Triangle/outline
Presenting theory Tarskis_Geometry.Tarski
Presenting theory Triangle.Angles
Presenting theory Triangle.Triangle
Presenting document UpDown_Scheme/document
Presenting document UpDown_Scheme/outline
Presenting theory UpDown_Scheme.Grid_Point
Presenting theory HOL-Analysis.Infinite_Products
Presenting theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
Presenting theory Smooth_Manifolds.Smooth
Presenting theory HOL-ODE-Numerics.Refine_Parallel
Presenting theory HOL-ODE-Numerics.Refine_Default
Presenting theory HOL-ODE-Numerics.Refine_Phantom
Presenting theory Smooth_Manifolds.Bump_Function
Presenting theory Tarskis_Geometry.Euclid_Tarski
Presenting theory Smooth_Manifolds.Chart
Presenting theory UpDown_Scheme.Grid
Presenting theory Smooth_Manifolds.Topological_Manifold
Presenting theory Tarskis_Geometry.Linear_Algebra2
Presenting theory Tarskis_Geometry.Action
Presenting theory UpDown_Scheme.Triangular_Function
Presenting theory UpDown_Scheme.UpDown_Scheme
Presenting theory HOL-ODE-Numerics.Refine_ScaleR2
Presenting theory Smooth_Manifolds.Differentiable_Manifold
Presenting theory UpDown_Scheme.Up
Presenting theory HOL.Conditionally_Complete_Lattices
Presenting theory HOL.Factorial
Presenting theory Ordinary_Differential_Equations.Poincare_Map
Presenting theory UpDown_Scheme.Down
Presenting theory Differential_Dynamic_Logic.Differential_Axioms
Presenting theory HOL.Binomial
Presenting theory UpDown_Scheme.Up_Down
Presenting theory HOL-Analysis.Infinite_Sum
Presenting theory Smooth_Manifolds.Partition_Of_Unity
Presenting theory UpDown_Scheme.Imperative
Presenting Virtual_Substitution ...
Presenting document Virtual_Substitution/document
Presenting document Virtual_Substitution/outline
Presenting theory HOL.Archimedean_Field
Presenting theory Differential_Dynamic_Logic.USubst
Presenting theory Ordinary_Differential_Equations.Reachability_Analysis
Presenting theory Ordinary_Differential_Equations.Flow_Congs
Presenting file "Tools/SMT/smt_real.ML"
Presenting file "Tools/SMT/z3_real.ML"
Presenting file "Tools/Argo/argo_real.ML"
Presenting theory Smooth_Manifolds.Tangent_Space
Presenting theory Tarskis_Geometry.Projective
Presenting theory HOL-Analysis.Infinite_Set_Sum
Presenting theory Ordinary_Differential_Equations.Cones
Presenting theory Ordinary_Differential_Equations.Linear_ODE
Presenting theory Ordinary_Differential_Equations.ODE_Analysis
Presenting Youngs_Inequality ...
Presenting document Youngs_Inequality/document
Presenting document Youngs_Inequality/outline
Presenting theory Smooth_Manifolds.Cotangent_Space
Presenting theory Smooth_Manifolds.Product_Manifold
Presenting theory Smooth_Manifolds.Sphere
Presenting theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
Presenting theory HOL.Topological_Spaces
Presenting theory Youngs_Inequality.Youngs
Presenting document pGCL/document
Presenting document pGCL/outline
Presenting theory Smooth_Manifolds.Projective_Space
Presenting document HOL-Auth/document
Presenting document HOL-Auth/outline
Presenting theory HOL-Auth.Message
Presenting theory HOL-Auth.Event
Presenting theory HOL.Vector_Spaces
Presenting theory pGCL.Expectations
Presenting theory HOL-Auth.Public
Presenting theory HOL-Analysis.Polytope
Presenting theory HOL-Auth.NS_Shared
Presenting theory HOL.Real_Vector_Spaces
Presenting theory HOL-Auth.Kerberos_BAN
Presenting theory HOL-Auth.Kerberos_BAN_Gets
Presenting theory HOL.Inequalities
Presenting theory pGCL.Transformers
Presenting theory HOL-Auth.KerberosIV
Presenting theory HOL-Analysis.Arcwise_Connected
Presenting theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
Presenting theory Tarskis_Geometry.Hyperbolic_Tarski
Presenting theory HOL-Auth.KerberosIV_Gets
Presenting theory pGCL.Induction
Presenting document HOL-UNITY/document
Presenting document HOL-UNITY/outline
Presenting theory HOL-UNITY.UNITY
Presenting theory HOL-UNITY.FP
Presenting theory HOL-UNITY.WFair
Presenting theory pGCL.Embedding
Presenting theory HOL-Auth.KerberosV
Presenting theory HOL-UNITY.Constrains
Presenting theory HOL-UNITY.SubstAx
Presenting theory HOL-Auth.OtwayRees
Presenting theory HOL-UNITY.Detects
Presenting theory HOL-ODE-Numerics.Refine_Reachability_Analysis
Presenting theory HOL-Auth.OtwayRees_AN
Presenting theory HOL-UNITY.Union
Presenting theory HOL-UNITY.Comp
Presenting theory HOL-Auth.OtwayRees_Bad
Presenting theory HOL-UNITY.Guar
Presenting theory HOL-Auth.OtwayReesBella
Presenting theory HOL-UNITY.Extend
Presenting theory HOL-Analysis.Retracts
Presenting theory HOL-Auth.WooLam
Presenting theory HOL-Auth.Recur
Presenting theory HOL-UNITY.Rename
Presenting theory HOL-Auth.Yahalom
Presenting theory pGCL.Healthiness
Presenting theory HOL-Auth.Yahalom2
Presenting theory HOL-UNITY.Lift_prog
Presenting theory HOL-Auth.Yahalom_Bad
Presenting theory HOL-UNITY.PPROD
Presenting theory HOL.Transcendental
Presenting theory HOL-Auth.ZhouGollmann
Presenting theory HOL-Auth.Auth_Shared
Presenting theory HOL-UNITY.ListOrder
Presenting theory HOL-Auth.NS_Public_Bad
Presenting theory HOL-Auth.NS_Public
Presenting theory HOL-UNITY.Follows
Presenting theory HOL-Auth.TLS
Presenting theory HOL-UNITY.Transformers
Presenting theory pGCL.Continuity
Presenting theory HOL-Auth.CertifiedEmail
Presenting theory HOL-Auth.Auth_Public
Presenting theory HOL-Analysis.Further_Topology
Presenting theory HOL-UNITY.ProgressSets
Presenting theory HOL-Auth.EventSC
Presenting theory HOL-Auth.All_Symmetric
Presenting theory Differential_Dynamic_Logic.USubst_Lemma
Presenting theory HOL-UNITY.UNITY_Main
Presenting file "UNITY_tactics.ML"
Presenting theory HOL-UNITY.Deadlock
Presenting theory HOL-UNITY.Common
Presenting theory HOL-Auth.Smartcard
Presenting theory HOL-UNITY.Network
Presenting theory HOL-UNITY.Token
Presenting theory HOL-UNITY.Channel
Presenting theory pGCL.LoopInduction
Presenting theory HOL-Analysis.Jordan_Curve
Presenting theory HOL-Analysis.Poly_Roots
Presenting theory HOL.MacLaurin
Presenting theory HOL-Analysis.Generalised_Binomial_Theorem
Presenting theory HOL-UNITY.Lift
Presenting theory Complex_Main
Presenting document HOL-Bali/document
Presenting document HOL-Bali/outline
Presenting theory HOL-UNITY.Mutex
Presenting theory HOL-Bali.Basis
Presenting theory HOL-Bali.Name
Presenting theory HOL-Bali.Type
Presenting theory HOL-Bali.Value
Presenting theory HOL-UNITY.Reach
Presenting theory Virtual_Substitution.QE
Presenting theory HOL-Analysis.Vitali_Covering_Theorem
Presenting theory HOL-UNITY.Reachability
Presenting theory HOL-Bali.Table
Presenting theory HOL-Auth.ShoupRubin
Presenting theory pGCL.Sublinearity
Presenting theory HOL-UNITY.NSP_Bad
Presenting theory HOL-UNITY.Handshake
Presenting theory HOL-Bali.Term
Presenting theory HOL-UNITY.Counter
Presenting theory HOL-UNITY.Counterc
Presenting theory HOL-Bali.Decl
Presenting theory HOL-UNITY.PriorityAux
Presenting theory HOL-UNITY.Priority
Presenting theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
Presenting theory HOL-UNITY.TimerArray
Presenting theory HOL-Bali.TypeRel
Presenting theory HOL-UNITY.Progress
Presenting theory Virtual_Substitution.MPolyExtension
Presenting theory HOL-UNITY.AllocBase
Presenting theory Differential_Dynamic_Logic.Uniform_Renaming
Presenting theory HOL-Auth.ShoupRubinBella
Presenting theory HOL-Auth.Auth_Smartcard
Presenting theory Differential_Dynamic_Logic.Pretty_Printer
Presenting theory HOL-Auth.Extensions
Presenting theory HOL-Auth.Analz
Presenting theory Virtual_Substitution.ExecutiblePolyProps
Presenting theory HOL-Bali.DeclConcepts
Presenting theory HOL-UNITY.Alloc
Presenting theory pGCL.WellDefined
Presenting theory HOL-Analysis.Change_Of_Vars
Presenting theory HOL-Auth.Guard
Presenting theory Virtual_Substitution.PolyAtoms
Presenting theory HOL-Auth.GuardK
Presenting theory HOL-ODE-Numerics.Init_ODE_Solver
Presenting theory HOL-Auth.Shared
Presenting theory HOL-UNITY.AllocImpl
Presenting theory HOL-Auth.Guard_Shared
Presenting theory HOL-UNITY.Client
Presenting theory HOL-Auth.Guard_OtwayRees
Presenting theory HOL-Analysis.Lipschitz
Presenting theory HOL-Bali.WellType
Presenting theory HOL-Auth.Guard_Yahalom
Presenting theory HOL-Auth.Auth_Guard_Shared
Presenting theory HOL-Analysis.Multivariate_Analysis
Presenting theory HOL-Auth.Guard_Public
Presenting theory HOL-Auth.List_Msg
Presenting theory HOL-Analysis.Simplex_Content
Presenting theory HOL-UNITY.Project
Presenting theory HOL-Analysis.FPS_Convergence
Presenting theory Virtual_Substitution.Debruijn
Presenting theory HOL-Analysis.Smooth_Paths
Presenting theory HOL-Analysis.Locally
Presenting theory HOL-UNITY.ELT
Presenting document HOL-Cardinals/document
Presenting document HOL-Cardinals/outline
Presenting theory HOL-Cardinals.Fun_More
Presenting theory HOL-Analysis.Abstract_Euclidean_Space
Presenting theory Virtual_Substitution.Reindex
Presenting theory pGCL.Algebra
Presenting theory HOL-Bali.DefiniteAssignment
Presenting theory HOL-Analysis.Function_Metric
Presenting theory HOL-Analysis.Analysis
Presenting Binding_Syntax_Theory ...
Presenting document Binding_Syntax_Theory/document
Presenting document Binding_Syntax_Theory/outline
Presenting theory HOL-Cardinals.Order_Relation_More
Presenting theory Binding_Syntax_Theory.Preliminaries
Presenting theory HOL-Cardinals.Wellfounded_More
Presenting theory Virtual_Substitution.Optimizations
Presenting theory pGCL.StructuredReasoning
Presenting theory pGCL.Automation
Presenting theory Binding_Syntax_Theory.QuasiTerms_Swap_Fresh
Presenting theory HOL-Auth.Guard_NS_Public
Presenting theory HOL-Cardinals.Wellorder_Relation
Presenting theory pGCL.Determinism
Presenting theory HOL-Cardinals.Wellorder_Embedding
Presenting theory Virtual_Substitution.OptimizationProofs
Presenting theory HOL-Cardinals.Order_Union
Presenting theory pGCL.Termination
Presenting theory HOL-Auth.Proto
Presenting theory HOL-Auth.Auth_Guard_Public
Presenting Ordinals_and_Cardinals ...
Presenting document Ordinals_and_Cardinals/document
Presenting document Ordinals_and_Cardinals/outline
Presenting theory Ordinals_and_Cardinals.Cardinal_Order_Relation_discontinued
Presenting document Sort_Encodings/document
Presenting document Sort_Encodings/outline
Presenting theory pGCL.Primitives
Presenting theory pGCL.LoopExamples
Presenting HOL-Combinatorics ...
Presenting document HOL-Combinatorics/document
Presenting document HOL-Combinatorics/outline
Presenting theory Sort_Encodings.Preliminaries
Presenting theory HOL-Combinatorics.Transposition
Presenting theory Sort_Encodings.TermsAndClauses
Presenting theory Sort_Encodings.Sig
Presenting theory HOL-Combinatorics.Stirling
Presenting theory Virtual_Substitution.VSAlgos
Presenting theory Differential_Dynamic_Logic.Proof_Checker
Presenting theory Binding_Syntax_Theory.QuasiTerms_PickFresh_Alpha
Presenting theory Sort_Encodings.M
Presenting theory Sort_Encodings.CM
Presenting theory Differential_Dynamic_Logic.Differential_Dynamic_Logic
Presenting document Blue_Eyes/document
Presenting document Blue_Eyes/outline
Presenting theory Blue_Eyes.Blue_Eyes
Presenting Gauss-Jordan-Elim-Fun ...
Presenting document Gauss-Jordan-Elim-Fun/document
Presenting document Gauss-Jordan-Elim-Fun/outline
Presenting theory Virtual_Substitution.Heuristic
Presenting theory HOL-Bali.WellForm
Presenting theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun
Presenting HOL-Data_Structures ...
Presenting theory Sort_Encodings.Mono
Presenting document HOL-Data_Structures/document
Presenting theory HOL-Data_Structures.Less_False
Presenting theory HOL-Cardinals.Wellorder_Constructions
Presenting theory HOL-Data_Structures.Sorting
Presenting theory Virtual_Substitution.PrettyPrinting
Presenting theory Sort_Encodings.Mcalc
Presenting theory HOL-Data_Structures.Balance
Presenting theory Sort_Encodings.T_G_Prelim
Presenting theory HOL-Data_Structures.Cmp
Presenting theory HOL-Data_Structures.Sorted_Less
Presenting theory HOL-Data_Structures.List_Ins_Del
Presenting theory Virtual_Substitution.Exports
Presenting theory HOL-Data_Structures.Set_Specs
Presenting theory HOL-Data_Structures.Tree_Set
Presenting theory Sort_Encodings.Mcalc2
Presenting theory HOL-Data_Structures.AList_Upd_Del
Presenting theory HOL-Data_Structures.Map_Specs
Presenting theory HOL-Data_Structures.Tree_Map
Presenting theory HOL-Data_Structures.Tree2
Presenting theory HOL-Data_Structures.Isin2
Presenting theory HOL-Bali.State
Presenting theory HOL-Data_Structures.Interval_Tree
Presenting theory HOL-Data_Structures.AVL_Set_Code
Presenting theory Virtual_Substitution.LinearCase
Presenting theory HOL-Data_Structures.AVL_Set
Presenting theory HOL-Data_Structures.Lookup2
Presenting theory Sort_Encodings.Mcalc2C
Presenting theory HOL-Data_Structures.AVL_Map
Presenting theory HOL-Data_Structures.AVL_Bal_Set
Presenting theory HOL-Combinatorics.Permutations
Presenting theory HOL-Data_Structures.AVL_Bal2_Set
Presenting theory HOL-Combinatorics.List_Permutation
Presenting theory HOL-ODE-Numerics.Example_Utilities
Presenting theory HOL-Data_Structures.Height_Balanced_Tree
Presenting theory HOL-Data_Structures.RBT
Presenting theory HOL-ODE-Numerics.ODE_Numerics
Presenting theory Binding_Syntax_Theory.QuasiTerms_Environments_Substitution
Presenting theory HOL-Bali.Eval
Presenting theory Binding_Syntax_Theory.Pick
Presenting theory HOL-Data_Structures.RBT_Set
Presenting theory HOL-Data_Structures.RBT_Set2
Presenting theory HOL-Combinatorics.Multiset_Permutations
Presenting theory HOL-Data_Structures.RBT_Map
Presenting theory HOL-Data_Structures.Tree23
Presenting theory HOL-Cardinals.Ordinal_Arithmetic
Presenting theory Binding_Syntax_Theory.Equiv_Relation2
Presenting theory HOL-Data_Structures.Tree23_Set
Presenting theory HOL-Data_Structures.Tree23_Map
Presenting theory Sort_Encodings.G
Presenting theory HOL-Data_Structures.Tree23_of_List
Presenting theory HOL-Combinatorics.Cycles
Presenting theory HOL-Data_Structures.Tree234
Presenting theory HOL-Combinatorics.Perm
Presenting theory HOL-Data_Structures.Tree234_Set
Presenting theory Sort_Encodings.T
Presenting theory Sort_Encodings.U
Presenting theory Sort_Encodings.CU
Presenting theory HOL-Combinatorics.Orbits
Presenting theory HOL-Combinatorics.Combinatorics
Presenting document Optics/document
Presenting document Optics/outline
Presenting theory Optics.Interp
Presenting theory HOL-Data_Structures.Tree234_Map
Presenting theory Virtual_Substitution.QuadraticCase
Presenting theory Sort_Encodings.E
Presenting theory HOL-Cardinals.Cardinal_Order_Relation
Presenting theory Optics.Lens_Laws
Presenting theory Binding_Syntax_Theory.Transition_QuasiTerms_Terms
Presenting theory Sort_Encodings.Encodings
Presenting theory HOL-Cardinals.Cardinal_Arithmetic
Presenting theory Optics.Lens_Algebra
Presenting document HOL-Examples/document
Presenting document HOL-Examples/outline
Presenting theory HOL-Data_Structures.Brother12_Set
Presenting theory HOL-Examples.Adhoc_Overloading_Examples
Presenting theory HOL-Examples.Ackermann
Presenting theory HOL-Examples.Cantor
Presenting theory HOL-Examples.Coherent
Presenting theory HOL-Examples.Commands
Presenting theory HOL-Examples.Drinker
Presenting theory HOL-Cardinals.Wellorder_Extension
Presenting theory HOL-Data_Structures.Brother12_Map
Presenting theory HOL-Cardinals.Cardinals
Presenting theory Optics.Lens_Order
Presenting theory Optics.Lens_Symmetric
Presenting theory HOL-Bali.DefiniteAssignmentCorrect
Presenting theory HOL-Examples.Functions
Presenting theory HOL-Examples.Groebner_Examples
Presenting theory HOL-Examples.Iff_Oracle
Presenting theory HOL-Examples.Induction_Schema
Presenting theory HOL-Examples.Knaster_Tarski
Presenting theory HOL-Cardinals.Bounded_Set
Presenting theory HOL-Examples.ML
Presenting HOL-Hahn_Banach ...
Presenting document HOL-Hahn_Banach/document
Presenting document HOL-Hahn_Banach/outline
Presenting theory HOL-Examples.Peirce
Presenting theory HOL-Hahn_Banach.Bounds
Presenting theory HOL-Examples.Records
Presenting theory HOL-Data_Structures.AA_Set
Presenting theory HOL-Hahn_Banach.Vector_Space
Presenting theory HOL-Examples.Rewrite_Examples
Presenting theory HOL-Examples.Seq
Presenting theory HOL-Data_Structures.AA_Map
Presenting theory HOL-Bali.Conform
Presenting theory HOL-Examples.Sqrt
Presenting document HOL-Hoare/document
Presenting document HOL-Hoare/outline
Presenting theory HOL-Data_Structures.Set2_Join
Presenting theory Optics.Lens_Instances
Presenting file "Lens_Record.ML"
Presenting file "Lens_Statespace.ML"
Presenting theory Virtual_Substitution.EliminateVariable
Presenting theory Optics.Lenses
Presenting theory HOL-Hoare.Hoare_Syntax
Presenting file "hoare_syntax.ML"
Presenting theory HOL-Hahn_Banach.Subspace
Presenting theory Optics.Prisms
Presenting file "Prism_Lib.ML"
Presenting theory HOL-Data_Structures.Set2_Join_RBT
Presenting theory HOL-Data_Structures.Array_Specs
Presenting theory HOL-Hahn_Banach.Normed_Space
Presenting theory HOL-Hoare.Hoare_Tac
Presenting file "hoare_tac.ML"
Presenting theory HOL-Data_Structures.Braun_Tree
Presenting theory HOL-Hahn_Banach.Linearform
Presenting theory Virtual_Substitution.LuckyFind
Presenting theory Optics.Channel_Type
Presenting file "Channel_Type.ML"
Presenting theory HOL-Hoare.Hoare_Logic
Presenting theory HOL-Eisbach.Eisbach
Presenting file "parse_tools.ML"
Presenting file "method_closure.ML"
Presenting file "eisbach_rule_insts.ML"
Presenting file "match_method.ML"
Presenting theory HOL-Hoare.Arith2
Presenting theory HOL-Hahn_Banach.Function_Order
Presenting theory HOL-Data_Structures.Array_Braun
Presenting theory HOL-Data_Structures.Trie_Fun
Presenting theory HOL-Eisbach.Eisbach_Tools
Presenting theory HOL-Data_Structures.Trie_Map
Presenting theory HOL-Data_Structures.Tries_Binary
Presenting theory HOL-Data_Structures.Queue_Spec
Presenting theory HOL-Data_Structures.Reverse
Presenting theory HOL-Hahn_Banach.Function_Norm
Presenting theory Optics.Dataspace
Presenting file "Dataspace.ML"
Presenting theory HOL-Data_Structures.Queue_2Lists
Presenting theory HOL-Data_Structures.Priority_Queue_Specs
Presenting theory HOL-Hahn_Banach.Zorn_Lemma
Presenting theory HOL-Data_Structures.Heaps
Presenting theory HOL-Hoare.Examples
Presenting theory HOL-Data_Structures.Leftist_Heap
Presenting theory Virtual_Substitution.EqualityVS
Presenting theory HOL-Hoare.Hoare_Logic_Abort
Presenting theory HOL-Data_Structures.Binomial_Heap
Presenting theory HOL-Hoare.ExamplesAbort
Presenting theory Optics.Scenes
Presenting theory HOL-Hoare.ExamplesTC
Presenting theory Optics.Optics
Presenting theory HOL-Data_Structures.Time_Funs
Presenting theory Binding_Syntax_Theory.Terms
Presenting theory Optics.Lens_Record_Example
Presenting theory HOL-Eisbach.Tests
Presenting theory Optics.Lens_State
Presenting HOL-Hoare_Parallel ...
Presenting document HOL-Hoare_Parallel/document
Presenting document HOL-Hoare_Parallel/outline
Presenting theory HOL-Hoare_Parallel.OG_Com
Presenting theory Virtual_Substitution.UniAtoms
Presenting theory HOL-Hoare.Pointers0
Presenting theory HOL-Hahn_Banach.Hahn_Banach_Sup_Lemmas
Presenting theory HOL-Eisbach.Examples
Presenting theory HOL-Hoare.Heap
Presenting theory HOL-Eisbach.Eisbach_Old_Appl_Syntax
Presenting theory HOL-Hoare.HeapSyntax
Presenting theory Virtual_Substitution.NegInfinity
Presenting theory HOL-Eisbach.Examples_FOL
Presenting theory HOL-Hoare_Parallel.OG_Tran
Presenting theory HOL-Eisbach.Example_Metric
Presenting theory HOL-Hahn_Banach.Hahn_Banach_Ext_Lemmas
Presenting theory HOL-Bali.TypeSafe
Presenting theory HOL-Hahn_Banach.Hahn_Banach_Lemmas
Presenting theory HOL-IMPP.Com
Presenting theory Virtual_Substitution.NegInfinityUni
Presenting theory HOL-Hoare.Pointer_Examples
Presenting theory HOL-Hoare.HeapSyntaxAbort
Presenting theory HOL-Data_Structures.Selection
Presenting theory HOL-Hoare.Pointer_ExamplesAbort
Presenting theory HOL-IMPP.Natural
Presenting theory Virtual_Substitution.Infinitesimals
Presenting theory HOL-IOA.Asig
Presenting theory HOL-Hoare_Parallel.OG_Hoare
Presenting theory HOL-Hahn_Banach.Hahn_Banach
Presenting HOL-Imperative_HOL ...
Presenting document HOL-Imperative_HOL/document
Presenting document HOL-Imperative_HOL/outline
Presenting theory HOL-Imperative_HOL.Heap
Presenting theory HOL-IMPP.Hoare
Presenting theory HOL-Bali.Evaln
Presenting theory HOL-IMPP.Misc
Presenting theory Virtual_Substitution.InfinitesimalsUni
Presenting theory HOL-Hoare_Parallel.OG_Tactics
Presenting theory HOL-IMPP.EvenOdd
Presenting Imperative_Insertion_Sort ...
Presenting document Imperative_Insertion_Sort/document
Presenting document Imperative_Insertion_Sort/outline
Presenting theory HOL-IOA.Solve
Presenting theory HOL-Hoare_Parallel.Quote_Antiquote
Presenting theory HOL-Imperative_HOL.Heap_Monad
Presenting theory Virtual_Substitution.DNFUni
Presenting theory HOL-Hoare_Parallel.OG_Syntax
Presenting theory HOL-Hoare.SchorrWaite
Presenting theory Imperative_Insertion_Sort.Imperative_Loops
Presenting theory HOL-Hoare.SepLogHeap
Presenting theory HOL-Hoare.Separation
Presenting document HOL-Induct/document
Presenting document HOL-Induct/outline
Presenting theory HOL-Induct.Common_Patterns
Presenting theory HOL-Hoare_Parallel.OG_Examples
Presenting theory HOL-Induct.Nested_Datatype
Presenting theory HOL-Imperative_HOL.Array
Presenting theory HOL-Bali.AxSem
Presenting theory HOL-Import.Import_Setup
Presenting file "import_data.ML"
Presenting file "import_rule.ML"
Presenting theory HOL-Hoare_Parallel.Graph
Presenting theory HOL-Import.HOL_Light_Maps
Presenting theory HOL-Induct.QuoDataType
Presenting document HOL-Lattice/document
Presenting document HOL-Lattice/outline
Presenting theory Imperative_Insertion_Sort.Imperative_Insertion_Sort
Presenting theory HOL-Lattice.Orders
Presenting theory HOL-Imperative_HOL.Ref
Presenting theory HOL-Imperative_HOL.Imperative_HOL
Presenting theory HOL-Induct.QuoNestedDataType
Presenting theory HOL-Imperative_HOL.Overview
Presenting theory HOL-Induct.Term
Presenting document HOL-Library/document
Presenting document HOL-Library/outline
Presenting theory HOL-Lattice.Bounds
Presenting theory HOL-Induct.Sexp
Presenting theory Virtual_Substitution.GeneralVSProofs
Presenting theory HOL-Bali.Example
Presenting theory HOL-Induct.SList
Presenting theory HOL-Hoare_Parallel.Gar_Coll
Presenting theory HOL-Induct.ABexp
Presenting theory HOL-Imperative_HOL.List_Sublist
Presenting theory HOL-Bali.AxExample
Presenting theory HOL-Induct.Infinitely_Branching_Tree
Presenting theory HOL-Lattice.Lattice
Presenting theory HOL-Imperative_HOL.Subarray
Presenting theory HOL-Induct.Ordinals
Presenting theory HOL-Induct.Sigma_Algebra
Presenting theory HOL-Induct.Comb
Presenting theory HOL-Lattice.CompleteLattice
Presenting document ADS_Functor/document
Presenting document ADS_Functor/outline
Presenting theory HOL-Induct.PropLog
Presenting theory ADS_Functor.Merkle_Interface
Presenting theory Virtual_Substitution.DNF
Presenting theory HOL-Induct.Com
Presenting Abs_Int_ITP2012 ...
Presenting document Abs_Int_ITP2012/document
Presenting document Abs_Int_ITP2012/outline
Presenting theory Abs_Int_ITP2012.Complete_Lattice_ix
Presenting theory HOL-Imperative_HOL.Imperative_Quicksort
Presenting theory HOL-Library.AList
Presenting theory Binding_Syntax_Theory.Well_Sorted_Terms
Presenting theory HOL-Imperative_HOL.Imperative_Reverse
Presenting theory Abs_Int_ITP2012.ACom
Presenting theory HOL-Hoare_Parallel.Mul_Gar_Coll
Presenting theory HOL-Library.Adhoc_Overloading
Presenting file "adhoc_overloading.ML"
Presenting theory Abs_Int_ITP2012.Collecting
Presenting theory HOL-Hoare_Parallel.RG_Com
Presenting theory HOL-Library.Function_Algebras
Presenting theory Virtual_Substitution.VSQuad
Presenting theory HOL-Library.Set_Algebras
Presenting theory HOL-Bali.AxSound
Presenting theory Abs_Int_ITP2012.Abs_Int0
Presenting theory Abs_Int_ITP2012.Abs_State
Presenting theory HOL-Library.BigO
Presenting theory ADS_Functor.ADS_Construction
Presenting theory HOL-Library.BNF_Axiomatization
Presenting file "$ISABELLE_HOME/src/HOL/Tools/BNF/bnf_axiomatization.ML"
Presenting theory Abs_Int_ITP2012.Abs_Int1
Presenting theory Virtual_Substitution.HeuristicProofs
Presenting theory HOL-Hoare_Parallel.RG_Tran
Presenting theory Virtual_Substitution.ExportProofs
Presenting Abstract-Rewriting ...
Presenting document Abstract-Rewriting/document
Presenting document Abstract-Rewriting/outline
Presenting theory Abs_Int_ITP2012.Abs_Int2
Presenting theory HOL-Bali.AxCompl
Presenting theory Abs_Int_ITP2012.Abs_Int2_ivl
Presenting theory HOL-Imperative_HOL.Linked_Lists
Presenting theory Abstract-Rewriting.Seq
Presenting theory HOL-Imperative_HOL.Sorted_List
Presenting theory HOL-Bali.Trans
Presenting theory ADS_Functor.Generic_ADS_Construction
Presenting Decreasing-Diagrams ...
Presenting document Decreasing-Diagrams/document
Presenting document Decreasing-Diagrams/outline
Presenting theory ADS_Functor.Inclusion_Proof_Construction
Presenting theory ADS_Functor.Canton_Transaction_Tree
Presenting theory HOL-Imperative_HOL.SatChecker
Presenting theory Abs_Int_ITP2012.Abs_Int3
Presenting Decreasing-Diagrams-II ...
Presenting document Decreasing-Diagrams-II/document
Presenting document Decreasing-Diagrams-II/outline
Presenting theory HOL-Imperative_HOL.Imperative_HOL_ex
Presenting First_Order_Terms ...
Presenting document First_Order_Terms/document
Presenting document First_Order_Terms/outline
Presenting theory First_Order_Terms.Transitive_Closure_More
Presenting theory First_Order_Terms.Seq_More
Presenting theory Decreasing-Diagrams-II.Decreasing_Diagrams_II_Aux
Presenting theory First_Order_Terms.Fun_More
Presenting theory Abs_Int_ITP2012.Abs_Int1_const
Presenting theory First_Order_Terms.Option_Monad
Presenting theory Abs_Int_ITP2012.Abs_Int1_parity
Presenting Knuth_Bendix_Order ...
Presenting document Knuth_Bendix_Order/document
Presenting document Knuth_Bendix_Order/outline
Presenting theory Knuth_Bendix_Order.Order_Pair
Presenting theory HOL-Hoare_Parallel.RG_Hoare
Presenting theory HOL-Hoare_Parallel.RG_Syntax
Presenting theory First_Order_Terms.Term
Presenting theory Decreasing-Diagrams-II.Decreasing_Diagrams_II
Presenting theory HOL-Hoare_Parallel.RG_Examples
Presenting theory HOL-Hoare_Parallel.Hoare_Parallel
Presenting Weighted_Path_Order ...
Presenting document Weighted_Path_Order/document
Presenting document Weighted_Path_Order/outline
Presenting Multiset_Ordering_NPC ...
Presenting document Multiset_Ordering_NPC/document
Presenting document Multiset_Ordering_NPC/outline
Presenting theory First_Order_Terms.Term_Pair_Multiset
Presenting theory Weighted_Path_Order.Status
Presenting theory Weighted_Path_Order.Precedence
Presenting theory Knuth_Bendix_Order.Lexicographic_Extension
Presenting theory Weighted_Path_Order.Relations
Presenting theory Weighted_Path_Order.List_Order
Presenting theory Multiset_Ordering_NPC.Multiset_Ordering_More
Presenting theory Knuth_Bendix_Order.Subterm_and_Context
Presenting theory Knuth_Bendix_Order.Term_Aux
Presenting theory Multiset_Ordering_NPC.Propositional_Formula
Presenting theory First_Order_Terms.Abstract_Matching
Presenting theory Weighted_Path_Order.Multiset_Extension_Pair
Presenting theory Abstract-Rewriting.Abstract_Rewriting
Presenting theory First_Order_Terms.Unifiers
Presenting theory Weighted_Path_Order.Multiset_Extension_Pair_Impl
Presenting theory Knuth_Bendix_Order.KBO
Presenting Stateful_Protocol_Composition_and_Typing ...
Presenting document Stateful_Protocol_Composition_and_Typing/document
Presenting document Stateful_Protocol_Composition_and_Typing/outline
Presenting theory Weighted_Path_Order.Multiset_Extension2
Presenting theory Decreasing-Diagrams.Decreasing_Diagrams
Presenting theory First_Order_Terms.Abstract_Unification
Presenting Automated_Stateful_Protocol_Verification ...
Presenting document Automated_Stateful_Protocol_Verification/document
Presenting document Automated_Stateful_Protocol_Verification/outline
Presenting theory Weighted_Path_Order.Multiset_Extension2_Impl
Presenting theory Stateful_Protocol_Composition_and_Typing.Miscellaneous
Presenting theory Multiset_Ordering_NPC.Multiset_Ordering_in_NP
Presenting theory Abstract-Rewriting.Relative_Rewriting
Presenting theory First_Order_Terms.Unification
Presenting theory Stateful_Protocol_Composition_and_Typing.Messages
Presenting theory Abstract-Rewriting.SN_Orders
Presenting theory Automated_Stateful_Protocol_Verification.Transactions
Presenting theory First_Order_Terms.Matching
Presenting theory Automated_Stateful_Protocol_Verification.Term_Abstraction
Presenting theory Abstract-Rewriting.SN_Order_Carrier
Presenting document Matrix/document
Presenting document Matrix/outline
Presenting theory Multiset_Ordering_NPC.Multiset_Ordering_NP_Hard
Presenting theory First_Order_Terms.Subsumption
Presenting document Matrix_Tensor/document
Presenting document Matrix_Tensor/outline
Presenting theory Matrix.Utility
Presenting theory Weighted_Path_Order.WPO
Presenting theory Matrix.Ordered_Semiring
Presenting theory Binding_Syntax_Theory.Iteration
Presenting theory Weighted_Path_Order.RPO
Presenting theory Weighted_Path_Order.LPO
Presenting theory Multiset_Ordering_NPC.RPO_NP_Hard
Presenting theory Weighted_Path_Order.KBO_Transformation
Presenting document Knot_Theory/document
Presenting document Knot_Theory/outline
Presenting theory Knot_Theory.Preliminaries
Presenting theory Knot_Theory.Tangles
Presenting theory Matrix.Matrix_Legacy
Presenting theory Weighted_Path_Order.KBO_as_WPO
Presenting theory Weighted_Path_Order.Executable_Orders
Presenting Minsky_Machines ...
Presenting document Minsky_Machines/document
Presenting document Minsky_Machines/outline
Presenting document Polynomials/document
Presenting document Polynomials/outline
Presenting theory Minsky_Machines.Recursive_Inseparability
Presenting theory Polynomials.Utils
Presenting theory Binding_Syntax_Theory.Semantic_Domains
Presenting theory Polynomials.MPoly_Type
Presenting theory Minsky_Machines.Minsky
Presenting Abstract_Completeness ...
Presenting document Abstract_Completeness/document
Presenting document Abstract_Completeness/outline
Presenting theory Abstract_Completeness.Abstract_Completeness
Presenting theory Knot_Theory.Tangle_Algebra
Presenting theory Knot_Theory.Tangle_Relation
Presenting theory Abstract_Completeness.Propositional_Logic
Presenting theory Polynomials.More_MPoly_Type
Presenting Abstract_Soundness ...
Presenting document Abstract_Soundness/document
Presenting document Abstract_Soundness/outline
Presenting theory Abstract_Soundness.Finite_Proof_Soundness
Presenting theory Knot_Theory.Tangle_Moves
Presenting theory Stateful_Protocol_Composition_and_Typing.More_Unification
Presenting theory Matrix_Tensor.Matrix_Tensor
Presenting theory Abstract_Soundness.Infinite_Proof_Soundness
Presenting theory Knot_Theory.Link_Algebra
Presenting Amortized_Complexity ...
Presenting document Amortized_Complexity/document
Presenting document Amortized_Complexity/outline
Presenting document Dynamic_Tables/document
Presenting document Dynamic_Tables/outline
Presenting theory Amortized_Complexity.Amortized_Framework0
Presenting theory Dynamic_Tables.Tables_real
Presenting theory Amortized_Complexity.Amortized_Framework
Presenting theory Dynamic_Tables.Tables_nat
Presenting Bell_Numbers_Spivey ...
Presenting document Bell_Numbers_Spivey/document
Presenting document Bell_Numbers_Spivey/outline
Presenting theory Polynomials.Power_Products
Presenting theory Knot_Theory.Example
Presenting theory Bell_Numbers_Spivey.Bell_Numbers
Presenting Card_Equiv_Relations ...
Presenting document Card_Equiv_Relations/document
Presenting document Card_Equiv_Relations/outline
Presenting theory Stateful_Protocol_Composition_and_Typing.Intruder_Deduction
Presenting theory Amortized_Complexity.Amortized_Examples
Presenting theory Amortized_Complexity.Priority_Queue_ops_merge
Presenting theory Card_Equiv_Relations.Card_Equiv_Relations
Presenting theory Card_Equiv_Relations.Card_Partial_Equiv_Relations
Presenting document Binomial-Heaps/document
Presenting document Binomial-Heaps/outline
Presenting theory Amortized_Complexity.Skew_Heap_Analysis
Presenting theory Amortized_Complexity.Lemmas_log
Presenting theory Binding_Syntax_Theory.Recursion
Presenting theory Amortized_Complexity.Splay_Tree_Analysis_Base
Presenting theory Polynomials.More_Modules
Presenting Boolean_Expression_Checkers ...
Presenting document Boolean_Expression_Checkers/document
Presenting document Boolean_Expression_Checkers/outline
Presenting theory Binomial-Heaps.BinomialHeap
Presenting theory Amortized_Complexity.Splay_Tree_Analysis
Presenting theory Boolean_Expression_Checkers.Boolean_Expression_Checkers
Presenting theory Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping
Presenting theory Boolean_Expression_Checkers.Boolean_Expression_Example
Presenting document Buildings/document
Presenting document Buildings/outline
Presenting theory Amortized_Complexity.Splay_Tree_Analysis_Optimal
Presenting theory Amortized_Complexity.Priority_Queue_ops
Presenting theory Amortized_Complexity.Splay_Heap_Analysis
Presenting theory Binomial-Heaps.SkewBinomialHeap
Presenting theory Binomial-Heaps.Test
Presenting Card_Number_Partitions ...
Presenting document Card_Number_Partitions/document
Presenting document Card_Number_Partitions/outline
Presenting theory Card_Number_Partitions.Additions_to_Main
Presenting theory Amortized_Complexity.Pairing_Heap_Tree_Analysis
Presenting theory Card_Number_Partitions.Number_Partition
Presenting theory Card_Number_Partitions.Card_Number_Partitions
Presenting document Category2/document
Presenting document Category2/outline
Presenting theory Buildings.Prelim
Presenting theory Amortized_Complexity.Pairing_Heap_Tree_Analysis2
Presenting theory Category2.Category
Presenting theory Category2.Universe
Presenting theory Amortized_Complexity.Pairing_Heap_List1_Analysis
Presenting theory Amortized_Complexity.Pairing_Heap_List1_Analysis2
Presenting theory Stateful_Protocol_Composition_and_Typing.Strands_and_Constraints
Presenting theory Polynomials.MPoly_Type_Class
Presenting theory Knot_Theory.Kauffman_Matrix
Presenting theory Amortized_Complexity.Pairing_Heap_List2_Analysis
Presenting document Category3/document
Presenting document Category3/outline
Presenting theory Category2.MonadicEquationalTheory
Presenting theory Category3.Category
Presenting theory Category3.DualCategory
Presenting theory Category2.Functors
Presenting theory Category3.ConcreteCategory
Presenting theory Category3.EpiMonoIso
Presenting theory Category3.InitialTerminal
Presenting theory Category2.NatTrans
Presenting theory Stateful_Protocol_Composition_and_Typing.Lazy_Intruder
Presenting theory Category2.SetCat
Presenting theory Buildings.Algebra
Presenting theory Knot_Theory.Computations
Presenting theory Category3.Functor
Presenting theory Category3.Subcategory
Presenting theory Category2.Yoneda
Presenting theory Knot_Theory.Linkrel_Kauffman
Presenting theory Buildings.Simplicial
Presenting MonoidalCategory ...
Presenting document MonoidalCategory/document
Presenting theory Knot_Theory.Kauffman_Invariance
Presenting document MonoidalCategory/outline
Presenting theory Knot_Theory.Knot_Theory
Presenting Combinatorics_Words ...
Presenting document Combinatorics_Words/document
Presenting document Combinatorics_Words/manual
Presenting theory Combinatorics_Words.Arithmetical_Hints
Presenting theory HOL-Library.BNF_Corec
Presenting file "$ISABELLE_HOME/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML"
Presenting file "$ISABELLE_HOME/src/HOL/Tools/BNF/bnf_gfp_grec.ML"
Presenting file "$ISABELLE_HOME/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML"
Presenting file "$ISABELLE_HOME/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML"
Presenting file "$ISABELLE_HOME/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML"
Presenting file "$ISABELLE_HOME/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
Presenting theory Combinatorics_Words.Reverse_Symmetry
Presenting theory Polynomials.MPoly_Type_Class_Ordered
Presenting theory HOL-Library.While_Combinator
Presenting theory Polynomials.Poly_Mapping_Finite_Map
Presenting theory MonoidalCategory.MonoidalCategory
Presenting theory HOL-Library.Bourbaki_Witt_Fixpoint
Presenting theory HOL-Library.Char_ord
Presenting theory HOL-Library.Phantom_Type
Presenting theory Polynomials.MPoly_Type_Class_FMap
Presenting theory Polynomials.PP_Type
Presenting theory Category3.SetCategory
Presenting theory HOL-Library.Cardinality
Presenting theory MonoidalCategory.MonoidalFunctor
Presenting theory HOL-Library.Code_Cardinality
Presenting theory Combinatorics_Words.CoWBasic
Presenting theory Buildings.Chamber
Presenting theory HOL-Library.Case_Converter
Presenting file "case_converter.ML"
Presenting theory Combinatorics_Words.Submonoids
Presenting theory Stateful_Protocol_Composition_and_Typing.Typed_Model
Presenting theory Combinatorics_Words.Periodicity_Lemma
Presenting theory Combinatorics_Words.Lyndon_Schutzenberger
Presenting theory Combinatorics_Words.CoWAll
Presenting Combinatorics_Words_Graph_Lemma ...
Presenting document Combinatorics_Words_Graph_Lemma/document
Presenting document Combinatorics_Words_Graph_Lemma/outline
Presenting theory Category3.SetCat
Presenting theory HOL-Library.Code_Lazy
Presenting file "code_lazy.ML"
Presenting theory Category3.ProductCategory
Presenting theory Buildings.Coxeter
Presenting theory Combinatorics_Words_Graph_Lemma.Graph_Lemma
Presenting Combinatorics_Words_Lyndon ...
Presenting document Combinatorics_Words_Lyndon/document
Presenting document Combinatorics_Words_Lyndon/outline
Presenting theory MonoidalCategory.FreeMonoidalCategory
Presenting theory Category3.NaturalTransformation
Presenting theory Category3.BinaryFunctor
Presenting theory HOL-Library.Code_Test
Presenting file "code_test.ML"
Presenting theory HOL-Library.Combine_PER
Presenting theory Combinatorics_Words_Lyndon.Lyndon
Presenting theory Category3.FunctorCategory
Presenting theory Combinatorics_Words_Lyndon.Lyndon_Addition
Presenting document ConcurrentIMP/document
Presenting document ConcurrentIMP/outline
Presenting theory MonoidalCategory.CartesianMonoidalCategory
Presenting document CoreC++/document
Presenting document CoreC++/outline
Presenting theory ConcurrentIMP.CIMP_pred
Presenting theory CoreC++.Auxiliary
Presenting theory ConcurrentIMP.Infinite_Sequences
Presenting theory CoreC++.Type
Presenting theory CoreC++.Value
Presenting theory Buildings.Building
Presenting document Core_DOM/document
Presenting document Core_DOM/outline
Presenting theory CoreC++.Expr
Presenting theory CoreC++.Decl
Presenting theory CoreC++.ClassRel
Presenting theory Core_DOM.Hiding_Type_Variables
Presenting theory Core_DOM.Ref
Presenting theory Core_DOM.Core_DOM_Basic_Datatypes
Presenting theory Core_DOM.BaseClass
Presenting theory Category3.Yoneda
Presenting theory ConcurrentIMP.LTL
Presenting theory Core_DOM.Heap_Error_Monad
Presenting theory Polynomials.OAlist
Presenting theory ConcurrentIMP.CIMP_lang
Presenting theory Stateful_Protocol_Composition_and_Typing.Typing_Result
Presenting theory Core_DOM.BaseMonad
Presenting theory Core_DOM.ObjectPointer
Presenting theory Core_DOM.ObjectClass
Presenting theory Core_DOM.ObjectMonad
Presenting theory Core_DOM.NodePointer
Presenting theory Core_DOM.NodeClass
Presenting theory Core_DOM.NodeMonad
Presenting theory Core_DOM.ElementPointer
Presenting theory Core_DOM.CharacterDataPointer
Presenting theory Core_DOM.DocumentPointer
Presenting theory Core_DOM.ShadowRootPointer
Presenting theory CoreC++.SubObj
Presenting theory Polynomials.OAlist_Poly_Mapping
Presenting theory CoreC++.Objects
Presenting theory Core_DOM.ElementClass
Presenting theory CoreC++.Exceptions
Presenting theory CoreC++.Syntax
Presenting theory CoreC++.State
Presenting theory ConcurrentIMP.CIMP_vcg
Presenting theory Core_DOM.ElementMonad
Presenting theory ConcurrentIMP.CIMP_vcg_rules
Presenting theory Core_DOM.CharacterDataClass
Presenting theory ConcurrentIMP.CIMP
Presenting theory ConcurrentIMP.CIMP_locales
Presenting theory ConcurrentIMP.CIMP_one_place_buffer
Presenting theory ConcurrentIMP.CIMP_unbounded_buffer
Presenting document Shadow_DOM/document
Presenting document Shadow_DOM/outline
Presenting theory Core_DOM.CharacterDataMonad
Presenting theory Shadow_DOM.ShadowRootClass
Presenting theory CoreC++.BigStep
Presenting theory Core_DOM.DocumentClass
Presenting theory HOL-Library.Complete_Partial_Order2
Presenting theory Polynomials.Term_Order
Presenting theory Shadow_DOM.ShadowRootMonad
Presenting theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Model
Presenting theory Core_DOM.DocumentMonad
Presenting theory Stateful_Protocol_Composition_and_Typing.Stateful_Strands
Presenting theory HOL-Library.Conditional_Parametricity
Presenting file "conditional_parametricity.ML"
Presenting theory Polynomials.MPoly_Type_Class_OAlist
Presenting theory Category3.Adjunction
Presenting theory HOL-Library.Confluence
Presenting theory Polynomials.Quasi_PM_Power_Products