[EnvInject] - Loading node environment variables.
workermtahpc (mta_hpc) in workspace /media/data/jenkins/workspace/isabelle-all Building remotely on
[isabelle-all] $ hg showconfig paths.default
[isabelle-all] $ hg pull --rev default
http://isabelle.in.tum.de/repos/isabelle/ pulling from
https://isabelle.in.tum.de/repos/isabelle/ real URL is
[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 4a064fad28b2b7c4a7a969334fdf22fc4165afc8 --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(4a064fad28b2b7c4a7a969334fdf22fc4165afc8)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
https://foss.heptapod.net/isa-afp/afp-devel/ pulling from
[afp] $ hg update --clean --rev default
5 files updated, 0 files merged, 1 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 ad6ac3e1e8981de68ea7639bb49d9d34d59ba37d --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(ad6ac3e1e8981de68ea7639bb49d9d34d59ba37d)" --encoding UTF-8 --encodingmode replace
[isabelle-all] $ /bin/sh -xe /tmp/jenkins10280419717426917380.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/Boolos_Curious_Inference (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 AFP/Risk_Free_Lending (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/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/Stalnaker_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/Combinatorics_Words (AFP)
Session AFP/Combinatorics_Words_Graph_Lemma (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/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/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/Schutz_Spacetime (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/Hales_Jewett (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 AFP/IMP_Compiler_Reuse (AFP)
Session Doc/Implementation (doc)
Session AFP/Implicational_Logic (AFP)
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/Involutions2Squares (AFP)
Session AFP/Jacobson_Basic_Algebra (AFP)
Session AFP/Grothendieck_Schemes (AFP)
Session AFP/Pluennecke_Ruzsa_Inequality (AFP)
Session AFP/Khovanskii_Theorem (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/Maximum_Segment_Sum (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/Undirected_Graph_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/SCC_Bloemen_Sequential (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/Security_Protocol_Refinement (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/Separation_Logic_Unbounded (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/Weighted_Arithmetic_Geometric_Mean (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/Universal_Hash_Families (AFP)
Session AFP/Frequency_Moments (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/Number_Theoretic_Transform (AFP)
Session AFP/CRYSTALS-Kyber (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/Commuting_Hermitian (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/Safe_Range_RC (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 Complex_Bounded_Operators ...
Complex_Bounded_Operators: theory Deriving.Comparator
Complex_Bounded_Operators: theory Containers.Extend_Partial_Order
Complex_Bounded_Operators: theory Containers.List_Fusion
Complex_Bounded_Operators: theory Deriving.Derive_Manager
Complex_Bounded_Operators: theory Containers.Equal
Complex_Bounded_Operators: theory Deriving.Generator_Aux
Complex_Bounded_Operators: theory HOL-Cardinals.Fun_More
Complex_Bounded_Operators: theory HOL-Cardinals.Order_Relation_More
Complex_Bounded_Operators: theory Containers.Closure_Set
Complex_Bounded_Operators: theory HOL-Cardinals.Order_Union
Complex_Bounded_Operators: theory HOL-Computational_Algebra.Fraction_Field
Complex_Bounded_Operators: theory HOL-Library.Adhoc_Overloading
Complex_Bounded_Operators: theory HOL-Library.Char_ord
Complex_Bounded_Operators: theory HOL-Cardinals.Wellorder_Extension
Complex_Bounded_Operators: theory Deriving.Equality_Generator
Complex_Bounded_Operators: theory HOL-Library.Monad_Syntax
Complex_Bounded_Operators: theory HOL-Cardinals.Wellfounded_More
Complex_Bounded_Operators: theory HOL-Library.Code_Abstract_Nat
Complex_Bounded_Operators: theory Containers.Containers_Auxiliary
Complex_Bounded_Operators: theory HOL-Library.Code_Target_Int
Complex_Bounded_Operators: theory HOL-Cardinals.Wellorder_Relation
Complex_Bounded_Operators: theory HOL-Library.Code_Target_Nat
Complex_Bounded_Operators: theory HOL-Library.Complemented_Lattices
Complex_Bounded_Operators: theory HOL-Cardinals.Wellorder_Embedding
Complex_Bounded_Operators: theory HOL-Algebra.Congruence
Complex_Bounded_Operators: theory HOL-Library.Code_Target_Numeral
Complex_Bounded_Operators: theory Jordan_Normal_Form.Missing_Misc
Complex_Bounded_Operators: theory Deriving.Equality_Instances
Complex_Bounded_Operators: theory HOL-Cardinals.Wellorder_Constructions
Complex_Bounded_Operators: theory HOL-Library.Function_Algebras
Complex_Bounded_Operators: theory HOL-Library.IArray
Complex_Bounded_Operators: theory HOL-Library.More_List
Complex_Bounded_Operators: theory Deriving.Compare
Complex_Bounded_Operators: theory Deriving.Comparator_Generator
Complex_Bounded_Operators: theory Containers.Lexicographic_Order
Complex_Bounded_Operators: theory HOL-Computational_Algebra.Normalized_Fraction
Complex_Bounded_Operators: theory HOL-Algebra.Order
Complex_Bounded_Operators: theory HOL-Cardinals.Cardinal_Order_Relation
Complex_Bounded_Operators: theory HOL-Cardinals.Ordinal_Arithmetic
Complex_Bounded_Operators: theory Containers.Containers_Generator
Complex_Bounded_Operators: theory Containers.Set_Linorder
Complex_Bounded_Operators: theory HOL-Library.RBT_Impl
Complex_Bounded_Operators: theory Deriving.Compare_Generator
Complex_Bounded_Operators: theory Containers.Collection_Enum
Complex_Bounded_Operators: theory HOL-Cardinals.Cardinal_Arithmetic
Complex_Bounded_Operators: theory Deriving.Compare_Instances
Complex_Bounded_Operators: theory HOL-Algebra.Lattice
Complex_Bounded_Operators: theory Containers.Collection_Eq
Complex_Bounded_Operators: theory HOL-Cardinals.Cardinals
Complex_Bounded_Operators: theory HOL-Library.Rewrite
Complex_Bounded_Operators: theory HOL-Types_To_Sets.Types_To_Sets
Complex_Bounded_Operators: theory Polynomial_Interpolation.Missing_Unsorted
Complex_Bounded_Operators: theory Cauchy.CauchysMeanTheorem
Complex_Bounded_Operators: theory Containers.DList_Set
Complex_Bounded_Operators: theory HOL-Computational_Algebra.Polynomial
Complex_Bounded_Operators: theory HOL-Examples.Sqrt
Complex_Bounded_Operators: theory HOL-Algebra.Complete_Lattice
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces0
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Ordered_Fields
Complex_Bounded_Operators: theory HOL-Algebra.Group
Complex_Bounded_Operators: theory Jordan_Normal_Form.Conjugate
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_General
Complex_Bounded_Operators: theory HOL-Algebra.Coset
Complex_Bounded_Operators: theory HOL-Algebra.FiniteProduct
Complex_Bounded_Operators: theory HOL-Algebra.Ring
Complex_Bounded_Operators: theory Banach_Steinhaus.Banach_Steinhaus_Missing
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Vector_Spaces
Complex_Bounded_Operators: theory Banach_Steinhaus.Banach_Steinhaus
Complex_Bounded_Operators: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
Complex_Bounded_Operators: theory Sqrt_Babylonian.Log_Impl
Complex_Bounded_Operators: theory Sqrt_Babylonian.NthRoot_Impl
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Operator_Norm
Complex_Bounded_Operators: theory Polynomial_Interpolation.Ring_Hom
Complex_Bounded_Operators: theory Sqrt_Babylonian.Sqrt_Babylonian
Complex_Bounded_Operators: theory Real_Impl.Real_Impl
Complex_Bounded_Operators: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Complex_Bounded_Operators: theory HOL-Computational_Algebra.Polynomial_Factorial
Complex_Bounded_Operators: theory Show.Show
Complex_Bounded_Operators: theory HOL-Algebra.Module
Complex_Bounded_Operators: theory Jordan_Normal_Form.Missing_Ring
Complex_Bounded_Operators: theory Containers.Collection_Order
Complex_Bounded_Operators: theory Show.Show_Instances
Complex_Bounded_Operators: theory VectorSpace.FunctionLemmas
Complex_Bounded_Operators: theory VectorSpace.RingModuleFacts
Complex_Bounded_Operators: theory VectorSpace.MonoidSums
Complex_Bounded_Operators: theory VectorSpace.LinearCombinations
Complex_Bounded_Operators: theory Jordan_Normal_Form.Matrix
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Vector_Spaces
Complex_Bounded_Operators: theory VectorSpace.SumSpaces
Complex_Bounded_Operators: theory VectorSpace.VectorSpace
Complex_Bounded_Operators: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
Complex_Bounded_Operators: theory Jordan_Normal_Form.Show_Matrix
Complex_Bounded_Operators: theory Polynomial_Interpolation.Missing_Polynomial
Complex_Bounded_Operators: theory Jordan_Normal_Form.Column_Operations
Complex_Bounded_Operators: theory Jordan_Normal_Form.Determinant
Complex_Bounded_Operators: theory Polynomial_Factorization.Order_Polynomial
Complex_Bounded_Operators: theory Polynomial_Interpolation.Ring_Hom_Poly
Complex_Bounded_Operators: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product0
Complex_Bounded_Operators: theory Jordan_Normal_Form.Determinant_Impl
Complex_Bounded_Operators: theory Jordan_Normal_Form.Char_Poly
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Inner_Product
Complex_Bounded_Operators: theory Jordan_Normal_Form.Missing_VectorSpace
Complex_Bounded_Operators: theory Jordan_Normal_Form.Jordan_Normal_Form
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Euclidean_Space0
Complex_Bounded_Operators: theory Complex_Bounded_Operators.One_Dimensional_Spaces
Complex_Bounded_Operators: theory Jordan_Normal_Form.VS_Connect
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function0
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_Bounded_Linear_Function
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Complex_L2
Complex_Bounded_Operators: theory Jordan_Normal_Form.Gram_Schmidt
Complex_Bounded_Operators: theory Jordan_Normal_Form.Matrix_Kernel
Complex_Bounded_Operators: theory Jordan_Normal_Form.Schur_Decomposition
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Jordan_Normal_Form
Complex_Bounded_Operators: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Matrix
Complex_Bounded_Operators: theory Containers.RBT_ext
Complex_Bounded_Operators: theory Deriving.RBT_Comparator_Impl
Complex_Bounded_Operators: theory Containers.RBT_Mapping2
Complex_Bounded_Operators: theory Containers.RBT_Set2
Complex_Bounded_Operators: theory Containers.Set_Impl
Complex_Bounded_Operators: theory Jordan_Normal_Form.Matrix_IArray_Impl
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code
Complex_Bounded_Operators: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
Complex_Bounded_Operators: theory Jordan_Normal_Form.Matrix_Impl
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Extra_Pretty_Code_Examples
Complex_Bounded_Operators: theory Complex_Bounded_Operators.Cblinfun_Code_Examples
Preparing Complex_Bounded_Operators/document ...
Finished Complex_Bounded_Operators/document (0:00:36 elapsed time)
Preparing Complex_Bounded_Operators/outline ...
Finished Complex_Bounded_Operators/outline (0:00:14 elapsed time)
Timing Complex_Bounded_Operators (8 threads, 368.528s elapsed time, 2478.271s cpu time, 263.989s GC time, factor 6.72)
Finished Complex_Bounded_Operators (0:07:50 elapsed time, 0:45:25 cpu time, factor 5.79)
Registers: theory HOL-Eisbach.Eisbach
Registers: theory HOL-Library.Type_Length
Registers: theory HOL-Library.Z2
Registers: theory Registers.Axioms
Registers: theory Registers.Axioms_Classical
Registers: theory Registers.Laws
Registers: theory Registers.Laws_Classical
Registers: theory Registers.Misc
Registers: theory HOL-Library.Word
Registers: theory Registers.Axioms_Complement
Registers: theory Registers.Laws_Complement
Registers: theory Registers.Classical_Extra
Registers: theory Registers.Finite_Tensor_Product
Registers: theory Registers.Axioms_Quantum
Registers: theory Registers.Finite_Tensor_Product_Matrices
Registers: theory Registers.Quantum
Registers: theory Registers.Laws_Quantum
Registers: theory Registers.Quantum_Extra
Registers: theory Registers.Axioms_Complement_Quantum
Registers: theory Registers.QHoare
Registers: theory Registers.Teleport
Registers: theory Registers.Laws_Complement_Quantum
Registers: theory Registers.Check_Autogenerated_Files
Registers: theory Registers.Quantum_Extra2
Registers: theory Registers.Pure_States
Preparing Registers/document ...
Finished Registers/document (0:00:15 elapsed time)
Preparing Registers/outline ...
Finished Registers/outline (0:00:07 elapsed time)
Timing Registers (8 threads, 69.686s elapsed time, 370.904s cpu time, 10.172s GC time, factor 5.32)
Finished Registers (0:01:15 elapsed time, 0:06:16 cpu time, factor 4.99)
Presentation in "/media/data/jenkins/workspace/isabelle-all/browser_info"
Presenting Complex_Bounded_Operators in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Complex_Bounded_Operators" ...
Presenting Timed_Automata in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Timed_Automata" ...
Presenting Store_Buffer_Reduction in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Store_Buffer_Reduction" ...
Presenting Simpl in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Simpl" ...
Presenting Planarity_Certificates in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Planarity_Certificates" ...
Presenting Topological_Semantics in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Topological_Semantics" ...
Presenting Registers in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Registers" ...
Presenting Goedel_HFSet_Semantic in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Goedel_HFSet_Semantic" ...
Presenting Goedel_HFSet_Semanticless in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Goedel_HFSet_Semanticless" ...
Presenting document Goedel_HFSet_Semantic/document
Presenting document Goedel_HFSet_Semantic/outline
Presenting document Store_Buffer_Reduction/document
Presenting document Store_Buffer_Reduction/outline
Presenting document Topological_Semantics/document
Presenting document Topological_Semantics/outline
Presenting document Timed_Automata/document
Presenting document Timed_Automata/outline
Presenting document Goedel_HFSet_Semanticless/document
Presenting document Goedel_HFSet_Semanticless/outline
Presenting document Planarity_Certificates/document
Presenting document Planarity_Certificates/outline
Presenting document Registers/document
Presenting document Registers/outline
Presenting document Complex_Bounded_Operators/document
Presenting document Complex_Bounded_Operators/outline
Presenting document Simpl/document
Presenting document Simpl/outline
Presenting theory "Registers.Axioms"
Presenting theory "Planarity_Certificates.Lib"
Presenting theory "Topological_Semantics.sse_boolean_algebra"
Presenting theory "HOL-Types_To_Sets.Types_To_Sets"
Presenting file "~~/src/HOL/Types_To_Sets/local_typedef.ML"
Presenting file "~~/src/HOL/Types_To_Sets/unoverloading.ML"
Presenting file "~~/src/HOL/Types_To_Sets/internalize_sort.ML"
Presenting file "~~/src/HOL/Types_To_Sets/unoverload_type.ML"
Presenting file "~~/src/HOL/Types_To_Sets/unoverload_def.ML"
Presenting theory "Registers.Laws"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "Registers.Axioms_Complement"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "Planarity_Certificates.OptionMonad"
Presenting theory "Topological_Semantics.sse_boolean_algebra_quantification"
Presenting theory "Banach_Steinhaus.Banach_Steinhaus_Missing"
Presenting theory "HOL-Library.Cancellation"
Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
Presenting theory "Topological_Semantics.sse_operation_positive"
Presenting theory "HOL-Library.Cancellation"
Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
Presenting theory "Banach_Steinhaus.Banach_Steinhaus"
Presenting theory "Topological_Semantics.sse_operation_positive_quantification"
Presenting theory "HOL-Library.Complemented_Lattices"
Presenting theory "HOL-Library.Function_Algebras"
Presenting theory "Registers.Laws_Complement"
Presenting theory "HOL-Cardinals.Fun_More"
Presenting theory "Planarity_Certificates.NonDetMonad"
Presenting theory "HOL-Cardinals.Order_Relation_More"
Presenting theory "HOL-Cardinals.Wellfounded_More"
Presenting theory "HOL-Cardinals.Wellorder_Relation"
Presenting theory "HOL-Cardinals.Wellorder_Embedding"
Presenting theory "HOL-Cardinals.Order_Union"
Presenting theory "Registers.Axioms_Classical"
Presenting theory "Planarity_Certificates.NonDetMonadLemmas"
Presenting theory "Planarity_Certificates.OptionMonadND"
Presenting theory "HOL-Cardinals.Wellorder_Constructions"
Presenting theory "Planarity_Certificates.WP"
Presenting file "$AFP/Planarity_Certificates/l4v/lib/wp/WP-method.ML"
Presenting theory "Topological_Semantics.sse_operation_negative"
Presenting theory "Registers.Laws_Classical"
Presenting theory "HOL-Library.Z2"
Presenting theory "Planarity_Certificates.OptionMonadWP"
Presenting theory "Registers.Misc"
Presenting theory "Topological_Semantics.sse_operation_negative_quantification"
Presenting theory "HOL-Cardinals.Ordinal_Arithmetic"
Presenting theory "HOL-Library.Multiset"
Presenting theory "Registers.Classical_Extra"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "HOL-Library.FuncSet"
Presenting theory "HOL-Library.Old_Recdef"
Presenting file "~~/src/HOL/Library/old_recdef.ML"
Presenting theory "Timed_Automata.Floyd_Warshall"
Presenting theory "HOL-Library.Multiset"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "HOL-Cardinals.Cardinal_Order_Relation"
Presenting theory "Registers.Finite_Tensor_Product"
Presenting theory "HOL-Library.Disjoint_Sets"
Presenting theory "Timed_Automata.Timed_Automata"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "Topological_Semantics.topo_operators_basic"
Presenting theory "HOL-Combinatorics.Transposition"
Presenting theory "HOL-Cardinals.Cardinal_Arithmetic"
Presenting theory "HOL-Cardinals.Wellorder_Extension"
Presenting theory "HOL-Cardinals.Cardinals"
Presenting theory "Registers.Axioms_Quantum"
Presenting theory "Timed_Automata.DBM"
Presenting theory "Complex_Bounded_Operators.Extra_General"
Presenting theory "Complex_Bounded_Operators.Extra_Vector_Spaces"
Presenting theory "Topological_Semantics.topo_operators_derivative"
Presenting theory "Complex_Bounded_Operators.Extra_Ordered_Fields"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "Topological_Semantics.topo_alexandrov"
Presenting theory "Complex_Bounded_Operators.Extra_Operator_Norm"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "Complex_Bounded_Operators.Complex_Vector_Spaces0"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "Topological_Semantics.topo_frontier_algebra"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "Timed_Automata.Paths_Cycles"
Presenting theory "HOL-Combinatorics.Permutations"
Presenting theory "Complex_Bounded_Operators.Complex_Vector_Spaces"
Presenting theory "Graph_Theory.Rtrancl_On"
Presenting theory "HOL-Library.FSet"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "Complex_Bounded_Operators.Complex_Inner_Product0"
Presenting theory "Registers.Laws_Quantum"
Presenting theory "HOL-Library.FSet"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "Registers.Quantum"
Presenting theory "Timed_Automata.DBM_Basics"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "Simpl.Language"
Presenting theory "HOL-Library.Old_Datatype"
Presenting theory "Registers.Quantum_Extra"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "Registers.QHoare"
Presenting theory "Complex_Bounded_Operators.Complex_Inner_Product"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "FinFun.FinFun"
Presenting theory "Complex_Bounded_Operators.One_Dimensional_Spaces"
Presenting theory "Registers.Finite_Tensor_Product_Matrices"
Presenting theory "HOL-Library.Type_Length"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Library.Rewrite"
Presenting file "~~/src/HOL/Library/cconv.ML"
Presenting file "~~/src/HOL/Library/rewrite.ML"
Presenting theory "Complex_Bounded_Operators.Complex_Euclidean_Space0"
Presenting theory "Complex_Bounded_Operators.Complex_Bounded_Linear_Function0"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "Timed_Automata.DBM_Operations"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "FinFun.FinFun"
Presenting theory "HOL-Library.Countable_Complete_Lattices"
Presenting theory "Topological_Semantics.topo_negation_conditions"
Presenting theory "HOL-Library.Order_Continuity"
Presenting theory "Timed_Automata.DBM_Zone_Semantics"
Presenting theory "Topological_Semantics.topo_negation_fixedpoints"
Presenting theory "HOL-Library.Extended_Nat"
Presenting theory "Complex_Bounded_Operators.Complex_Bounded_Linear_Function"
Presenting theory "HOL-Library.Liminf_Limsup"
Presenting theory "Timed_Automata.Misc"
Presenting theory "Nominal2.Nominal2_Base"
Presenting file "$AFP/Nominal2/nominal_basics.ML"
Presenting file "$AFP/Nominal2/nominal_thmdecls.ML"
Presenting file "$AFP/Nominal2/nominal_permeq.ML"
Presenting file "$AFP/Nominal2/nominal_library.ML"
Presenting file "$AFP/Nominal2/nominal_atoms.ML"
Presenting file "$AFP/Nominal2/nominal_eqvt.ML"
Presenting theory "Timed_Automata.DBM_Normalization"
Presenting theory "HOL-Library.Quotient_Syntax"
Presenting theory "HOL-Library.Quotient_Set"
Presenting theory "HOL-Library.Quotient_Product"
Presenting theory "HOL-Library.Quotient_Option"
Presenting theory "HOL-Library.Quotient_List"
Presenting theory "Complex_Bounded_Operators.Complex_L2"
Presenting theory "Topological_Semantics.ex_LFIs"
Presenting theory "Polynomial_Interpolation.Ring_Hom"
Presenting theory "Jordan_Normal_Form.Missing_Misc"
Presenting theory "Nominal2.Nominal2_Abs"
Presenting theory "HOL-Algebra.Congruence"
Presenting theory "HOL-Algebra.Order"
Presenting theory "Topological_Semantics.topo_strict_implication"
Presenting theory "Nominal2.Nominal2_FCB"
Presenting theory "HOL-Algebra.Lattice"
Presenting theory "HOL-Library.Extended_Real"
Presenting theory "HOL-Algebra.Complete_Lattice"
Presenting theory "Graph_Theory.Stuff"
Presenting theory "HOL-Algebra.Group"
Presenting theory "Topological_Semantics.ex_subminimal_logics"
Presenting theory "Graph_Theory.Digraph"
Presenting theory "Graph_Theory.Bidirected_Digraph"
Presenting theory "HOL-Algebra.FiniteProduct"
Presenting theory "Topological_Semantics.topo_derivative_algebra"
Presenting theory "HOL-Library.Word"
Presenting theory "HOL-Algebra.Ring"
Presenting theory "Nominal2.Nominal2_Base"
Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
Presenting file "$AFP/Nominal2/nominal_basics.ML"
Presenting file "$AFP/Nominal2/nominal_thmdecls.ML"
Presenting file "$AFP/Nominal2/nominal_permeq.ML"
Presenting file "$AFP/Nominal2/nominal_library.ML"
Presenting theory "Topological_Semantics.ex_LFUs"
Presenting file "$AFP/Nominal2/nominal_atoms.ML"
Presenting file "$AFP/Nominal2/nominal_eqvt.ML"
Presenting theory "HOL-Library.Quotient_Syntax"
Presenting theory "Jordan_Normal_Form.Missing_Ring"
Presenting theory "Jordan_Normal_Form.Conjugate"
Presenting theory "Topological_Semantics.topo_border_algebra"
Presenting theory "HOL-Library.Quotient_Set"
Presenting theory "HOL-Algebra.Module"
Presenting theory "HOL-Library.Quotient_Product"
Presenting theory "Topological_Semantics.topo_closure_algebra"
Presenting theory "Graph_Theory.Arc_Walk"
Presenting theory "HOL-Library.Quotient_Option"
Presenting theory "Topological_Semantics.topo_interior_algebra"
Presenting Transitive-Closure-II in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Transitive-Closure-II" ...
Presenting document Transitive-Closure-II/document
Presenting document Transitive-Closure-II/outline
Presenting theory "HOL-Library.Quotient_List"
Presenting theory "Registers.Teleport"
Presenting theory "Timed_Automata.Regions_Beta"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "Graph_Theory.Pair_Digraph"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Jordan_Normal_Form.Matrix"
Presenting theory "HOL-Library.While_Combinator"
Presenting theory "Simpl.Semantic"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "Nominal2.Nominal2_Abs"
Presenting theory "HOL-Algebra.Coset"
Presenting theory "VectorSpace.RingModuleFacts"
Presenting theory "VectorSpace.FunctionLemmas"
Presenting theory "VectorSpace.MonoidSums"
Presenting theory "Transitive-Closure-II.RTrancl"
Presenting Tree_Decomposition in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tree_Decomposition" ...
Presenting document Tree_Decomposition/document
Presenting document Tree_Decomposition/outline
Presenting theory "Nominal2.Nominal2_FCB"
Presenting theory "Registers.Axioms_Complement_Quantum"
Presenting theory "Simpl.HoarePartialDef"
Presenting theory "VectorSpace.LinearCombinations"
Presenting theory "Tree_Decomposition.Graph"
Presenting theory "Graph_Theory.Digraph_Component"
Presenting theory "VectorSpace.SumSpaces"
Presenting theory "Tree_Decomposition.Tree"
Presenting theory "VectorSpace.VectorSpace"
Presenting theory "Tree_Decomposition.TreeDecomposition"
Presenting theory "Tree_Decomposition.TreewidthTree"
Presenting theory "Graph_Theory.Vertex_Walk"
Presenting theory "Graph_Theory.Digraph_Component_Vwalk"
Presenting theory "Tree_Decomposition.TreewidthCompleteGraph"
Presenting theory "Tree_Decomposition.ExampleInstantiations"
Presenting Tutorial in "/media/data/jenkins/workspace/isabelle-all/browser_info/Doc/Tutorial" ...
Presenting document Tutorial/tutorial
Presenting theory "Tutorial.Base"
Presenting theory "Tutorial.ToyList_Test"
Presenting theory "Jordan_Normal_Form.Missing_VectorSpace"
Presenting theory "Tutorial.ToyList"
Presenting theory "Registers.Laws_Complement_Quantum"
Presenting theory "Tutorial.Ifexpr"
Presenting theory "Registers.Quantum_Extra2"
Presenting theory "Store_Buffer_Reduction.ReduceStoreBuffer"
Presenting theory "Tutorial.CodeGen"
Presenting theory "Tutorial.Trie"
Presenting theory "Jordan_Normal_Form.Gauss_Jordan_Elimination"
Presenting theory "Graph_Theory.Digraph_Isomorphism"
Presenting theory "Tutorial.ABexpr"
Presenting theory "Tutorial.unfoldnested"
Presenting theory "Jordan_Normal_Form.Column_Operations"
Presenting theory "Tutorial.Nested"
Presenting theory "Tutorial.Fundata"
Presenting theory "HOL-Library.More_List"
Presenting theory "Nominal2.Nominal2"
Presenting file "$AFP/Nominal2/nominal_dt_data.ML"
Presenting file "$AFP/Nominal2/nominal_dt_rawfuns.ML"
Presenting file "$AFP/Nominal2/nominal_dt_alpha.ML"
Presenting file "$AFP/Nominal2/nominal_dt_quot.ML"
Presenting file "$AFP/Nominal2/nominal_induct.ML"
Presenting file "$AFP/Nominal2/nominal_inductive.ML"
Presenting file "$AFP/Nominal2/nominal_function_common.ML"
Presenting file "$AFP/Nominal2/nominal_function_core.ML"
Presenting file "$AFP/Nominal2/nominal_mutual.ML"
Presenting file "$AFP/Nominal2/nominal_function.ML"
Presenting file "$AFP/Nominal2/nominal_termination.ML"
Presenting theory "Tutorial.fun0"
Presenting theory "Tutorial.simp2"
Presenting theory "Tutorial.PDL"
Presenting theory "HOL-Combinatorics.Orbits"
Presenting theory "Tutorial.CTL"
Presenting theory "Timed_Automata.Regions"
Presenting theory "Graph_Theory.Auxiliary"
Presenting theory "Tutorial.CTLind"
Presenting theory "HereditarilyFinite.HF"
Presenting theory "Tutorial.Setup"
Presenting file "~~/src/Doc/antiquote_setup.ML"
Presenting file "~~/src/Doc/more_antiquote.ML"
Presenting theory "Tutorial.Even"
Presenting theory "HereditarilyFinite.Ordinal"
Presenting theory "Tutorial.Mutual"
Presenting theory "Tutorial.Star"
Presenting theory "Graph_Theory.Subdivision"
Presenting theory "HereditarilyFinite.Rank"
Presenting theory "Tutorial.AB"
Presenting theory "Tutorial.Advanced"
Presenting theory "Tutorial.Tree"
Presenting theory "Tutorial.Tree2"
Presenting theory "Tutorial.Plus"
Presenting theory "Tutorial.case_exprs"
Presenting theory "Tutorial.fakenat"
Presenting theory "Timed_Automata.Closure"
Presenting theory "HOL-Computational_Algebra.Polynomial"
Presenting theory "Tutorial.natsum"
Presenting theory "Tutorial.pairs2"
Presenting theory "Tutorial.Option2"
Presenting theory "Tutorial.types"
Presenting theory "Tutorial.prime_def"
Presenting theory "Tutorial.simp"
Presenting theory "Tutorial.Itrev"
Presenting theory "Tutorial.AdvancedInd"
Presenting theory "HereditarilyFinite.OrdArith"
Presenting theory "Tutorial.appendix"
Presenting theory "Simpl.HoarePartialProps"
Presenting theory "Graph_Theory.Euler"
Presenting theory "HOL-Computational_Algebra.Fraction_Field"
Presenting theory "HOL-Computational_Algebra.Normalized_Fraction"
Presenting theory "Tutorial.Message"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting theory "HOL-Computational_Algebra.Polynomial_Factorial"
Presenting theory "Tutorial.Event"
Presenting theory "Timed_Automata.Approx_Beta"
Presenting theory "Tutorial.Public"
Presenting theory "Polynomial_Interpolation.Missing_Unsorted"
Presenting theory "HOL-Library.Rewrite"
Presenting file "~~/src/HOL/Library/cconv.ML"
Presenting file "~~/src/HOL/Library/rewrite.ML"
Presenting theory "Tutorial.NS_Public"
Presenting theory "Tutorial.Documents"
Presenting theory "Incompleteness.SyntaxN"
Presenting theory "Tutorial.Numbers"
Presenting theory "Tutorial.Pairs"
Presenting theory "Tutorial.Records"
Presenting theory "Simpl.HoarePartial"
Presenting theory "Tutorial.Typedefs"
Presenting theory "Tutorial.Overloading"
Presenting theory "Tutorial.Axioms"
Presenting theory "Tutorial.Basic"
Presenting theory "Tutorial.Blast"
Presenting theory "Tutorial.Force"
Presenting theory "Tutorial.TPrimes"
Presenting theory "Timed_Automata.Normalized_Zone_Semantics"
Presenting theory "Tutorial.Forward"
Presenting theory "Tutorial.Tacticals"
Presenting theory "Tutorial.find2"
Presenting Typeclass_Hierarchy in "/media/data/jenkins/workspace/isabelle-all/browser_info/Doc/Typeclass_Hierarchy" ...
Presenting document Typeclass_Hierarchy/typeclass_hierarchy
Presenting theory "Tutorial.Examples"
Presenting theory "Tutorial.Functions"
Presenting theory "Tutorial.Relations"
Presenting theory "Tutorial.Recur"
Presenting Types_Tableaus_and_Goedels_God in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Types_Tableaus_and_Goedels_God" ...
Presenting document Types_Tableaus_and_Goedels_God/document
Presenting document Types_Tableaus_and_Goedels_God/outline
Presenting theory "Types_Tableaus_and_Goedels_God.Relations"
Presenting theory "Types_Tableaus_and_Goedels_God.IHOML"
Presenting theory "HOL-Library.Cancellation"
Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
Presenting theory "Incompleteness.Coding"
Presenting theory "Types_Tableaus_and_Goedels_God.IHOML_Examples"
Presenting theory "Types_Tableaus_and_Goedels_God.GoedelProof_P1"
Presenting theory "Graph_Theory.Kuratowski"
Presenting theory "Jordan_Normal_Form.Determinant"
Presenting theory "Graph_Theory.Weighted_Graph"
Presenting theory "Types_Tableaus_and_Goedels_God.GoedelProof_P2"
Presenting theory "Registers.Pure_States"
Presenting theory "Registers.Check_Autogenerated_Files"
Presenting UPF in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UPF" ...
Presenting document UPF/document
Presenting document UPF/outline
Presenting theory "Types_Tableaus_and_Goedels_God.FittingProof"
Presenting theory "Graph_Theory.Shortest_Path"
Presenting theory "Graph_Theory.Graph_Theory"
Presenting theory "Types_Tableaus_and_Goedels_God.AndersonProof"
Presenting UPF_Firewall in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UPF_Firewall" ...
Presenting document UPF_Firewall/document
Presenting document UPF_Firewall/outline
Presenting theory "UPF_Firewall.NetworkCore"
Presenting theory "UPF_Firewall.DatatypeAddress"
Presenting theory "UPF_Firewall.DatatypePort"
Presenting theory "UPF_Firewall.IntegerAddress"
Presenting theory "UPF_Firewall.IntegerPort"
Presenting theory "UPF.Monads"
Presenting theory "Jordan_Normal_Form.VS_Connect"
Presenting theory "UPF_Firewall.IntegerPort_TCPUDP"
Presenting theory "UPF.UPFCore"
Presenting theory "UPF_Firewall.IPv4"
Presenting theory "UPF.ElementaryPolicies"
Presenting theory "Incompleteness.Predicates"
Presenting theory "UPF_Firewall.IPv4_TCPUDP"
Presenting theory "UPF_Firewall.NetworkModels"
Presenting theory "UPF_Firewall.PolicyCore"
Presenting theory "UPF_Firewall.PolicyCombinators"
Presenting theory "UPF.SeqComposition"
Presenting theory "Planarity_Certificates.Graph_Genus"
Presenting theory "Jordan_Normal_Form.Gram_Schmidt"
Presenting theory "UPF.ParallelComposition"
Presenting theory "UPF_Firewall.PortCombinators"
Presenting theory "Incompleteness.Sigma"
Presenting theory "UPF_Firewall.ProtocolPortCombinators"
Presenting theory "UPF_Firewall.Ports"
Presenting theory "UPF_Firewall.PacketFilter"
Presenting theory "UPF.Normalisation"
Presenting theory "List-Index.List_Index"
Presenting theory "UPF.NormalisationTestSpecification"
Presenting theory "Planarity_Certificates.List_Aux"
Presenting theory "UPF.Analysis"
Presenting theory "Polynomial_Interpolation.Missing_Polynomial"
Presenting theory "Simpl.Termination"
Presenting theory "UPF_Firewall.NAT"
Presenting theory "Polynomial_Factorization.Order_Polynomial"
Presenting theory "UPF.Service"
Presenting theory "Planarity_Certificates.Executable_Permutations"
Presenting theory "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
Presenting theory "UPF.ServiceExample"
Presenting theory "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized"
Presenting Universal_Turing_Machine in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Universal_Turing_Machine" ...
Presenting document Universal_Turing_Machine/document
Presenting document Universal_Turing_Machine/outline
Presenting theory "Transitive-Closure.Transitive_Closure_Impl"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "HOL-Library.Code_Binary_Nat"
Presenting theory "HOL-Library.Multiset"
Presenting theory "UPF_Firewall.FWNormalisationCore"
Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "Nominal2.Nominal2"
Presenting theory "HOL-Library.Code_Target_Numeral"
Presenting file "$AFP/Nominal2/nominal_dt_data.ML"
Presenting file "$AFP/Nominal2/nominal_dt_rawfuns.ML"
Presenting file "$AFP/Nominal2/nominal_dt_alpha.ML"
Presenting file "$AFP/Nominal2/nominal_dt_quot.ML"
Presenting file "$AFP/Nominal2/nominal_induct.ML"
Presenting file "$AFP/Nominal2/nominal_inductive.ML"
Presenting file "$AFP/Nominal2/nominal_function_common.ML"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting file "$AFP/Nominal2/nominal_function_core.ML"
Presenting theory "Incompleteness.Coding_Predicates"
Presenting file "$AFP/Nominal2/nominal_mutual.ML"
Presenting file "$AFP/Nominal2/nominal_function.ML"
Presenting file "$AFP/Nominal2/nominal_termination.ML"
Presenting theory "Planarity_Certificates.Digraph_Map_Impl"
Presenting theory "Typeclass_Hierarchy.Setup"
Presenting file "~~/src/Doc/antiquote_setup.ML"
Presenting file "~~/src/Doc/more_antiquote.ML"
Presenting theory "Typeclass_Hierarchy.Typeclass_Hierarchy"
Presenting Van_Emde_Boas_Trees in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Van_Emde_Boas_Trees" ...
Presenting document Van_Emde_Boas_Trees/document
Presenting document Van_Emde_Boas_Trees/outline
Presenting theory "Universal_Turing_Machine.Turing"
Presenting theory "Planarity_Certificates.Planar_Complete"
Presenting theory "Planarity_Certificates.Reachablen"
Presenting theory "Jordan_Normal_Form.Char_Poly"
Presenting theory "Planarity_Certificates.Permutations_2"
Presenting theory "HOL-Library.Old_Datatype"
Presenting theory "Universal_Turing_Machine.Turing_aux"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "Planarity_Certificates.Planar_Subdivision"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Imperative_HOL.Heap"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "Incompleteness.Pf_Predicates"
Presenting theory "HereditarilyFinite.HF"
Presenting theory "Van_Emde_Boas_Trees.Heap_Time_Monad"
Presenting theory "HOL-Library.Case_Converter"
Presenting file "~~/src/HOL/Library/case_converter.ML"
Presenting theory "Jordan_Normal_Form.Schur_Decomposition"
Presenting theory "HOL-Library.Simps_Case_Conv"
Presenting file "~~/src/HOL/Library/simps_case_conv.ML"
Presenting theory "Van_Emde_Boas_Trees.Array_Time"
Presenting theory "Van_Emde_Boas_Trees.Heap"
Presenting theory "Van_Emde_Boas_Trees.Ref_Time"
Presenting theory "Van_Emde_Boas_Trees.Imperative_HOL_Time"
Presenting theory "Van_Emde_Boas_Trees.Syntax_Match"
Presenting theory "HereditarilyFinite.Ordinal"
Presenting theory "Complex_Bounded_Operators.Extra_Jordan_Normal_Form"
Presenting theory "HOL-Library.Cancellation"
Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
Presenting theory "HereditarilyFinite.Rank"
Presenting theory "Planarity_Certificates.Planar_Subgraph"
Presenting theory "Planarity_Certificates.Kuratowski_Combinatorial"
Presenting theory "Planarity_Certificates.Simpl_Anno"
Presenting theory "Planarity_Certificates.Check_Non_Planarity_Impl"
Presenting theory "Simpl.SmallStep"
Presenting theory "Universal_Turing_Machine.BlanksDoNotMatter"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting theory "Simpl.HoareTotalDef"
Presenting theory "HereditarilyFinite.OrdArith"
Presenting theory "UPF_Firewall.NormalisationGenericProofs"
Presenting theory "Complex_Bounded_Operators.Cblinfun_Matrix"
Presenting theory "HOL-Library.Multiset"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "HOL-ex.Quicksort"
Presenting theory "HOL-Library.Option_ord"
Presenting theory "Planarity_Certificates.Check_Non_Planarity_Verification"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "Containers.Containers_Auxiliary"
Presenting theory "Case_Labeling.Case_Labeling"
Presenting file "$AFP/Case_Labeling/print_nested_cases.ML"
Presenting file "$AFP/Case_Labeling/util.ML"
Presenting file "$AFP/Case_Labeling/casify.ML"
Presenting theory "Planarity_Certificates.AutoCorres_Misc"
Presenting theory "Planarity_Certificates.Setup_AutoCorres"
Presenting file "$AFP/Case_Labeling/util.ML"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting theory "Deriving.Generator_Aux"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "Goedel_HFSet_Semanticless.SyntaxN"
Presenting theory "Containers.Containers_Generator"
Presenting file "$AFP/Containers/containers_generator.ML"
Presenting theory "Incompleteness.II_Prelims"
Presenting theory "Planarity_Certificates.Check_Planarity_Verification"
Presenting theory "Planarity_Certificates.Planarity_Certificates"
Presenting Van_der_Waerden in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Van_der_Waerden" ...
Presenting document Van_der_Waerden/document
Presenting document Van_der_Waerden/outline
Presenting theory "Incompleteness.Pseudo_Coding"
Presenting theory "Containers.Collection_Enum"
Presenting file "$AFP/Containers/cenum_generator.ML"
Presenting theory "HOL-Library.FuncSet"
Presenting theory "Universal_Turing_Machine.ComposableTMs"
Presenting theory "Goedel_HFSet_Semanticless.Coding"
Presenting theory "Van_der_Waerden.Digits"
Presenting theory "Van_der_Waerden.Van_der_Waerden"
Presenting VeriComp in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/VeriComp" ...
Presenting document VeriComp/document
Presenting document VeriComp/outline
Presenting theory "VeriComp.Behaviour"
Presenting theory "Universal_Turing_Machine.ComposedTMs"
Presenting theory "VeriComp.Well_founded"
Presenting theory "VeriComp.Inf"
Presenting theory "VeriComp.Transfer_Extras"
Presenting theory "VeriComp.Semantics"
Presenting theory "VeriComp.Language"
Presenting theory "VeriComp.Simulation"
Presenting theory "Goedel_HFSet_Semanticless.Predicates"
Presenting theory "VeriComp.Compiler"
Presenting theory "VeriComp.Fixpoint"
Presenting Verified-Prover in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Verified-Prover" ...
Presenting document Verified-Prover/document
Presenting document Verified-Prover/outline
Presenting theory "Deriving.Equality_Generator"
Presenting file "$AFP/Deriving/Equality_Generator/equality_generator.ML"
Presenting theory "Deriving.Equality_Instances"
Presenting theory "Goedel_HFSet_Semanticless.Sigma"
Presenting theory "Automatic_Refinement.Misc"
Presenting theory "Universal_Turing_Machine.Numerals"
Presenting theory "Containers.Collection_Eq"
Presenting file "$AFP/Containers/ceq_generator.ML"
Presenting theory "Containers.Equal"
Presenting theory "Universal_Turing_Machine.Numerals_Ex"
Presenting theory "Verified-Prover.Prover"
Presenting theory "Goedel_HFSet_Semanticless.Coding_Predicates"
Presenting Verified_SAT_Based_AI_Planning in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Verified_SAT_Based_AI_Planning" ...
Presenting theory "UPF_Firewall.NormalisationIntegerPortProof"
Presenting document Verified_SAT_Based_AI_Planning/document
Presenting document Verified_SAT_Based_AI_Planning/outline
Presenting theory "Incompleteness.Quote"
Presenting theory "Verified_SAT_Based_AI_Planning.List_Supplement"
Presenting theory "Verified_SAT_Based_AI_Planning.Map_Supplement"
Presenting theory "Goedel_HFSet_Semanticless.Pf_Predicates"
Presenting theory "Containers.DList_Set"
Presenting theory "HOL-Library.Case_Converter"
Presenting file "~~/src/HOL/Library/case_converter.ML"
Presenting theory "HOL-Library.Simps_Case_Conv"
Presenting file "~~/src/HOL/Library/simps_case_conv.ML"
Presenting theory "Propositional_Proof_Systems.CNF"
Presenting theory "Propositional_Proof_Systems.CNF_Sema"
Presenting theory "Van_Emde_Boas_Trees.Assertions"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "Incompleteness.Functions"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "Containers.List_Fusion"
Presenting theory "HOL-Library.Char_ord"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "Containers.Lexicographic_Order"
Presenting theory "Propositional_Proof_Systems.Formulas"
Presenting theory "Universal_Turing_Machine.Turing_Hoare"
Presenting theory "Van_Emde_Boas_Trees.Hoare_Triple"
Presenting theory "Propositional_Proof_Systems.CNF_Formulas"
Presenting theory "Containers.Extend_Partial_Order"
Presenting theory "Propositional_Proof_Systems.Sema"
Presenting theory "Propositional_Proof_Systems.CNF_Formulas_Sema"
Presenting theory "Van_Emde_Boas_Trees.Refine_Imp_Hol"
Presenting theory "Verified_SAT_Based_AI_Planning.CNF_Supplement"
Presenting theory "Verified_SAT_Based_AI_Planning.CNF_Semantics_Supplement"
Presenting theory "Verified_SAT_Based_AI_Planning.State_Variable_Representation"
Presenting theory "Universal_Turing_Machine.SemiIdTM"
Presenting theory "Verified_SAT_Based_AI_Planning.STRIPS_Representation"
Presenting theory "Incompleteness.Goedel_I"
Presenting theory "Goedel_HFSet_Semantic.Instance"
Presenting VolpanoSmith in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/VolpanoSmith" ...
Presenting document VolpanoSmith/document
Presenting document VolpanoSmith/outline
Presenting theory "Verified_SAT_Based_AI_Planning.STRIPS_Semantics"
Presenting theory "Universal_Turing_Machine.Turing_HaltingConditions"
Presenting theory "Verified_SAT_Based_AI_Planning.SAS_Plus_Representation"
Presenting theory "Verified_SAT_Based_AI_Planning.SAS_Plus_Semantics"
Presenting theory "Universal_Turing_Machine.OneStrokeTM"
Presenting theory "Van_Emde_Boas_Trees.Automation"
Presenting theory "Van_Emde_Boas_Trees.Sep_Main"
Presenting theory "VolpanoSmith.Semantics"
Presenting theory "Simpl.HoareTotalProps"
Presenting theory "Universal_Turing_Machine.WeakCopyTM"
Presenting theory "HOL-Imperative_HOL.Heap_Monad"
Presenting theory "Verified_SAT_Based_AI_Planning.SAS_Plus_STRIPS"
Presenting theory "Containers.Set_Linorder"
Presenting theory "VolpanoSmith.secTypes"
Presenting theory "List-Index.List_Index"
Presenting theory "Deriving.Comparator"
Presenting theory "VolpanoSmith.Execute"
Presenting theory "HOL-Imperative_HOL.Array"
Presenting WHATandWHERE_Security in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/WHATandWHERE_Security" ...
Presenting document WHATandWHERE_Security/document
Presenting document WHATandWHERE_Security/outline
Presenting theory "Strong_Security.Types"
Presenting theory "WHATandWHERE_Security.WHATWHERE_Security"
Presenting theory "HOL-Imperative_HOL.Ref"
Presenting theory "HOL-Imperative_HOL.Imperative_HOL"
Presenting theory "Van_Emde_Boas_Trees.Imperative_HOL_Add"
Presenting theory "WHATandWHERE_Security.Up_To_Technique"
Presenting theory "WHATandWHERE_Security.MWLs"
Presenting theory "Deriving.Comparator_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/comparator_generator.ML"
Presenting theory "Store_Buffer_Reduction.ReduceStoreBufferSimulation"
Presenting theory "Van_Emde_Boas_Trees.Time_Reasoning"
Presenting theory "Van_Emde_Boas_Trees.Simple_TBOUND_Cond"
Presenting theory "Deriving.Compare"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_code.ML"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Example_Setup"
Presenting theory "WHATandWHERE_Security.Parallel_Composition"
Presenting theory "Verified_SAT_Based_AI_Planning.SAT_Plan_Base"
Presenting theory "WHATandWHERE_Security.WHATWHERE_Secure_Skip_Assign"
Presenting theory "Deriving.Compare_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_generator.ML"
Presenting theory "Simpl.HoareTotal"
Presenting theory "Deriving.Compare_Instances"
Presenting theory "UPF_Firewall.NormalisationIPPProofs"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "UPF_Firewall.ElementaryRules"
Presenting theory "UPF_Firewall.FWNormalisation"
Presenting theory "UPF_Firewall.LTL_alike"
Presenting theory "Simpl.Hoare"
Presenting theory "UPF_Firewall.StatefulCore"
Presenting theory "Simpl.StateSpace"
Presenting theory "HOL-Library.Countable_Complete_Lattices"
Presenting theory "UPF_Firewall.FTP"
Presenting theory "Containers.Collection_Order"
Presenting theory "Verified_SAT_Based_AI_Planning.SAT_Plan_Extensions"
Presenting file "$AFP/Containers/ccompare_generator.ML"
Presenting theory "HOL-Library.Order_Continuity"
Presenting theory "UPF_Firewall.FTP_WithPolicy"
Presenting theory "Verified_SAT_Based_AI_Planning.SAT_Solve_SAS_Plus"
Presenting theory "AI_Planning_Languages_Semantics.SASP_Semantics"
Presenting theory "Goedel_HFSet_Semanticless.II_Prelims"
Presenting theory "HOL-Library.Extended_Nat"
Presenting theory "Store_Buffer_Reduction.PIMP"
Presenting theory "UPF_Firewall.VOIP"
Presenting theory "Store_Buffer_Reduction.SyntaxTweaks"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "Store_Buffer_Reduction.Abbrevs"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "HOL-Library.Code_Target_Numeral"
Presenting theory "Goedel_HFSet_Semanticless.Pseudo_Coding"
Presenting theory "WHATandWHERE_Security.Language_Composition"
Presenting theory "Verified_SAT_Based_AI_Planning.AST_SAS_Plus_Equivalence"
Presenting theory "UPF_Firewall.FTPVOIP"
Presenting theory "UPF_Firewall.StatefulFW"
Presenting theory "UPF_Firewall.UPF-Firewall"
Presenting theory "UPF_Firewall.DMZDatatype"
Presenting theory "UPF_Firewall.DMZInteger"
Presenting theory "UPF_Firewall.DMZ"
Presenting theory "WHATandWHERE_Security.Type_System"
Presenting theory "Strong_Security.Expr"
Presenting theory "HOL-Library.Tree"
Presenting theory "UPF_Firewall.Voice_over_IP"
Presenting theory "Strong_Security.Domain_example"
Presenting theory "HOL-Data_Structures.Tree2"
Presenting theory "HOL-Data_Structures.RBT"
Presenting theory "HOL-Data_Structures.Cmp"
Presenting theory "HOL-Data_Structures.Less_False"
Presenting theory "UPF_Firewall.Transformation01"
Presenting theory "HOL-Data_Structures.Sorted_Less"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Definitions"
Presenting theory "HOL-Data_Structures.List_Ins_Del"
Presenting theory "HOL-Data_Structures.Set_Specs"
Presenting theory "HOL-Data_Structures.Isin2"
Presenting theory "Store_Buffer_Reduction.Variants"
Presenting theory "UPF_Firewall.Transformation02"
Presenting theory "UPF_Firewall.Transformation"
Presenting theory "WHATandWHERE_Security.Type_System_example"
Presenting WOOT_Strong_Eventual_Consistency in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/WOOT_Strong_Eventual_Consistency" ...
Presenting document WOOT_Strong_Eventual_Consistency/document
Presenting document WOOT_Strong_Eventual_Consistency/outline
Presenting theory "HOL-Data_Structures.RBT_Set"
Presenting theory "UPF_Firewall.NAT-FW"
Presenting theory "Store_Buffer_Reduction.Text"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Member"
Presenting theory "UPF_Firewall.PersonalFirewallInt"
Presenting theory "HOL-Data_Structures.AList_Upd_Del"
Presenting theory "Store_Buffer_Reduction.Preliminaries"
Presenting Weight_Balanced_Trees in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Weight_Balanced_Trees" ...
Presenting document Weight_Balanced_Trees/document
Presenting document Weight_Balanced_Trees/outline
Presenting theory "HOL-Data_Structures.Map_Specs"
Presenting theory "HOL-Data_Structures.Lookup2"
Presenting theory "UPF_Firewall.PersonalFirewallIpv4"
Presenting theory "UPF_Firewall.PersonalFirewallDatatype"
Presenting theory "UPF_Firewall.PersonalFirewall"
Presenting theory "UPF_Firewall.Examples"
Presenting Weighted_Arithmetic_Geometric_Mean in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Weighted_Arithmetic_Geometric_Mean" ...
Presenting document Weighted_Arithmetic_Geometric_Mean/document
Presenting document Weighted_Arithmetic_Geometric_Mean/outline
Presenting theory "HOL-Data_Structures.RBT_Map"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "Certification_Monads.Error_Syntax"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "HOL-Library.Tree"
Presenting theory "Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean"
Presenting theory "Weight_Balanced_Trees.Weight_Balanced_Trees_log"
Presenting Word_Lib in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Word_Lib" ...
Presenting theory "AI_Planning_Languages_Semantics.SASP_Checker"
Presenting document Word_Lib/document
Presenting document Word_Lib/outline
Presenting theory "HOL-Data_Structures.Tree2"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "HOL-Data_Structures.Cmp"
Presenting theory "HOL-Data_Structures.Less_False"
Presenting theory "HOL-Data_Structures.Sorted_Less"
Presenting theory "HOL-Data_Structures.List_Ins_Del"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "HOL-Data_Structures.Set2_Join"
Presenting theory "Certification_Monads.Error_Monad"
Presenting theory "HOL-Data_Structures.Set_Specs"
Presenting theory "HOL-Data_Structures.Isin2"
Presenting theory "WOOT_Strong_Eventual_Consistency.ErrorMonad"
Presenting theory "Verified_SAT_Based_AI_Planning.Set2_Join_RBT"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "HOL-Library.Numeral_Type"
Presenting theory "HOL-Library.Type_Length"
Presenting theory "Word_Lib.More_Arithmetic"
Presenting theory "Word_Lib.Even_More_List"
Presenting theory "Datatype_Order_Generator.Derive_Aux"
Presenting file "$AFP/Datatype_Order_Generator/derive_aux.ML"
Presenting theory "Weight_Balanced_Trees.Weight_Balanced_Trees"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Insert"
Presenting Complx in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Complx" ...
Presenting document Complx/document
Presenting document Complx/outline
Presenting theory "Verified_SAT_Based_AI_Planning.Solve_SASP"
Presenting IEEE_Floating_Point in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/IEEE_Floating_Point" ...
Presenting document IEEE_Floating_Point/document
Presenting document IEEE_Floating_Point/outline
Presenting theory "Complx.Language"
Presenting theory "HOL-Library.Log_Nat"
Presenting theory "Universal_Turing_Machine.StrongCopyTM"
Presenting theory "HOL-Library.Lattice_Algebras"
Presenting theory "Goedel_HFSet_Semanticless.Quote"
Presenting theory "Datatype_Order_Generator.Order_Generator"
Presenting file "$AFP/Datatype_Order_Generator/order_generator.ML"
Presenting theory "WOOT_Strong_Eventual_Consistency.Data"
Presenting theory "WOOT_Strong_Eventual_Consistency.BasicAlgorithms"
Presenting theory "WOOT_Strong_Eventual_Consistency.CreateAlgorithms"
Presenting theory "WOOT_Strong_Eventual_Consistency.IntegrateAlgorithm"
Presenting theory "HOL-Library.Product_Lexorder"
Presenting theory "WOOT_Strong_Eventual_Consistency.DistributedExecution"
Presenting theory "HOL-Library.List_Lexorder"
Presenting theory "WOOT_Strong_Eventual_Consistency.SortKeys"
Presenting theory "Universal_Turing_Machine.TuringDecidable"
Presenting theory "Complx.SmallStep"
Presenting theory "Universal_Turing_Machine.TuringReducible"
Presenting theory "HOL-Library.RBT_Impl"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "Complx.OG_Annotations"
Presenting theory "HOL-Library.Sublist"
Presenting theory "Universal_Turing_Machine.SimpleGoedelEncoding"
Presenting theory "Containers.RBT_ext"
Presenting theory "Word_Lib.More_Sublist"
Presenting theory "Word_Lib.More_Misc"
Presenting theory "Goedel_HFSet_Semanticless.Functions"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting theory "Deriving.RBT_Comparator_Impl"
Presenting theory "HOL-Library.Float"
Presenting theory "Universal_Turing_Machine.HaltingProblems_K_H"
Presenting theory "WOOT_Strong_Eventual_Consistency.Psi"
Presenting theory "IEEE_Floating_Point.IEEE"
Presenting theory "Containers.RBT_Mapping2"
Presenting theory "Van_Emde_Boas_Trees.VEBT_InsertCorrectness"
Presenting theory "Universal_Turing_Machine.HaltingProblems_K_aux"
Presenting theory "Complx.OG_Hoare"
Presenting theory "IEEE_Floating_Point.IEEE_Properties"
Presenting theory "Containers.RBT_Set2"
Presenting theory "Containers.Closure_Set"
Presenting theory "IEEE_Floating_Point.FP64"
Presenting theory "HOL-Library.Sublist"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "Van_Emde_Boas_Trees.VEBT_MinMax"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "WOOT_Strong_Eventual_Consistency.Sorting"
Presenting theory "Complx.SeqCatch_decomp"
Presenting theory "Goedel_HFSet_Semanticless.Goedel_I"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "HOL-Library.Code_Target_Numeral"
Presenting theory "WOOT_Strong_Eventual_Consistency.Consistency"
Presenting theory "IEEE_Floating_Point.Conversion_IEEE_Float"
Presenting theory "Goedel_HFSet_Semanticless.Instance"
Presenting IP_Addresses in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/IP_Addresses" ...
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting document IP_Addresses/document
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting document IP_Addresses/outline
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "IEEE_Floating_Point.Double"
Presenting Simple_Firewall in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Simple_Firewall" ...
Presenting document Simple_Firewall/document
Presenting document Simple_Firewall/outline
Presenting theory "Simple_Firewall.Lib_Enum_toString"
Presenting theory "WOOT_Strong_Eventual_Consistency.CreateConsistent"
Presenting theory "Simple_Firewall.L4_Protocol"
Presenting theory "Simple_Firewall.Simple_Packet"
Presenting theory "Simple_Firewall.Firewall_Common_Decision_State"
Presenting theory "HOL-Library.Char_ord"
Presenting theory "HOL-Library.Cancellation"
Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
Presenting theory "Universal_Turing_Machine.TuringComputable"
Presenting theory "Simpl.AlternativeSmallStep"
Presenting theory "Universal_Turing_Machine.DitherTM"
Presenting theory "Simple_Firewall.Iface"
Presenting theory "Simple_Firewall.SimpleFw_Syntax"
Presenting theory "Simpl.Simpl_Heap"
Presenting theory "Simple_Firewall.SimpleFw_Semantics"
Presenting theory "WOOT_Strong_Eventual_Consistency.IntegrateInsertCommute"
Presenting theory "Simple_Firewall.List_Product_More"
Presenting theory "Simple_Firewall.Option_Helpers"
Presenting theory "Simpl.HeapList"
Presenting theory "Complx.OG_Soundness"
Presenting theory "Simple_Firewall.Generic_SimpleFw"
Presenting theory "Universal_Turing_Machine.CopyTM"
Presenting theory "Simple_Firewall.Shadowed"
Presenting theory "Complx.Cache_Tactics"
Presenting theory "WOOT_Strong_Eventual_Consistency.StrongConvergence"
Presenting theory "Simple_Firewall.IP_Partition_Preliminaries"
Presenting theory "Universal_Turing_Machine.TuringUnComputable_H2"
Presenting theory "WOOT_Strong_Eventual_Consistency.SEC"
Presenting theory "Simple_Firewall.GroupF"
Presenting theory "Simple_Firewall.IP_Addr_WordInterval_toString"
Presenting theory "Simple_Firewall.Primitives_toString"
Presenting theory "Universal_Turing_Machine.TuringUnComputable_H2_original"
Presenting theory "WOOT_Strong_Eventual_Consistency.Example"
Presenting Routing in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Routing" ...
Presenting document Routing/document
Presenting document Routing/outline
Presenting theory "Routing.Linorder_Helper"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Succ"
Presenting theory "Complx.OG_Tactics"
Presenting theory "Pure-ex.Guess"
Presenting theory "Simple_Firewall.Service_Matrix"
Presenting theory "HOL-Statespace.DistinctTreeProver"
Presenting file "~~/src/HOL/Statespace/distinct_tree_prover.ML"
Presenting theory "Simple_Firewall.SimpleFw_toString"
Presenting theory "Complx.OG_Syntax"
Presenting Iptables_Semantics in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Iptables_Semantics" ...
Presenting document Iptables_Semantics/document
Presenting document Iptables_Semantics/outline
Presenting theory "Iptables_Semantics.List_Misc"
Presenting theory "HOL-Statespace.StateFun"
Presenting theory "Iptables_Semantics.Negation_Type"
Presenting theory "Complx.Examples"
Presenting theory "Iptables_Semantics.WordInterval_Lists"
Presenting theory "HOL-Library.Word"
Presenting theory "Iptables_Semantics.Repeat_Stabilize"
Presenting theory "Routing.Routing_Table"
Presenting theory "Universal_Turing_Machine.Abacus_Mopup"
Presenting theory "Iptables_Semantics.Firewall_Common"
Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
Presenting theory "HOL-Library.LaTeXsugar"
Presenting theory "Containers.Set_Impl"
Presenting file "$AFP/Containers/set_impl_generator.ML"
Presenting theory "HOL-Library.Multiset"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "Word_Lib.More_Divides"
Presenting theory "Routing.Linux_Router"
Presenting theory "HOL-ex.Quicksort"
Presenting theory "Iptables_Semantics.Semantics"
Presenting theory "Iptables_Semantics.Matching"
Presenting theory "HOL-Library.Option_ord"
Presenting theory "Complx.SumArr"
Presenting Iptables_Semantics_Examples in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Iptables_Semantics_Examples" ...
Presenting document Iptables_Semantics_Examples/document
Presenting document Iptables_Semantics_Examples/outline
Presenting theory "Routing.IpRoute_Parser"
Presenting file "$AFP/Routing/IpRoute_Parser.ml"
Presenting LOFT in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LOFT" ...
Presenting document LOFT/document
Presenting document LOFT/outline
Presenting theory "Iptables_Semantics.Ruleset_Update"
Presenting theory "LOFT.OpenFlow_Helpers"
Presenting theory "LOFT.Sort_Descending"
Presenting theory "LOFT.List_Group"
Presenting theory "HOL-Library.List_Lexorder"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "Iptables_Semantics.Call_Return_Unfolding"
Presenting theory "LOFT.OpenFlow_Matches"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Pred"
Presenting theory "LOFT.OpenFlow_Action"
Presenting theory "Iptables_Semantics.Ternary"
Presenting theory "Iptables_Semantics.Matching_Ternary"
Presenting theory "HOL-Statespace.StateSpaceLocale"
Presenting file "~~/src/HOL/Statespace/state_space.ML"
Presenting file "~~/src/HOL/Statespace/state_fun.ML"
Presenting theory "Jordan_Normal_Form.Matrix_Kernel"
Presenting theory "LOFT.Semantics_OpenFlow"
Presenting theory "Iptables_Semantics.Semantics_Ternary"
Presenting theory "LOFT.OpenFlow_Serialize"
Presenting theory "Iptables_Semantics.Datatype_Selectors"
Presenting theory "Word_Lib.More_Word"
Presenting theory "Iptables_Semantics.IpAddresses"
Presenting theory "Iptables_Semantics.L4_Protocol_Flags"
Presenting theory "Iptables_Semantics.Ports"
Presenting theory "Simpl.Generalise"
Presenting file "$AFP/Simpl/generalise_state.ML"
Presenting theory "Iptables_Semantics.Conntrack_State"
Presenting theory "Iptables_Semantics.Tagged_Packet"
Presenting theory "Word_Lib.Strict_part_mono"
Presenting theory "LOFT.Featherweight_OpenFlow_Comparison"
Presenting theory "Iptables_Semantics.Common_Primitive_Syntax"
Presenting theory "Iptables_Semantics.Unknown_Match_Tacs"
Presenting theory "Iptables_Semantics.Common_Primitive_Matcher_Generic"
Presenting theory "Complex_Bounded_Operators.Cblinfun_Code"
Presenting theory "Iptables_Semantics.Common_Primitive_Matcher"
Presenting theory "HOL-Examples.Sqrt"
Presenting theory "Iptables_Semantics.Example_Semantics"
Presenting theory "Word_Lib.Many_More"
Presenting theory "Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary"
Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"
Presenting theory "Iptables_Semantics_Examples.Parser_Test"
Presenting theory "Sqrt_Babylonian.Log_Impl"
Presenting theory "Iptables_Semantics_Examples.Parser6_Test"
Presenting theory "Iptables_Semantics.Alternative_Semantics"
Presenting theory "Iptables_Semantics_Examples.Small_Examples"
Presenting theory "LOFT.LinuxRouter_OpenFlow_Translation"
Presenting theory "Iptables_Semantics_Examples.Ports_Fail"
Presenting theory "Iptables_Semantics_Examples.Contrived_Example"
Presenting theory "Iptables_Semantics.Semantics_Stateful"
Presenting theory "Iptables_Semantics_Examples.iptables_Ln_tuned_parsed"
Presenting theory "LOFT.OF_conv_test"
Presenting theory "LOFT.RFC2544"
Presenting theory "Automatic_Refinement.Misc"
Presenting theory "Word_Lib.Aligned"
Presenting theory "Iptables_Semantics_Examples.Analyze_Synology_Diskstation"
Presenting theory "Iptables_Semantics.Semantics_Goto"
Presenting theory "Word_Lib.Next_and_Prev"
Presenting theory "LOFT.OpenFlow_Documentation"
Presenting Interval_Arithmetic_Word32 in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Interval_Arithmetic_Word32" ...
Presenting document Interval_Arithmetic_Word32/document
Presenting document Interval_Arithmetic_Word32/outline
Presenting theory "HOL-Library.Signed_Division"
Presenting theory "Iptables_Semantics.Negation_Type_DNF"
Presenting theory "IP_Addresses.NumberWang_IPv4"
Presenting theory "Iptables_Semantics.Matching_Embeddings"
Presenting theory "Word_Lib.Signed_Division_Word"
Presenting theory "IP_Addresses.NumberWang_IPv6"
Presenting theory "Word_Lib.Bit_Comprehension"
Presenting theory "Cauchy.CauchysMeanTheorem"
Presenting theory "Word_Lib.Most_significant_bit"
Presenting theory "Word_Lib.Least_significant_bit"
Presenting theory "Iptables_Semantics.Fixed_Action"
Presenting theory "Word_Lib.Generic_set_bit"
Presenting theory "Iptables_Semantics.Normalized_Matches"
Presenting theory "IP_Addresses.WordInterval"
Presenting theory "Iptables_Semantics.Negation_Type_Matching"
Presenting theory "IP_Addresses.Hs_Compat"
Presenting theory "Iptables_Semantics_Examples.Analyze_Ringofsaturn_com"
Presenting theory "IP_Addresses.IP_Address"
Presenting theory "IP_Addresses.IPv4"
Presenting theory "Universal_Turing_Machine.Abacus"
Presenting theory "Iptables_Semantics.Primitive_Normalization"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Delete"
Presenting theory "Iptables_Semantics.MatchExpr_Fold"
Presenting theory "Iptables_Semantics.Common_Primitive_Lemmas"
Presenting theory "Sqrt_Babylonian.NthRoot_Impl"
Presenting theory "Universal_Turing_Machine.Abacus_alt_Compile"
Presenting theory "Word_Lib.Bits_Int"
Presenting theory "Sqrt_Babylonian.Sqrt_Babylonian"
Presenting theory "Word_Lib.Typedef_Morphisms"
Presenting theory "Word_Lib.Singleton_Bit_Shifts"
Presenting theory "Word_Lib.Legacy_Aliases"
Presenting theory "Iptables_Semantics.Ports_Normalize"
Presenting theory "Iptables_Semantics.IpAddresses_Normalize"
Presenting theory "Universal_Turing_Machine.Abacus_Hoare"
Presenting theory "Iptables_Semantics.Interfaces_Normalize"
Presenting theory "Iptables_Semantics.Word_Upto"
Presenting theory "IP_Addresses.IPv6"
Presenting theory "Universal_Turing_Machine.Rec_Def"
Presenting theory "Real_Impl.Real_Impl"
Presenting theory "Universal_Turing_Machine.Rec_Ex"
Presenting theory "Iptables_Semantics.Protocols_Normalize"
Presenting theory "Iptables_Semantics.Remdups_Rev"
Presenting theory "IP_Addresses.Prefix_Match"
Presenting theory "Interval_Arithmetic_Word32.Interval_Word32"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "Iptables_Semantics.Ipassmt"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "IP_Addresses.CIDR_Split"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "HOL-Library.Product_Lexorder"
Presenting theory "HOL-Library.Code_Target_Numeral"
Presenting theory "IP_Addresses.WordInterval_Sorted"
Presenting theory "Iptables_Semantics.No_Spoof"
Presenting theory "HOL-Library.IArray"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "Interval_Arithmetic_Word32.Finite_String"
Presenting theory "Word_Lib.Reversed_Bit_Lists"
Presenting theory "Iptables_Semantics.Common_Primitive_toString"
Presenting theory "Iptables_Semantics.Routing_IpAssmt"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "Iptables_Semantics.Output_Interface_Replace"
Presenting theory "Jordan_Normal_Form.Matrix_IArray_Impl"
Presenting theory "Iptables_Semantics.Interface_Replace"
Presenting theory "Iptables_Semantics.Optimizing"
Presenting theory "Jordan_Normal_Form.Gauss_Jordan_IArray_Impl"
Presenting theory "Word_Lib.Bitwise"
Presenting theory "Interval_Arithmetic_Word32.Interpreter"
Presenting theory "Word_Lib.Examples"
Presenting Native_Word in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Native_Word" ...
Presenting document Native_Word/document
Presenting document Native_Word/outline
Presenting file "$AFP/Simpl/hoare.ML"
Presenting file "$AFP/Simpl/hoare_syntax.ML"
Presenting theory "Word_Lib.Bit_Comprehension_Int"
Presenting theory "Native_Word.Code_Target_Word_Base"
Presenting theory "Simpl.SyntaxTest"
Presenting theory "Word_Lib.Signed_Words"
Presenting theory "Word_Lib.Bitwise_Signed"
Presenting theory "Word_Lib.Enumeration"
Presenting theory "Iptables_Semantics.Transform"
Presenting theory "Native_Word.Word_Type_Copies"
Presenting theory "Native_Word.Code_Int_Integer_Conversion"
Presenting theory "Word_Lib.Enumeration_Word"
Presenting theory "Word_Lib.Hex_Words"
Presenting theory "Van_Emde_Boas_Trees.VEBT_DeleteCorrectness"
Presenting theory "Word_Lib.Norm_Words"
Presenting theory "Iptables_Semantics.Conntrack_State_Transform"
Presenting theory "Native_Word.Code_Target_Integer_Bit"
Presenting theory "Iptables_Semantics_Examples.Analyze_SQRL_Shorewall"
Presenting theory "Word_Lib.Rsplit"
Presenting theory "Word_Lib.Syntax_Bundles"
Presenting theory "Word_Lib.Type_Syntax"
Presenting theory "Jordan_Normal_Form.Determinant_Impl"
Presenting theory "Iptables_Semantics.Primitive_Abstract"
Presenting theory "Iptables_Semantics_Examples.SQRL_2015_nospoof"
Presenting theory "Simpl.VcgEx"
Presenting theory "Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing"
Presenting theory "Native_Word.Uint64"
Presenting theory "Iptables_Semantics.SimpleFw_Compliance"
Presenting theory "Native_Word.Uint32"
Presenting theory "Iptables_Semantics_Examples.Analyze_medium_sized_company"
Presenting X86_Semantics in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/X86_Semantics" ...
Presenting document X86_Semantics/document
Presenting document X86_Semantics/outline
Presenting theory "Iptables_Semantics.Semantics_Embeddings"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "Simpl.VcgExSP"
Presenting theory "Iptables_Semantics.Iptables_Semantics"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "Native_Word.Code_Int_Integer_Conversion"
Presenting theory "Native_Word.Uint16"
Presenting theory "Native_Word.Code_Target_Integer_Bit"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "Native_Word.Code_Target_Int_Bit"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Uniqueness"
Presenting theory "Simpl.VcgExTotal"
Presenting theory "Iptables_Semantics.Code_Interface"
Presenting theory "Native_Word.Uint8"
Presenting theory "HOL-Library.Cancellation"
Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
Presenting file "$AFP/Show/show_generator.ML"
Presenting theory "HOL-Library.Numeral_Type"
Presenting theory "Jordan_Normal_Form.Show_Matrix"
Presenting theory "HOL-Library.Type_Length"
Presenting theory "Native_Word.Uint"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Height"
Presenting theory "Native_Word.Native_Cast"
Presenting theory "Native_Word.Native_Cast_Uint"
Presenting theory "Iptables_Semantics.Parser6"
Presenting theory "Iptables_Semantics.No_Spoof_Embeddings"
Presenting theory "HOL-Library.Old_Datatype"
Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "Iptables_Semantics.Parser"
Presenting theory "Iptables_Semantics.Code_haskell"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "Iptables_Semantics.Access_Matrix_Embeddings"
Presenting theory "Iptables_Semantics.Documentation"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
Presenting ZFC_in_HOL in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/ZFC_in_HOL" ...
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting document ZFC_in_HOL/document
Presenting document ZFC_in_HOL/outline
Presenting theory "HOL-Eisbach.Eisbach_Tools"
Presenting theory "Word_Lib.Word_EqI"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "IP_Addresses.IP_Address_Parser"
Presenting theory "IP_Addresses.Lib_Numbers_toString"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Imperative_HOL.Heap"
Presenting theory "IP_Addresses.Lib_Word_toString"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "IP_Addresses.Lib_List_toString"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "IP_Addresses.IP_Address_toString"
Presenting theory "IP_Addresses.Prefix_Match_toString"
Presenting CZH_Foundations in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CZH_Foundations" ...
Presenting document CZH_Foundations/document
Presenting document CZH_Foundations/outline
Presenting theory "CZH_Foundations.CZH_Sets_MIF"
Presenting theory "CZH_Foundations.CZH_Utilities"
Presenting theory "CZH_Foundations.CZH_Introduction"
Presenting theory "Intro_Dest_Elim.IDE_Tools"
Presenting file "$AFP/Intro_Dest_Elim/IDE_Tools/IDE_Utilities.ML"
Presenting theory "HOL-Library.FuncSet"
Presenting theory "Word_Lib.Word_Lemmas"
Presenting theory "Intro_Dest_Elim.IHOL_IDE"
Presenting file "$AFP/Intro_Dest_Elim/IDE.ML"
Presenting theory "HOL-Library.Equipollence"
Presenting theory "Conditional_Simplification.CS_Tools"
Presenting file "$AFP/Conditional_Simplification/CS_Tools/More_Tactical.ML"
Presenting file "$AFP/Conditional_Simplification/CS_Tools/CS_Stats.ML"
Presenting theory "HOL-Cardinals.Fun_More"
Presenting theory "Word_Lib.Word_8"
Presenting theory "Word_Lib.Word_16"
Presenting theory "Word_Lib.Word_Syntax"
Presenting theory "Word_Lib.Word_Names"
Presenting theory "HOL-Cardinals.Order_Relation_More"
Presenting theory "HOL-Cardinals.Wellfounded_More"
Presenting theory "HOL-Imperative_HOL.Heap_Monad"
Presenting theory "Native_Word.Native_Word_Imperative_HOL"
Presenting theory "HOL-Cardinals.Wellorder_Relation"
Presenting theory "HOL-Library.Word"
Presenting theory "HOL-Cardinals.Wellorder_Embedding"
Presenting theory "HOL-Library.Multiset"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
Presenting theory "HOL-Cardinals.Order_Union"
Presenting theory "Word_Lib.Syntax_Bundles"
Presenting theory "Word_Lib.More_Word_Operations"
Presenting theory "Simpl.Quicksort"
Presenting theory "Simpl.XVcg"
Presenting theory "Word_Lib.More_Arithmetic"
Presenting theory "Simpl.XVcgEx"
Presenting theory "Word_Lib.Word_32"
Presenting theory "Universal_Turing_Machine.Recursive"
Presenting theory "Word_Lib.Word_Lib_Sumo"
Presenting theory "Word_Lib.Machine_Word_32_Basics"
Presenting theory "Word_Lib.More_Divides"
Presenting theory "HOL-Library.Code_Test"
Presenting file "~~/src/HOL/Library/code_test.ML"
Presenting theory "Simpl.ProcParEx"
Presenting theory "Word_Lib.Machine_Word_32"
Presenting theory "Word_Lib.Word_64"
Presenting theory "HOL-Cardinals.Wellorder_Constructions"
Presenting theory "Word_Lib.Machine_Word_64_Basics"
Presenting theory "Word_Lib.Machine_Word_64"
Presenting theory "Word_Lib.Guide"
Presenting CZH_Elementary_Categories in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CZH_Elementary_Categories" ...
Presenting document CZH_Elementary_Categories/document
Presenting document CZH_Elementary_Categories/outline
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Introduction"
Presenting theory "Conditional_Simplification.IHOL_CS"
Presenting file "$AFP/Conditional_Simplification/CS_TimeIt.ML"
Presenting file "$AFP/Conditional_Simplification/CS_UM.ML"
Presenting file "$AFP/Conditional_Simplification/CS_Cond_Simp.ML"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Bounds"
Presenting theory "Simpl.ProcParExSP"
Presenting theory "HOL-Library.Discrete"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Category"
Presenting theory "Simpl.Closure"
Presenting theory "HOL-Cardinals.Ordinal_Arithmetic"
Presenting theory "Universal_Turing_Machine.Recs_alt_Def"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Small_Category"
Presenting theory "Universal_Turing_Machine.Recs_alt_Ex"
Presenting theory "Simpl.ClosureEx"
Presenting theory "Word_Lib.More_Word"
Presenting theory "HOL-Cardinals.Cardinal_Order_Relation"
Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"
Presenting theory "Word_Lib.Bit_Comprehension"
Presenting theory "Word_Lib.Most_significant_bit"
Presenting theory "Word_Lib.Least_significant_bit"
Presenting theory "HOL-Cardinals.Cardinal_Arithmetic"
Presenting theory "Word_Lib.Generic_set_bit"
Presenting theory "HOL-Cardinals.Wellorder_Extension"
Presenting theory "HOL-Cardinals.Cardinals"
Presenting theory "ZFC_in_HOL.ZFC_Library"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Functor"
Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form_Existence"
Presenting theory "ZFC_in_HOL.ZFC_in_HOL"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Small_Functor"
Presenting theory "Word_Lib.Bits_Int"
Presenting theory "Show.Show_Instances"
Presenting theory "Jordan_Normal_Form.Matrix_Impl"
Presenting theory "Complex_Bounded_Operators.Extra_Pretty_Code_Examples"
Presenting theory "Word_Lib.Typedef_Morphisms"
Presenting theory "Complex_Bounded_Operators.Cblinfun_Code_Examples"
Presenting theory "Simpl.Compose"
Presenting theory "Word_Lib.Even_More_List"
Presenting theory "ZFC_in_HOL.ZFC_Cardinals"
Presenting theory "Simpl.ComposeEx"
Presenting theory "HOL-Statespace.StateSpaceSyntax"
Presenting theory "Van_Emde_Boas_Trees.VEBT_DeleteBounds"
Presenting theory "HOL-Library.LaTeXsugar"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_NTCF"
Presenting theory "ZFC_in_HOL.Kirby"
Presenting theory "Simpl.UserGuide"
Presenting theory "Simpl.Simpl"
Presenting CZH_Universal_Constructions in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CZH_Universal_Constructions" ...
Presenting theory "HOL-Library.Sublist"
Presenting document CZH_Universal_Constructions/document
Presenting document CZH_Universal_Constructions/outline
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Introduction"
Presenting theory "ZFC_in_HOL.Ordinal_Exp"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Small_NTCF"
Presenting theory "Native_Word.Native_Word_Test"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Space"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "ZFC_in_HOL.Cantor_NF"
Presenting theory "Native_Word.Code_Target_Int_Bit"
Presenting theory "Native_Word.Native_Word_Test_Emu"
Presenting theory "Native_Word.Native_Word_Test_PolyML"
Presenting theory "Native_Word.Native_Word_Test_PolyML2"
Presenting theory "Native_Word.Native_Word_Test_PolyML64"
Presenting theory "Native_Word.Native_Word_Test_Scala"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting theory "Native_Word.Native_Word_Test_GHC"
Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
Presenting theory "Native_Word.Native_Word_Test_MLton"
Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
Presenting theory "Native_Word.Native_Word_Test_MLton2"
Presenting theory "Native_Word.Native_Word_Test_OCaml"
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting theory "Native_Word.Native_Word_Test_OCaml2"
Presenting theory "Native_Word.Native_Word_Test_SMLNJ"
Presenting theory "Native_Word.Native_Word_Test_SMLNJ2"
Presenting theory "CZH_Foundations.CZH_Sets_Introduction"
Presenting theory "ZFC_in_HOL.ZFC_Typeclasses"
Presenting theory "Native_Word.Uint_Userguide"
Presenting HOL-Proofs in "/media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs" ...
Presenting HOL-Proofs-Extraction in "/media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Extraction" ...
Presenting document HOL-Proofs-Extraction/document
Presenting document HOL-Proofs-Extraction/outline
Presenting theory "HOL-Proofs-Extraction.Util"
Presenting theory "HOL-Proofs-Extraction.QuotRem"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Intf_Functional"
Presenting theory "Word_Lib.Aligned"
Presenting theory "HOL-Proofs-Extraction.Greatest_Common_Divisor"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Universal"
Presenting theory "Word_Lib.Singleton_Bit_Shifts"
Presenting theory "Word_Lib.Legacy_Aliases"
Presenting theory "HOL-Proofs-Extraction.Warshall"
Presenting theory "HOL-Proofs-Extraction.Higman"
Presenting theory "HOL-Library.Open_State_Syntax"
Presenting theory "HOL-Proofs-Extraction.Higman_Extraction"
Presenting theory "CZH_Foundations.CZH_Sets_Sets"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "CZH_Foundations.CZH_Sets_Nat"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "HOL-Library.Code_Target_Numeral"
Presenting theory "Universal_Turing_Machine.UF"
Presenting theory "HOL-Proofs-Extraction.Pigeonhole"
Presenting theory "HOL-Library.Cancellation"
Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Limit"
Presenting theory "HOL-Library.Rewrite"
Presenting file "~~/src/HOL/Library/cconv.ML"
Presenting file "~~/src/HOL/Library/rewrite.ML"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Limit_IT"
Presenting theory "Word_Lib.Reversed_Bit_Lists"
Presenting theory "Van_Emde_Boas_Trees.VEBT_List_Assn"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Limit_Product"
Presenting theory "Word_Lib.Bitwise"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_PCategory"
Presenting theory "X86_Semantics.BitByte"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Limit_Pullback"
Presenting theory "CZH_Foundations.CZH_Sets_BRelations"
Presenting theory "X86_Semantics.Memory"
Presenting theory "Deriving.Generator_Aux"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Subcategory"
Presenting theory "X86_Semantics.State"
Presenting theory "Deriving.Comparator"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Simple"
Presenting theory "CZH_Foundations.CZH_Sets_IF"
Presenting theory "CZH_Foundations.CZH_Sets_Equipollence"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Limit_Equalizer"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Discrete"
Presenting theory "CZH_Foundations.CZH_Sets_Cardinality"
Presenting theory "CZH_Foundations.CZH_Sets_Ordinals"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Pointed"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_SS"
Presenting theory "X86_Semantics.X86_InstructionSemantics"
Presenting theory "HOL-Library.Multiset"
Presenting theory "CZH_Foundations.CZH_Sets_FSequences"
Presenting theory "Deriving.Comparator_Generator"
Presenting theory "Tools.Code_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/comparator_generator.ML"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Representable"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting file "~~/src/Tools/cache_io.ML"
Presenting file "~~/src/Tools/Code/code_preproc.ML"
Presenting file "~~/src/Tools/Code/code_symbol.ML"
Presenting file "~~/src/Tools/Code/code_thingol.ML"
Presenting file "~~/src/Tools/Code/code_simp.ML"
Presenting file "~~/src/Tools/Code/code_printer.ML"
Presenting theory "Deriving.Compare"
Presenting file "~~/src/Tools/Code/code_target.ML"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_code.ML"
Presenting file "~~/src/Tools/Code/code_namespace.ML"
Presenting file "~~/src/Tools/Code/code_ml.ML"
Presenting file "~~/src/Tools/Code/code_haskell.ML"
Presenting file "~~/src/Tools/Code/code_scala.ML"
Presenting file "~~/src/Tools/Code/code_runtime.ML"
Presenting file "~~/src/Tools/nbe.ML"
Presenting theory "Deriving.Compare_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_generator.ML"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Parallel"
Presenting theory "HOL-Library.Char_ord"
Presenting theory "Deriving.Compare_Instances"
Presenting theory "CZH_Foundations.CZH_Sets_FBRelations"
Presenting theory "Universal_Turing_Machine.UTM"
Presenting theory "Deriving.Equality_Generator"
Presenting file "$AFP/Deriving/Equality_Generator/equality_generator.ML"
Presenting theory "Deriving.Equality_Instances"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "Universal_Turing_Machine.GeneratedCode"
Presenting HOL-Proofs-Lambda in "/media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Lambda" ...
Presenting document HOL-Proofs-Lambda/document
Presenting document HOL-Proofs-Lambda/outline
Presenting theory "HOL-Proofs-Lambda.Lambda"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "CZH_Foundations.CZH_Sets_VNHS"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Complete"
Presenting theory "HOL-Proofs-Lambda.Commutation"
Presenting theory "HOL-Proofs-Lambda.ParRed"
Presenting theory "CZH_Foundations.CZH_Sets_NOP"
Presenting theory "HOL-Library.Numeral_Type"
Presenting theory "HOL-Proofs-Lambda.Eta"
Presenting theory "HOL-Library.Type_Length"
Presenting theory "HOL-Proofs-Lambda.ListApplication"
Presenting theory "HOL-Computational_Algebra.Factorial_Ring"
Presenting theory "HOL-Proofs-Lambda.LambdaType"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Comma"
Presenting theory "HOL-Proofs-Lambda.ListOrder"
Presenting theory "HOL-Proofs-Lambda.ListBeta"
Presenting theory "HOL-Proofs-Lambda.InductTermi"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting theory "HOL-Proofs-Lambda.StrongNorm"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Set"
Presenting theory "HOL-Proofs-Lambda.NormalForm"
Presenting theory "HOL-Library.Rewrite"
Presenting file "~~/src/HOL/Library/cconv.ML"
Presenting file "~~/src/HOL/Library/rewrite.ML"
Presenting theory "CZH_Foundations.HOL_CContinuum"
Presenting theory "HOL-Proofs-Lambda.Standardization"
Presenting theory "HOL-Computational_Algebra.Euclidean_Algorithm"
Presenting theory "X86_Semantics.StateCleanUp"
Presenting file "$AFP/X86_Semantics/MySubst.ML"
Presenting theory "X86_Semantics.SymbolicExecution"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "X86_Semantics.Examples"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Comma"
Presenting theory "X86_Semantics.X86_Parse"
Presenting file "$AFP/X86_Semantics/X86_Parse.ML"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Rel"
Presenting theory "X86_Semantics.Example_WC"
Presenting HOL-Proofs-ex in "/media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-ex" ...
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Par"
Presenting theory "HOL-Computational_Algebra.Primes"
Presenting theory "HOL-Proofs-ex.Hilbert_Classical"
Presenting theory "HOL-Proofs-Lambda.WeakNorm"
Presenting theory "HOL-Proofs-ex.Proof_Terms"
Presenting theory "HOL-Examples.Drinker"
Presenting theory "HOL-Proofs-ex.XML_Data"
Presenting theory "CZH_Foundations.CZH_Sets_ZQR"
Presenting theory "HOL-Proofs-Extraction.Euclid"
Presenting theory "CZH_Foundations.CZH_EX_Replacement"
Presenting theory "CZH_Foundations.CZH_EX_TS"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Set"
Presenting theory "CZH_Foundations.CZH_EX_Algebra"
Presenting theory "CZH_Foundations.CZH_Sets_Conclusions"
Presenting theory "CZH_Foundations.CZH_DG_Introduction"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_GRPH"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_SemiCAT"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Adjoints"
Presenting theory "CZH_Elementary_Categories.CZH_DG_CAT"
Presenting theory "CZH_Foundations.CZH_DG_Digraph"
Presenting theory "HOL-Library.Word"
Presenting theory "CZH_Foundations.CZH_DG_Small_Digraph"
Presenting theory "CZH_Elementary_Categories.CZH_SMC_CAT"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_CAT"
Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
Presenting theory "Word_Lib.More_Arithmetic"
Presenting theory "CZH_Elementary_Categories.CZH_DG_FUNCT"
Presenting theory "Word_Lib.More_Divides"
Presenting theory "CZH_Elementary_Categories.CZH_SMC_FUNCT"
Presenting theory "CZH_Foundations.CZH_DG_DGHM"
Presenting theory "Word_Lib.More_Word"
Presenting theory "CZH_Foundations.CZH_DG_Small_DGHM"
Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"
Presenting theory "Word_Lib.Most_significant_bit"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_FUNCT"
Presenting theory "Word_Lib.Least_significant_bit"
Presenting theory "CZH_Foundations.CZH_DG_TDGHM"
Presenting theory "Word_Lib.Generic_set_bit"
Presenting theory "Word_Lib.Bit_Comprehension"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Kan"
Presenting theory "HOL-Library.Signed_Division"
Presenting theory "Word_Lib.Signed_Division_Word"
Presenting theory "CZH_Foundations.CZH_DG_Small_TDGHM"
Presenting theory "Native_Word.Code_Target_Word_Base"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Hom"
Presenting theory "Native_Word.Word_Type_Copies"
Presenting theory "Native_Word.Code_Int_Integer_Conversion"
Presenting theory "Native_Word.Code_Target_Integer_Bit"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Cone"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Small_Cone"
Presenting theory "Native_Word.Uint32"
Presenting theory "Collections.HashCode"
Presenting theory "Deriving.Hash_Generator"
Presenting file "$AFP/Deriving/Hash_Generator/hash_generator.ML"
Presenting theory "Deriving.Hash_Instances"
Presenting theory "Deriving.Countable_Generator"
Presenting theory "Deriving.Derive"
Presenting theory "CZH_Foundations.CZH_DG_PDigraph"
Presenting theory "CZH_Foundations.CZH_DG_Subdigraph"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_PWKan"
Presenting theory "CZH_Foundations.CZH_DG_Simple"
Presenting theory "CZH_Foundations.CZH_DG_GRPH"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Yoneda"
Presenting theory "Van_Emde_Boas_Trees.VEBT_BuildupMemImp"
Presenting theory "CZH_Foundations.CZH_DG_Rel"
Presenting file "~~/src/Tools/misc_legacy.ML"
Presenting file "~~/src/Tools/try.ML"
Presenting file "~~/src/Tools/quickcheck.ML"
Presenting theory "Van_Emde_Boas_Trees.VEBT_SuccPredImperative"
Presenting file "~~/src/Tools/solve_direct.ML"
Presenting file "~~/src/Tools/IsaPlanner/zipper.ML"
Presenting file "~~/src/Tools/IsaPlanner/isand.ML"
Presenting file "~~/src/Tools/IsaPlanner/rw_inst.ML"
Presenting theory "CZH_Foundations.CZH_DG_Par"
Presenting file "~~/src/Provers/hypsubst.ML"
Presenting file "~~/src/Provers/splitter.ML"
Presenting file "~~/src/Provers/classical.ML"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_PWKan_Example"
Presenting file "~~/src/Provers/blast.ML"
Presenting file "~~/src/Provers/clasimp.ML"
Presenting theory "CZH_Foundations.CZH_DG_Set"
Presenting file "~~/src/Tools/eqsubst.ML"
Presenting file "~~/src/Provers/quantifier1.ML"
Presenting file "~~/src/Tools/atomize_elim.ML"
Presenting file "~~/src/Tools/cong_tac.ML"
Presenting file "~~/src/Tools/intuitionistic.ML"
Presenting file "~~/src/Tools/project_rule.ML"
Presenting file "~~/src/Tools/subtyping.ML"
Presenting theory "CZH_Foundations.CZH_DG_Conclusions"
Presenting theory "CZH_Foundations.CZH_SMC_Introduction"
Presenting file "~~/src/Tools/case_product.ML"
Presenting file "~~/src/HOL/Tools/hologic.ML"
Presenting theory "Van_Emde_Boas_Trees.VEBT_DelImperative"
Presenting file "~~/src/HOL/Tools/rewrite_hol_proof.ML"
Presenting file "~~/src/HOL/Tools/simpdata.ML"
Presenting file "~~/src/Tools/induct.ML"
Presenting file "~~/src/Tools/induction.ML"
Presenting file "~~/src/Tools/induct_tacs.ML"
Presenting file "~~/src/Tools/coherent.ML"
Presenting theory "CZH_Universal_Constructions.CZH_UCAT_Conclusions"
Presenting file "~~/src/HOL/Tools/cnf.ML"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Order"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Intf_Imperative"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Small_Order"
Presenting theory "Van_Emde_Boas_Trees.VEBT_Example"
Presenting theory "CZH_Foundations.CZH_SMC_Semicategory"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Ordinal"
Presenting theory "CZH_Foundations.CZH_SMC_Small_Semicategory"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_CSimplicial"
Presenting theory "CZH_Foundations.CZH_SMC_Semifunctor"
Presenting theory "HOL.Orderings"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Structure_Example"
Presenting file "~~/src/Provers/order_procedure.ML"
Presenting file "~~/src/Provers/order_tac.ML"
Presenting theory "CZH_Foundations.CZH_SMC_Small_Semifunctor"
Presenting theory "CZH_Elementary_Categories.CZH_ECAT_Conclusions"
Presenting theory "HOL.Groups"
Presenting theory "CZH_Foundations.CZH_SMC_NTSMCF"
Presenting file "~~/src/HOL/Tools/group_cancel.ML"
Presenting theory "HOL.Lattices"
Presenting theory "CZH_Foundations.CZH_SMC_Small_NTSMCF"
Presenting theory "HOL.Boolean_Algebras"
Presenting file "~~/src/HOL/Tools/boolean_algebra_cancel.ML"
Presenting theory "CZH_Foundations.CZH_SMC_PSemicategory"
Presenting theory "CZH_Foundations.CZH_SMC_Subsemicategory"
Presenting theory "CZH_Foundations.CZH_SMC_Simple"
Presenting theory "HOL.Typedef"
Presenting file "~~/src/HOL/Tools/typedef.ML"
Presenting theory "CZH_Foundations.CZH_SMC_Rel"
Presenting theory "CZH_Foundations.CZH_SMC_Par"
Presenting file "~~/src/HOL/Tools/functor.ML"
Presenting theory "CZH_Foundations.CZH_SMC_Set"
Presenting theory "HOL.Complete_Lattices"
Presenting theory "CZH_Foundations.CZH_SMC_GRPH"
Presenting theory "CZH_Foundations.CZH_DG_SemiCAT"
Presenting theory "CZH_Foundations.CZH_SMC_SemiCAT"
Presenting theory "CZH_Foundations.CZH_SMC_Conclusions"
Presenting theory "HOL.Ctr_Sugar"
Presenting file "~~/src/HOL/Tools/Ctr_Sugar/case_translation.ML"
Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML"
Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML"
Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML"
Presenting file "~~/src/HOL/Tools/coinduction.ML"
Presenting theory "HOL.Inductive"
Presenting file "~~/src/HOL/Tools/inductive.ML"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_data.ML"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_primrec.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML"
Presenting theory "HOL.Product_Type"
Presenting file "~~/src/HOL/Tools/split_rule.ML"
Presenting file "~~/src/HOL/Tools/set_comprehension_pointfree.ML"
Presenting file "~~/src/HOL/Tools/inductive_set.ML"
Presenting theory "HOL.Sum_Type"
Presenting file "~~/src/HOL/Tools/arith_data.ML"
Presenting file "~~/src/Provers/Arith/cancel_div_mod.ML"
Presenting file "~~/src/HOL/Tools/nat_arith.ML"
Presenting theory "HOL.Fields"
Presenting file "~~/src/Provers/Arith/fast_lin_arith.ML"
Presenting file "~~/src/HOL/Tools/lin_arith.ML"
Presenting theory "HOL.Finite_Set"
Presenting theory "HOL.Relation"
Presenting theory "HOL.Transitive_Closure"
Presenting file "~~/src/Provers/trancl.ML"
Presenting theory "HOL.Wellfounded"
Presenting theory "HOL.Order_Relation"
Presenting theory "HOL.Hilbert_Choice"
Presenting file "~~/src/HOL/Tools/choice_specification.ML"
Presenting theory "HOL.BNF_Wellorder_Relation"
Presenting theory "HOL.BNF_Wellorder_Embedding"
Presenting theory "HOL.BNF_Wellorder_Constructions"
Presenting theory "HOL.BNF_Cardinal_Order_Relation"
Presenting theory "HOL.BNF_Cardinal_Arithmetic"
Presenting theory "HOL.Fun_Def_Base"
Presenting file "~~/src/HOL/Tools/Function/function_lib.ML"
Presenting file "~~/src/HOL/Tools/Function/function_common.ML"
Presenting file "~~/src/HOL/Tools/Function/function_context_tree.ML"
Presenting file "~~/src/HOL/Tools/Function/sum_tree.ML"
Presenting theory "HOL.BNF_Def"
Presenting file "~~/src/HOL/Tools/BNF/bnf_util.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_def_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_def.ML"
Presenting theory "HOL.BNF_Composition"
Presenting file "~~/src/HOL/Tools/BNF/bnf_comp_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_comp.ML"
Presenting theory "HOL.Basic_BNFs"
Presenting theory "HOL.BNF_Fixpoint_Base"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_util_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_util.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML"
Presenting theory "HOL.BNF_Least_Fixpoint"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_util.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_compat.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_size.ML"
Presenting file "~~/src/HOL/Tools/datatype_simprocs.ML"
Presenting theory "HOL.Equiv_Relations"
Presenting theory "HOL.Basic_BNF_LFPs"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML"
Presenting file "~~/src/HOL/Tools/Meson/meson.ML"
Presenting file "~~/src/HOL/Tools/Meson/meson_clausify.ML"
Presenting file "~~/src/HOL/Tools/Meson/meson_tactic.ML"
Presenting file "~~/src/HOL/Tools/ATP/atp_util.ML"
Presenting file "~~/src/HOL/Tools/ATP/atp_problem.ML"
Presenting file "~~/src/HOL/Tools/ATP/atp_proof.ML"
Presenting file "~~/src/HOL/Tools/ATP/atp_proof_redirect.ML"
Presenting file "~~/src/HOL/Tools/lambda_lifting.ML"
Presenting file "~~/src/HOL/Tools/monomorph.ML"
Presenting file "~~/src/HOL/Tools/ATP/atp_problem_generate.ML"
Presenting file "~~/src/HOL/Tools/ATP/atp_proof_reconstruct.ML"
Presenting file "~~/src/Tools/Metis/metis.ML"
Presenting file "~~/src/HOL/Tools/Metis/metis_generate.ML"
Presenting file "~~/src/HOL/Tools/Metis/metis_reconstruct.ML"
Presenting file "~~/src/HOL/Tools/Metis/metis_tactic.ML"
Presenting theory "HOL.Transfer"
Presenting file "~~/src/HOL/Tools/Transfer/transfer.ML"
Presenting file "~~/src/HOL/Tools/Transfer/transfer_bnf.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML"
Presenting theory "HOL.Lifting"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_util.ML"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_info.ML"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_bnf.ML"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_term.ML"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_def.ML"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_setup.ML"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_def_code_dt.ML"
Presenting theory "HOL.Quotient"
Presenting file "~~/src/HOL/Tools/Quotient/quotient_info.ML"
Presenting file "~~/src/HOL/Tools/Quotient/quotient_term.ML"
Presenting file "~~/src/HOL/Tools/Quotient/quotient_type.ML"
Presenting file "~~/src/HOL/Tools/Quotient/quotient_def.ML"
Presenting file "~~/src/HOL/Tools/Quotient/quotient_tacs.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lift.ML"
Presenting file "~~/src/HOL/Tools/numeral.ML"
Presenting theory "HOL.Groups_Big"
Presenting theory "HOL.Complete_Partial_Order"
Presenting theory "HOL.Option"
Presenting theory "HOL.Partial_Function"
Presenting file "~~/src/HOL/Tools/Function/partial_function.ML"
Presenting file "~~/src/Tools/Argo/argo_expr.ML"
Presenting file "~~/src/Tools/Argo/argo_term.ML"
Presenting file "~~/src/Tools/Argo/argo_lit.ML"
Presenting file "~~/src/Tools/Argo/argo_proof.ML"
Presenting file "~~/src/Tools/Argo/argo_rewr.ML"
Presenting file "~~/src/Tools/Argo/argo_cls.ML"
Presenting file "~~/src/Tools/Argo/argo_common.ML"
Presenting file "~~/src/Tools/Argo/argo_cc.ML"
Presenting file "~~/src/Tools/Argo/argo_simplex.ML"
Presenting file "~~/src/Tools/Argo/argo_thy.ML"
Presenting file "~~/src/Tools/Argo/argo_heap.ML"
Presenting file "~~/src/Tools/Argo/argo_cdcl.ML"
Presenting file "~~/src/Tools/Argo/argo_core.ML"
Presenting file "~~/src/Tools/Argo/argo_clausify.ML"
Presenting file "~~/src/Tools/Argo/argo_solver.ML"
Presenting file "~~/src/HOL/Tools/Argo/argo_tactic.ML"
Presenting file "~~/src/HOL/Tools/prop_logic.ML"
Presenting file "~~/src/HOL/Tools/sat_solver.ML"
Presenting file "~~/src/HOL/Tools/sat.ML"
Presenting file "~~/src/HOL/Tools/Argo/argo_sat_solver.ML"
Presenting theory "HOL.Fun_Def"
Presenting file "~~/src/HOL/Tools/Function/function_core.ML"
Presenting file "~~/src/HOL/Tools/Function/mutual.ML"
Presenting file "~~/src/HOL/Tools/Function/pattern_split.ML"
Presenting file "~~/src/HOL/Tools/Function/relation.ML"
Presenting file "~~/src/HOL/Tools/Function/function_elims.ML"
Presenting file "~~/src/HOL/Tools/Function/function.ML"
Presenting file "~~/src/HOL/Tools/Function/pat_completeness.ML"
Presenting file "~~/src/HOL/Tools/Function/fun.ML"
Presenting file "~~/src/HOL/Tools/Function/induction_schema.ML"
Presenting file "~~/src/HOL/Tools/Function/measure_functions.ML"
Presenting file "~~/src/HOL/Tools/Function/lexicographic_order.ML"
Presenting file "~~/src/HOL/Tools/Function/termination.ML"
Presenting file "~~/src/HOL/Tools/Function/scnp_solve.ML"
Presenting file "~~/src/HOL/Tools/Function/scnp_reconstruct.ML"
Presenting file "~~/src/HOL/Tools/Function/fun_cases.ML"
Presenting file "~~/src/HOL/Tools/int_arith.ML"
Presenting theory "HOL.Lattices_Big"
Presenting theory "HOL.Euclidean_Division"
Presenting theory "HOL.Parity"
Presenting theory "HOL.Numeral_Simprocs"
Presenting file "~~/src/Provers/Arith/assoc_fold.ML"
Presenting file "~~/src/Provers/Arith/cancel_numerals.ML"
Presenting file "~~/src/Provers/Arith/combine_numerals.ML"
Presenting file "~~/src/Provers/Arith/cancel_numeral_factor.ML"
Presenting file "~~/src/Provers/Arith/extract_common_term.ML"
Presenting file "~~/src/HOL/Tools/numeral_simprocs.ML"
Presenting file "~~/src/HOL/Tools/nat_numeral_simprocs.ML"
Presenting theory "HOL.Semiring_Normalization"
Presenting file "~~/src/HOL/Tools/semiring_normalizer.ML"
Presenting theory "HOL.Groebner_Basis"
Presenting file "~~/src/HOL/Tools/groebner.ML"
Presenting theory "HOL.Set_Interval"
Presenting theory "HOL.Presburger"
Presenting file "~~/src/HOL/Tools/Qelim/qelim.ML"
Presenting file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"
Presenting file "~~/src/HOL/Tools/Qelim/cooper.ML"
Presenting file "~~/src/HOL/Tools/try0.ML"
Presenting theory "HOL.Divides"
Presenting file "~~/src/HOL/Tools/SMT/smt_util.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_failure.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_config.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_builtin.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_datatypes.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_normalize.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_translate.ML"
Presenting file "~~/src/HOL/Tools/SMT/smtlib.ML"
Presenting file "~~/src/HOL/Tools/SMT/smtlib_interface.ML"
Presenting file "~~/src/HOL/Tools/SMT/smtlib_proof.ML"
Presenting file "~~/src/HOL/Tools/SMT/smtlib_isar.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_proof.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_isar.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_solver.ML"
Presenting file "~~/src/HOL/Tools/SMT/cvc_interface.ML"
Presenting file "~~/src/HOL/Tools/SMT/lethe_proof.ML"
Presenting file "~~/src/HOL/Tools/SMT/lethe_isar.ML"
Presenting file "~~/src/HOL/Tools/SMT/lethe_proof_parse.ML"
Presenting file "~~/src/HOL/Tools/SMT/cvc_proof_parse.ML"
Presenting file "~~/src/HOL/Tools/SMT/conj_disj_perm.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_replay_methods.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_replay.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_replay_arith.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_interface.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_replay_rules.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_replay_methods.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_replay.ML"
Presenting file "~~/src/HOL/Tools/SMT/lethe_replay_methods.ML"
Presenting file "~~/src/HOL/Tools/SMT/verit_replay_methods.ML"
Presenting file "~~/src/HOL/Tools/SMT/verit_strategies.ML"
Presenting file "~~/src/HOL/Tools/SMT/verit_replay.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_systems.ML"
Presenting theory "HOL.Sledgehammer"
Presenting file "~~/src/HOL/Tools/ATP/system_on_tptp.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML"
Presenting theory "HOL.Lifting_Set"
Presenting theory "HOL.Groups_List"
Presenting theory "HOL.Bit_Operations"
Presenting theory "HOL.Code_Numeral"
Presenting theory "HOL.Random"
Presenting theory "HOL.String"
Presenting file "~~/src/HOL/Tools/string_syntax.ML"
Presenting file "~~/src/HOL/Tools/literal.ML"
Presenting theory "HOL.Typerep"
Presenting theory "HOL.Predicate"
Presenting theory "HOL.Lazy_Sequence"
Presenting theory "HOL.Limited_Sequence"
Presenting theory "HOL.Code_Evaluation"
Presenting file "~~/src/HOL/Tools/code_evaluation.ML"
Presenting file "~~/src/HOL/Tools/value_command.ML"
Presenting file "~~/src/HOL/Tools/reification.ML"
Presenting theory "HOL.Quickcheck_Random"
Presenting file "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML"
Presenting file "~~/src/HOL/Tools/Quickcheck/random_generators.ML"
Presenting theory "HOL.Random_Pred"
Presenting theory "HOL.Random_Sequence"
Presenting theory "HOL.Quickcheck_Exhaustive"
Presenting file "~~/src/HOL/Tools/Quickcheck/exhaustive_generators.ML"
Presenting file "~~/src/HOL/Tools/Quickcheck/abstract_generators.ML"
Presenting theory "HOL.Predicate_Compile"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/core_data.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/mode_inference.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile.ML"
Presenting theory "HOL.Quickcheck_Narrowing"
Presenting file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"
Presenting file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"
Presenting file "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
Presenting file "~~/src/HOL/Tools/Quickcheck/find_unused_assms.ML"
Presenting theory "HOL.Mirabelle"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_util.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_arith.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_metis.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_try0.ML"
Presenting theory "HOL.Extraction"
Presenting theory "HOL.Record"
Presenting file "~~/src/HOL/Tools/record.ML"
Presenting theory "HOL.Nitpick"
Presenting file "~~/src/HOL/Tools/Nitpick/kodkod.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/kodkod_sat.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_util.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_hol.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_mono.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_preproc.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_scope.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_peephole.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_rep.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_nut.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_kodkod.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_model.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_commands.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_tests.ML"
Presenting theory "HOL.Nunchaku"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_util.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_collect.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_problem.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_translate.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_model.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_display.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_tool.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_commands.ML"
Presenting theory "HOL.BNF_Greatest_Fixpoint"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_util.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML"
Presenting theory "HOL.Filter"
Presenting theory "HOL.Conditionally_Complete_Lattices"
Presenting theory "HOL.Factorial"
Presenting theory "HOL.Binomial"
Presenting theory "HOL-Library.Realizers"
Group AFP: 0:09:06 elapsed time, 0:51:42 cpu time, factor 5.68
Group main: 0:00:00 elapsed time
Group large: 0:00:00 elapsed time
Group no_doc: 0:00:00 elapsed time
Group doc: 0:00:00 elapsed time
Group timing: 0:00:00 elapsed time
Overall: 0:17:25 elapsed time, 0:51:42 cpu time, factor 2.97
using [/media/data/jenkins/workspace/isabelle-all/bin/isabelle]
Preparing site generation in out/hugo
Cleaning up generated files...
Build in /media/data/jenkins/workspace/isabelle-all/afp/web/index.html
Started calculate disk usage of build
Finished Calculation of disk usage of build in 0 seconds
Started calculate disk usage of workspace
Finished Calculation of disk usage of workspace in 0 seconds