Started by an SCM change
Running as SYSTEM
[EnvInject] - Loading node environment variables.
Building remotely on workermtahpc (mta_hpc) in workspace /media/data/jenkins/workspace/isabelle-all
[isabelle-all] $ hg showconfig paths.default
[isabelle-all] $ hg pull --rev default
pulling from http://isabelle.in.tum.de/repos/isabelle/
real URL is https://isabelle.in.tum.de/repos/isabelle/
no changes found
[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 1cadc477f644c89c0fae513f51ff81f4af684c1d --template exists\n
exists
[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(1cadc477f644c89c0fae513f51ff81f4af684c1d)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
[afp] $ hg pull --rev default
pulling from https://foss.heptapod.net/isa-afp/afp-devel/
no changes found
[afp] $ hg update --clean --rev default
2007 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp] $ hg --config extensions.purge= clean --all
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg log --rev a0663cd726cc06543f9689efe66c628dfdb6af7e --template exists\n
exists
[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(a0663cd726cc06543f9689efe66c628dfdb6af7e)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-all] $ /bin/sh -xe /tmp/jenkins12050969793957505254.sh
+ Admin/jenkins/run_build all
+ set -e
+ PROFILE=all
+ shift
+ bin/isabelle components -a
+ bin/isabelle jedit -bf
### 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) ...
+ bin/isabelle ocaml_setup
# 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:
       opam update

[NOTE] Package zarith is already installed (current version is 1.12).
+ bin/isabelle ghc_setup
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
+ bin/isabelle ci_build all

=== CONFIGURATION ===

ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-a5d5fba90286/x86_64_32-linux"
ML_SYSTEM="polyml-5.9"
ML_OPTIONS="-H 4000 --maxheap 8G"
jobs = 8, threads = 8, numa = true

=== BUILD ===

Build started at Fri, 2 Jun 2023 13:15:35 +0200
Isabelle id 1cadc477f644
AFP id 7aa9ab057cd7

=== LOG ===

Session Pure/Pure
Session Misc/CTT
Session Misc/Cube
Session FOL/FOL
Session FOL/CCL
Session FOL/FOL-ex
Session FOL/FOLP
Session FOL/FOLP-ex
Session Doc/Intro (doc)
Session FOL/LCF
Session Doc/Logics (doc)
Session Doc/Nitpick (doc)
Session Pure/Pure-Examples
Session Pure/Pure-ex
Session Misc/SML
Session Misc/Sequents
Session Doc/Sledgehammer (doc)
Session AFP/SpecCheck (AFP)
Session Misc/Tools
Session HOL/HOL (main)
Session AFP/AVL-Trees (AFP)
Session AFP/AWN (AFP)
Session AFP/Abortable_Linearizable_Modules (AFP)
Session AFP/Abstract-Hoare-Logics (AFP)
Session AFP/Ackermanns_not_PR (AFP)
Session AFP/AnselmGod (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/Bondy (AFP)
Session AFP/Boolos_Curious_Inference (AFP)
Session AFP/Boolos_Curious_Inference_Automated (AFP)
Session AFP/BytecodeLogicJmlTypes (AFP)
Session AFP/C2KA_DistributedSystems (AFP)
Session AFP/CISC-Kernel (AFP)
Session AFP/CYK (AFP)
Session AFP/Cauchy (AFP)
Session AFP/Sqrt_Babylonian (AFP)
Session Doc/Classes (doc)
Session AFP/ClockSynchInst (AFP)
Session AFP/Compiling-Exceptions-Correctly (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 Doc/Demo_EPTCS (doc)
Session Doc/Demo_Easychair (doc)
Session Doc/Demo_FoilTeX (doc)
Session Doc/Demo_LIPIcs (doc)
Session Doc/Demo_LLNCS (doc)
Session AFP/Depth-First-Search (AFP)
Session AFP/Digit_Expansions (AFP)
Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
Session AFP/DiskPaxos (AFP)
Session AFP/Example-Submission (AFP)
Session AFP/FFT (AFP)
Session AFP/FLP (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 Doc/Functions (doc)
Session AFP/GPU_Kernel_PL (AFP)
Session AFP/GenClock (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/Generic_Deriving (AFP)
Session AFP/GewirthPGCProof (AFP)
Session AFP/GoedelGod (AFP)
Session AFP/Goodstein_Lambda (AFP)
Session HOL/HOL-Cardinals (timing)
Session AFP/Binding_Syntax_Theory (AFP)
Session AFP/Epistemic_Logic (AFP)
Session AFP/Public_Announcement_Logic (AFP)
Session AFP/Stalnaker_Logic (AFP)
Session AFP/Ordinals_and_Cardinals (AFP)
Session AFP/Risk_Free_Lending (AFP)
Session HOL/HOL-Hoare
Session HOL/HOL-Hoare_Parallel (timing)
Session HOL/HOL-IMPP
Session HOL/HOL-IOA
Session HOL/HOL-Import
Session HOL/HOL-Lattice
Session HOL/HOL-Library (main timing)
Session AFP/ADS_Functor (AFP)
Session AFP/Approximation_Algorithms (AFP)
Session AFP/ArrowImpossibilityGS (AFP)
Session AFP/Auto2_HOL (AFP)
Session AFP/BNF_CC (AFP)
Session AFP/BNF_Operations (AFP)
Session AFP/Binomial-Heaps (AFP)
Session AFP/Birkhoff_Finite_Distributive_Lattices (AFP)
Session AFP/Boolean_Expression_Checkers (AFP)
Session AFP/Bounded_Deducibility_Security (AFP)
Session AFP/BD_Security_Compositional (AFP)
Session AFP/CoSMeDis (AFP)
Session AFP/CoCon (AFP)
Session AFP/CoSMed (AFP)
Session AFP/Buildings (AFP)
Session AFP/CRDT (AFP)
Session AFP/IMAP-CRDT (AFP)
Session AFP/Card_Multisets (AFP)
Session AFP/Card_Number_Partitions (AFP)
Session AFP/Category (AFP)
Session Doc/Codegen (doc)
Session AFP/CofGroups (AFP)
Session AFP/CommCSL (AFP)
Session AFP/Complete_Non_Orders (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/CoreC++ (AFP)
Session AFP/Core_DOM (AFP)
Session AFP/Shadow_DOM (AFP)
Session AFP/DOM_Components (AFP)
Session AFP/Core_SC_DOM (AFP)
Session AFP/Shadow_SC_DOM (AFP)
Session AFP/SC_DOM_Components (AFP)
Session Doc/Datatypes (doc)
Session Doc/Corec (doc)
Session AFP/Decl_Sem_Fun_PL (AFP)
Session AFP/Encodability_Process_Calculi (AFP)
Session AFP/Euler_Partition (AFP)
Session AFP/FOL-Fitting (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/FinFun (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 AFP/Valuation (AFP)
Session HOL/HOL-Auth (timing)
Session HOL/HOL-UNITY (timing)
Session HOL/HOL-Bali (timing)
Session HOL/HOL-Combinatorics (main timing)
Session AFP/Blue_Eyes (AFP)
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/Edwards_Elliptic_Curves_Group (AFP)
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 AFP/VectorSpace (AFP)
Session HOL/HOL-Analysis (main timing)
Session AFP/Actuarial_Mathematics (AFP)
Session AFP/Cayley_Hamilton (AFP)
Session AFP/Coinductive (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/Topology (AFP)
Session AFP/Complex_Geometry (AFP)
Session AFP/Poincare_Disc (AFP)
Session AFP/Differential_Game_Logic (AFP)
Session AFP/First_Welfare_Theorem (AFP)
Session AFP/Green (AFP)
Session HOL/HOL-Analysis-ex
Session HOL/HOL-Complex_Analysis (main timing)
Session AFP/Cartan_FP (AFP)
Session HOL/HOL-Eisbach
Session AFP/AOT (AFP)
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/Combinatorial_Enumeration_Algorithms (AFP)
Session AFP/Case_Labeling (AFP)
Session AFP/Clean (AFP)
Session AFP/Combinatorics_Words (AFP)
Session AFP/Combinatorics_Words_Graph_Lemma (AFP)
Session AFP/Binary_Code_Imprimitive (AFP)
Session AFP/Two_Generated_Word_Monoids_Intersection (AFP)
Session AFP/Cook_Levin (AFP)
Session AFP/Dependent_SIFUM_Type_Systems (AFP)
Session AFP/Dependent_SIFUM_Refinement (AFP)
Session Doc/Eisbach (doc)
Session HOL/HOL-Hahn_Banach
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/Lp (AFP)
Session AFP/MDP-Rewards (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/Skip_Lists (AFP)
Session AFP/Source_Coding_Theorem (AFP)
Session AFP/Turans_Graph_Theorem (AFP)
Session AFP/Hyperdual (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/Octonions (AFP)
Session AFP/Ptolemys_Theorem (AFP)
Session AFP/Quaternions (AFP)
Session AFP/Rank_Nullity_Theorem (AFP)
Session AFP/Gauss_Jordan (AFP)
Session AFP/Echelon_Form (AFP)
Session AFP/Hermite (AFP)
Session AFP/Tarskis_Geometry (AFP)
Session AFP/Triangle (AFP)
Session AFP/Chord_Segments (AFP)
Session AFP/Stewart_Apollonius (AFP)
Session AFP/Youngs_Inequality (AFP)
Session AFP/pGCL (AFP)
Session HOL/HOL-Examples
Session HOL/HOL-Isar_Examples
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/Bernoulli (AFP)
Session AFP/DigitsInBase (AFP)
Session AFP/E_Transcendental (AFP)
Session AFP/Elliptic_Curves_Group_Law (AFP)
Session AFP/Fermat3_4 (AFP)
Session HOL/HOL-Data_Structures (timing)
Session AFP/Efficient-Mergesort (AFP)
Session HOL/HOL-Codegenerator_Test
Session AFP/Query_Optimization (AFP)
Session HOL/HOL-ex (timing)
Session AFP/Automatic_Refinement (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Lehmer (AFP)
Session AFP/Lifting_the_Exponent (AFP)
Session AFP/Padic_Ints (AFP)
Session AFP/Padic_Field (AFP)
Session AFP/Pratt_Certificate (AFP)
Session AFP/Bertrands_Postulate (AFP)
Session AFP/Prime_Harmonic_Series (AFP)
Session AFP/RSAPSS (AFP)
Session AFP/SumSquares (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 HOL/HOL-IMP (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-Induct
Session HOL/HOL-Metis_Examples (timing)
Session HOL/HOL-Proofs (timing)
Session HOL/HOL-Proofs-Extraction (timing)
Session HOL/HOL-Proofs-ex
Session HOL/HOL-Proofs-Lambda (timing)
Session AFP/Applicative_Lifting (AFP)
Session AFP/Free-Groups (AFP)
Session AFP/Stern_Brocot (AFP)
Session AFP/HereditarilyFinite (AFP)
Session AFP/HyperCTL (AFP)
Session AFP/Integration (AFP)
Session AFP/Isabelle_Meta_Model (AFP)
Session AFP/LTL (AFP)
Session AFP/Stuttering_Equivalence (AFP)
Session AFP/Landau_Symbols (AFP)
Session AFP/Akra_Bazzi (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/Optics (AFP)
Session AFP/UTP-Toolkit (AFP)
Session AFP/UTP (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/Pell (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 (AFP)
Session AFP/Matrix_Tensor (AFP)
Session AFP/Knot_Theory (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/Safe_OCL (AFP)
Session AFP/Schutz_Spacetime (AFP)
Session AFP/Selection_Heap_Sort (AFP)
Session AFP/Simplex (AFP)
Session AFP/Skew_Heap (AFP)
Session AFP/Solidity (AFP)
Session AFP/Sort_Encodings (AFP)
Session AFP/Splay_Tree (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/SuperCalc (AFP)
Session Doc/System (doc)
Session AFP/Szemeredi_Regularity (AFP)
Session AFP/Roth_Arithmetic_Progressions (AFP)
Session AFP/Tail_Recursive_Functions (AFP)
Session AFP/TortoiseHare (AFP)
Session AFP/Trie (AFP)
Session AFP/Flyspeck-Tame (AFP)
Session AFP/Twelvefold_Way (AFP)
Session AFP/Vickrey_Clarke_Groves (AFP)
Session HOL/HOL-Matrix_LP
Session HOL/HOL-MicroJava (timing)
Session HOL/HOL-Mirabelle-ex
Session HOL/HOL-Mutabelle
Session HOL/HOL-NanoJava
Session HOL/HOL-Nitpick_Examples
Session HOL/HOL-Nominal
Session AFP/CCS (AFP)
Session HOL/HOL-Nominal-Examples (timing)
Session AFP/Lam-ml-Normalization (AFP)
Session AFP/Pi_Calculus (AFP)
Session AFP/Psi_Calculi (AFP)
Session AFP/SequentInvertibility (AFP)
Session HOL/HOL-Predicate_Compile_Examples (timing)
Session HOL/HOL-Prolog
Session HOL/HOL-Quickcheck_Examples (timing)
Session HOL/HOL-Real_Asymp
Session AFP/Cotangent_PFD_Formula (AFP)
Session AFP/Fourier (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 AFP/Lambert_W (AFP)
Session HOL/HOL-SET_Protocol (timing)
Session HOL/HOL-SMT_Examples (timing)
Session HOL/HOL-SPARK
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session HOL/HOL-SPARK-Manual
Session HOL/HOL-Statespace
Session HOL/HOL-TLA
Session HOL/HOL-TLA-Buffer
Session HOL/HOL-TLA-Inc
Session HOL/HOL-TLA-Memory
Session HOL/HOL-TPTP
Session HOL/HOL-Types_To_Sets
Session AFP/Banach_Steinhaus (AFP)
Session AFP/Smooth_Manifolds (AFP)
Session AFP/Types_To_Sets_Extension (AFP)
Session HOL/HOL-Unix
Session HOL/HOL-ZF
Session AFP/Category2 (AFP)
Session HOL/HOLCF (main timing)
Session AFP/Circus (AFP)
Session AFP/HOL-CSP (AFP)
Session HOL/HOLCF-IMP
Session HOL/HOLCF-Library
Session AFP/CSP_RefTK (AFP)
Session HOL/HOLCF-FOCUS
Session HOL/HOLCF-ex
Session AFP/PCF (AFP)
Session AFP/HOLCF-Prelude (AFP)
Session AFP/BirdKMP (AFP)
Session HOL/HOLCF-Tutorial
Session HOL/IOA (timing)
Session HOL/IOA-ABP
Session HOL/IOA-NTP
Session HOL/IOA-Storage
Session HOL/IOA-ex
Session AFP/Shivers-CFA (AFP)
Session AFP/Stream-Fusion (AFP)
Session AFP/Tycon (AFP)
Session AFP/WorkerWrapper (AFP)
Session AFP/Hales_Jewett (AFP)
Session Misc/Haskell
Session AFP/Heard_Of (AFP)
Session AFP/Consensus_Refined (AFP)
Session AFP/Hello_World (AFP)
Session AFP/HoareForDivergence (AFP)
Session AFP/Hood_Melville_Queue (AFP)
Session AFP/HotelKeyCards (AFP)
Session Doc/How_to_Prove_it (no_doc)
Session AFP/Huffman (AFP)
Session AFP/Hybrid_Logic (AFP)
Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
Session AFP/HyperHoareLogic (AFP)
Session AFP/IFC_Tracking (AFP)
Session AFP/IMP2 (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/IsaGeoCoq (AFP)
Session AFP/IsaNet (AFP)
Session Doc/Isar_Ref (doc)
Session AFP/Isabelle_C (AFP)
Session Doc/JEdit (doc)
Session AFP/Jacobson_Basic_Algebra (AFP)
Session AFP/Grothendieck_Schemes (AFP)
Session AFP/Pluennecke_Ruzsa_Inequality (AFP)
Session AFP/Khovanskii_Theorem (AFP)
Session AFP/Kneser_Cauchy_Davenport (AFP)
Session AFP/JiveDataStoreModel (AFP)
Session AFP/Key_Agreement_Strong_Adversaries (AFP)
Session AFP/Kleene_Algebra (AFP)
Session AFP/KAD (AFP)
Session AFP/KAT_and_DRA (AFP)
Session AFP/Algebraic_VCs (AFP)
Session AFP/Multirelations (AFP)
Session AFP/Quantales (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/LambdaMu (AFP)
Session AFP/LatticeProperties (AFP)
Session AFP/DataRefinementIBP (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Lazy_Case (AFP)
Session AFP/Lifting_Definition_Option (AFP)
Session AFP/List-Index (AFP)
Session AFP/Comparison_Sort_Lower_Bound (AFP)
Session AFP/Jinja (AFP)
Session AFP/Dominance_CHK (AFP)
Session AFP/HRB-Slicing (AFP)
Session AFP/InformationFlowSlicing_Inter (AFP)
Session AFP/Slicing (AFP)
Session AFP/InformationFlowSlicing (AFP)
Session AFP/JinjaDCI (AFP)
Session AFP/Regression_Test_Selection (AFP)
Session AFP/List_Update (AFP)
Session AFP/Quick_Sort_Cost (AFP)
Session AFP/Random_BSTs (AFP)
Session AFP/Randomised_BSTs (AFP)
Session AFP/Treaps (AFP)
Session AFP/Randomised_Social_Choice (AFP)
Session AFP/Fishburn_Impossibility (AFP)
Session AFP/PAPP_Impossibility (AFP)
Session AFP/SDS_Impossibility (AFP)
Session AFP/List_Interleaving (AFP)
Session AFP/List_Inversions (AFP)
Session AFP/LocalLexing (AFP)
Session Doc/Locales (doc)
Session AFP/Locally-Nameless-Sigma (AFP)
Session AFP/Logging_Independent_Anonymity (AFP)
Session AFP/Lowe_Ontological_Argument (AFP)
Session AFP/MHComputation (AFP)
Session AFP/MLSS_Decision_Proc (AFP)
Session Doc/Main (doc)
Session AFP/Marriage (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Matroids (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/Maximum_Segment_Sum (AFP)
Session AFP/Median_Of_Medians_Selection (AFP)
Session AFP/KD_Tree (AFP)
Session AFP/Menger (AFP)
Session AFP/Mereology (AFP)
Session AFP/Metalogic_ProofChecker (AFP)
Session AFP/MiniML (AFP)
Session AFP/Modular_Assembly_Kit_Security (AFP)
Session AFP/MonoBoolTranAlgebra (AFP)
Session AFP/Multitape_To_Singletape_TM (AFP)
Session AFP/Name_Carrying_Type_Inference (AFP)
Session AFP/Nano_JSON (AFP)
Session AFP/Nash_Williams (AFP)
Session AFP/No_FTL_observers (AFP)
Session AFP/No_FTL_observers_Gen_Rel (AFP)
Session AFP/Nominal2 (AFP)
Session AFP/Incompleteness (AFP)
Session AFP/Surprise_Paradox (AFP)
Session AFP/LambdaAuth (AFP)
Session AFP/Launchbury (AFP)
Session AFP/Call_Arity (AFP)
Session AFP/Modal_Logics_for_NTS (AFP)
Session AFP/Rewriting_Z (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/NormByEval (AFP)
Session AFP/OpSets (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/Ordinal (AFP)
Session AFP/Nested_Multisets_Ordinals (AFP)
Session AFP/Design_Theory (AFP)
Session AFP/Undirected_Graph_Theory (AFP)
Session AFP/Balog_Szemeredi_Gowers (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/PAL (AFP)
Session AFP/PLM (AFP)
Session AFP/PSemigroupsConvolution (AFP)
Session AFP/Package_logic (AFP)
Session AFP/Combinable_Wands (AFP)
Session AFP/Paraconsistency (AFP)
Session AFP/Parity_Game (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 Doc/Prog_Prove (doc)
Session AFP/Projective_Geometry (AFP)
Session AFP/Proof_Strategy_Language (AFP)
Session AFP/PropResPI (AFP)
Session AFP/Propositional_Logic_Class (AFP)
Session AFP/Propositional_Proof_Systems (AFP)
Session AFP/PseudoHoops (AFP)
Session AFP/Ramsey-Infinite (AFP)
Session AFP/Real_Power (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/Rensets (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/SIFPL (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/Sauer_Shelah_Lemma (AFP)
Session AFP/Security_Protocol_Refinement (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/Hoare_Time (AFP)
Session AFP/Separata (AFP)
Session AFP/Separation_Logic_Unbounded (AFP)
Session AFP/Simpl (AFP)
Session AFP/BDD (AFP)
Session AFP/SimplifiedOntologicalArgument (AFP)
Session AFP/Sliding_Window_Algorithm (AFP)
Session AFP/Statecharts (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/StrictOmegaCategories (AFP)
Session AFP/Strong_Security (AFP)
Session Doc/Sugar (doc)
Session AFP/Sunflowers (AFP)
Session AFP/Clique_and_Monotone_Circuits (AFP)
Session AFP/Suppes_Theorem (AFP)
Session AFP/Probability_Inequality_Completeness (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/Synthetic_Completeness (AFP)
Session AFP/Szpilrajn (AFP)
Session AFP/Combinatorics_Words_Lyndon (AFP)
Session AFP/TESL_Language (AFP)
Session AFP/TLA (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 AFP/Tree_Enumeration (AFP)
Session Doc/Tutorial (doc)
Session Doc/Typeclass_Hierarchy (doc)
Session AFP/Types_Tableaus_and_Goedels_God (AFP)
Session AFP/UPF (AFP)
Session AFP/UPF_Firewall (AFP)
Session AFP/Universal_Turing_Machine (AFP)
Session AFP/Van_der_Waerden (AFP)
Session AFP/VeriComp (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/Word_Lib (AFP)
Session AFP/Complx (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Routing (AFP)
Session AFP/Interval_Arithmetic_Word32 (AFP)
Session AFP/LEM (AFP)
Session AFP/Native_Word (AFP)
Session AFP/Collections (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/Deriving (AFP)
Session AFP/CAVA_Base (AFP)
Session AFP/CAVA_Automata (AFP)
Session AFP/DFS_Framework (AFP)
Session AFP/Gabow_SCC (AFP)
Session AFP/LTL_to_GBA (AFP)
Session AFP/Promela (AFP)
Session AFP/Containers (AFP)
Session AFP/CHERI-C_Memory_Model (AFP)
Session AFP/Collections_Examples (AFP)
Session AFP/Containers-Benchmarks (AFP)
Session AFP/Eval_FO (AFP)
Session AFP/MFOTL_Monitor (AFP)
Session AFP/Generic_Join (AFP)
Session AFP/MFODL_Monitor_Optimized (AFP)
Session AFP/VYDRA_MDL (AFP)
Session AFP/Formula_Derivatives (AFP)
Session AFP/MSO_Regex_Equivalence (AFP)
Session AFP/Show (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/CakeML (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/Optimal_BST (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/Dirichlet_L (AFP)
Session AFP/Gauss_Sums (AFP)
Session AFP/Three_Squares (AFP)
Session AFP/Prime_Number_Theorem (AFP)
Session AFP/Prime_Distribution_Elementary (AFP)
Session AFP/IMO2019 (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/Farkas (AFP)
Session AFP/Isabelle_Marries_Dirac (AFP)
Session AFP/Knuth_Bendix_Order (AFP)
Session AFP/Functional_Ordered_Resolution_Prover (AFP)
Session AFP/Simple_Clause_Learning (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/Efficient_Weighted_Path_Order (AFP)
Session AFP/Given_Clause_Loops (AFP)
Session AFP/Multiset_Ordering_NPC (AFP)
Session AFP/Linear_Recurrences (AFP)
Session AFP/Perron_Frobenius (AFP)
Session AFP/MDP-Algorithms (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/CVP_Hardness (AFP)
Session AFP/LLL_Factorization (AFP)
Session AFP/Linear_Inequalities (AFP)
Session AFP/LP_Duality (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/Polynomials (AFP)
Session AFP/Deep_Learning (AFP)
Session AFP/QHLProver (AFP)
Session AFP/Projective_Measurements (AFP)
Session AFP/Commuting_Hermitian (AFP)
Session AFP/Expander_Graphs (AFP)
Session AFP/Distributed_Distinct_Elements (AFP)
Session AFP/TsirelsonBound (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/Schwartz_Zippel (AFP)
Session AFP/Virtual_Substitution (AFP)
Session AFP/Real_Impl (AFP)
Session AFP/Complex_Bounded_Operators (AFP)
Session AFP/Registers (AFP)
Session AFP/QR_Decomposition (AFP)
Session AFP/XML (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/Formal_SSA (AFP)
Session AFP/Minimal_SSA (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/SM_Base (AFP)
Session AFP/SM (AFP)
Session AFP/CAVA_Setup (AFP)
Session AFP/CAVA_LTL_Modelchecker (AFP)
Session AFP/Transitive-Closure (AFP)
Session AFP/KBPs (AFP)
Session AFP/LTL_to_DRA (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/Quantifier_Elimination_Hybrid (AFP)
Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
Session AFP/FSM_Tests (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/LOFT (AFP)
Session AFP/Mersenne_Primes (AFP)
Session AFP/MiniSail (AFP)
Session AFP/Separation_Logic_Imperative_HOL (AFP)
Session AFP/Sepref_Prereq (AFP)
Session AFP/ROBDD (AFP)
Session AFP/Refine_Imperative_HOL (AFP)
Session AFP/BTree (AFP)
Session AFP/Floyd_Warshall (AFP)
Session AFP/Sepref_Basic (AFP)
Session AFP/Sepref_IICF (AFP)
Session AFP/Flow_Networks (AFP)
Session AFP/EdmondsKarp_Maxflow (AFP)
Session AFP/MFMC_Countable (AFP)
Session AFP/Probabilistic_While (AFP)
Session AFP/CryptHOL (AFP)
Session AFP/ABY3_Protocols (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/Kruskal (AFP)
Session AFP/PAC_Checker (AFP)
Session AFP/VerifyThis2018 (AFP)
Session AFP/VerifyThis2019 (AFP)
Session AFP/Simplicial_complexes_and_boolean_functions (AFP)
Session AFP/UpDown_Scheme (AFP)
Session AFP/WebAssembly (AFP)
Session AFP/SPARCv8 (AFP)
Session AFP/X86_Semantics (AFP)
Session AFP/ZFC_in_HOL (AFP)
Session AFP/CZH_Foundations (AFP)
Session AFP/CZH_Elementary_Categories (AFP)
Session AFP/CZH_Universal_Constructions (AFP)
Session AFP/Category3 (AFP)
Session AFP/MonoidalCategory (AFP)
Session AFP/Ordinal_Partitions (AFP)
Session AFP/Wetzels_Problem (AFP)
Session FOL/ZF (main timing)
Session Doc/Logics_ZF (doc)
Session AFP/Recursion-Addition (AFP)
Session FOL/ZF-AC
Session FOL/ZF-Coind
Session FOL/ZF-Constructible
Session AFP/Delta_System_Lemma (AFP)
Session AFP/Transitive_Models (AFP)
Session AFP/Independence_CH (AFP)
Session AFP/Forcing (AFP)
Session FOL/ZF-IMP
Session FOL/ZF-Induct
Session FOL/ZF-UNITY (timing)
Session FOL/ZF-Resid
Session FOL/ZF-ex
Building Frequency_Moments on hpcisabelle/0 ...
Building Suppes_Theorem on hpcisabelle/1 ...
Building Commuting_Hermitian on hpcisabelle/2 ...
Running Schwartz_Zippel on hpcisabelle/3 ...
Running MLSS_Decision_Proc on hpcisabelle/4 ...
Running ABY3_Protocols on hpcisabelle/5 ...
Running Binary_Code_Imprimitive on hpcisabelle/6 ...
Running CVP_Hardness on hpcisabelle/7 ...
Suppes_Theorem: theory Propositional_Logic_Class.Implication_Logic
Suppes_Theorem: theory HOL-Library.Cancellation
Suppes_Theorem: theory HOL-Library.Old_Datatype
Suppes_Theorem: theory HOL-Library.Nat_Bijection
Suppes_Theorem: theory HOL-Combinatorics.Transposition
Suppes_Theorem: theory HOL-Library.FuncSet
Binary_Code_Imprimitive: theory Combinatorics_Words_Graph_Lemma.Glued_Codes
Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Square_Interpretation
MLSS_Decision_Proc: theory Graph_Theory.Rtrancl_On
MLSS_Decision_Proc: theory Fresh_Identifiers.Fresh
MLSS_Decision_Proc: theory HOL-Library.Adhoc_Overloading
MLSS_Decision_Proc: theory HOL-Combinatorics.Transposition
MLSS_Decision_Proc: theory HOL-Library.Cancellation
MLSS_Decision_Proc: theory HOL-Library.Infinite_Set
MLSS_Decision_Proc: theory HOL-Library.FuncSet
MLSS_Decision_Proc: theory HOL-Library.Nat_Bijection
Frequency_Moments: theory HOL-Eisbach.Eisbach
Frequency_Moments: theory HOL-Combinatorics.Stirling
Frequency_Moments: theory HOL-Library.Code_Abstract_Nat
Frequency_Moments: theory HOL-Decision_Procs.Dense_Linear_Order
Frequency_Moments: theory HOL-Number_Theory.Cong
Frequency_Moments: theory HOL-Library.Code_Target_Int
Frequency_Moments: theory HOL-Algebra.Congruence
Frequency_Moments: theory Card_Partitions.Set_Partition
Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian_Misc
MLSS_Decision_Proc: theory HOL-Library.Old_Datatype
Schwartz_Zippel: theory HOL-Computational_Algebra.Fraction_Field
Schwartz_Zippel: theory HOL-Computational_Algebra.Nth_Powers
Schwartz_Zippel: theory HOL-Computational_Algebra.Group_Closure
Schwartz_Zippel: theory HOL-Computational_Algebra.Squarefree
Schwartz_Zippel: theory HOL-Library.Fun_Lexorder
Schwartz_Zippel: theory HOL-Algebra.Congruence
Schwartz_Zippel: theory Jordan_Normal_Form.Missing_Misc
Schwartz_Zippel: theory HOL-Library.Function_Algebras
Suppes_Theorem: theory Propositional_Logic_Class.Classical_Logic
ABY3_Protocols: theory ABY3_Protocols.Finite_Number_Type
ABY3_Protocols: theory ABY3_Protocols.Spmf_Common
Schwartz_Zippel: theory HOL-Library.Groups_Big_Fun
Commuting_Hermitian: theory Commuting_Hermitian.Spectral_Theory_Complements
CVP_Hardness: theory CVP_Hardness.Reduction
CVP_Hardness: theory CVP_Hardness.Digits_int
CVP_Hardness: theory Algebraic_Numbers.Bivariate_Polynomials
CVP_Hardness: theory BenOr_Kozen_Reif.More_Matrix
CVP_Hardness: theory CVP_Hardness.Partition
CVP_Hardness: theory CVP_Hardness.Subset_Sum
MLSS_Decision_Proc: theory HOL-Library.Rewrite
ABY3_Protocols: theory ABY3_Protocols.Additive_Sharing
MLSS_Decision_Proc: theory Fresh_Identifiers.Fresh_Nat
MLSS_Decision_Proc: theory HOL-Library.Sublist
Suppes_Theorem: theory HOL-Library.Disjoint_Sets
Suppes_Theorem: theory HOL-Library.Countable
Schwartz_Zippel: theory Abstract-Rewriting.Seq
Frequency_Moments: theory HOL-Library.Code_Target_Nat
Schwartz_Zippel: theory HOL-Library.Ramsey
Suppes_Theorem: theory HOL-Library.Multiset
Frequency_Moments: theory HOL-Combinatorics.List_Permutation
Suppes_Theorem: theory Propositional_Logic_Class.Classical_Logic_Completeness
ABY3_Protocols: theory ABY3_Protocols.Sharing_Lemmas
Schwartz_Zippel: theory HOL-Library.More_List
Schwartz_Zippel: theory HOL-Library.While_Combinator
MLSS_Decision_Proc: theory HOL-Library.Liminf_Limsup
ABY3_Protocols: theory ABY3_Protocols.Multiplication
ABY3_Protocols: theory ABY3_Protocols.Shuffle
MLSS_Decision_Proc: theory List-Index.List_Index
Frequency_Moments: theory HOL-Library.Function_Algebras
CVP_Hardness: theory Algebraic_Numbers.Resultant
ABY3_Protocols: theory ABY3_Protocols.Multiplication_Synthesization
Schwartz_Zippel: theory Polynomials.More_Modules
MLSS_Decision_Proc: theory HereditarilyFinite.HF
Commuting_Hermitian: theory Commuting_Hermitian.Commuting_Hermitian
Binary_Code_Imprimitive: theory Binary_Code_Imprimitive.Binary_Code_Imprimitive
Schwartz_Zippel: theory HOL-Library.Poly_Mapping
Frequency_Moments: theory HOL-Library.Code_Target_Numeral
Frequency_Moments: theory HOL-Library.List_Lexorder
Frequency_Moments: theory HOL-Library.Power_By_Squaring
Frequency_Moments: theory HOL-Number_Theory.Eratosthenes
Frequency_Moments: theory HOL-Library.Landau_Symbols
Frequency_Moments: theory HOL-Library.Lattice_Algebras
Schwartz_Zippel: theory Polynomial_Interpolation.Missing_Unsorted
CVP_Hardness: theory CVP_Hardness.Lattice_int
Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial
Schwartz_Zippel: theory Jordan_Normal_Form.Conjugate
Schwartz_Zippel: theory Skip_Lists.Pi_pmf
MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Logic
MLSS_Decision_Proc: theory HOL-Library.Disjoint_Sets
Schwartz_Zippel: theory HOL-Algebra.Order
Schwartz_Zippel: theory Open_Induction.Restricted_Predicates
CVP_Hardness: theory CVP_Hardness.CVP_p
MLSS_Decision_Proc: theory HOL-Library.Multiset
MLSS_Decision_Proc: theory HOL-Library.Countable
Schwartz_Zippel: theory HOL-Computational_Algebra.Normalized_Fraction
Frequency_Moments: theory HOL-Library.Log_Nat
Frequency_Moments: theory Card_Partitions.Injectivity_Solver
Preparing Binary_Code_Imprimitive/document ...
Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom
Frequency_Moments: theory Median_Method.Median
MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Suc_Theory
Schwartz_Zippel: theory Regular-Sets.Regular_Set
Frequency_Moments: theory Universal_Hash_Families.Definitions
Frequency_Moments: theory HOL-Algebra.Order
Frequency_Moments: theory Universal_Hash_Families.Preliminary_Results
Frequency_Moments: theory Card_Partitions.Card_Partitions
Suppes_Theorem: theory HOL-Combinatorics.Permutations
Schwartz_Zippel: theory Well_Quasi_Orders.Infinite_Sequences
Preparing ABY3_Protocols/document ...
Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Elements
MLSS_Decision_Proc: theory HereditarilyFinite.Ordinal
Schwartz_Zippel: theory HOL-Algebra.Lattice
Schwartz_Zippel: theory Polynomials.MPoly_Type
Finished Binary_Code_Imprimitive/document (0:00:09 elapsed time)
Preparing Binary_Code_Imprimitive/outline ...
Schwartz_Zippel: theory Well_Quasi_Orders.Least_Enum
Frequency_Moments: theory Ergodic_Theory.SG_Library_Complement
Suppes_Theorem: theory HOL-Combinatorics.List_Permutation
Frequency_Moments: theory HOL-Number_Theory.Mod_Exp
Suppes_Theorem: theory Propositional_Logic_Class.List_Utilities
Frequency_Moments: theory Bell_Numbers_Spivey.Bell_Numbers
Finished ABY3_Protocols/document (0:00:05 elapsed time)
Preparing ABY3_Protocols/outline ...
Suppes_Theorem: theory Propositional_Logic_Class.Classical_Connectives
Frequency_Moments: theory Card_Equiv_Relations.Card_Equiv_Relations
Frequency_Moments: theory Equivalence_Relation_Enumeration.Equivalence_Relation_Enumeration
MLSS_Decision_Proc: theory HereditarilyFinite.Finitary
Suppes_Theorem: theory Suppes_Theorem.Probability_Logic
MLSS_Decision_Proc: theory HereditarilyFinite.Rank
Suppes_Theorem: theory Suppes_Theorem.Suppes_Theorem
Finished Binary_Code_Imprimitive/outline (0:00:05 elapsed time)
Timing Binary_Code_Imprimitive (8 threads, 24.662s elapsed time, 20.935s cpu time, 0.615s GC time, factor 0.85)
Finished Binary_Code_Imprimitive (0:00:26 elapsed time, 0:00:23 cpu time, factor 0.88)
Frequency_Moments: theory HOL-Algebra.Lattice
Running CommCSL on hpcisabelle/6 ...
Schwartz_Zippel: theory Polynomials.More_MPoly_Type
Finished ABY3_Protocols/outline (0:00:03 elapsed time)
Timing ABY3_Protocols (8 threads, 16.408s elapsed time, 39.187s cpu time, 0.911s GC time, factor 2.39)
Finished ABY3_Protocols (0:00:33 elapsed time, 0:00:43 cpu time, factor 1.31)
Frequency_Moments: theory HOL-Number_Theory.Fib
Running Edwards_Elliptic_Curves_Group on hpcisabelle/5 ...
MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Semantics
MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_HF_Extras
MLSS_Decision_Proc: theory HOL-Library.Countable_Set
CVP_Hardness: theory LLL_Basis_Reduction.Missing_Lemmas
Edwards_Elliptic_Curves_Group: theory HOL-Library.Rewrite
Edwards_Elliptic_Curves_Group: theory HOL-Library.FuncSet
CommCSL: theory CommCSL.PartialMap
Frequency_Moments: theory Lp.Functional_Spaces
CommCSL: theory CommCSL.PosRat
Frequency_Moments: theory HOL-Number_Theory.Prime_Powers
CommCSL: theory CommCSL.FractionalHeap
Schwartz_Zippel: theory HOL-Algebra.Complete_Lattice
CommCSL: theory CommCSL.StateModel
CVP_Hardness: theory LLL_Basis_Reduction.Norms
Frequency_Moments: theory HOL-Number_Theory.Totient
MLSS_Decision_Proc: theory HOL-Library.Countable_Complete_Lattices
CommCSL: theory CommCSL.Lang
Frequency_Moments: theory HOL-Algebra.Complete_Lattice
Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Congruence
Schwartz_Zippel: theory HOL-Algebra.Group
Frequency_Moments: theory Frequency_Moments.Landau_Ext
Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Order
CommCSL: theory CommCSL.CommCSL
Frequency_Moments: theory HOL-Algebra.Group
Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Lattice
Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Complete_Lattice
MLSS_Decision_Proc: theory HOL-Library.Order_Continuity
MLSS_Decision_Proc: theory HOL-Combinatorics.Permutations
Schwartz_Zippel: theory HOL-Algebra.FiniteProduct
MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Typing_Defs
Preparing Commuting_Hermitian/document ...
Edwards_Elliptic_Curves_Group: theory HOL-Algebra.Group
MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Calculus
Frequency_Moments: theory Lp.Lp
MLSS_Decision_Proc: theory HOL-Library.Extended_Nat
Schwartz_Zippel: theory HOL-Algebra.Ring
MLSS_Decision_Proc: theory HOL-Combinatorics.Orbits
MLSS_Decision_Proc: theory HOL-Library.Extended_Real
MLSS_Decision_Proc: theory Graph_Theory.Auxiliary
Schwartz_Zippel: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial_FPS
Schwartz_Zippel: theory Polynomials.MPoly_Type_Univariate
Schwartz_Zippel: theory HOL-Computational_Algebra.Polynomial_Factorial
Finished Commuting_Hermitian/document (0:00:06 elapsed time)
Preparing Commuting_Hermitian/outline ...
CommCSL: theory CommCSL.AbstractCommutativity
Edwards_Elliptic_Curves_Group: theory Edwards_Elliptic_Curves_Group.Edwards_Elliptic_Curves_Group
Frequency_Moments: theory HOL-Algebra.Coset
Frequency_Moments: theory HOL-Algebra.FiniteProduct
Preparing Suppes_Theorem/document ...
Frequency_Moments: theory HOL-Library.Interval
MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Typing
Frequency_Moments: theory HOL-Library.Float
Finished Commuting_Hermitian/outline (0:00:02 elapsed time)
Timing Commuting_Hermitian (8 threads, 14.470s elapsed time, 95.869s cpu time, 2.507s GC time, factor 6.63)
Finished Commuting_Hermitian (0:01:05 elapsed time, 0:02:15 cpu time, factor 2.09)
Running TsirelsonBound on hpcisabelle/2 ...
Schwartz_Zippel: theory HOL-Computational_Algebra.Formal_Laurent_Series
MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Typing_Urelems
Frequency_Moments: theory HOL-Algebra.Ring
TsirelsonBound: theory TsirelsonBound.Tensor_Mat_Compl_Properties
Schwartz_Zippel: theory Polynomial_Interpolation.Missing_Polynomial
CommCSL: theory CommCSL.Guards
Finished Suppes_Theorem/document (0:00:04 elapsed time)
Preparing Suppes_Theorem/outline ...
CVP_Hardness: theory CVP_Hardness.infnorm
CVP_Hardness: theory CVP_Hardness.Additional_Lemmas
CVP_Hardness: theory CVP_Hardness.CVP_vec
Schwartz_Zippel: theory HOL-Algebra.Module
Finished Suppes_Theorem/outline (0:00:03 elapsed time)
Timing Suppes_Theorem (8 threads, 62.277s elapsed time, 103.047s cpu time, 4.255s GC time, factor 1.65)
Finished Suppes_Theorem (0:01:13 elapsed time, 0:02:04 cpu time, factor 1.70)
CVP_Hardness: theory CVP_Hardness.BHLE
Running Efficient_Weighted_Path_Order on hpcisabelle/1 ...
Schwartz_Zippel: theory Jordan_Normal_Form.Missing_Ring
Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.Indexed_Term
CVP_Hardness: theory CVP_Hardness.SVP_vec
Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.List_Memo_Functions
CommCSL: theory CommCSL.Safety
TsirelsonBound: theory TsirelsonBound.Matrix_L2_Operator_Norm
MLSS_Decision_Proc: theory Graph_Theory.Stuff
Frequency_Moments: theory HOL-Algebra.Generated_Groups
Schwartz_Zippel: theory Polynomial_Factorization.Order_Polynomial
Frequency_Moments: theory HOL-Algebra.Divisibility
Schwartz_Zippel: theory Polynomial_Interpolation.Ring_Hom_Poly
MLSS_Decision_Proc: theory Graph_Theory.Digraph
Schwartz_Zippel: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
TsirelsonBound: theory TsirelsonBound.Density_Matrix_Basics
Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.WPO_Approx
TsirelsonBound: theory TsirelsonBound.Tsirelson
Frequency_Moments: theory Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.WPO_Mem_Impl
Schwartz_Zippel: theory HOL-Computational_Algebra.Computational_Algebra
MLSS_Decision_Proc: theory Graph_Theory.Arc_Walk
MLSS_Decision_Proc: theory Graph_Theory.Bidirected_Digraph
Frequency_Moments: theory HOL-Library.Interval_Float
Schwartz_Zippel: theory Symmetric_Polynomials.Vieta
MLSS_Decision_Proc: theory Graph_Theory.Vertex_Walk
MLSS_Decision_Proc: theory Graph_Theory.Pair_Digraph
MLSS_Decision_Proc: theory Graph_Theory.Weighted_Graph
MLSS_Decision_Proc: theory Graph_Theory.Shortest_Path
Schwartz_Zippel: theory Symmetric_Polynomials.Symmetric_Polynomials
Frequency_Moments: theory HOL-Algebra.Elementary_Groups
Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.RPO_Unbounded
Efficient_Weighted_Path_Order: theory Efficient_Weighted_Path_Order.RPO_Mem_Impl
Preparing Efficient_Weighted_Path_Order/document ...
CommCSL: theory CommCSL.Soundness
Frequency_Moments: theory HOL-Decision_Procs.Approximation_Bounds
Schwartz_Zippel: theory Jordan_Normal_Form.Matrix
Frequency_Moments: theory HOL-Algebra.AbelCoset
Finished Efficient_Weighted_Path_Order/document (0:00:05 elapsed time)
Preparing Efficient_Weighted_Path_Order/outline ...
Frequency_Moments: theory HOL-Algebra.Module
Schwartz_Zippel: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
Finished Efficient_Weighted_Path_Order/outline (0:00:03 elapsed time)
Timing Efficient_Weighted_Path_Order (8 threads, 16.502s elapsed time, 33.112s cpu time, 1.757s GC time, factor 2.01)
Finished Efficient_Weighted_Path_Order (0:00:23 elapsed time, 0:00:36 cpu time, factor 1.56)
Running HyperHoareLogic on hpcisabelle/1 ...
Schwartz_Zippel: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
MLSS_Decision_Proc: theory Graph_Theory.Digraph_Component
Preparing TsirelsonBound/document ...
HyperHoareLogic: theory HyperHoareLogic.Language
Frequency_Moments: theory HOL-Algebra.Ideal
HyperHoareLogic: theory HyperHoareLogic.Logic
MLSS_Decision_Proc: theory Graph_Theory.Digraph_Component_Vwalk
MLSS_Decision_Proc: theory Graph_Theory.Digraph_Isomorphism
MLSS_Decision_Proc: theory Graph_Theory.Subdivision
Finished TsirelsonBound/document (0:00:06 elapsed time)
Preparing TsirelsonBound/outline ...
Frequency_Moments: theory HOL-Algebra.RingHom
Schwartz_Zippel: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
Frequency_Moments: theory HOL-Algebra.QuotRing
Frequency_Moments: theory HOL-Algebra.UnivPoly
HyperHoareLogic: theory HyperHoareLogic.Examples
Finished TsirelsonBound/outline (0:00:02 elapsed time)
HyperHoareLogic: theory HyperHoareLogic.ProgramHyperproperties
Timing TsirelsonBound (8 threads, 27.733s elapsed time, 147.242s cpu time, 2.060s GC time, factor 5.31)
Finished TsirelsonBound (0:00:40 elapsed time, 0:02:32 cpu time, factor 3.75)
Running MHComputation on hpcisabelle/2 ...
MLSS_Decision_Proc: theory Graph_Theory.Kuratowski
MLSS_Decision_Proc: theory Graph_Theory.Euler
MHComputation: theory MHComputation.MHComputation
CommCSL: theory CommCSL.NonInterference
HyperHoareLogic: theory HyperHoareLogic.Expressivity
Frequency_Moments: theory HOL-Algebra.IntRing
Schwartz_Zippel: theory Jordan_Normal_Form.Column_Operations
Schwartz_Zippel: theory Jordan_Normal_Form.Determinant
Preparing MHComputation/document ...
Preparing Edwards_Elliptic_Curves_Group/document ...
Finished MHComputation/document (0:00:02 elapsed time)
Preparing MHComputation/outline ...
Frequency_Moments: theory HOL-Algebra.Multiplicative_Group
Finished MHComputation/outline (0:00:02 elapsed time)
Timing MHComputation (8 threads, 5.282s elapsed time, 5.573s cpu time, 0.162s GC time, factor 1.06)
Finished MHComputation (0:00:07 elapsed time, 0:00:07 cpu time, factor 1.06)
Running No_FTL_observers_Gen_Rel on hpcisabelle/2 ...
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Sorts
Preparing CVP_Hardness/document ...
MLSS_Decision_Proc: theory Graph_Theory.Graph_Theory
Frequency_Moments: theory HOL-Algebra.Ring_Divisibility
Frequency_Moments: theory HOL-Algebra.Subrings
Frequency_Moments: theory HOL-Number_Theory.Residues
MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Realisation
Preparing HyperHoareLogic/document ...
Frequency_Moments: theory HOL-Algebra.Embedded_Algebras
Frequency_Moments: theory HOL-Number_Theory.Euler_Criterion
Frequency_Moments: theory HOL-Number_Theory.Gauss
Frequency_Moments: theory HOL-Number_Theory.Quadratic_Reciprocity
Frequency_Moments: theory HOL-Number_Theory.Pocklington
MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Proc
Frequency_Moments: theory HOL-Number_Theory.Residue_Primitive_Roots
Finished Edwards_Elliptic_Curves_Group/document (0:00:11 elapsed time)
Preparing Edwards_Elliptic_Curves_Group/outline ...
Finished CVP_Hardness/document (0:00:06 elapsed time)
Preparing CVP_Hardness/outline ...
Frequency_Moments: theory HOL-Number_Theory.Number_Theory
Frequency_Moments: theory Lehmer.Lehmer
Frequency_Moments: theory Pratt_Certificate.Pratt_Certificate
Frequency_Moments: theory HOL-Algebra.Polynomials
Finished HyperHoareLogic/document (0:00:06 elapsed time)
Preparing HyperHoareLogic/outline ...
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxEField
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Points
Finished Edwards_Elliptic_Curves_Group/outline (0:00:04 elapsed time)
Timing Edwards_Elliptic_Curves_Group (8 threads, 85.450s elapsed time, 293.444s cpu time, 6.085s GC time, factor 3.43)
Finished Edwards_Elliptic_Curves_Group (0:01:27 elapsed time, 0:04:58 cpu time, factor 3.40)
Running Probability_Inequality_Completeness on hpcisabelle/5 ...
Finished CVP_Hardness/outline (0:00:03 elapsed time)
Timing CVP_Hardness (8 threads, 133.522s elapsed time, 460.562s cpu time, 8.300s GC time, factor 3.45)
Finished CVP_Hardness (0:02:18 elapsed time, 0:07:47 cpu time, factor 3.39)
Running Rensets on hpcisabelle/7 ...
Frequency_Moments: theory Bertrands_Postulate.Bertrand
Probability_Inequality_Completeness: theory Probability_Inequality_Completeness.Probability_Inequality_Completeness
Rensets: theory Rensets.Lambda_Terms
Finished HyperHoareLogic/outline (0:00:03 elapsed time)
Timing HyperHoareLogic (8 threads, 9.588s elapsed time, 49.475s cpu time, 1.506s GC time, factor 5.16)
Finished HyperHoareLogic (0:00:25 elapsed time, 0:00:52 cpu time, factor 2.04)
Running Simple_Clause_Learning on hpcisabelle/1 ...
MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Proc_Code
Simple_Clause_Learning: theory Deriving.Comparator
Simple_Clause_Learning: theory Deriving.Generator_Aux
Simple_Clause_Learning: theory Deriving.Derive_Manager
Simple_Clause_Learning: theory Simple_Clause_Learning.Multiset_Order_Extra
Simple_Clause_Learning: theory Word_Lib.Bit_Comprehension
Simple_Clause_Learning: theory HOL-Cardinals.Order_Union
Simple_Clause_Learning: theory Word_Lib.More_Divides
Simple_Clause_Learning: theory Word_Lib.Signed_Division_Word
Simple_Clause_Learning: theory Nested_Multisets_Ordinals.Multiset_More
Simple_Clause_Learning: theory Deriving.Countable_Generator
Rensets: theory Rensets.Nominal_Sets
Rensets: theory Rensets.Rensets
Rensets: theory Rensets.FRBCE_Rensets
Simple_Clause_Learning: theory HOL-Cardinals.Wellorder_Extension
Frequency_Moments: theory HOL-Algebra.Polynomial_Divisibility
Rensets: theory Rensets.Examples
Rensets: theory Rensets.Substitutive_Sets
Rensets: theory Rensets.Rensets_to_Nominal_Sets
Rensets: theory Rensets.All
MLSS_Decision_Proc: theory MLSS_Decision_Proc.MLSS_Proc_All
Frequency_Moments: theory Frequency_Moments.Frequency_Moments_Preliminary_Results
Simple_Clause_Learning: theory Deriving.Equality_Generator
Simple_Clause_Learning: theory Coinductive.Coinductive_Nat
Simple_Clause_Learning: theory List-Index.List_Index
Simple_Clause_Learning: theory Matrix.Utility
Simple_Clause_Learning: theory Native_Word.Code_Int_Integer_Conversion
Simple_Clause_Learning: theory Open_Induction.Restricted_Predicates
Preparing Rensets/document ...
Frequency_Moments: theory Finite_Fields.Finite_Fields_Preliminary_Results
Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
Simple_Clause_Learning: theory Deriving.Equality_Instances
Simple_Clause_Learning: theory Polynomial_Factorization.Missing_List
Frequency_Moments: theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
Frequency_Moments: theory Universal_Hash_Families.Carter_Wegman_Hash_Family
Simple_Clause_Learning: theory Ordered_Resolution_Prover.Map2
Frequency_Moments: theory Frequency_Moments.K_Smallest
Simple_Clause_Learning: theory Knuth_Bendix_Order.Order_Pair
Frequency_Moments: theory Frequency_Moments.Probability_Ext
Simple_Clause_Learning: theory Simple_Clause_Learning.First_Order_Terms_Extra
Finished Rensets/document (0:00:04 elapsed time)
Preparing Rensets/outline ...
Simple_Clause_Learning: theory Ordered_Resolution_Prover.Clausal_Logic
Simple_Clause_Learning: theory Knuth_Bendix_Order.Subterm_and_Context
Simple_Clause_Learning: theory Deriving.Compare
Frequency_Moments: theory Frequency_Moments.Product_PMF_Ext
Simple_Clause_Learning: theory Deriving.Comparator_Generator
Simple_Clause_Learning: theory Coinductive.Coinductive_List
Simple_Clause_Learning: theory Knuth_Bendix_Order.Lexicographic_Extension
Finished Rensets/outline (0:00:03 elapsed time)
Timing Rensets (8 threads, 14.270s elapsed time, 63.309s cpu time, 1.558s GC time, factor 4.44)
Finished Rensets (0:00:16 elapsed time, 0:01:06 cpu time, factor 4.09)
Running Three_Squares on hpcisabelle/7 ...
Simple_Clause_Learning: theory Simple_Clause_Learning.Abstract_Renaming_Apart
Simple_Clause_Learning: theory Simple_Clause_Learning.Relation_Extra
Preparing MLSS_Decision_Proc/document ...
Three_Squares: theory Pure-ex.Guess
Three_Squares: theory HOL-Eisbach.Eisbach
Three_Squares: theory HOL-Computational_Algebra.Fraction_Field
Three_Squares: theory HOL-Combinatorics.Stirling
Three_Squares: theory HOL-Computational_Algebra.Group_Closure
Three_Squares: theory HOL-Library.Adhoc_Overloading
Three_Squares: theory HOL-Decision_Procs.Dense_Linear_Order
Three_Squares: theory HOL-Library.BNF_Corec
Three_Squares: theory HOL-Computational_Algebra.Nth_Powers
Simple_Clause_Learning: theory Simple_Clause_Learning.Trail_Induced_Ordering
Simple_Clause_Learning: theory Ordered_Resolution_Prover.Herbrand_Interpretation
Finished MLSS_Decision_Proc/document (0:00:02 elapsed time)
Preparing MLSS_Decision_Proc/outline ...
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Functions
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Norms
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.WorldView
Three_Squares: theory Three_Squares.Low_Dimensional_Linear_Algebra
Simple_Clause_Learning: theory Ordered_Resolution_Prover.Abstract_Substitution
Simple_Clause_Learning: theory Ordered_Resolution_Prover.Ground_Resolution_Model
Finished MLSS_Decision_Proc/outline (0:00:02 elapsed time)
Timing MLSS_Decision_Proc (8 threads, 170.322s elapsed time, 547.852s cpu time, 20.685s GC time, factor 3.22)
Finished MLSS_Decision_Proc (0:02:53 elapsed time, 0:09:16 cpu time, factor 3.22)
Running Tree_Enumeration on hpcisabelle/4 ...
Tree_Enumeration: theory HOL-Library.Cancellation
Tree_Enumeration: theory HOL-Combinatorics.Transposition
Tree_Enumeration: theory HOL-Library.FuncSet
Tree_Enumeration: theory HOL-Library.Infinite_Set
Tree_Enumeration: theory HOL-Library.Nat_Bijection
Tree_Enumeration: theory HOL-Library.Old_Datatype
Tree_Enumeration: theory HOL-Library.Sublist
Tree_Enumeration: theory HOL-Library.Liminf_Limsup
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxTriangleInequality
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Vectors
Simple_Clause_Learning: theory Deriving.Compare_Generator
Three_Squares: theory HOL-Computational_Algebra.Squarefree
Three_Squares: theory HOL-Number_Theory.Cong
Preparing Probability_Inequality_Completeness/document ...
Simple_Clause_Learning: theory Ordered_Resolution_Prover.Inference_System
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxEventMinus
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxSelfMinus
Three_Squares: theory HOL-Library.Code_Abstract_Nat
Simple_Clause_Learning: theory Word_Lib.More_Arithmetic
Simple_Clause_Learning: theory Word_Lib.More_Word
Simple_Clause_Learning: theory Deriving.Compare_Instances
Tree_Enumeration: theory HOL-Library.Disjoint_Sets
Tree_Enumeration: theory HOL-Library.Countable
Three_Squares: theory HOL-Library.Code_Target_Nat
Three_Squares: theory HOL-Eisbach.Eisbach_Tools
Schwartz_Zippel: theory Regular-Sets.Regular_Exp
Tree_Enumeration: theory HOL-Library.Multiset
Three_Squares: theory HOL-Library.Code_Target_Int
Schwartz_Zippel: theory Regular-Sets.NDerivative
Schwartz_Zippel: theory Regular-Sets.Relation_Interpretation
Tree_Enumeration: theory Card_Partitions.Set_Partition
Three_Squares: theory HOL-Algebra.Congruence
Schwartz_Zippel: theory Regular-Sets.Equivalence_Checking
Three_Squares: theory HOL-Library.Function_Algebras
Schwartz_Zippel: theory Regular-Sets.Regexp_Method
Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full
Three_Squares: theory HOL-Library.Code_Target_Numeral
Three_Squares: theory HOL-Library.Power_By_Squaring
Simple_Clause_Learning: theory Ordered_Resolution_Prover.Unordered_Ground_Resolution
Three_Squares: theory HOL-Number_Theory.Eratosthenes
Three_Squares: theory HOL-Computational_Algebra.Normalized_Fraction
Three_Squares: theory HOL-Real_Asymp.Inst_Existentials
Schwartz_Zippel: theory Well_Quasi_Orders.Minimal_Bad_Sequences
Three_Squares: theory Bernoulli.Bernoulli
Simple_Clause_Learning: theory Knuth_Bendix_Order.Term_Aux
Three_Squares: theory HOL-Computational_Algebra.Field_as_Ring
Schwartz_Zippel: theory Well_Quasi_Orders.Almost_Full_Relations
Schwartz_Zippel: theory Polynomials.Utils
Finished Probability_Inequality_Completeness/document (0:00:16 elapsed time)
Preparing Probability_Inequality_Completeness/outline ...
Preparing CommCSL/document ...
Schwartz_Zippel: theory Well_Quasi_Orders.Well_Quasi_Orders
Three_Squares: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Three_Squares: theory HOL-Algebra.Order
Tree_Enumeration: theory HOL-Library.Countable_Set
Tree_Enumeration: theory HOL-Library.FSet
Simple_Clause_Learning: theory Native_Word.Code_Target_Word_Base
Three_Squares: theory HOL-Computational_Algebra.Polynomial_Factorial
Simple_Clause_Learning: theory Word_Lib.Bit_Shifts_Infix_Syntax
Three_Squares: theory HOL-Number_Theory.Mod_Exp
Simple_Clause_Learning: theory Word_Lib.Least_significant_bit
Three_Squares: theory HOL-Library.Going_To_Filter
Schwartz_Zippel: theory Polynomials.Power_Products
Three_Squares: theory HOL-Library.Lattice_Algebras
Simple_Clause_Learning: theory Knuth_Bendix_Order.KBO
Tree_Enumeration: theory HOL-Library.Countable_Complete_Lattices
Finished Probability_Inequality_Completeness/outline (0:00:05 elapsed time)
Timing Probability_Inequality_Completeness (8 threads, 35.902s elapsed time, 110.185s cpu time, 6.993s GC time, factor 3.07)
Finished Probability_Inequality_Completeness (0:00:38 elapsed time, 0:01:54 cpu time, factor 3.02)
Running Two_Generated_Word_Monoids_Intersection on hpcisabelle/5 ...
Simple_Clause_Learning: theory Simple_Clause_Learning.Ordered_Resolution_Prover_Extra
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Cardinalities
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Quadratics
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Translations
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.WorldLine
Two_Generated_Word_Monoids_Intersection: theory Combinatorics_Words_Graph_Lemma.Glued_Codes
Three_Squares: theory HOL-Library.Log_Nat
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.CauchySchwarz
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Matrices
Two_Generated_Word_Monoids_Intersection: theory Two_Generated_Word_Monoids_Intersection.Two_Generated_Word_Monoids_Intersection
Three_Squares: theory Bernoulli.Periodic_Bernpoly
Three_Squares: theory Winding_Number_Eval.Missing_Topology
Three_Squares: theory HOL-Algebra.Lattice
Three_Squares: theory Winding_Number_Eval.Missing_Analysis
Three_Squares: theory HOL-Number_Theory.Fib
Three_Squares: theory HOL-Number_Theory.Prime_Powers
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.ReverseCauchySchwarz
Three_Squares: theory HOL-Number_Theory.Totient
Frequency_Moments: theory Finite_Fields.Finite_Fields_Factorization_Ext
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.TangentLines
Three_Squares: theory HOL-Computational_Algebra.Computational_Algebra
Finished CommCSL/document (0:00:15 elapsed time)
Preparing CommCSL/outline ...
Three_Squares: theory Sturm_Tarski.PolyMisc
Simple_Clause_Learning: theory Word_Lib.Most_significant_bit
Three_Squares: theory HOL-Real_Asymp.Eventuallize
Three_Squares: theory HOL-Real_Asymp.Lazy_Eval
Frequency_Moments: theory Finite_Fields.Ring_Characteristic
Three_Squares: theory Sturm_Tarski.Sturm_Tarski
Schwartz_Zippel: theory Polynomials.MPoly_Type_Class
Simple_Clause_Learning: theory Word_Lib.Generic_set_bit
Three_Squares: theory Three_Squares.Quadratic_Forms
Three_Squares: theory HOL-Algebra.Complete_Lattice
Three_Squares: theory Landau_Symbols.Group_Sort
Finished CommCSL/outline (0:00:05 elapsed time)
Timing CommCSL (8 threads, 54.832s elapsed time, 332.569s cpu time, 17.592s GC time, factor 6.07)
Finished CommCSL (0:02:37 elapsed time, 0:05:44 cpu time, factor 2.18)
Running DigitsInBase on hpcisabelle/6 ...
Preparing Two_Generated_Word_Monoids_Intersection/document ...
Simple_Clause_Learning: theory Native_Word.Code_Target_Integer_Bit
Simple_Clause_Learning: theory Native_Word.Word_Type_Copies
Tree_Enumeration: theory HOL-Library.Order_Continuity
DigitsInBase: theory DigitsInBase.DigitsInBase
Tree_Enumeration: theory HOL-Library.Multiset_Order
Tree_Enumeration: theory HOL-Combinatorics.Permutations
Schwartz_Zippel: theory Factor_Algebraic_Polynomial.Poly_Connection
Schwartz_Zippel: theory Schwartz_Zippel.Schwartz_Zippel
Preparing DigitsInBase/document ...
Simple_Clause_Learning: theory Ordered_Resolution_Prover.Lazy_List_Liminf
Finished Two_Generated_Word_Monoids_Intersection/document (0:00:06 elapsed time)
Preparing Two_Generated_Word_Monoids_Intersection/outline ...
Tree_Enumeration: theory HOL-Library.Extended_Nat
Tree_Enumeration: theory Nested_Multisets_Ordinals.Multiset_More
Simple_Clause_Learning: theory Ordered_Resolution_Prover.Lazy_List_Chain
Schwartz_Zippel: theory Schwartz_Zippel.Rand_Perfect_Matching
Frequency_Moments: theory Universal_Hash_Families.Field
Frequency_Moments: theory Frequency_Moments.Frequency_Moments
Frequency_Moments: theory Frequency_Moments.Frequency_Moment_0
Frequency_Moments: theory Frequency_Moments.Frequency_Moment_2
Frequency_Moments: theory Frequency_Moments.Frequency_Moment_k
Finished DigitsInBase/document (0:00:03 elapsed time)
Preparing DigitsInBase/outline ...
Tree_Enumeration: theory HOL-Combinatorics.Multiset_Permutations
Tree_Enumeration: theory HOL-Library.Extended_Real
Tree_Enumeration: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
Finished Two_Generated_Word_Monoids_Intersection/outline (0:00:04 elapsed time)
Timing Two_Generated_Word_Monoids_Intersection (8 threads, 12.681s elapsed time, 21.882s cpu time, 0.883s GC time, factor 1.73)
Finished Two_Generated_Word_Monoids_Intersection (0:00:15 elapsed time, 0:00:23 cpu time, factor 1.52)
Running Given_Clause_Loops on hpcisabelle/5 ...
Tree_Enumeration: theory Design_Theory.Multisets_Extras
Finished DigitsInBase/outline (0:00:02 elapsed time)
Timing DigitsInBase (8 threads, 3.755s elapsed time, 9.440s cpu time, 0.169s GC time, factor 2.51)
Finished DigitsInBase (0:00:06 elapsed time, 0:00:13 cpu time, factor 2.12)
Tree_Enumeration: theory Design_Theory.Design_Basics
Given_Clause_Loops: theory Abstract-Rewriting.Seq
Given_Clause_Loops: theory Regular-Sets.Regular_Set
Given_Clause_Loops: theory Given_Clause_Loops.More_Given_Clause_Architectures
Simple_Clause_Learning: theory Saturation_Framework.Calculus
Simple_Clause_Learning: theory Simple_Clause_Learning.Wellfounded_Extra
Tree_Enumeration: theory Design_Theory.Design_Operations
Simple_Clause_Learning: theory Saturation_Framework_Extensions.Soundness
Simple_Clause_Learning: theory Saturation_Framework_Extensions.Standard_Redundancy_Criterion
Preparing Schwartz_Zippel/document ...
Given_Clause_Loops: theory Regular-Sets.Regular_Exp
Simple_Clause_Learning: theory Saturation_Framework_Extensions.Clausal_Calculus
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxLightMinus
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Sublemma3
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Cones
Given_Clause_Loops: theory Regular-Sets.NDerivative
Given_Clause_Loops: theory Regular-Sets.Relation_Interpretation
Three_Squares: theory Budan_Fourier.BF_Misc
Finished Schwartz_Zippel/document (0:00:03 elapsed time)
Preparing Schwartz_Zippel/outline ...
Simple_Clause_Learning: theory Simple_Clause_Learning.SCL_FOL
Tree_Enumeration: theory Design_Theory.Block_Designs
Tree_Enumeration: theory Girth_Chromatic.Girth_Chromatic_Misc
Tree_Enumeration: theory Undirected_Graph_Theory.Undirected_Graph_Basics
Three_Squares: theory HOL-Algebra.Group
Finished Schwartz_Zippel/outline (0:00:02 elapsed time)
Timing Schwartz_Zippel (8 threads, 237.579s elapsed time, 511.999s cpu time, 20.967s GC time, factor 2.16)
Finished Schwartz_Zippel (0:04:01 elapsed time, 0:08:41 cpu time, factor 2.16)
Given_Clause_Loops: theory Regular-Sets.Equivalence_Checking
Three_Squares: theory Landau_Symbols.Landau_Real_Products
Given_Clause_Loops: theory Regular-Sets.Regexp_Method
Given_Clause_Loops: theory Abstract-Rewriting.Abstract_Rewriting
Tree_Enumeration: theory Design_Theory.BIBD
Three_Squares: theory Winding_Number_Eval.Missing_Algebraic
Tree_Enumeration: theory Design_Theory.Resolvable_Designs
Given_Clause_Loops: theory Weighted_Path_Order.Relations
Given_Clause_Loops: theory Weighted_Path_Order.Multiset_Extension_Pair
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.LinearMaps
Given_Clause_Loops: theory Given_Clause_Loops.Given_Clause_Loops_Util
Given_Clause_Loops: theory Given_Clause_Loops.Prover_Queue
Given_Clause_Loops: theory Given_Clause_Loops.DISCOUNT_Loop
Given_Clause_Loops: theory Given_Clause_Loops.Otter_Loop
Given_Clause_Loops: theory Given_Clause_Loops.Prover_Lazy_List_Queue
Given_Clause_Loops: theory Given_Clause_Loops.Fair_Otter_Loop_Def
Given_Clause_Loops: theory Given_Clause_Loops.Fair_DISCOUNT_Loop
Given_Clause_Loops: theory Given_Clause_Loops.Zipperposition_Loop
Given_Clause_Loops: theory Given_Clause_Loops.iProver_Loop
Tree_Enumeration: theory Design_Theory.Group_Divisible_Designs
Three_Squares: theory HOL-Real_Asymp.Multiseries_Expansion
Three_Squares: theory Winding_Number_Eval.Missing_Transcendental
Three_Squares: theory Winding_Number_Eval.Cauchy_Index_Theorem
Three_Squares: theory HOL-Algebra.Coset
Given_Clause_Loops: theory Given_Clause_Loops.Fair_iProver_Loop
Given_Clause_Loops: theory Given_Clause_Loops.Fair_Zipperposition_Loop
Three_Squares: theory HOL-Algebra.FiniteProduct
Tree_Enumeration: theory Undirected_Graph_Theory.Graph_Triangles
Tree_Enumeration: theory Undirected_Graph_Theory.Undirected_Graph_Walks
Three_Squares: theory HOL-Library.Interval
Tree_Enumeration: theory Undirected_Graph_Theory.Bipartite_Graphs
Tree_Enumeration: theory Undirected_Graph_Theory.Connectivity
Given_Clause_Loops: theory Given_Clause_Loops.Fair_Otter_Loop_Complete
Three_Squares: theory HOL-Algebra.Ring
Three_Squares: theory HOL-Library.Float
Tree_Enumeration: theory Undirected_Graph_Theory.Graph_Theory_Relations
Tree_Enumeration: theory Undirected_Graph_Theory.Girth_Independence
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Affine
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Classification
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Proposition1
Simple_Clause_Learning: theory Native_Word.Uint32
Three_Squares: theory HOL-Algebra.Generated_Groups
Three_Squares: theory Landau_Symbols.Landau_Simprocs
Simple_Clause_Learning: theory Collections.HashCode
Simple_Clause_Learning: theory Deriving.Hash_Generator
Given_Clause_Loops: theory Given_Clause_Loops.Fair_Zipperposition_Loop_without_Ghosts
Three_Squares: theory Winding_Number_Eval.Winding_Number_Eval
Tree_Enumeration: theory Undirected_Graph_Theory.Undirected_Graphs_Root
Tree_Enumeration: theory Tree_Enumeration.Tree_Graph
Simple_Clause_Learning: theory Deriving.Hash_Instances
Simple_Clause_Learning: theory Deriving.Derive
Simple_Clause_Learning: theory Functional_Ordered_Resolution_Prover.IsaFoR_Term
Three_Squares: theory Landau_Symbols.Landau_More
Given_Clause_Loops: theory Given_Clause_Loops.Given_Clause_Loops
Three_Squares: theory HOL-Algebra.Elementary_Groups
Preparing Given_Clause_Loops/document ...
Three_Squares: theory HOL-Library.Interval_Float
Three_Squares: theory HOL-Decision_Procs.Approximation_Bounds
Three_Squares: theory HOL-Algebra.AbelCoset
Three_Squares: theory HOL-Algebra.Module
Three_Squares: theory HOL-Algebra.Ideal
Tree_Enumeration: theory Tree_Enumeration.Rooted_Tree
Tree_Enumeration: theory Tree_Enumeration.Labeled_Tree_Enumeration
Simple_Clause_Learning FAILED (see also "isabelle build_log -H Error Simple_Clause_Learning")
*** Duplicate fact declaration "SCL_FOL.grounding_of_clss_empty" vs. "SCL_FOL.grounding_of_clss_empty" (line 543 of "$AFP/Simple_Clause_Learning/SCL_FOL.thy")
*** The above error(s) occurred while activating facts of locale instance
*** substitution "(⋅a)" "Var" "(⊙)"
*** At command "global_interpretation" (line 543 of "$AFP/Simple_Clause_Learning/SCL_FOL.thy")
*** Undefined fact: "asymp.simps" (line 25 of "$AFP/Simple_Clause_Learning/Relation_Extra.thy")
*** At command "by" (line 25 of "$AFP/Simple_Clause_Learning/Relation_Extra.thy")
*** Undefined fact: "asymp.simps" (line 22 of "$AFP/Simple_Clause_Learning/Relation_Extra.thy")
*** At command "by" (line 22 of "$AFP/Simple_Clause_Learning/Relation_Extra.thy")
*** Failed to apply initial proof method (line 570 of "$AFP/Simple_Clause_Learning/First_Order_Terms_Extra.thy"):
*** goal (1 subgoal):
***  1. mgu t t = Some Var
*** At command "by" (line 570 of "$AFP/Simple_Clause_Learning/First_Order_Terms_Extra.thy")
*** Failed to apply initial proof method (line 558 of "$AFP/Simple_Clause_Learning/First_Order_Terms_Extra.thy"):
*** using this:
***   mgu s t = Some μ
*** goal (1 subgoal):
***  1. (⋀xs. ⟦unify [(s, t)] [] = Some xs; μ = subst_of xs⟧ ⟹ thesis) ⟹
***     thesis
*** At command "by" (line 558 of "$AFP/Simple_Clause_Learning/First_Order_Terms_Extra.thy")
*** Failed to apply initial proof method (line 537 of "$AFP/Simple_Clause_Learning/First_Order_Terms_Extra.thy"):
*** using this:
***   mgu s t = Some μ
*** goal (1 subgoal):
***  1. (⋀xs. ⟦unify [(s, t)] [] = Some xs; μ = subst_of xs⟧ ⟹ thesis) ⟹
***     thesis
*** At command "by" (line 537 of "$AFP/Simple_Clause_Learning/First_Order_Terms_Extra.thy")
Three_Squares: theory HOL-Algebra.RingHom
Finished Given_Clause_Loops/document (0:00:07 elapsed time)
Preparing Given_Clause_Loops/outline ...
Three_Squares: theory HOL-Algebra.QuotRing
Three_Squares: theory HOL-Algebra.UnivPoly
Three_Squares: theory HOL-Algebra.IntRing
Three_Squares: theory Finitely_Generated_Abelian_Groups.General_Auxiliary
Finished Given_Clause_Loops/outline (0:00:03 elapsed time)
Timing Given_Clause_Loops (8 threads, 38.634s elapsed time, 172.975s cpu time, 6.626s GC time, factor 4.48)
Finished Given_Clause_Loops (0:00:45 elapsed time, 0:03:01 cpu time, factor 3.96)
Three_Squares: theory HOL-Algebra.Multiplicative_Group
Tree_Enumeration: theory Tree_Enumeration.Rooted_Tree_Enumeration
Three_Squares: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
Three_Squares: theory Finitely_Generated_Abelian_Groups.Set_Multiplication
Three_Squares: theory Finitely_Generated_Abelian_Groups.Group_Hom
Three_Squares: theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups
Three_Squares: theory HOL-Number_Theory.Residues
Three_Squares: theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend
Three_Squares: theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups
Three_Squares: theory Finitely_Generated_Abelian_Groups.IDirProds
Three_Squares: theory HOL-Number_Theory.Euler_Criterion
Three_Squares: theory HOL-Number_Theory.Gauss
Three_Squares: theory HOL-Number_Theory.Quadratic_Reciprocity
Three_Squares: theory Three_Squares.Residues_Properties
Three_Squares: theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend
Three_Squares: theory HOL-Number_Theory.Pocklington
Three_Squares: theory HOL-Number_Theory.Residue_Primitive_Roots
Three_Squares: theory Finitely_Generated_Abelian_Groups.DirProds
Three_Squares: theory Finitely_Generated_Abelian_Groups.Group_Relations
Three_Squares: theory HOL-Number_Theory.Number_Theory
Three_Squares: theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups
Three_Squares: theory Dirichlet_L.Multiplicative_Characters
Three_Squares: theory Bernoulli.Bernoulli_FPS
Three_Squares: theory Dirichlet_Series.Dirichlet_Misc
Three_Squares: theory Dirichlet_Series.Multiplicative_Function
Three_Squares: theory Dirichlet_L.Dirichlet_Characters
Three_Squares: theory Dirichlet_Series.Dirichlet_Product
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.KeyLemma
Three_Squares: theory Dirichlet_Series.Dirichlet_Series
Three_Squares: theory Bernoulli.Bernoulli_Zeta
Three_Squares: theory Euler_MacLaurin.Euler_MacLaurin
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Sublemma4
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AxDiff
Three_Squares: theory Dirichlet_Series.Euler_Products
Three_Squares: theory Dirichlet_Series.Moebius_Mu
Three_Squares: theory Dirichlet_Series.More_Totient
Three_Squares: theory Dirichlet_Series.Divisor_Count
Three_Squares: theory Dirichlet_Series.Liouville_Lambda
Three_Squares: theory HOL-Real_Asymp.Real_Asymp
Three_Squares: theory Dirichlet_Series.Arithmetic_Summatory
Three_Squares: theory Lehmer.Lehmer
Three_Squares: theory Dirichlet_Series.Partial_Summation
Three_Squares: theory Pratt_Certificate.Pratt_Certificate
Three_Squares: theory Dirichlet_Series.Dirichlet_Series_Analysis
Three_Squares: theory Bertrands_Postulate.Bertrand
Three_Squares: theory Zeta_Function.Zeta_Library
Three_Squares: theory Zeta_Function.Zeta_Function
Three_Squares: theory Dirichlet_L.Dirichlet_L_Functions
Three_Squares: theory Dirichlet_L.Dirichlet_Theorem
Three_Squares: theory Three_Squares.Three_Squares
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.MainLemma
Preparing Tree_Enumeration/document ...
Finished Tree_Enumeration/document (0:00:06 elapsed time)
Preparing Tree_Enumeration/outline ...
Finished Tree_Enumeration/outline (0:00:03 elapsed time)
Timing Tree_Enumeration (8 threads, 133.433s elapsed time, 490.369s cpu time, 17.635s GC time, factor 3.68)
Finished Tree_Enumeration (0:02:15 elapsed time, 0:08:18 cpu time, factor 3.67)
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.TangentLineLemma
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.AffineConeLemma
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Proposition2
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.Proposition3
Preparing Frequency_Moments/document ...
Finished Frequency_Moments/document (0:00:08 elapsed time)
Preparing Frequency_Moments/outline ...
Finished Frequency_Moments/outline (0:00:04 elapsed time)
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.ObserverConeLemma
Timing Frequency_Moments (8 threads, 325.148s elapsed time, 1262.029s cpu time, 95.074s GC time, factor 3.88)
Finished Frequency_Moments (0:06:08 elapsed time, 0:22:45 cpu time, factor 3.71)
Building Expander_Graphs on hpcisabelle/6 ...
Expander_Graphs: theory Expander_Graphs.Extra_Congruence_Method
Expander_Graphs: theory Graph_Theory.Rtrancl_On
Expander_Graphs: theory HOL-Computational_Algebra.Fraction_Field
Expander_Graphs: theory Jordan_Normal_Form.Missing_Misc
Expander_Graphs: theory Abstract-Rewriting.Seq
Expander_Graphs: theory Perron_Frobenius.Bij_Nat
Expander_Graphs: theory HOL-Library.More_List
Expander_Graphs: theory HOL-Library.While_Combinator
Expander_Graphs: theory HOL-Types_To_Sets.Prerequisites
Expander_Graphs: theory Jordan_Normal_Form.Missing_Ring
Expander_Graphs: theory HOL-Types_To_Sets.Types_To_Sets
Expander_Graphs: theory Polynomial_Interpolation.Missing_Unsorted
Expander_Graphs: theory HOL-Computational_Algebra.Polynomial
Expander_Graphs: theory Jordan_Normal_Form.Conjugate
Expander_Graphs: theory HOL-Library.Code_Target_Numeral_Float
Expander_Graphs: theory HOL-Types_To_Sets.Group_On_With
Expander_Graphs: theory Perron_Frobenius.Cancel_Card_Constraint
Expander_Graphs: theory HOL-Decision_Procs.Approximation
Expander_Graphs: theory Graph_Theory.Stuff
Expander_Graphs: theory HOL-Computational_Algebra.Normalized_Fraction
Expander_Graphs: theory Graph_Theory.Digraph
Expander_Graphs: theory Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Multiset_Extras
Expander_Graphs: theory Expander_Graphs.Constructive_Chernoff_Bound
Expander_Graphs: theory Matrix.Utility
Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom
Expander_Graphs: theory Regular-Sets.Regular_Set
No_FTL_observers_Gen_Rel: theory No_FTL_observers_Gen_Rel.NoFTLGR
Expander_Graphs: theory VectorSpace.FunctionLemmas
Expander_Graphs: theory Graph_Theory.Arc_Walk
Expander_Graphs: theory Graph_Theory.Bidirected_Digraph
Expander_Graphs: theory VectorSpace.RingModuleFacts
Expander_Graphs: theory VectorSpace.MonoidSums
Expander_Graphs: theory Graph_Theory.Pair_Digraph
Expander_Graphs: theory VectorSpace.LinearCombinations
Expander_Graphs: theory Regular-Sets.Regular_Exp
Expander_Graphs: theory Jordan_Normal_Form.Matrix
Expander_Graphs: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Expander_Graphs: theory HOL-Computational_Algebra.Polynomial_Factorial
Expander_Graphs: theory Regular-Sets.NDerivative
Expander_Graphs: theory Regular-Sets.Relation_Interpretation
Expander_Graphs: theory VectorSpace.SumSpaces
Expander_Graphs: theory Polynomial_Interpolation.Missing_Polynomial
Expander_Graphs: theory VectorSpace.VectorSpace
Expander_Graphs: theory Graph_Theory.Digraph_Component
Expander_Graphs: theory Polynomial_Factorization.Order_Polynomial
Expander_Graphs: theory Polynomial_Interpolation.Ring_Hom_Poly
Expander_Graphs: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian_Misc
Expander_Graphs: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
Expander_Graphs: theory Jordan_Normal_Form.Column_Operations
Expander_Graphs: theory Regular-Sets.Equivalence_Checking
Expander_Graphs: theory Regular-Sets.Regexp_Method
Expander_Graphs: theory Jordan_Normal_Form.Determinant
Expander_Graphs: theory Graph_Theory.Digraph_Isomorphism
Expander_Graphs: theory Abstract-Rewriting.Abstract_Rewriting
Expander_Graphs: theory Jordan_Normal_Form.Char_Poly
Expander_Graphs: theory Jordan_Normal_Form.Missing_VectorSpace
Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Definition
Expander_Graphs: theory Abstract-Rewriting.SN_Orders
Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form
Expander_Graphs: theory Isabelle_Marries_Dirac.Basics
Expander_Graphs: theory Isabelle_Marries_Dirac.Binary_Nat
Expander_Graphs: theory Isabelle_Marries_Dirac.Quantum
Expander_Graphs: theory Jordan_Normal_Form.VS_Connect
Expander_Graphs: theory Expander_Graphs.Expander_Graphs_TTS
Expander_Graphs: theory Matrix.Ordered_Semiring
Expander_Graphs: theory Isabelle_Marries_Dirac.Complex_Vectors
Expander_Graphs: theory Matrix.Matrix_Legacy
Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Algebra
Expander_Graphs: theory Matrix_Tensor.Matrix_Tensor
Expander_Graphs: theory Isabelle_Marries_Dirac.Tensor
Expander_Graphs: theory Isabelle_Marries_Dirac.More_Tensor
Expander_Graphs: theory Jordan_Normal_Form.Gram_Schmidt
Expander_Graphs: theory Jordan_Normal_Form.Schur_Decomposition
Expander_Graphs: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
Expander_Graphs: theory Jordan_Normal_Form.Spectral_Radius
Expander_Graphs: theory QHLProver.Complex_Matrix
Expander_Graphs: theory Perron_Frobenius.HMA_Connect
Expander_Graphs: theory Expander_Graphs.Expander_Graphs_MGG
Expander_Graphs: theory QHLProver.Gates
Expander_Graphs: theory Projective_Measurements.Linear_Algebra_Complements
Expander_Graphs: theory Projective_Measurements.Projective_Measurements
Expander_Graphs: theory Commuting_Hermitian.Spectral_Theory_Complements
Expander_Graphs: theory Commuting_Hermitian.Commuting_Hermitian
Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Eigenvalues
Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Cheeger_Inequality
Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Walks
Preparing No_FTL_observers_Gen_Rel/document ...
Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Power_Construction
Expander_Graphs: theory Expander_Graphs.Expander_Graphs_Strongly_Explicit
Finished No_FTL_observers_Gen_Rel/document (0:00:10 elapsed time)
Preparing No_FTL_observers_Gen_Rel/outline ...
Finished No_FTL_observers_Gen_Rel/outline (0:00:04 elapsed time)
Timing No_FTL_observers_Gen_Rel (8 threads, 326.778s elapsed time, 1253.219s cpu time, 31.596s GC time, factor 3.84)
Finished No_FTL_observers_Gen_Rel (0:05:29 elapsed time, 0:21:02 cpu time, factor 3.83)
Preparing Three_Squares/document ...
Finished Three_Squares/document (0:00:05 elapsed time)
Preparing Three_Squares/outline ...
Finished Three_Squares/outline (0:00:03 elapsed time)
Timing Three_Squares (8 threads, 419.495s elapsed time, 1717.509s cpu time, 88.929s GC time, factor 4.09)
Finished Three_Squares (0:07:04 elapsed time, 0:28:58 cpu time, factor 4.09)
Preparing Expander_Graphs/document ...
Finished Expander_Graphs/document (0:00:11 elapsed time)
Preparing Expander_Graphs/outline ...
Finished Expander_Graphs/outline (0:00:04 elapsed time)
Timing Expander_Graphs (8 threads, 306.712s elapsed time, 1849.017s cpu time, 92.444s GC time, factor 6.03)
Finished Expander_Graphs (0:06:11 elapsed time, 0:33:32 cpu time, factor 5.41)
Running Distributed_Distinct_Elements on hpcisabelle/7 ...
Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Group_Closure
Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Nth_Powers
Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Squarefree
Distributed_Distinct_Elements: theory Discrete_Summation.Factorials
Distributed_Distinct_Elements: theory Finite_Fields.Formal_Polynomial_Derivatives
Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Polynomial_FPS
Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Misc
Distributed_Distinct_Elements: theory Landau_Symbols.Group_Sort
Distributed_Distinct_Elements: theory Dirichlet_Series.Multiplicative_Function
Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Product
Distributed_Distinct_Elements: theory Finite_Fields.Monic_Polynomial_Factorization
Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Formal_Laurent_Series
Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Real_Products
Distributed_Distinct_Elements: theory HOL-Computational_Algebra.Computational_Algebra
Distributed_Distinct_Elements: theory Landau_Symbols.Landau_Simprocs
Distributed_Distinct_Elements: theory Dirichlet_Series.Dirichlet_Series
Distributed_Distinct_Elements: theory Landau_Symbols.Landau_More
Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials_Aux
Distributed_Distinct_Elements: theory Stirling_Formula.Stirling_Formula
Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary
Distributed_Distinct_Elements: theory Dirichlet_Series.Moebius_Mu
Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins
Distributed_Distinct_Elements: theory Finite_Fields.Card_Irreducible_Polynomials
Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Pseudorandom_Combinators
Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds
Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm
Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff
Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level
Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy
Distributed_Distinct_Elements: theory Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm
Preparing Distributed_Distinct_Elements/document ...
Finished Distributed_Distinct_Elements/document (0:00:11 elapsed time)
Preparing Distributed_Distinct_Elements/outline ...
Finished Distributed_Distinct_Elements/outline (0:00:04 elapsed time)
Timing Distributed_Distinct_Elements (8 threads, 52.614s elapsed time, 302.732s cpu time, 8.291s GC time, factor 5.75)
Finished Distributed_Distinct_Elements (0:00:56 elapsed time, 0:05:09 cpu time, factor 5.45)
Presentation in "/media/data/jenkins/workspace/isabelle-all/browser_info"
Presenting Edwards_Elliptic_Curves_Group in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Edwards_Elliptic_Curves_Group" ...
Presenting Three_Squares in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Three_Squares" ...
Presenting Frequency_Moments in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Frequency_Moments" ...
Presenting Schwartz_Zippel in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Schwartz_Zippel" ...
Presenting Commuting_Hermitian in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Commuting_Hermitian" ...
Presenting ABY3_Protocols in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/ABY3_Protocols" ...
Presenting Distributed_Distinct_Elements in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Distributed_Distinct_Elements" ...
Presenting TsirelsonBound in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/TsirelsonBound" ...
Presenting Expander_Graphs in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Expander_Graphs" ...
Presenting document Edwards_Elliptic_Curves_Group/document
Presenting document Edwards_Elliptic_Curves_Group/outline
Presenting document Schwartz_Zippel/document
Presenting document TsirelsonBound/document
Presenting document Schwartz_Zippel/outline
Presenting document TsirelsonBound/outline
Presenting document Commuting_Hermitian/document
Presenting document Commuting_Hermitian/outline
Presenting document ABY3_Protocols/document
Presenting document ABY3_Protocols/outline
Presenting document Three_Squares/document
Presenting document Three_Squares/outline
Presenting document Distributed_Distinct_Elements/document
Presenting document Distributed_Distinct_Elements/outline
Presenting document Expander_Graphs/document
Presenting document Expander_Graphs/outline
Presenting document Frequency_Moments/document
Presenting document Frequency_Moments/outline
Presenting theory "ABY3_Protocols.Finite_Number_Type"
Presenting theory "Commuting_Hermitian.Commuting_Hermitian_Misc"
Presenting theory "HOL-Library.Log_Nat"
Presenting theory "Landau_Symbols.Group_Sort"
Presenting theory "HOL-Library.Groups_Big_Fun"
Presenting theory "HOL-Library.Fun_Lexorder"
Presenting theory "Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean"
Presenting theory "HOL-Number_Theory.Cong"
Presenting theory "ABY3_Protocols.Additive_Sharing"
Presenting theory "HOL-Library.Lattice_Algebras"
Presenting theory "HOL-Library.FuncSet"
Presenting theory "Commuting_Hermitian.Spectral_Theory_Complements"
Presenting theory "HOL-Algebra.Congruence"
Presenting theory "HOL-Library.More_List"
Presenting theory "ABY3_Protocols.Spmf_Common"
Presenting theory "Landau_Symbols.Landau_Real_Products"
Presenting theory "Expander_Graphs.Constructive_Chernoff_Bound"
Presenting theory "HOL-Algebra.Congruence"
Presenting theory "Graph_Theory.Rtrancl_On"
Presenting theory "Landau_Symbols.Landau_Simprocs"
Presenting theory "ABY3_Protocols.Sharing_Lemmas"
Presenting file "$AFP/Landau_Symbols/landau_simprocs.ML"
Presenting theory "HOL-Algebra.Order"
Presenting theory "Graph_Theory.Stuff"
Presenting theory "Landau_Symbols.Landau_More"
Presenting theory "HOL-Library.Poly_Mapping"
Presenting theory "HOL-Algebra.Lattice"
Presenting theory "Stirling_Formula.Stirling_Formula"
Presenting theory "HOL-Algebra.Order"
Presenting theory "Polynomials.MPoly_Type"
Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Preliminary"
Presenting theory "Graph_Theory.Digraph"
Presenting theory "HOL-Computational_Algebra.Squarefree"
Presenting theory "Dirichlet_Series.Dirichlet_Misc"
Presenting theory "Polynomials.More_MPoly_Type"
Presenting theory "HOL-Library.Float"
Presenting theory "Dirichlet_Series.Multiplicative_Function"
Presenting theory "HOL-Library.List_Lexorder"
Presenting theory "HOL-Algebra.Lattice"
Presenting theory "TsirelsonBound.Tensor_Mat_Compl_Properties"
Presenting theory "Dirichlet_Series.Dirichlet_Product"
Presenting theory "HOL-Algebra.Complete_Lattice"
Presenting theory "HOL-Computational_Algebra.Polynomial_FPS"
Presenting theory "Graph_Theory.Arc_Walk"
Presenting theory "Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators"
Presenting theory "Graph_Theory.Bidirected_Digraph"
Presenting theory "HOL-Number_Theory.Fib"
Presenting theory "HOL-Computational_Algebra.Formal_Laurent_Series"
Presenting theory "HOL-Algebra.Complete_Lattice"
Presenting theory "HOL-Computational_Algebra.Group_Closure"
Presenting theory "HOL-Number_Theory.Cong"
Presenting theory "HOL-Computational_Algebra.Nth_Powers"
Presenting theory "HOL-Computational_Algebra.Computational_Algebra"
Presenting theory "HOL-Algebra.Congruence"
Presenting theory "Dirichlet_Series.Dirichlet_Series"
Presenting theory "HOL-Algebra.Group"
Presenting theory "Graph_Theory.Pair_Digraph"
Presenting theory "HOL-Algebra.Order"
Presenting theory "Dirichlet_Series.Moebius_Mu"
Presenting theory "TsirelsonBound.Matrix_L2_Operator_Norm"
Presenting theory "ABY3_Protocols.Shuffle"
Presenting theory "Finite_Fields.Formal_Polynomial_Derivatives"
Presenting theory "ABY3_Protocols.Multiplication"
Presenting theory "Finite_Fields.Monic_Polynomial_Factorization"
Presenting theory "ABY3_Protocols.Multiplication_Synthesization"
Presenting theory "HOL-Algebra.Lattice"
Presenting Binary_Code_Imprimitive in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Binary_Code_Imprimitive" ...
Presenting document Binary_Code_Imprimitive/document
Presenting document Binary_Code_Imprimitive/outline
Presenting theory "Finite_Fields.Card_Irreducible_Polynomials_Aux"
Presenting theory "Finite_Fields.Card_Irreducible_Polynomials"
Presenting theory "Commuting_Hermitian.Commuting_Hermitian"
Presenting theory "HOL-Algebra.Group"
Presenting Two_Generated_Word_Monoids_Intersection in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Two_Generated_Word_Monoids_Intersection" ...
Presenting document Two_Generated_Word_Monoids_Intersection/document
Presenting document Two_Generated_Word_Monoids_Intersection/outline
Presenting theory "Distributed_Distinct_Elements.Pseudorandom_Combinators"
Presenting theory "Discrete_Summation.Factorials"
Presenting theory "TsirelsonBound.Density_Matrix_Basics"
Presenting theory "HOL-Library.Rewrite"
Presenting file "~~/src/HOL/Library/cconv.ML"
Presenting file "~~/src/HOL/Library/rewrite.ML"
Presenting theory "HOL-Algebra.Complete_Lattice"
Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Balls_and_Bins"
Presenting theory "Combinatorics_Words_Graph_Lemma.Glued_Codes"
Presenting theory "Binary_Code_Imprimitive.Binary_Square_Interpretation"
Presenting theory "Graph_Theory.Digraph_Component"
Presenting theory "HOL-Computational_Algebra.Polynomial"
Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Tail_Bounds"
Presenting theory "HOL-Algebra.Coset"
Presenting theory "Combinatorics_Words_Graph_Lemma.Glued_Codes"
Presenting theory "Polynomials.MPoly_Type_Univariate"
Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm"
Presenting theory "Jordan_Normal_Form.Missing_Misc"
Presenting theory "HOL-Algebra.Group"
Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff"
Presenting theory "HOL-Algebra.FiniteProduct"
Presenting theory "Graph_Theory.Digraph_Isomorphism"
Presenting theory "Expander_Graphs.Extra_Congruence_Method"
Presenting theory "TsirelsonBound.Tsirelson"
Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level"
Presenting theory "Polynomial_Interpolation.Ring_Hom"
Presenting theory "Expander_Graphs.Expander_Graphs_Multiset_Extras"
Presenting Efficient_Weighted_Path_Order in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Efficient_Weighted_Path_Order" ...
Presenting document Efficient_Weighted_Path_Order/document
Presenting document Efficient_Weighted_Path_Order/outline
Presenting theory "Jordan_Normal_Form.Conjugate"
Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy"
Presenting theory "Two_Generated_Word_Monoids_Intersection.Two_Generated_Word_Monoids_Intersection"
Presenting theory "HOL-Computational_Algebra.Fraction_Field"
Presenting CommCSL in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CommCSL" ...
Presenting document CommCSL/document
Presenting document CommCSL/outline
Presenting theory "Binary_Code_Imprimitive.Binary_Code_Imprimitive"
Presenting theory "CommCSL.PartialMap"
Presenting theory "HOL-Algebra.Ring"
Presenting CVP_Hardness in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CVP_Hardness" ...
Presenting document CVP_Hardness/document
Presenting document CVP_Hardness/outline
Presenting theory "CVP_Hardness.Reduction"
Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
Presenting theory "HOL-Computational_Algebra.Normalized_Fraction"
Presenting theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm"
Presenting theory "CommCSL.PosRat"
Presenting DigitsInBase in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DigitsInBase" ...
Presenting document DigitsInBase/document
Presenting document DigitsInBase/outline
Presenting theory "HOL-Algebra.Module"
Presenting theory "Efficient_Weighted_Path_Order.Indexed_Term"
Presenting theory "HOL-Algebra.AbelCoset"
Presenting theory "DigitsInBase.DigitsInBase"
Presenting Given_Clause_Loops in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Given_Clause_Loops" ...
Presenting theory "HOL-Computational_Algebra.Polynomial_Factorial"
Presenting document Given_Clause_Loops/document
Presenting document Given_Clause_Loops/outline
Presenting theory "HOL-Algebra.Ideal"
Presenting theory "HOL-Algebra.Coset"
Presenting theory "HOL-Algebra.RingHom"
Presenting theory "CommCSL.FractionalHeap"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Polynomial_Interpolation.Missing_Unsorted"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "HOL-Algebra.FiniteProduct"
Presenting theory "Expander_Graphs.Expander_Graphs_Definition"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "Edwards_Elliptic_Curves_Group.Edwards_Elliptic_Curves_Group"
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 "Efficient_Weighted_Path_Order.List_Memo_Functions"
Presenting theory "Polynomial_Interpolation.Missing_Polynomial"
Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
Presenting theory "Expander_Graphs.Expander_Graphs_TTS"
Presenting theory "HOL-Algebra.UnivPoly"
Presenting theory "HOL-Algebra.Ring"
Presenting theory "Weighted_Path_Order.Relations"
Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
Presenting theory "BenOr_Kozen_Reif.More_Matrix"
Presenting theory "Efficient_Weighted_Path_Order.WPO_Approx"
Presenting theory "HOL-Algebra.Module"
Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly"
Presenting theory "Weighted_Path_Order.Multiset_Extension_Pair"
Presenting theory "Polynomial_Factorization.Order_Polynomial"
Presenting theory "HOL-Algebra.Generated_Groups"
Presenting theory "Given_Clause_Loops.Given_Clause_Loops_Util"
Presenting theory "Given_Clause_Loops.More_Given_Clause_Architectures"
Presenting theory "Expander_Graphs.Expander_Graphs_Algebra"
Presenting theory "Given_Clause_Loops.DISCOUNT_Loop"
Presenting theory "Polynomial_Interpolation.Ring_Hom"
Presenting theory "HOL-Algebra.AbelCoset"
Presenting theory "CommCSL.StateModel"
Presenting theory "Given_Clause_Loops.Prover_Queue"
Presenting theory "Jordan_Normal_Form.Missing_Misc"
Presenting theory "Jordan_Normal_Form.Missing_Ring"
Presenting theory "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
Presenting theory "HOL-Algebra.Elementary_Groups"
Presenting theory "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized"
Presenting theory "Given_Clause_Loops.Fair_DISCOUNT_Loop"
Presenting theory "HOL-Computational_Algebra.Polynomial_FPS"
Presenting theory "HOL-Algebra.Ideal"
Presenting theory "Given_Clause_Loops.Otter_Loop"
Presenting theory "Jordan_Normal_Form.Matrix"
Presenting theory "HOL-Algebra.RingHom"
Presenting theory "Given_Clause_Loops.Fair_Otter_Loop_Def"
Presenting theory "Efficient_Weighted_Path_Order.WPO_Mem_Impl"
Presenting theory "Given_Clause_Loops.iProver_Loop"
Presenting theory "CVP_Hardness.Lattice_int"
Presenting theory "CVP_Hardness.Partition"
Presenting theory "HOL-Algebra.Multiplicative_Group"
Presenting theory "HOL-Library.More_List"
Presenting theory "CommCSL.Lang"
Presenting theory "CVP_Hardness.Subset_Sum"
Presenting theory "Efficient_Weighted_Path_Order.RPO_Unbounded"
Presenting theory "HOL-Number_Theory.Totient"
Presenting theory "CVP_Hardness.CVP_p"
Presenting theory "Efficient_Weighted_Path_Order.RPO_Mem_Impl"
Presenting HyperHoareLogic in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HyperHoareLogic" ...
Presenting document HyperHoareLogic/document
Presenting document HyperHoareLogic/outline
Presenting theory "HOL-Number_Theory.Residues"
Presenting theory "Given_Clause_Loops.Fair_iProver_Loop"
Presenting theory "Given_Clause_Loops.Fair_Otter_Loop_Complete"
Presenting theory "HOL-Number_Theory.Euler_Criterion"
Presenting theory "HOL-Computational_Algebra.Polynomial"
Presenting theory "HyperHoareLogic.Language"
Presenting theory "Given_Clause_Loops.Zipperposition_Loop"
Presenting theory "Algebraic_Numbers.Bivariate_Polynomials"
Presenting theory "HOL-Number_Theory.Gauss"
Presenting theory "HOL-Computational_Algebra.Fraction_Field"
Presenting theory "HOL-Computational_Algebra.Normalized_Fraction"
Presenting theory "HOL-Algebra.UnivPoly"
Presenting theory "HOL-Computational_Algebra.Polynomial_Factorial"
Presenting theory "CommCSL.CommCSL"
Presenting theory "Polynomial_Interpolation.Missing_Unsorted"
Presenting theory "HOL-Computational_Algebra.Formal_Laurent_Series"
Presenting theory "HOL-Number_Theory.Quadratic_Reciprocity"
Presenting theory "Given_Clause_Loops.Prover_Lazy_List_Queue"
Presenting theory "HOL-Computational_Algebra.Group_Closure"
Presenting theory "HOL-Algebra.Generated_Groups"
Presenting theory "Polynomial_Interpolation.Missing_Polynomial"
Presenting theory "Three_Squares.Residues_Properties"
Presenting theory "HOL-Computational_Algebra.Nth_Powers"
Presenting theory "HOL-Computational_Algebra.Squarefree"
Presenting theory "Polynomial_Factorization.Order_Polynomial"
Presenting theory "HOL-Computational_Algebra.Computational_Algebra"
Presenting theory "Algebraic_Numbers.Resultant"
Presenting theory "Symmetric_Polynomials.Vieta"
Presenting theory "HOL-Algebra.Elementary_Groups"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
Presenting theory "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized"
Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly"
Presenting theory "Three_Squares.Low_Dimensional_Linear_Algebra"
Presenting theory "LLL_Basis_Reduction.Missing_Lemmas"
Presenting theory "Symmetric_Polynomials.Symmetric_Polynomials"
Presenting theory "Given_Clause_Loops.Fair_Zipperposition_Loop"
Presenting theory "Power_Sum_Polynomials.Power_Sum_Polynomials_Library"
Presenting theory "LLL_Basis_Reduction.Norms"
Presenting theory "Jordan_Normal_Form.Gauss_Jordan_Elimination"
Presenting theory "CVP_Hardness.infnorm"
Presenting theory "Hermite_Lindemann.More_Multivariate_Polynomial_HLW"
Presenting theory "HOL-Algebra.Multiplicative_Group"
Presenting theory "Jordan_Normal_Form.Column_Operations"
Presenting theory "Three_Squares.Quadratic_Forms"
Presenting theory "CVP_Hardness.CVP_vec"
Presenting theory "HyperHoareLogic.Logic"
Presenting theory "HOL-Library.Ramsey"
Presenting theory "CVP_Hardness.Digits_int"
Presenting theory "Finitely_Generated_Abelian_Groups.Set_Multiplication"
Presenting theory "CVP_Hardness.Additional_Lemmas"
Presenting theory "Given_Clause_Loops.Fair_Zipperposition_Loop_without_Ghosts"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "Given_Clause_Loops.Given_Clause_Loops"
Presenting MHComputation in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MHComputation" ...
Presenting document MHComputation/document
Presenting document MHComputation/outline
Presenting theory "MHComputation.MHComputation"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting MLSS_Decision_Proc in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MLSS_Decision_Proc" ...
Presenting document MLSS_Decision_Proc/document
Presenting document MLSS_Decision_Proc/outline
Presenting theory "Finitely_Generated_Abelian_Groups.Miscellaneous_Groups"
Presenting theory "MLSS_Decision_Proc.MLSS_Logic"
Presenting theory "HOL-Number_Theory.Totient"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Jordan_Normal_Form.Determinant"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "HOL-Library.While_Combinator"
Presenting theory "HyperHoareLogic.Examples"
Presenting theory "HOL-Number_Theory.Residues"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "Finitely_Generated_Abelian_Groups.Generated_Groups_Extend"
Presenting theory "Jordan_Normal_Form.Char_Poly"
Presenting theory "HOL-Number_Theory.Eratosthenes"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "Well_Quasi_Orders.Least_Enum"
Presenting theory "HOL-Library.Power_By_Squaring"
Presenting theory "HereditarilyFinite.HF"
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "HOL-Number_Theory.Mod_Exp"
Presenting theory "HOL-Number_Theory.Euler_Criterion"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "HyperHoareLogic.ProgramHyperproperties"
Presenting theory "HereditarilyFinite.Ordinal"
Presenting theory "Well_Quasi_Orders.Almost_Full"
Presenting theory "HOL-Number_Theory.Gauss"
Presenting theory "CommCSL.AbstractCommutativity"
Presenting theory "HereditarilyFinite.Rank"
Presenting theory "MLSS_Decision_Proc.MLSS_HF_Extras"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "HereditarilyFinite.Finitary"
Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
Presenting theory "Graph_Theory.Rtrancl_On"
Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
Presenting theory "HOL-Number_Theory.Quadratic_Reciprocity"
Presenting theory "Polynomials.Utils"
Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form"
Presenting theory "HOL-Library.Function_Algebras"
Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
Presenting theory "VectorSpace.RingModuleFacts"
Presenting theory "VectorSpace.FunctionLemmas"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "VectorSpace.MonoidSums"
Presenting theory "CVP_Hardness.BHLE"
Presenting theory "HOL-Algebra.QuotRing"
Presenting theory "Polynomials.Power_Products"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Number_Theory.Pocklington"
Presenting theory "HOL-Algebra.IntRing"
Presenting theory "Polynomials.More_Modules"
Presenting theory "VectorSpace.LinearCombinations"
Presenting theory "CVP_Hardness.SVP_vec"
Presenting No_FTL_observers_Gen_Rel in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/No_FTL_observers_Gen_Rel" ...
Presenting theory "HOL-Library.Infinite_Set"
Presenting document No_FTL_observers_Gen_Rel/document
Presenting document No_FTL_observers_Gen_Rel/outline
Presenting theory "Finitely_Generated_Abelian_Groups.General_Auxiliary"
Presenting theory "VectorSpace.SumSpaces"
Presenting theory "HOL-Number_Theory.Prime_Powers"
Presenting theory "No_FTL_observers_Gen_Rel.Sorts"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "Polynomials.MPoly_Type_Class"
Presenting theory "HOL-Library.Countable_Complete_Lattices"
Presenting theory "Finitely_Generated_Abelian_Groups.IDirProds"
Presenting theory "No_FTL_observers_Gen_Rel.Points"
Presenting theory "Factor_Algebraic_Polynomial.Poly_Connection"
Presenting theory "HOL-Number_Theory.Residue_Primitive_Roots"
Presenting theory "No_FTL_observers_Gen_Rel.WorldView"
Presenting theory "HOL-Number_Theory.Number_Theory"
Presenting theory "HOL-Library.Order_Continuity"
Presenting theory "Skip_Lists.Pi_pmf"
Presenting theory "No_FTL_observers_Gen_Rel.Functions"
Presenting theory "No_FTL_observers_Gen_Rel.WorldLine"
Presenting theory "HOL-Library.Interval"
Presenting theory "Schwartz_Zippel.Schwartz_Zippel"
Presenting theory "HOL-Library.Extended_Nat"
Presenting theory "CommCSL.Guards"
Presenting theory "HOL-Algebra.Congruence"
Presenting theory "HOL-Library.Interval_Float"
Presenting theory "VectorSpace.VectorSpace"
Presenting theory "No_FTL_observers_Gen_Rel.Translations"
Presenting theory "HOL-Algebra.Order"
Presenting theory "No_FTL_observers_Gen_Rel.AxSelfMinus"
Presenting theory "HOL-Algebra.Lattice"
Presenting theory "Finitely_Generated_Abelian_Groups.Finite_Product_Extend"
Presenting theory "No_FTL_observers_Gen_Rel.TangentLines"
Presenting theory "No_FTL_observers_Gen_Rel.Cones"
Presenting theory "HOL-Library.Liminf_Limsup"
Presenting theory "No_FTL_observers_Gen_Rel.AxLightMinus"
Presenting theory "HOL-Algebra.Complete_Lattice"
Presenting theory "Finitely_Generated_Abelian_Groups.Group_Hom"
Presenting theory "No_FTL_observers_Gen_Rel.Proposition1"
Presenting theory "No_FTL_observers_Gen_Rel.AxEField"
Presenting theory "No_FTL_observers_Gen_Rel.Norms"
Presenting theory "No_FTL_observers_Gen_Rel.AxTriangleInequality"
Presenting theory "Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups"
Presenting theory "HOL-Algebra.Group"
Presenting theory "No_FTL_observers_Gen_Rel.Sublemma3"
Presenting theory "HOL-Decision_Procs.Dense_Linear_Order"
Presenting theory "HOL-Algebra.FiniteProduct"
Presenting theory "Jordan_Normal_Form.Missing_VectorSpace"
Presenting file "~~/src/HOL/Decision_Procs/langford_data.ML"
Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff_data.ML"
Presenting file "~~/src/HOL/Decision_Procs/langford.ML"
Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"
Presenting theory "No_FTL_observers_Gen_Rel.Vectors"
Presenting theory "HOL-Algebra.Ring"
Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
Presenting theory "No_FTL_observers_Gen_Rel.CauchySchwarz"
Presenting theory "Jordan_Normal_Form.Missing_Ring"
Presenting theory "No_FTL_observers_Gen_Rel.Matrices"
Presenting theory "Jordan_Normal_Form.Conjugate"
Presenting theory "HOL-Algebra.Module"
Presenting theory "HyperHoareLogic.Expressivity"
Presenting Rensets in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rensets" ...
Presenting document Rensets/document
Presenting document Rensets/outline
Presenting theory "No_FTL_observers_Gen_Rel.LinearMaps"
Presenting theory "Finitely_Generated_Abelian_Groups.DirProds"
Presenting theory "Jordan_Normal_Form.Matrix"
Presenting theory "Jordan_Normal_Form.VS_Connect"
Presenting theory "HOL-Library.Extended_Real"
Presenting theory "Finitely_Generated_Abelian_Groups.Group_Relations"
Presenting theory "No_FTL_observers_Gen_Rel.Affine"
Presenting theory "Graph_Theory.Stuff"
Presenting theory "No_FTL_observers_Gen_Rel.Sublemma4"
Presenting theory "Jordan_Normal_Form.Gauss_Jordan_Elimination"
Presenting theory "Rensets.Lambda_Terms"
Presenting theory "HOL-Decision_Procs.Approximation_Bounds"
Presenting theory "Jordan_Normal_Form.Gram_Schmidt"
Presenting theory "Graph_Theory.Digraph"
Presenting theory "Jordan_Normal_Form.Column_Operations"
Presenting theory "Rensets.Rensets"
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 "HOL-Library.Code_Target_Int"
Presenting theory "Rensets.Nominal_Sets"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "Rensets.Rensets_to_Nominal_Sets"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "HOL-Library.Code_Target_Numeral"
Presenting theory "No_FTL_observers_Gen_Rel.MainLemma"
Presenting theory "Lehmer.Lehmer"
Presenting theory "Jordan_Normal_Form.Schur_Decomposition"
Presenting theory "No_FTL_observers_Gen_Rel.AxDiff"
Presenting theory "CommCSL.Safety"
Presenting theory "Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups"
Presenting theory "Rensets.FRBCE_Rensets"
Presenting theory "No_FTL_observers_Gen_Rel.TangentLineLemma"
Presenting theory "No_FTL_observers_Gen_Rel.Proposition2"
Presenting theory "No_FTL_observers_Gen_Rel.AxEventMinus"
Presenting theory "Rensets.Substitutive_Sets"
Presenting theory "No_FTL_observers_Gen_Rel.Proposition3"
Presenting theory "No_FTL_observers_Gen_Rel.ObserverConeLemma"
Presenting theory "Jordan_Normal_Form.Determinant"
Presenting theory "Rensets.Examples"
Presenting theory "Rensets.All"
Presenting theory "Pratt_Certificate.Pratt_Certificate"
Presenting Suppes_Theorem in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Suppes_Theorem" ...
Presenting document Suppes_Theorem/document
Presenting document Suppes_Theorem/outline
Presenting theory "No_FTL_observers_Gen_Rel.Quadratics"
Presenting file "$AFP/Pratt_Certificate/pratt.ML"
Presenting theory "Schwartz_Zippel.Rand_Perfect_Matching"
Presenting theory "Propositional_Logic_Class.Implication_Logic"
Presenting Probability_Inequality_Completeness in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probability_Inequality_Completeness" ...
Presenting document Probability_Inequality_Completeness/document
Presenting document Probability_Inequality_Completeness/outline
Presenting theory "Propositional_Logic_Class.Classical_Logic"
Presenting theory "Propositional_Logic_Class.Classical_Logic_Completeness"
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 "No_FTL_observers_Gen_Rel.Classification"
Presenting theory "Dirichlet_L.Multiplicative_Characters"
Presenting theory "HOL-Number_Theory.Fib"
Presenting theory "No_FTL_observers_Gen_Rel.ReverseCauchySchwarz"
Presenting theory "Bertrands_Postulate.Bertrand"
Presenting theory "HOL-Number_Theory.Eratosthenes"
Presenting theory "HOL-Library.Power_By_Squaring"
Presenting theory "HOL-Number_Theory.Mod_Exp"
Presenting file "$AFP/Bertrands_Postulate/bertrand.ML"
Presenting theory "No_FTL_observers_Gen_Rel.KeyLemma"
Presenting theory "No_FTL_observers_Gen_Rel.Cardinalities"
Presenting theory "Jordan_Normal_Form.Jordan_Normal_Form_Existence"
Presenting theory "HOL-Number_Theory.Pocklington"
Presenting theory "No_FTL_observers_Gen_Rel.AffineConeLemma"
Presenting theory "Frequency_Moments.Frequency_Moments_Preliminary_Results"
Presenting theory "HOL-Combinatorics.List_Permutation"
Presenting theory "HOL-Number_Theory.Prime_Powers"
Presenting theory "No_FTL_observers_Gen_Rel.NoFTLGR"
Presenting Tree_Enumeration in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tree_Enumeration" ...
Presenting document Tree_Enumeration/document
Presenting document Tree_Enumeration/outline
Presenting theory "Jordan_Normal_Form.Spectral_Radius"
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 "HOL-Number_Theory.Residue_Primitive_Roots"
Presenting theory "Perron_Frobenius.Bij_Nat"
Presenting theory "HOL-Library.Multiset"
Presenting theory "HOL-Number_Theory.Number_Theory"
Presenting theory "Dirichlet_Series.Dirichlet_Misc"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "Dirichlet_Series.Multiplicative_Function"
Presenting theory "Perron_Frobenius.Cancel_Card_Constraint"
Presenting file "$AFP/Perron_Frobenius/cancel_card_constraint.ML"
Presenting theory "Dirichlet_L.Dirichlet_Characters"
Presenting theory "Bernoulli.Bernoulli"
Presenting theory "Bernoulli.Periodic_Bernpoly"
Presenting theory "HOL-Computational_Algebra.Fraction_Field"
Presenting theory "HOL-Computational_Algebra.Fundamental_Theorem_Algebra"
Presenting theory "HOL-Computational_Algebra.Group_Closure"
Presenting theory "HOL-Library.FuncSet"
Presenting theory "HOL-Computational_Algebra.Normalized_Fraction"
Presenting theory "HOL-Computational_Algebra.Nth_Powers"
Presenting theory "Perron_Frobenius.HMA_Connect"
Presenting theory "HOL-Library.Multiset"
Presenting theory "HOL-Computational_Algebra.Polynomial_Factorial"
Presenting theory "HOL-Algebra.Divisibility"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "Isabelle_Marries_Dirac.Basics"
Presenting theory "HOL-Computational_Algebra.Squarefree"
Presenting theory "HOL-Computational_Algebra.Computational_Algebra"
Presenting theory "HOL-Combinatorics.Stirling"
Presenting theory "HOL-Library.Disjoint_Sets"
Presenting theory "Isabelle_Marries_Dirac.Binary_Nat"
Presenting theory "HOL-Combinatorics.Transposition"
Presenting theory "Bernoulli.Bernoulli_FPS"
Presenting theory "HOL-Library.FuncSet"
Presenting theory "HOL-Library.Multiset"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "HOL-Library.Disjoint_Sets"
Presenting theory "Euler_MacLaurin.Euler_MacLaurin"
Presenting theory "HOL-Algebra.QuotRing"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "Bernoulli.Bernoulli_Zeta"
Presenting theory "HOL-Library.Going_To_Filter"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "HOL-Library.FuncSet"
Presenting theory "HOL-Combinatorics.Permutations"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Algebra.Ring_Divisibility"
Presenting theory "Graph_Theory.Bidirected_Digraph"
Presenting theory "Isabelle_Marries_Dirac.Quantum"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "HOL-Library.Disjoint_Sets"
Presenting theory "HOL-Algebra.Subrings"
Presenting theory "Isabelle_Marries_Dirac.Complex_Vectors"
Presenting theory "HOL-Combinatorics.Transposition"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "Graph_Theory.Arc_Walk"
Presenting theory "HOL-Library.Countable_Complete_Lattices"
Presenting theory "Matrix.Utility"
Presenting theory "Probability_Inequality_Completeness.Probability_Inequality_Completeness"
Presenting theory "HOL-Library.Order_Continuity"
Presenting theory "Graph_Theory.Pair_Digraph"
Presenting theory "HOL-Library.Extended_Nat"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "HOL-Library.Liminf_Limsup"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "HOL-Combinatorics.Permutations"
Presenting theory "HOL-Combinatorics.List_Permutation"
Presenting theory "Graph_Theory.Digraph_Component"
Presenting theory "HOL-Library.While_Combinator"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Graph_Theory.Vertex_Walk"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Graph_Theory.Digraph_Component_Vwalk"
Presenting theory "HOL-Algebra.Polynomials"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "Propositional_Logic_Class.List_Utilities"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "HOL-Library.BNF_Corec"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML"
Presenting theory "Graph_Theory.Digraph_Isomorphism"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
Presenting theory "HOL-Real_Asymp.Lazy_Eval"
Presenting file "~~/src/HOL/Real_Asymp/lazy_eval.ML"
Presenting theory "HOL-Real_Asymp.Inst_Existentials"
Presenting file "~~/src/HOL/Real_Asymp/inst_existentials.ML"
Presenting theory "HOL-Real_Asymp.Eventuallize"
Presenting theory "Propositional_Logic_Class.Classical_Connectives"
Presenting theory "HOL-Combinatorics.Orbits"
Presenting theory "HOL-Algebra.Embedded_Algebras"
Presenting theory "Graph_Theory.Auxiliary"
Presenting theory "Graph_Theory.Subdivision"
Presenting theory "HOL-Library.Old_Datatype"
Presenting theory "HOL-Library.Extended_Real"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "Graph_Theory.Euler"
Presenting theory "Girth_Chromatic.Girth_Chromatic_Misc"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "Suppes_Theorem.Probability_Logic"
Presenting theory "Undirected_Graph_Theory.Undirected_Graph_Basics"
Presenting theory "HOL-Library.Rewrite"
Presenting file "~~/src/HOL/Library/cconv.ML"
Presenting file "~~/src/HOL/Library/rewrite.ML"
Presenting theory "HOL-Algebra.Polynomial_Divisibility"
Presenting theory "Suppes_Theorem.Suppes_Theorem"
Presenting theory "Undirected_Graph_Theory.Undirected_Graph_Walks"
Presenting theory "HOL-Real_Asymp.Multiseries_Expansion"
Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
Presenting theory "Undirected_Graph_Theory.Connectivity"
Presenting theory "Finite_Fields.Finite_Fields_Preliminary_Results"
Presenting theory "Graph_Theory.Kuratowski"
Presenting theory "Undirected_Graph_Theory.Girth_Independence"
Presenting file "~~/src/HOL/Real_Asymp/asymptotic_basis.ML"
Presenting file "~~/src/HOL/Real_Asymp/exp_log_expression.ML"
Presenting file "~~/src/HOL/Real_Asymp/expansion_interface.ML"
Presenting file "~~/src/HOL/Real_Asymp/multiseries_expansion.ML"
Presenting theory "HOL-Combinatorics.Transposition"
Presenting theory "Graph_Theory.Weighted_Graph"
Presenting file "~~/src/HOL/Real_Asymp/real_asymp.ML"
Presenting theory "Finite_Fields.Finite_Fields_Factorization_Ext"
Presenting theory "Graph_Theory.Shortest_Path"
Presenting theory "Graph_Theory.Graph_Theory"
Presenting theory "Abstract-Rewriting.SN_Orders"
Presenting theory "HOL-Algebra.IntRing"
Presenting theory "MLSS_Decision_Proc.MLSS_Realisation"
Presenting theory "Matrix.Ordered_Semiring"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "MLSS_Decision_Proc.MLSS_Semantics"
Presenting theory "Finite_Fields.Ring_Characteristic"
Presenting theory "HOL-Real_Asymp.Multiseries_Expansion_Bounds"
Presenting file "~~/src/HOL/Real_Asymp/multiseries_expansion_bounds.ML"
Presenting theory "Universal_Hash_Families.Field"
Presenting theory "Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials"
Presenting theory "HOL-Real_Asymp.Real_Asymp"
Presenting file "~~/src/HOL/Real_Asymp/real_asymp_diag.ML"
Presenting theory "HOL-Combinatorics.Permutations"
Presenting theory "Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation"
Presenting theory "Dirichlet_Series.Dirichlet_Product"
Presenting theory "HOL-Library.Sublist"
Presenting theory "Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities"
Presenting theory "Matrix.Matrix_Legacy"
Presenting theory "MLSS_Decision_Proc.MLSS_Typing_Defs"
Presenting theory "Frequency_Moments.Frequency_Moments"
Presenting theory "HOL-Combinatorics.Multiset_Permutations"
Presenting theory "Dirichlet_Series.Dirichlet_Series"
Presenting theory "Undirected_Graph_Theory.Graph_Triangles"
Presenting theory "Dirichlet_Series.Moebius_Mu"
Presenting theory "MLSS_Decision_Proc.MLSS_Calculus"
Presenting theory "Dirichlet_Series.More_Totient"
Presenting theory "Dirichlet_Series.Liouville_Lambda"
Presenting theory "Median_Method.Median"
Presenting theory "Dirichlet_Series.Divisor_Count"
Presenting theory "Undirected_Graph_Theory.Bipartite_Graphs"
Presenting theory "Dirichlet_Series.Arithmetic_Summatory"
Presenting theory "Dirichlet_Series.Partial_Summation"
Presenting theory "Frequency_Moments.K_Smallest"
Presenting theory "MLSS_Decision_Proc.MLSS_Typing"
Presenting theory "Universal_Hash_Families.Definitions"
Presenting theory "Dirichlet_Series.Euler_Products"
Presenting theory "Universal_Hash_Families.Preliminary_Results"
Presenting theory "Card_Partitions.Set_Partition"
Presenting theory "Universal_Hash_Families.Carter_Wegman_Hash_Family"
Presenting theory "Dirichlet_Series.Dirichlet_Series_Analysis"
Presenting theory "HOL-Library.Multiset_Order"
Presenting theory "Sturm_Tarski.PolyMisc"
Presenting theory "HOL-Computational_Algebra.Field_as_Ring"
Presenting theory "Sturm_Tarski.Sturm_Tarski"
Presenting theory "HOL-Library.Landau_Symbols"
Presenting theory "MLSS_Decision_Proc.MLSS_Proc"
Presenting theory "Winding_Number_Eval.Missing_Topology"
Presenting theory "Fresh_Identifiers.Fresh"
Presenting theory "Frequency_Moments.Landau_Ext"
Presenting theory "Budan_Fourier.BF_Misc"
Presenting theory "HOL-Library.Sublist"
Presenting theory "Winding_Number_Eval.Missing_Algebraic"
Presenting theory "Frequency_Moments.Probability_Ext"
Presenting theory "MLSS_Decision_Proc.MLSS_Suc_Theory"
Presenting theory "Winding_Number_Eval.Missing_Transcendental"
Presenting theory "Frequency_Moments.Product_PMF_Ext"
Presenting theory "Winding_Number_Eval.Missing_Analysis"
Presenting theory "MLSS_Decision_Proc.MLSS_Typing_Urelems"
Presenting theory "Fresh_Identifiers.Fresh_Nat"
Presenting theory "Nested_Multisets_Ordinals.Multiset_More"
Presenting theory "Nested_Multisets_Ordinals.Duplicate_Free_Multiset"
Presenting theory "CommCSL.Soundness"
Presenting theory "List-Index.List_Index"
Presenting theory "CommCSL.NonInterference"
Presenting theory "Frequency_Moments.Frequency_Moment_0"
Presenting theory "MLSS_Decision_Proc.MLSS_Proc_Code"
Presenting theory "Design_Theory.Multisets_Extras"
Presenting theory "MLSS_Decision_Proc.MLSS_Proc_All"
Presenting theory "HOL-Combinatorics.Stirling"
Presenting theory "Design_Theory.Design_Basics"
Presenting theory "Winding_Number_Eval.Cauchy_Index_Theorem"
Presenting theory "Card_Partitions.Set_Partition"
Presenting theory "Design_Theory.Design_Operations"
Presenting theory "Design_Theory.Block_Designs"
Presenting theory "Design_Theory.BIBD"
Presenting theory "Design_Theory.Resolvable_Designs"
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 "Card_Partitions.Injectivity_Solver"
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 "Card_Partitions.Card_Partitions"
Presenting theory "HOL-Eisbach.Eisbach_Tools"
Presenting theory "Design_Theory.Group_Divisible_Designs"
Presenting theory "Bell_Numbers_Spivey.Bell_Numbers"
Presenting theory "Undirected_Graph_Theory.Graph_Theory_Relations"
Presenting theory "Undirected_Graph_Theory.Undirected_Graphs_Root"
Presenting theory "Card_Equiv_Relations.Card_Equiv_Relations"
Presenting theory "Equivalence_Relation_Enumeration.Equivalence_Relation_Enumeration"
Presenting theory "Tree_Enumeration.Tree_Graph"
Presenting theory "Winding_Number_Eval.Winding_Number_Eval"
Presenting theory "Tree_Enumeration.Labeled_Tree_Enumeration"
Presenting theory "Frequency_Moments.Frequency_Moment_2"
Presenting theory "HOL-Library.Function_Algebras"
Presenting theory "Zeta_Function.Zeta_Library"
Presenting theory "Pure-ex.Guess"
Presenting theory "Matrix_Tensor.Matrix_Tensor"
Presenting theory "HOL-Library.FSet"
Presenting theory "Ergodic_Theory.SG_Library_Complement"
Presenting theory "Isabelle_Marries_Dirac.Tensor"
Presenting theory "Lp.Functional_Spaces"
Presenting theory "Zeta_Function.Zeta_Function"
Presenting theory "Tree_Enumeration.Rooted_Tree"
Presenting theory "Isabelle_Marries_Dirac.More_Tensor"
Presenting theory "Tree_Enumeration.Rooted_Tree_Enumeration"
Presenting theory "Dirichlet_L.Dirichlet_L_Functions"
Presenting theory "HOL-Library.Lattice_Algebras"
Presenting theory "Lp.Lp"
Presenting theory "HOL-Library.Interval"
Presenting theory "QHLProver.Complex_Matrix"
Presenting theory "HOL-Library.Log_Nat"
Presenting file "$AFP/QHLProver/mat_alg.ML"
Presenting theory "HOL-Library.Float"
Presenting theory "QHLProver.Gates"
Presenting theory "HOL-Types_To_Sets.Prerequisites"
Presenting theory "HOL-Library.Interval_Float"
Presenting theory "Frequency_Moments.Frequency_Moment_k"
Presenting theory "HOL-Types_To_Sets.Group_On_With"
Presenting theory "HOL-Decision_Procs.Dense_Linear_Order"
Presenting file "~~/src/HOL/Decision_Procs/langford_data.ML"
Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff_data.ML"
Presenting file "~~/src/HOL/Decision_Procs/langford.ML"
Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"
Presenting theory "Projective_Measurements.Linear_Algebra_Complements"
Presenting theory "HOL-Decision_Procs.Approximation_Bounds"
Presenting theory "Projective_Measurements.Projective_Measurements"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "HOL-Library.Code_Target_Numeral"
Presenting theory "Lehmer.Lehmer"
Presenting theory "Commuting_Hermitian.Spectral_Theory_Complements"
Presenting theory "Pratt_Certificate.Pratt_Certificate"
Presenting file "$AFP/Pratt_Certificate/pratt.ML"
Presenting theory "Commuting_Hermitian.Commuting_Hermitian_Misc"
Presenting theory "Bertrands_Postulate.Bertrand"
Presenting file "$AFP/Bertrands_Postulate/bertrand.ML"
Presenting theory "HOL-Library.Function_Algebras"
Presenting theory "Landau_Symbols.Group_Sort"
Presenting theory "Commuting_Hermitian.Commuting_Hermitian"
Presenting theory "Landau_Symbols.Landau_Real_Products"
Presenting theory "Landau_Symbols.Landau_Simprocs"
Presenting file "$AFP/Landau_Symbols/landau_simprocs.ML"
Presenting theory "Landau_Symbols.Landau_More"
Presenting theory "Dirichlet_L.Dirichlet_Theorem"
Presenting theory "Expander_Graphs.Expander_Graphs_Eigenvalues"
Presenting theory "Three_Squares.Three_Squares"
Presenting theory "Expander_Graphs.Expander_Graphs_Cheeger_Inequality"
Presenting theory "HOL-Library.Code_Target_Numeral_Float"
Presenting theory "HOL-Decision_Procs.Approximation"
Presenting file "~~/src/HOL/Decision_Procs/approximation.ML"
Presenting file "~~/src/HOL/Decision_Procs/approximation_generator.ML"
Presenting theory "Expander_Graphs.Expander_Graphs_MGG"
Presenting theory "Expander_Graphs.Expander_Graphs_Walks"
Presenting theory "Expander_Graphs.Expander_Graphs_Power_Construction"
Presenting theory "Expander_Graphs.Expander_Graphs_Strongly_Explicit"
Unfinished session(s): Simple_Clause_Learning

=== TIMING ===

Group AFP: 0:50:40 elapsed time, 2:57:49 cpu time, factor 3.51
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:19:08 elapsed time, 2:57:49 cpu time, factor 9.29

=== FAILED SESSIONS ===

Session Simple_Clause_Learning: FAILED 1

=== DEPENDENCIES ===

Generating dependencies file ...
Writing dependencies file ...

=== REPORT ===

Writing report file ...

=== SITEGEN ===

Writing status file ...
Running sitegen ...
using [/media/data/jenkins/workspace/isabelle-all/bin/isabelle]
Preparing site generation in out/hugo
Cleaning up generated files...
Preparing topics...
Preparing licenses...
Preparing releases...
Preparing authors...
Extracting keywords...
Preparing entries...
Preparing statistics...
Preparing project files
Preparing devel version...
Finished sitegen preparation.
Cleaning output dir...
Building site...
Build in /media/data/jenkins/workspace/isabelle-all/afp/web/index.html
Packing tars ...

=== NOTIFICATIONS ===


=== COMPLETED ===

Build step 'Execute shell' marked build as failure
ERROR: Failed to evaluate groovy script.
java.lang.InterruptedException
	at java.base/java.lang.Object.wait(Native Method)
	at hudson.remoting.Request$1.get(Request.java:318)
	at hudson.remoting.Request$1.get(Request.java:240)
	at hudson.remoting.FutureAdapter.get(FutureAdapter.java:66)
	at hudson.FilePath.copyRecursiveTo(FilePath.java:2831)
	at hudson.FilePath.copyRecursiveTo(FilePath.java:2792)
	at hudson.FilePath.copyRecursiveTo(FilePath.java:2780)
	at hudson.FilePath.copyRecursiveTo(FilePath.java:2763)
	at hudson.FilePath.copyRecursiveTo(FilePath.java:2748)
	at hudson.FilePath$copyRecursiveTo$2.call(Unknown Source)
	at org.codehaus.groovy.runtime.callsite.CallSiteArray.defaultCall(CallSiteArray.java:47)
	at org.codehaus.groovy.runtime.callsite.AbstractCallSite.call(AbstractCallSite.java:116)
	at org.codehaus.groovy.runtime.callsite.AbstractCallSite.call(AbstractCallSite.java:128)
	at Script1.run(Script1.groovy:17)
	at groovy.lang.GroovyShell.evaluate(GroovyShell.java:574)
	at groovy.lang.GroovyShell.evaluate(GroovyShell.java:612)
	at groovy.lang.GroovyShell.evaluate(GroovyShell.java:583)
	at org.jenkinsci.plugins.scriptsecurity.sandbox.groovy.SecureGroovyScript.evaluate(SecureGroovyScript.java:450)
	at org.jenkinsci.plugins.scriptsecurity.sandbox.groovy.SecureGroovyScript.evaluate(SecureGroovyScript.java:387)
	at org.jvnet.hudson.plugins.groovypostbuild.GroovyPostbuildRecorder.perform(GroovyPostbuildRecorder.java:406)
	at hudson.tasks.BuildStepMonitor$1.perform(BuildStepMonitor.java:20)
	at hudson.model.AbstractBuild$AbstractBuildExecution.perform(AbstractBuild.java:818)
	at hudson.model.AbstractBuild$AbstractBuildExecution.performAllBuildSteps(AbstractBuild.java:767)
	at hudson.model.Build$BuildExecution.post2(Build.java:179)
	at hudson.model.AbstractBuild$AbstractBuildExecution.post(AbstractBuild.java:711)
	at hudson.model.Run.execute(Run.java:1925)
	at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44)
	at hudson.model.ResourceController.execute(ResourceController.java:101)
	at hudson.model.Executor.run(Executor.java:442)
Build step 'Groovy Postbuild' marked build as failure
Started calculate disk usage of build
Finished Calculation of disk usage of build in 0 seconds
Email was triggered for: Failure - 1st
Trigger Failure - Any was overridden by another trigger and will not send an email.
Trigger Failure - Still was overridden by another trigger and will not send an email.
Sending email for trigger: Failure - 1st
Sending email to: isabelle-ci@mailman46.in.tum.de
ERROR: Could not send email as a part of the post-build publishers.
java.lang.IllegalStateException: Jenkins.instance is missing. Read the documentation of Jenkins.getInstanceOrNull to see what you are doing wrong.
	at jenkins.model.Jenkins.get(Jenkins.java:814)
	at hudson.plugins.emailext.plugins.EmailTrigger.getDescriptor(EmailTrigger.java:144)
	at hudson.plugins.emailext.ExtendedEmailPublisher.getRuntimeMacros(ExtendedEmailPublisher.java:671)
	at hudson.plugins.emailext.ExtendedEmailPublisher.executeScript(ExtendedEmailPublisher.java:695)
	at hudson.plugins.emailext.ExtendedEmailPublisher.executePostsendScript(ExtendedEmailPublisher.java:683)
	at hudson.plugins.emailext.ExtendedEmailPublisher.sendMail(ExtendedEmailPublisher.java:641)
	at hudson.plugins.emailext.ExtendedEmailPublisher._perform(ExtendedEmailPublisher.java:484)
	at hudson.plugins.emailext.ExtendedEmailPublisher.perform(ExtendedEmailPublisher.java:385)
	at hudson.tasks.BuildStepMonitor$1.perform(BuildStepMonitor.java:20)
	at hudson.model.AbstractBuild$AbstractBuildExecution.perform(AbstractBuild.java:818)
	at hudson.model.AbstractBuild$AbstractBuildExecution.performAllBuildSteps(AbstractBuild.java:767)
	at hudson.model.Build$BuildExecution.cleanUp(Build.java:189)
	at hudson.model.Run.execute(Run.java:1947)
	at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44)
	at hudson.model.ResourceController.execute(ResourceController.java:101)
	at hudson.model.Executor.run(Executor.java:442)
ERROR: Build step failed with exception
java.lang.IllegalStateException: Jenkins.instance is missing. Read the documentation of Jenkins.getInstanceOrNull to see what you are doing wrong.
	at jenkins.model.Jenkins.get(Jenkins.java:814)
	at hudson.plugins.emailext.ExtendedEmailPublisher.getDescriptor(ExtendedEmailPublisher.java:1194)
	at hudson.plugins.emailext.ExtendedEmailPublisher.debug(ExtendedEmailPublisher.java:367)
	at hudson.plugins.emailext.ExtendedEmailPublisher.sendMail(ExtendedEmailPublisher.java:663)
	at hudson.plugins.emailext.ExtendedEmailPublisher._perform(ExtendedEmailPublisher.java:484)
	at hudson.plugins.emailext.ExtendedEmailPublisher.perform(ExtendedEmailPublisher.java:385)
	at hudson.tasks.BuildStepMonitor$1.perform(BuildStepMonitor.java:20)
	at hudson.model.AbstractBuild$AbstractBuildExecution.perform(AbstractBuild.java:818)
	at hudson.model.AbstractBuild$AbstractBuildExecution.performAllBuildSteps(AbstractBuild.java:767)
	at hudson.model.Build$BuildExecution.cleanUp(Build.java:189)
	at hudson.model.Run.execute(Run.java:1947)
	at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44)
	at hudson.model.ResourceController.execute(ResourceController.java:101)
	at hudson.model.Executor.run(Executor.java:442)
ERROR: Post-build steps failed
java.lang.IllegalStateException: Jenkins.instance is missing. Read the documentation of Jenkins.getInstanceOrNull to see what you are doing wrong.
	at jenkins.model.Jenkins.get(Jenkins.java:814)
	at hudson.plugins.emailext.ExtendedEmailPublisher.getDescriptor(ExtendedEmailPublisher.java:1194)
	at hudson.plugins.emailext.ExtendedEmailPublisher.getDescriptor(ExtendedEmailPublisher.java:102)
	at hudson.model.AbstractBuild$AbstractBuildExecution.reportError(AbstractBuild.java:786)
	at hudson.model.AbstractBuild$AbstractBuildExecution.performAllBuildSteps(AbstractBuild.java:775)
	at hudson.model.Build$BuildExecution.cleanUp(Build.java:189)
	at hudson.model.Run.execute(Run.java:1947)
	at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44)
	at hudson.model.ResourceController.execute(ResourceController.java:101)
	at hudson.model.Executor.run(Executor.java:442)
FATAL: Jenkins.instance is missing. Read the documentation of Jenkins.getInstanceOrNull to see what you are doing wrong.
java.lang.IllegalStateException: Jenkins.instance is missing. Read the documentation of Jenkins.getInstanceOrNull to see what you are doing wrong.
	at jenkins.model.Jenkins.get(Jenkins.java:814)
	at hudson.tasks.BuildTrigger.execute(BuildTrigger.java:274)
	at hudson.model.AbstractBuild$AbstractBuildExecution.cleanUp(AbstractBuild.java:728)
	at hudson.model.Build$BuildExecution.cleanUp(Build.java:194)
	at hudson.model.Run.execute(Run.java:1947)
	at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44)
	at hudson.model.ResourceController.execute(ResourceController.java:101)
	at hudson.model.Executor.run(Executor.java:442)
Finished: FAILURE