![[Jenkins]](/jenkins/static/109fb1e5/images/svgs/logo.svg){kind=logo}
[EnvInject] - Loading node environment variables.
Building remotely on workermtahpc (mta_hpc) in workspace /media/data/jenkins/workspace/isabelle-all
[isabelle-all] $ hg showconfig paths.default
[isabelle-all] $ hg pull --rev default
pulling from http://isabelle.in.tum.de/repos/isabelle/
real URL is https://isabelle.in.tum.de/repos/isabelle/
[isabelle-all] $ hg update --clean --rev default
0 files updated, 0 files merged, 0 files removed, 0 files unresolved
[isabelle-all] $ hg log --rev . --template {node}
[isabelle-all] $ hg log --rev . --template {rev}
[isabelle-all] $ hg log --rev 1cadc477f644c89c0fae513f51ff81f4af684c1d --template exists\n
[isabelle-all] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(1cadc477f644c89c0fae513f51ff81f4af684c1d)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
pulling from https://foss.heptapod.net/isa-afp/afp-devel/
[afp] $ hg update --clean --rev default
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
[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
[isabelle-all] $ /bin/sh -xe /tmp/jenkins12050969793957505254.sh
### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle.jar) ...
### Building graph browser (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_graphbrowser.jar) ...
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_admin.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
[NOTE] Package zarith is already installed (current version is 1.12).
stack will use a sandboxed GHC it installed
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
The Glorious Glasgow Haskell Compilation System, version 8.10.7
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-a5d5fba90286/x86_64_32-linux"
Session Doc/Sledgehammer (doc)
Session AFP/Abortable_Linearizable_Modules (AFP)
Session AFP/Abstract-Hoare-Logics (AFP)
Session AFP/Ackermanns_not_PR (AFP)
Session AFP/Aristotles_Assertoric_Syllogistic (AFP)
Session AFP/Attack_Trees (AFP)
Session AFP/AxiomaticCategoryTheory (AFP)
Session AFP/Belief_Revision (AFP)
Session AFP/BinarySearchTree (AFP)
Session AFP/Binomial-Queues (AFP)
Session AFP/Boolos_Curious_Inference (AFP)
Session AFP/Boolos_Curious_Inference_Automated (AFP)
Session AFP/BytecodeLogicJmlTypes (AFP)
Session AFP/C2KA_DistributedSystems (AFP)
Session AFP/Sqrt_Babylonian (AFP)
Session AFP/ClockSynchInst (AFP)
Session AFP/Compiling-Exceptions-Correctly (AFP)
Session AFP/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_Easychair (doc)
Session Doc/Demo_FoilTeX (doc)
Session AFP/Depth-First-Search (AFP)
Session AFP/Digit_Expansions (AFP)
Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
Session AFP/Example-Submission (AFP)
Session AFP/FeatherweightJava (AFP)
Session AFP/Featherweight_OCL (AFP)
Session AFP/FileRefinement (AFP)
Session AFP/FocusStreamsCaseStudies (AFP)
Session AFP/Foundation_of_geometry (AFP)
Session AFP/Free-Boolean-Algebra (AFP)
Session AFP/Fresh_Identifiers (AFP)
Session AFP/FunWithFunctions (AFP)
Session AFP/FunWithTilings (AFP)
Session AFP/GPU_Kernel_PL (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/Generic_Deriving (AFP)
Session AFP/GewirthPGCProof (AFP)
Session AFP/Goodstein_Lambda (AFP)
Session HOL/HOL-Cardinals (timing)
Session AFP/Binding_Syntax_Theory (AFP)
Session AFP/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_Parallel (timing)
Session HOL/HOL-Library (main timing)
Session AFP/Approximation_Algorithms (AFP)
Session AFP/ArrowImpossibilityGS (AFP)
Session AFP/BNF_Operations (AFP)
Session AFP/Binomial-Heaps (AFP)
Session AFP/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/Card_Multisets (AFP)
Session AFP/Card_Number_Partitions (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/DOM_Components (AFP)
Session AFP/Shadow_SC_DOM (AFP)
Session AFP/SC_DOM_Components (AFP)
Session AFP/Decl_Sem_Fun_PL (AFP)
Session AFP/Encodability_Process_Calculi (AFP)
Session AFP/Euler_Partition (AFP)
Session AFP/FOL_Seq_Calc1 (AFP)
Session AFP/FOL_Axiomatic (AFP)
Session AFP/FOL_Harrison (AFP)
Session AFP/Factored_Transition_System_Bounding (AFP)
Session AFP/Extended_Finite_State_Machines (AFP)
Session AFP/Extended_Finite_State_Machine_Inference (AFP)
Session AFP/Finger-Trees (AFP)
Session AFP/Finite-Map-Extras (AFP)
Session AFP/Generalized_Counting_Sort (AFP)
Session AFP/Graph_Saturation (AFP)
Session AFP/Group-Ring-Module (AFP)
Session HOL/HOL-UNITY (timing)
Session HOL/HOL-Combinatorics (main timing)
Session AFP/Derangements (AFP)
Session AFP/Discrete_Summation (AFP)
Session AFP/Gauss-Jordan-Elim-Fun (AFP)
Session AFP/Graph_Theory (AFP)
Session AFP/ShortestPath (AFP)
Session HOL/HOL-Computational_Algebra (main timing)
Session AFP/Descartes_Sign_Rule (AFP)
Session HOL/HOL-Algebra (main timing)
Session AFP/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 HOL/HOL-Analysis (main timing)
Session AFP/Actuarial_Mathematics (AFP)
Session AFP/Cayley_Hamilton (AFP)
Session AFP/DynamicArchitectures (AFP)
Session AFP/Architectural_Design_Patterns (AFP)
Session AFP/Lazy-Lists-II (AFP)
Session AFP/Stream_Fusion_Code (AFP)
Session AFP/Complex_Geometry (AFP)
Session AFP/Poincare_Disc (AFP)
Session AFP/Differential_Game_Logic (AFP)
Session AFP/First_Welfare_Theorem (AFP)
Session HOL/HOL-Complex_Analysis (main timing)
Session AFP/Allen_Calculus (AFP)
Session AFP/Card_Partitions (AFP)
Session AFP/Bell_Numbers_Spivey (AFP)
Session AFP/Card_Equiv_Relations (AFP)
Session AFP/Equivalence_Relation_Enumeration (AFP)
Session AFP/Falling_Factorial_Sum (AFP)
Session AFP/Combinatorial_Enumeration_Algorithms (AFP)
Session AFP/Case_Labeling (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/Dependent_SIFUM_Type_Systems (AFP)
Session AFP/Dependent_SIFUM_Refinement (AFP)
Session HOL/HOL-Homology (timing)
Session HOL/HOL-Probability (main timing)
Session AFP/Buffons_Needle (AFP)
Session AFP/Density_Compiler (AFP)
Session AFP/DiscretePricing (AFP)
Session AFP/Ergodic_Theory (AFP)
Session AFP/Gromov_Hyperbolicity (AFP)
Session AFP/Laws_of_Large_Numbers (AFP)
Session AFP/Fisher_Yates (AFP)
Session AFP/Girth_Chromatic (AFP)
Session AFP/Random_Graph_Subgraph_Threshold (AFP)
Session HOL/HOL-Probability-ex (timing)
Session AFP/Hahn_Jordan_Decomposition (AFP)
Session AFP/Markov_Models (AFP)
Session AFP/Monad_Normalisation (AFP)
Session AFP/Monomorphic_Monad (AFP)
Session AFP/Neumann_Morgenstern_Utility (AFP)
Session AFP/Probabilistic_Noninterference (AFP)
Session AFP/Probabilistic_System_Zoo (AFP)
Session AFP/Quasi_Borel_Spaces (AFP)
Session AFP/Source_Coding_Theorem (AFP)
Session AFP/Turans_Graph_Theorem (AFP)
Session AFP/Irrationality_J_Hancl (AFP)
Session AFP/Kuratowski_Closure_Complement (AFP)
Session AFP/Laplace_Transform (AFP)
Session AFP/Lower_Semicontinuous (AFP)
Session AFP/Minkowskis_Theorem (AFP)
Session AFP/Ptolemys_Theorem (AFP)
Session AFP/Rank_Nullity_Theorem (AFP)
Session AFP/Gauss_Jordan (AFP)
Session AFP/Echelon_Form (AFP)
Session AFP/Tarskis_Geometry (AFP)
Session AFP/Chord_Segments (AFP)
Session AFP/Stewart_Apollonius (AFP)
Session AFP/Youngs_Inequality (AFP)
Session HOL/HOL-Nonstandard_Analysis (timing)
Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
Session HOL/HOL-Number_Theory (main timing)
Session AFP/Arith_Prog_Rel_Primes (AFP)
Session AFP/DigitsInBase (AFP)
Session AFP/E_Transcendental (AFP)
Session AFP/Elliptic_Curves_Group_Law (AFP)
Session HOL/HOL-Data_Structures (timing)
Session AFP/Efficient-Mergesort (AFP)
Session HOL/HOL-Codegenerator_Test
Session AFP/Query_Optimization (AFP)
Session AFP/Automatic_Refinement (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Lifting_the_Exponent (AFP)
Session AFP/Pratt_Certificate (AFP)
Session AFP/Bertrands_Postulate (AFP)
Session AFP/Prime_Harmonic_Series (AFP)
Session AFP/Liouville_Numbers (AFP)
Session AFP/Lucas_Theorem (AFP)
Session AFP/DPRM_Theorem (AFP)
Session AFP/Mason_Stothers (AFP)
Session AFP/Polynomial_Interpolation (AFP)
Session AFP/Formal_Puiseux_Series (AFP)
Session AFP/Probabilistic_Prime_Tests (AFP)
Session AFP/Rep_Fin_Groups (AFP)
Session AFP/Sturm_Sequences (AFP)
Session AFP/Safe_Distance (AFP)
Session AFP/Special_Function_Bounds (AFP)
Session AFP/Sturm_Tarski (AFP)
Session AFP/Budan_Fourier (AFP)
Session AFP/Three_Circles (AFP)
Session AFP/Winding_Number_Eval (AFP)
Session AFP/Count_Complex_Roots (AFP)
Session HOL/HOL-Corec_Examples (timing)
Session HOL/HOL-Datatype_Examples (timing)
Session AFP/Abs_Int_ITP2012 (AFP)
Session AFP/Relational-Incorrectness-Logic (AFP)
Session HOL/HOL-Imperative_HOL (timing)
Session AFP/Auto2_Imperative_HOL (AFP)
Session AFP/Imperative_Insertion_Sort (AFP)
Session HOL/HOL-Metis_Examples (timing)
Session HOL/HOL-Proofs (timing)
Session HOL/HOL-Proofs-Extraction (timing)
Session HOL/HOL-Proofs-Lambda (timing)
Session AFP/Applicative_Lifting (AFP)
Session AFP/Stern_Brocot (AFP)
Session AFP/HereditarilyFinite (AFP)
Session AFP/Isabelle_Meta_Model (AFP)
Session AFP/Stuttering_Equivalence (AFP)
Session AFP/Landau_Symbols (AFP)
Session AFP/Catalan_Numbers (AFP)
Session AFP/Error_Function (AFP)
Session AFP/Euler_MacLaurin (AFP)
Session AFP/LightweightJava (AFP)
Session AFP/LinearQuantifierElim (AFP)
Session AFP/List-Infinite (AFP)
Session AFP/Nat-Interval-Logic (AFP)
Session AFP/AutoFocus-Stream (AFP)
Session AFP/Median_Method (AFP)
Session AFP/MuchAdoAboutTwo (AFP)
Session AFP/Order_Lattice_Props (AFP)
Session AFP/POPLmark-deBruijn (AFP)
Session AFP/Pairing_Heap (AFP)
Session AFP/Password_Authentication_Protocol (AFP)
Session AFP/Prefix_Free_Code_Combinators (AFP)
Session AFP/Presburger-Automata (AFP)
Session AFP/Priority_Queue_Braun (AFP)
Session AFP/Program-Conflict-Analysis (AFP)
Session AFP/Regular-Sets (AFP)
Session AFP/Abstract-Rewriting (AFP)
Session AFP/Decreasing-Diagrams (AFP)
Session AFP/First_Order_Terms (AFP)
Session AFP/Stateful_Protocol_Composition_and_Typing (AFP)
Session AFP/Automated_Stateful_Protocol_Verification (AFP)
Session AFP/Matrix_Tensor (AFP)
Session AFP/Coinductive_Languages (AFP)
Session AFP/Finite_Automata_HF (AFP)
Session AFP/Functional-Automata (AFP)
Session AFP/Posix-Lexing (AFP)
Session AFP/ResiduatedTransitionSystem (AFP)
Session AFP/Ribbon_Proofs (AFP)
Session AFP/SATSolverVerification (AFP)
Session AFP/Schutz_Spacetime (AFP)
Session AFP/Selection_Heap_Sort (AFP)
Session AFP/Sort_Encodings (AFP)
Session AFP/Amortized_Complexity (AFP)
Session AFP/Dynamic_Tables (AFP)
Session AFP/Root_Balanced_Tree (AFP)
Session AFP/Closest_Pair_Points (AFP)
Session AFP/Stable_Matching (AFP)
Session AFP/Szemeredi_Regularity (AFP)
Session AFP/Roth_Arithmetic_Progressions (AFP)
Session AFP/Tail_Recursive_Functions (AFP)
Session AFP/TortoiseHare (AFP)
Session AFP/Flyspeck-Tame (AFP)
Session AFP/Twelvefold_Way (AFP)
Session AFP/Vickrey_Clarke_Groves (AFP)
Session HOL/HOL-MicroJava (timing)
Session HOL/HOL-Nitpick_Examples
Session HOL/HOL-Nominal-Examples (timing)
Session AFP/Lam-ml-Normalization (AFP)
Session AFP/SequentInvertibility (AFP)
Session HOL/HOL-Predicate_Compile_Examples (timing)
Session HOL/HOL-Quickcheck_Examples (timing)
Session AFP/Cotangent_PFD_Formula (AFP)
Session AFP/Furstenberg_Topology (AFP)
Session HOL/HOL-Real_Asymp-Manual
Session AFP/Sophomores_Dream (AFP)
Session AFP/Stirling_Formula (AFP)
Session AFP/Irrationals_From_THEBOOK (AFP)
Session HOL/HOL-SET_Protocol (timing)
Session HOL/HOL-SMT_Examples (timing)
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session AFP/Banach_Steinhaus (AFP)
Session AFP/Smooth_Manifolds (AFP)
Session AFP/Types_To_Sets_Extension (AFP)
Session HOL/HOLCF (main timing)
Session AFP/HOLCF-Prelude (AFP)
Session AFP/Stream-Fusion (AFP)
Session AFP/WorkerWrapper (AFP)
Session AFP/Hales_Jewett (AFP)
Session AFP/Consensus_Refined (AFP)
Session AFP/HoareForDivergence (AFP)
Session AFP/Hood_Melville_Queue (AFP)
Session AFP/HotelKeyCards (AFP)
Session Doc/How_to_Prove_it (no_doc)
Session AFP/Hybrid_Logic (AFP)
Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
Session AFP/HyperHoareLogic (AFP)
Session AFP/IFC_Tracking (AFP)
Session AFP/IMP2_Binary_Heap (AFP)
Session AFP/IMP_Compiler (AFP)
Session AFP/IMP_Compiler_Reuse (AFP)
Session Doc/Implementation (doc)
Session AFP/Implicational_Logic (AFP)
Session AFP/Impossible_Geometry (AFP)
Session AFP/Inductive_Confidentiality (AFP)
Session AFP/Inductive_Inference (AFP)
Session AFP/InfPathElimination (AFP)
Session AFP/Intro_Dest_Elim (AFP)
Session AFP/Involutions2Squares (AFP)
Session AFP/Jacobson_Basic_Algebra (AFP)
Session AFP/Grothendieck_Schemes (AFP)
Session AFP/Pluennecke_Ruzsa_Inequality (AFP)
Session AFP/Khovanskii_Theorem (AFP)
Session AFP/Kneser_Cauchy_Davenport (AFP)
Session AFP/JiveDataStoreModel (AFP)
Session AFP/Key_Agreement_Strong_Adversaries (AFP)
Session AFP/Kleene_Algebra (AFP)
Session AFP/Algebraic_VCs (AFP)
Session AFP/Multirelations (AFP)
Session AFP/Transformer_Semantics (AFP)
Session AFP/Regular_Algebras (AFP)
Session AFP/Relation_Algebra (AFP)
Session AFP/Relational_Paths (AFP)
Session AFP/Residuated_Lattices (AFP)
Session AFP/Knights_Tour (AFP)
Session AFP/LatticeProperties (AFP)
Session AFP/DataRefinementIBP (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Lifting_Definition_Option (AFP)
Session AFP/Comparison_Sort_Lower_Bound (AFP)
Session AFP/Dominance_CHK (AFP)
Session AFP/InformationFlowSlicing_Inter (AFP)
Session AFP/InformationFlowSlicing (AFP)
Session AFP/Regression_Test_Selection (AFP)
Session AFP/Quick_Sort_Cost (AFP)
Session AFP/Randomised_BSTs (AFP)
Session AFP/Randomised_Social_Choice (AFP)
Session AFP/Fishburn_Impossibility (AFP)
Session AFP/PAPP_Impossibility (AFP)
Session AFP/SDS_Impossibility (AFP)
Session AFP/List_Interleaving (AFP)
Session AFP/List_Inversions (AFP)
Session AFP/Locally-Nameless-Sigma (AFP)
Session AFP/Logging_Independent_Anonymity (AFP)
Session AFP/Lowe_Ontological_Argument (AFP)
Session AFP/MHComputation (AFP)
Session AFP/MLSS_Decision_Proc (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/Maximum_Segment_Sum (AFP)
Session AFP/Median_Of_Medians_Selection (AFP)
Session AFP/Metalogic_ProofChecker (AFP)
Session AFP/Modular_Assembly_Kit_Security (AFP)
Session AFP/MonoBoolTranAlgebra (AFP)
Session AFP/Multitape_To_Singletape_TM (AFP)
Session AFP/Name_Carrying_Type_Inference (AFP)
Session AFP/Nash_Williams (AFP)
Session AFP/No_FTL_observers (AFP)
Session AFP/No_FTL_observers_Gen_Rel (AFP)
Session AFP/Incompleteness (AFP)
Session AFP/Surprise_Paradox (AFP)
Session AFP/Modal_Logics_for_NTS (AFP)
Session AFP/Noninterference_CSP (AFP)
Session AFP/Noninterference_Ipurge_Unwinding (AFP)
Session AFP/Noninterference_Generic_Unwinding (AFP)
Session AFP/Noninterference_Inductive_Unwinding (AFP)
Session AFP/Noninterference_Sequential_Composition (AFP)
Session AFP/Noninterference_Concurrent_Composition (AFP)
Session AFP/Open_Induction (AFP)
Session AFP/Well_Quasi_Orders (AFP)
Session AFP/Decreasing-Diagrams-II (AFP)
Session AFP/Myhill-Nerode (AFP)
Session AFP/Nested_Multisets_Ordinals (AFP)
Session AFP/Design_Theory (AFP)
Session AFP/Undirected_Graph_Theory (AFP)
Session AFP/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/PSemigroupsConvolution (AFP)
Session AFP/Package_logic (AFP)
Session AFP/Combinable_Wands (AFP)
Session AFP/Paraconsistency (AFP)
Session AFP/GaleStewart_Games (AFP)
Session AFP/Partial_Function_MR (AFP)
Session AFP/Physical_Quantities (AFP)
Session AFP/Pop_Refinement (AFP)
Session AFP/Possibilistic_Noninterference (AFP)
Session AFP/Priority_Search_Trees (AFP)
Session AFP/Prim_Dijkstra_Simple (AFP)
Session AFP/Projective_Geometry (AFP)
Session AFP/Proof_Strategy_Language (AFP)
Session AFP/Propositional_Logic_Class (AFP)
Session AFP/Propositional_Proof_Systems (AFP)
Session AFP/Ramsey-Infinite (AFP)
Session AFP/Real_Time_Deque (AFP)
Session AFP/Recursion-Theory-I (AFP)
Session AFP/Minsky_Machines (AFP)
Session AFP/RefinementReactive (AFP)
Session AFP/Regex_Equivalence (AFP)
Session AFP/Relational_Method (AFP)
Session AFP/Resolution_FOL (AFP)
Session AFP/Robbins-Conjecture (AFP)
Session AFP/Roy_Floyd_Warshall (AFP)
Session AFP/SCC_Bloemen_Sequential (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/Sauer_Shelah_Lemma (AFP)
Session AFP/Security_Protocol_Refinement (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/Separation_Logic_Unbounded (AFP)
Session AFP/SimplifiedOntologicalArgument (AFP)
Session AFP/Sliding_Window_Algorithm (AFP)
Session AFP/Stellar_Quorums (AFP)
Session AFP/Stone_Algebras (AFP)
Session AFP/Stone_Relation_Algebras (AFP)
Session AFP/Stone_Kleene_Relation_Algebras (AFP)
Session AFP/Aggregation_Algebras (AFP)
Session AFP/Relational_Disjoint_Set_Forests (AFP)
Session AFP/Relational_Minimum_Spanning_Trees (AFP)
Session AFP/Relational_Forests (AFP)
Session AFP/Subset_Boolean_Algebras (AFP)
Session AFP/Correctness_Algebras (AFP)
Session AFP/Store_Buffer_Reduction (AFP)
Session AFP/StrictOmegaCategories (AFP)
Session AFP/Strong_Security (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/Combinatorics_Words_Lyndon (AFP)
Session AFP/TESL_Language (AFP)
Session AFP/Timed_Automata (AFP)
Session AFP/Probabilistic_Timed_Automata (AFP)
Session AFP/Topological_Semantics (AFP)
Session AFP/Transitive-Closure-II (AFP)
Session AFP/Tree_Decomposition (AFP)
Session AFP/Tree_Enumeration (AFP)
Session Doc/Typeclass_Hierarchy (doc)
Session AFP/Types_Tableaus_and_Goedels_God (AFP)
Session AFP/UPF_Firewall (AFP)
Session AFP/Universal_Turing_Machine (AFP)
Session AFP/Van_der_Waerden (AFP)
Session AFP/Interpreter_Optimizations (AFP)
Session AFP/Verified-Prover (AFP)
Session AFP/VolpanoSmith (AFP)
Session AFP/WHATandWHERE_Security (AFP)
Session AFP/Weight_Balanced_Trees (AFP)
Session AFP/Weighted_Arithmetic_Geometric_Mean (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Interval_Arithmetic_Word32 (AFP)
Session AFP/Abstract_Completeness (AFP)
Session AFP/Abstract_Soundness (AFP)
Session AFP/FOL_Seq_Calc3 (AFP)
Session AFP/Incredible_Proof_Machine (AFP)
Session AFP/CAVA_Automata (AFP)
Session AFP/DFS_Framework (AFP)
Session AFP/CHERI-C_Memory_Model (AFP)
Session AFP/Collections_Examples (AFP)
Session AFP/Containers-Benchmarks (AFP)
Session AFP/MFOTL_Monitor (AFP)
Session AFP/Generic_Join (AFP)
Session AFP/MFODL_Monitor_Optimized (AFP)
Session AFP/Formula_Derivatives (AFP)
Session AFP/MSO_Regex_Equivalence (AFP)
Session AFP/Affine_Arithmetic (AFP)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/Differential_Dynamic_Logic (AFP)
Session AFP/Hybrid_Systems_VCs (AFP)
Session AFP/Matrices_for_ODEs (AFP)
Session AFP/Taylor_Models (AFP)
Session AFP/Certification_Monads (AFP)
Session AFP/AI_Planning_Languages_Semantics (AFP)
Session AFP/Verified_SAT_Based_AI_Planning (AFP)
Session AFP/Dict_Construction (AFP)
Session AFP/Formula_Derivatives-Examples (AFP)
Session AFP/Monad_Memo_DP (AFP)
Session AFP/Hidden_Markov_Models (AFP)
Session AFP/Polynomial_Factorization (AFP)
Session AFP/Amicable_Numbers (AFP)
Session AFP/Dirichlet_Series (AFP)
Session AFP/Finite_Fields (AFP)
Session AFP/Universal_Hash_Families (AFP)
Session AFP/Frequency_Moments (AFP)
Session AFP/Zeta_Function (AFP)
Session AFP/Three_Squares (AFP)
Session AFP/Prime_Number_Theorem (AFP)
Session AFP/Prime_Distribution_Elementary (AFP)
Session AFP/Irrational_Series_Erdos_Straus (AFP)
Session AFP/Transcendence_Series_Hancl_Rucki (AFP)
Session AFP/Zeta_3_Irrational (AFP)
Session AFP/Gaussian_Integers (AFP)
Session AFP/Jordan_Normal_Form (AFP)
Session AFP/Isabelle_Marries_Dirac (AFP)
Session AFP/Knuth_Bendix_Order (AFP)
Session AFP/Functional_Ordered_Resolution_Prover (AFP)
Session AFP/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/Linear_Programming (AFP)
Session AFP/Number_Theoretic_Transform (AFP)
Session AFP/CRYSTALS-Kyber (AFP)
Session AFP/Smith_Normal_Form (AFP)
Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP)
Session AFP/Deep_Learning (AFP)
Session AFP/Projective_Measurements (AFP)
Session AFP/Commuting_Hermitian (AFP)
Session AFP/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/Complex_Bounded_Operators (AFP)
Session AFP/QR_Decomposition (AFP)
Session AFP/Van_Emde_Boas_Trees (AFP)
Session AFP/Dijkstra_Shortest_Path (AFP)
Session AFP/Koenigsberg_Friendship (AFP)
Session AFP/FOL_Seq_Calc2 (AFP)
Session AFP/Gale_Shapley (AFP)
Session AFP/HOL-ODE-Numerics (AFP)
Session AFP/HOL-ODE-ARCH-COMP (AFP)
Session AFP/HOL-ODE-Examples (AFP large)
Session AFP/Lorenz_Approximation (AFP)
Session AFP/Lorenz_C0 (AFP large)
Session AFP/Lorenz_C1 (AFP large)
Session AFP/Poincare_Bendixson (AFP)
Session AFP/Safe_Range_RC (AFP)
Session AFP/Transition_Systems_and_Automata (AFP)
Session AFP/Adaptive_State_Counting (AFP)
Session AFP/Buchi_Complementation (AFP)
Session AFP/LTL_Master_Theorem (AFP)
Session AFP/LTL_Normal_Form (AFP)
Session AFP/Partial_Order_Reduction (AFP)
Session AFP/CAVA_LTL_Modelchecker (AFP)
Session AFP/Transitive-Closure (AFP)
Session AFP/Network_Security_Policy_Verification (AFP)
Session AFP/Planarity_Certificates (AFP)
Session AFP/Tree-Automata (AFP)
Session AFP/Datatype_Order_Generator (AFP)
Session AFP/Higher_Order_Terms (AFP)
Session AFP/CakeML_Codegen (AFP)
Session AFP/Old_Datatype_Show (AFP)
Session AFP/Quantifier_Elimination_Hybrid (AFP)
Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/Mersenne_Primes (AFP)
Session AFP/Separation_Logic_Imperative_HOL (AFP)
Session AFP/Sepref_Prereq (AFP)
Session AFP/Refine_Imperative_HOL (AFP)
Session AFP/Floyd_Warshall (AFP)
Session AFP/Sepref_Basic (AFP)
Session AFP/Flow_Networks (AFP)
Session AFP/EdmondsKarp_Maxflow (AFP)
Session AFP/MFMC_Countable (AFP)
Session AFP/Probabilistic_While (AFP)
Session AFP/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/VerifyThis2018 (AFP)
Session AFP/VerifyThis2019 (AFP)
Session AFP/Simplicial_complexes_and_boolean_functions (AFP)
Session AFP/UpDown_Scheme (AFP)
Session AFP/X86_Semantics (AFP)
Session AFP/CZH_Foundations (AFP)
Session AFP/CZH_Elementary_Categories (AFP)
Session AFP/CZH_Universal_Constructions (AFP)
Session AFP/MonoidalCategory (AFP)
Session AFP/Ordinal_Partitions (AFP)
Session AFP/Wetzels_Problem (AFP)
Session AFP/Recursion-Addition (AFP)
Session AFP/Delta_System_Lemma (AFP)
Session AFP/Transitive_Models (AFP)
Session AFP/Independence_CH (AFP)
Building 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
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
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)
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)
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"):
*** 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"):
*** 1. (⋀xs. ⟦unify [(s, t)] [] = Some xs; μ = subst_of xs⟧ ⟹ 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"):
*** 1. (⋀xs. ⟦unify [(s, t)] [] = Some xs; μ = subst_of xs⟧ ⟹ 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 "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"
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
using [/media/data/jenkins/workspace/isabelle-all/bin/isabelle]
Preparing site generation in out/hugo
Cleaning up generated files...
Build in /media/data/jenkins/workspace/isabelle-all/afp/web/index.html
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)