1 changesets found
10:46:11[AAB808E7A3A90D7441318DC80DDAE14AC542D145-testboard] $ /usr/bin/hg unbundle xfer.hg
10:46:11adding changesets
10:46:11adding manifests
10:46:11adding file changes
10:46:11added 1 changesets with 1 changes to 1 files (+1 heads)
10:46:11new changesets ca7e7e41374e (1 drafts)
10:46:11(run 'hg heads .' to see heads, 'hg merge' to merge)
10:46:11Agent node cache lock released for node workermta1.
10:46:11[testboard] $ /usr/bin/hg pull --rev default /media/data/jenkins/hgcache/AAB808E7A3A90D7441318DC80DDAE14AC542D145-testboard
10:46:11pulling from /media/data/jenkins/hgcache/AAB808E7A3A90D7441318DC80DDAE14AC542D145-testboard
10:46:11no changes found
10:46:111 local changesets published
10:46:11[testboard] $ /usr/bin/hg update --clean --rev default
10:46:121 files updated, 0 files merged, 0 files removed, 0 files unresolved
10:46:12[testboard] $ /usr/bin/hg log --rev . --template {node}
10:46:12[testboard] $ /usr/bin/hg log --rev . --template {rev}
10:46:12[testboard] $ /usr/bin/hg log --rev ccd140385fcaa506aaba784f64cd925cc4bbb251 --template exists\n
10:46:12exists
10:46:12[testboard] $ /usr/bin/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(ccd140385fcaa506aaba784f64cd925cc4bbb251)" --encoding UTF-8 --encodingmode replace
10:46:12[testboard] $ /bin/sh -xe /tmp/jenkins5165714731076030694.sh
10:46:12+ set -ex
10:46:12+ [ -d afp ]
10:46:12+ [ -z ]
10:46:12+ AFP_URL=https://foss.heptapod.net/isa-afp/afp-devel/10:46:12+ hg id --id --rev default https://foss.heptapod.net/isa-afp/afp-devel/10:46:13+ AFP_REVISION=97397bd46b35
10:46:13+ cd afp
10:46:13+ hg pull https://foss.heptapod.net/isa-afp/afp-devel/10:46:13Rufe von https://foss.heptapod.net/isa-afp/afp-devel/ ab
10:46:13Suche nach Änderungen
10:46:13Keine Änderungen gefunden
10:46:13+ hg up -C -r 97397bd46b35
10:46:130 Dateien aktualisiert, 0 Dateien zusammengeführt, 0 Dateien entfernt, 0 Dateien ungelöst
10:46:13[testboard] $ /bin/sh -xe /tmp/jenkins4015888800386434878.sh
10:46:13+ Admin/jenkins/run_build testboard
10:46:13+ set -e
10:46:13+ PROFILE=testboard
10:46:13+ shift
10:46:13+ bin/isabelle components -a
10:46:14+ bin/isabelle jedit -bf
10:46:14### Building Isabelle/Scala (/media/data/jenkins/workspace/testboard/lib/classes/isabelle.jar) ...
10:47:10### Building Demo (/media/data/jenkins/workspace/testboard/src/Tools/Demo/lib/demo.jar) ...
10:47:11### Building graph browser (/media/data/jenkins/workspace/testboard/lib/classes/isabelle_graphbrowser.jar) ...
10:47:12Hinweis: Einige Eingabedateien verwenden nicht geprüfte oder unsichere Vorgänge.
10:47:12Hinweis: Wiederholen Sie die Kompilierung mit -Xlint:unchecked, um Details zu erhalten.
10:47:12### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/testboard/lib/classes/isabelle_admin.jar) ...
10:47:12### Building AFP/Tools (/media/data/jenkins/workspace/testboard/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
10:47:15### Building AFP/Tools (/media/data/jenkins/workspace/testboard/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
10:47:18+ bin/isabelle ocaml_setup
10:47:18# Run eval $(opam env) to update the current shell environment
10:47:19[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
10:47:19 opam update
10:47:1910:47:19[NOTE] Package zarith is already installed (current version is 1.12).
10:47:19+ bin/isabelle ghc_setup
10:47:21Stack will use a sandboxed GHC it installed. To use this GHC and packages outside of a project,
10:47:21consider using: stack ghc, stack ghci, stack runghc, or stack exec.
10:47:21The Glorious Glasgow Haskell Compilation System, version 9.6.4
10:47:22+ bin/isabelle go_setup
10:47:23Component directory "/media/data/jenkins/.isabelle/contrib/go-1.22.1"
10:47:23### Platform x86_64-linux already installed
10:47:23+ bin/isabelle ci_build testboard
10:47:2610:47:26=== CONFIGURATION ===
10:47:2610:47:26ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
10:47:26ISABELLE_BUILD_OPTIONS=""
10:47:2610:47:26ML_PLATFORM="x86_64_32-linux"
10:47:26ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.9.1/x86_64_32-linux"
10:47:26ML_SYSTEM="polyml-5.9.1"
10:47:26ML_OPTIONS="-H 4000 --maxheap 8G"
10:47:26jobs = 10, threads = 4, numa = false
10:47:2610:47:26=== BUILD ===
10:47:2610:47:26Build started at Wed, 29 May 2024 08:47:26 GMT
10:47:26Isabelle id ca7e7e41374e
10:47:27AFP id 97397bd46b35
10:47:2710:47:27=== LOG ===
10:47:2710:47:29Session Pure/Pure
10:47:29Session Misc/CTT
10:47:29Session Misc/Cube
10:47:29Session FOL/FOL
10:47:29Session FOL/CCL
10:47:29Session FOL/FOL-ex
10:47:29Session FOL/FOLP
10:47:29Session FOL/FOLP-ex
10:47:29Session Doc/Intro (doc)
10:47:30Session FOL/LCF
10:47:30Session Doc/Logics (doc)
10:47:30Session Doc/Nitpick (doc)
10:47:30Session Pure/Pure-Examples
10:47:30Session Pure/Pure-ex
10:47:30Session Misc/SML
10:47:30Session Misc/Sequents
10:47:30Session Doc/Sledgehammer (doc)
10:47:30Session AFP/SpecCheck (AFP)
10:47:30Session Misc/Tools
10:47:30Session HOL/HOL (main)
10:47:31Session AFP/AVL-Trees (AFP)
10:47:31Session AFP/AWN (AFP)
10:47:31Session AFP/Abortable_Linearizable_Modules (AFP)
10:47:31Session AFP/Abstract-Hoare-Logics (AFP)
10:47:31Session AFP/Ackermanns_not_PR (AFP)
10:47:31Session AFP/AnselmGod (AFP)
10:47:31Session AFP/Aristotles_Assertoric_Syllogistic (AFP)
10:47:31Session AFP/Attack_Trees (AFP)
10:47:31Session AFP/AxiomaticCategoryTheory (AFP)
10:47:31Session AFP/Belief_Revision (AFP)
10:47:31Session AFP/BinarySearchTree (AFP)
10:47:31Session AFP/Binomial-Queues (AFP)
10:47:31Session AFP/Bondy (AFP)
10:47:31Session AFP/Boolos_Curious_Inference (AFP)
10:47:31Session AFP/Boolos_Curious_Inference_Automated (AFP)
10:47:31Session AFP/BytecodeLogicJmlTypes (AFP)
10:47:31Session AFP/C2KA_DistributedSystems (AFP)
10:47:31Session AFP/CISC-Kernel (AFP)
10:47:31Session AFP/CYK (AFP)
10:47:31Session AFP/Cauchy (AFP)
10:47:31Session AFP/Sqrt_Babylonian (AFP)
10:47:31Session Doc/Classes (doc)
10:47:32Session AFP/ClockSynchInst (AFP)
10:47:32Session AFP/Compiling-Exceptions-Correctly (AFP)
10:47:32Session AFP/ComponentDependencies (AFP)
10:47:32Session AFP/Concurrent_Revisions (AFP)
10:47:32Session AFP/CondNormReasHOL (AFP)
10:47:32Session AFP/Constructor_Funs (AFP)
10:47:32Session AFP/CryptoBasedCompositionalProperties (AFP)
10:47:32Session AFP/DCR-ExecutionEquivalence (AFP)
10:47:32Session AFP/DPT-SAT-Solver (AFP)
10:47:32Session AFP/Dedekind_Real (AFP)
10:47:32Session Doc/Demo_EPTCS (doc)
10:47:32Session Doc/Demo_Easychair (doc)
10:47:32Session Doc/Demo_FoilTeX (doc)
10:47:32Session Doc/Demo_LIPIcs (doc)
10:47:32Session Doc/Demo_LLNCS (doc)
10:47:32Session AFP/Depth-First-Search (AFP)
10:47:32Session AFP/Digit_Expansions (AFP)
10:47:32Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
10:47:32Session AFP/DiskPaxos (AFP)
10:47:32Session AFP/Eudoxus_Reals (AFP)
10:47:32Session AFP/Example-Submission (AFP)
10:47:32Session AFP/FFT (AFP)
10:47:32Session AFP/FLP (AFP)
10:47:32Session AFP/FeatherweightJava (AFP)
10:47:32Session AFP/Featherweight_OCL (AFP)
10:47:32Session AFP/FileRefinement (AFP)
10:47:32Session AFP/FocusStreamsCaseStudies (AFP)
10:47:32Session AFP/Foundation_of_geometry (AFP)
10:47:33Session AFP/Free-Boolean-Algebra (AFP)
10:47:33Session AFP/Fresh_Identifiers (AFP)
10:47:33Session AFP/FunWithFunctions (AFP)
10:47:33Session AFP/FunWithTilings (AFP)
10:47:33Session Doc/Functions (doc)
10:47:33Session AFP/GPU_Kernel_PL (AFP)
10:47:33Session AFP/GenClock (AFP)
10:47:33Session AFP/General-Triangle (AFP)
10:47:33Session AFP/Generic_Deriving (AFP)
10:47:33Session AFP/GewirthPGCProof (AFP)
10:47:33Session AFP/Go (AFP)
10:47:33Session AFP/GoedelGod (AFP)
10:47:33Session AFP/Goodstein_Lambda (AFP)
10:47:33Session AFP/Gray_Codes (AFP)
10:47:33Session HOL/HOL-Cardinals (timing)
10:47:33Session AFP/Binding_Syntax_Theory (AFP)
10:47:33Session AFP/Epistemic_Logic (AFP)
10:47:33Session AFP/Public_Announcement_Logic (AFP)
10:47:33Session AFP/Stalnaker_Logic (AFP)
10:47:33Session AFP/Ordinals_and_Cardinals (AFP)
10:47:33Session AFP/Risk_Free_Lending (AFP)
10:47:33Session HOL/HOL-Hoare
10:47:33Session HOL/HOL-Hoare_Parallel (timing)
10:47:33Session HOL/HOL-IMPP
10:47:33Session HOL/HOL-IOA
10:47:33Session HOL/HOL-Import
10:47:33Session HOL/HOL-Lattice
10:47:33Session HOL/HOL-Library (main timing)
10:47:34Session AFP/ADS_Functor (AFP)
10:47:34Session AFP/Approximation_Algorithms (AFP)
10:47:34Session AFP/ArrowImpossibilityGS (AFP)
10:47:34Session AFP/Auto2_HOL (AFP)
10:47:34Session AFP/BNF_CC (AFP)
10:47:34Session AFP/BNF_Operations (AFP)
10:47:34Session AFP/Binomial-Heaps (AFP)
10:47:34Session AFP/Birkhoff_Finite_Distributive_Lattices (AFP)
10:47:34Session AFP/Boolean_Expression_Checkers (AFP)
10:47:34Session AFP/Bounded_Deducibility_Security (AFP)
10:47:34Session AFP/BD_Security_Compositional (AFP)
10:47:34Session AFP/CoSMeDis (AFP)
10:47:34Session AFP/CoCon (AFP)
10:47:35Session AFP/CoSMed (AFP)
10:47:35Session AFP/Buildings (AFP)
10:47:35Session AFP/CRDT (AFP)
10:47:35Session AFP/IMAP-CRDT (AFP)
10:47:35Session AFP/Card_Multisets (AFP)
10:47:35Session AFP/Card_Number_Partitions (AFP)
10:47:35Session AFP/Category (AFP)
10:47:35Session Doc/Codegen (doc)
10:47:35Session AFP/CofGroups (AFP)
10:47:35Session AFP/CommCSL (AFP)
10:47:35Session AFP/Complete_Non_Orders (AFP)
10:47:35Session AFP/Completeness (AFP)
10:47:35Session AFP/ConcurrentIMP (AFP)
10:47:35Session AFP/Concurrent_Ref_Alg (AFP)
10:47:35Session AFP/Conditional_Simplification (AFP)
10:47:36Session AFP/Conditional_Transfer_Rule (AFP)
10:47:36Session AFP/CoreC++ (AFP)
10:47:36Session AFP/Core_DOM (AFP)
10:47:36Session AFP/Shadow_DOM (AFP)
10:47:36Session AFP/DOM_Components (AFP)
10:47:36Session AFP/Core_SC_DOM (AFP)
10:47:36Session AFP/Shadow_SC_DOM (AFP)
10:47:36Session AFP/SC_DOM_Components (AFP)
10:47:37Session AFP/Coupledsim_Contrasim (AFP)
10:47:37Session Doc/Datatypes (doc)
10:47:37Session Doc/Corec (doc)
10:47:37Session AFP/Decl_Sem_Fun_PL (AFP)
10:47:37Session AFP/Directed_Sets (AFP)
10:47:37Session AFP/Earley_Parser (AFP)
10:47:37Session AFP/Encodability_Process_Calculi (AFP)
10:47:37Session AFP/Euler_Partition (AFP)
10:47:37Session AFP/FOL-Fitting (AFP)
10:47:37Session AFP/FOL_Seq_Calc1 (AFP)
10:47:37Session AFP/FOL_Axiomatic (AFP)
10:47:37Session AFP/FOL_Harrison (AFP)
10:47:37Session AFP/Factored_Transition_System_Bounding (AFP)
10:47:38Session AFP/FinFun (AFP)
10:47:38Session AFP/Extended_Finite_State_Machines (AFP)
10:47:38Session AFP/Extended_Finite_State_Machine_Inference (AFP)
10:47:38Session AFP/Finger-Trees (AFP)
10:47:38Session AFP/Finite-Map-Extras (AFP)
10:47:38Session AFP/Fixed_Length_Vector (AFP)
10:47:38Session AFP/Generalized_Counting_Sort (AFP)
10:47:38Session AFP/Graph_Saturation (AFP)
10:47:38Session AFP/Group-Ring-Module (AFP)
10:47:38Session AFP/Valuation (AFP)
10:47:38Session HOL/HOL-Auth (timing)
10:47:38Session HOL/HOL-UNITY (timing)
10:47:39Session HOL/HOL-Bali (timing)
10:47:39Session HOL/HOL-Combinatorics (main timing)
10:47:39Session AFP/Blue_Eyes (AFP)
10:47:39Session AFP/Derangements (AFP)
10:47:39Session AFP/Discrete_Summation (AFP)
10:47:39Session AFP/Gauss-Jordan-Elim-Fun (AFP)
10:47:39Session AFP/Graph_Theory (AFP)
10:47:39Session AFP/ShortestPath (AFP)
10:47:39Session HOL/HOL-Computational_Algebra (main timing)
10:47:40Session AFP/Descartes_Sign_Rule (AFP)
10:47:40Session HOL/HOL-Algebra (main timing)
10:47:40Session AFP/Edwards_Elliptic_Curves_Group (AFP)
10:47:40Session AFP/Finitely_Generated_Abelian_Groups (AFP)
10:47:40Session HOL/HOL-Decision_Procs (timing)
10:47:40Session HOL/HOL-Quotient_Examples (timing)
10:47:40Session AFP/Interpolation_Polynomials_HOL_Algebra (AFP)
10:47:40Session AFP/Localization_Ring (AFP)
10:47:40Session AFP/Orbit_Stabiliser (AFP)
10:47:40Session AFP/Perfect-Number-Thm (AFP)
10:47:40Session AFP/Secondary_Sylow (AFP)
10:47:40Session AFP/Jordan_Hoelder (AFP)
10:47:41Session AFP/VectorSpace (AFP)
10:47:41Session HOL/HOL-Examples
10:47:41Session HOL/HOL-Isar_Examples
10:47:41Session HOL/HOL-Nonstandard_Analysis (timing)
10:47:41Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
10:47:41Session HOL/HOL-Number_Theory (main timing)
10:47:41Session AFP/Arith_Prog_Rel_Primes (AFP)
10:47:41Session AFP/DigitsInBase (AFP)
10:47:41Session AFP/Elliptic_Curves_Group_Law (AFP)
10:47:41Session AFP/Crypto_Standards (AFP)
10:47:42Session AFP/Fermat3_4 (AFP)
10:47:42Session HOL/HOL-Data_Structures (timing)
10:47:42Session AFP/Efficient-Mergesort (AFP)
10:47:42Session AFP/Go_Test_Quick (AFP)
10:47:42Session AFP/Go_Test_Slow (AFP)
10:47:42Session HOL/HOL-Codegenerator_Test
10:47:42Session AFP/Query_Optimization (AFP)
10:47:43Session HOL/HOL-ex (timing)
10:47:43Session AFP/Lehmer (AFP)
10:47:43Session AFP/Lifting_the_Exponent (AFP)
10:47:43Session AFP/Padic_Ints (AFP)
10:47:43Session AFP/Padic_Field (AFP)
10:47:43Session AFP/Pratt_Certificate (AFP)
10:47:43Session AFP/Bertrands_Postulate (AFP)
10:47:43Session AFP/RSAPSS (AFP)
10:47:43Session AFP/SumSquares (AFP)
10:47:43Session AFP/Liouville_Numbers (AFP)
10:47:43Session AFP/Lucas_Theorem (AFP)
10:47:43Session AFP/DPRM_Theorem (AFP)
10:47:44Session AFP/Mason_Stothers (AFP)
10:47:44Session AFP/Polynomial_Interpolation (AFP)
10:47:44Session AFP/Formal_Puiseux_Series (AFP)
10:47:44Session AFP/Rep_Fin_Groups (AFP)
10:47:44Session AFP/Sturm_Sequences (AFP)
10:47:44Session AFP/Special_Function_Bounds (AFP)
10:47:44Session AFP/Sturm_Tarski (AFP)
10:47:44Session AFP/Budan_Fourier (AFP)
10:47:44Session AFP/Three_Circles (AFP)
10:47:44Session HOL/HOL-Corec_Examples (timing)
10:47:44Session HOL/HOL-Datatype_Examples (timing)
10:47:44Session HOL/HOL-IMP (timing)
10:47:44Session AFP/Abs_Int_ITP2012 (AFP)
10:47:44Session AFP/Relational-Incorrectness-Logic (AFP)
10:47:44Session HOL/HOL-Imperative_HOL (timing)
10:47:45Session AFP/Auto2_Imperative_HOL (AFP)
10:47:45Session AFP/Imperative_Insertion_Sort (AFP)
10:47:45Session HOL/HOL-Induct
10:47:45Session HOL/HOL-Metis_Examples (timing)
10:47:45Session HOL/HOL-Proofs (timing)
10:47:45Session HOL/HOL-Proofs-Extraction (timing)
10:47:46Session HOL/HOL-Proofs-ex
10:47:46Session HOL/HOL-Proofs-Lambda (timing)
10:47:46Session AFP/HereditarilyFinite (AFP)
10:47:46Session AFP/HyperCTL (AFP)
10:47:46Session AFP/IO_Language_Conformance (AFP)
10:47:46Session AFP/Integration (AFP)
10:47:46Session AFP/Isabelle_Meta_Model (AFP)
10:47:46Session AFP/Isabelle_hoops (AFP)
10:47:46Session AFP/LTL (AFP)
10:47:46Session AFP/Stuttering_Equivalence (AFP)
10:47:46Session AFP/Landau_Symbols (AFP)
10:47:46Session AFP/LightweightJava (AFP)
10:47:46Session AFP/LinearQuantifierElim (AFP)
10:47:46Session AFP/List-Infinite (AFP)
10:47:46Session AFP/Nat-Interval-Logic (AFP)
10:47:46Session AFP/AutoFocus-Stream (AFP)
10:47:46Session AFP/MuchAdoAboutTwo (AFP)
10:47:46Session AFP/Order_Lattice_Props (AFP)
10:47:46Session AFP/POPLmark-deBruijn (AFP)
10:47:46Session AFP/Pairing_Heap (AFP)
10:47:46Session AFP/Password_Authentication_Protocol (AFP)
10:47:46Session AFP/Pell (AFP)
10:47:46Session AFP/Prefix_Free_Code_Combinators (AFP)
10:47:46Session AFP/Presburger-Automata (AFP)
10:47:46Session AFP/Priority_Queue_Braun (AFP)
10:47:47Session AFP/Program-Conflict-Analysis (AFP)
10:47:47Session AFP/QBF_Solver_Verification (AFP)
10:47:47Session AFP/Regular-Sets (AFP)
10:47:47Session AFP/Abstract-Rewriting (AFP)
10:47:47Session AFP/Decreasing-Diagrams (AFP)
10:47:47Session AFP/Matrix (AFP)
10:47:47Session AFP/Matrix_Tensor (AFP)
10:47:47Session AFP/Knot_Theory (AFP)
10:47:47Session AFP/Coinductive_Languages (AFP)
10:47:47Session AFP/Finite_Automata_HF (AFP)
10:47:47Session AFP/Functional-Automata (AFP)
10:47:47Session AFP/Isabelle_DOF (AFP)
10:47:47Session AFP/Posix-Lexing (AFP)
10:47:47Session AFP/ResiduatedTransitionSystem (AFP)
10:47:47Session AFP/Ribbon_Proofs (AFP)
10:47:47Session AFP/SATSolverVerification (AFP)
10:47:48Session AFP/Safe_OCL (AFP)
10:47:48Session AFP/Schutz_Spacetime (AFP)
10:47:48Session AFP/Selection_Heap_Sort (AFP)
10:47:48Session AFP/Simplex (AFP)
10:47:48Session AFP/Skew_Heap (AFP)
10:47:48Session AFP/Sort_Encodings (AFP)
10:47:48Session AFP/Splay_Tree (AFP)
10:47:48Session AFP/Amortized_Complexity (AFP)
10:47:48Session AFP/Dynamic_Tables (AFP)
10:47:48Session AFP/Root_Balanced_Tree (AFP)
10:47:48Session AFP/Stable_Matching (AFP)
10:47:48Session AFP/SuperCalc (AFP)
10:47:48Session Doc/System (doc)
10:47:48Session AFP/Tail_Recursive_Functions (AFP)
10:47:48Session AFP/TortoiseHare (AFP)
10:47:48Session AFP/Trie (AFP)
10:47:48Session AFP/Flyspeck-Tame (AFP)
10:47:48Session AFP/Vickrey_Clarke_Groves (AFP)
10:47:48Session AFP/Zeckendorf (AFP)
10:47:48Session HOL/HOL-Matrix_LP
10:47:48Session HOL/HOL-Mutabelle
10:47:48Session HOL/HOL-NanoJava
10:47:48Session HOL/HOL-Nitpick_Examples
10:47:49Session HOL/HOL-Nominal
10:47:49Session AFP/CCS (AFP)
10:47:49Session HOL/HOL-Nominal-Examples (timing)
10:47:49Session AFP/Lam-ml-Normalization (AFP)
10:47:49Session AFP/Pi_Calculus (AFP)
10:47:49Session AFP/Psi_Calculi (AFP)
10:47:49Session AFP/Broadcast_Psi (AFP)
10:47:50Session AFP/SequentInvertibility (AFP)
10:47:50Session HOL/HOL-Predicate_Compile_Examples (timing)
10:47:50Session HOL/HOL-Prolog
10:47:50Session HOL/HOL-Quickcheck_Examples (timing)
10:47:50Session HOL/HOL-Real_Asymp
10:47:51Session HOL/HOL-Analysis (main timing)
10:47:52Session AFP/Akra_Bazzi (AFP)
10:47:52Session AFP/Closest_Pair_Points (AFP)
10:47:52Session AFP/Cardinality_Continuum (AFP)
10:47:52Session AFP/Catalan_Numbers (AFP)
10:47:52Session AFP/Cayley_Hamilton (AFP)
10:47:52Session AFP/Chebyshev_Polynomials (AFP)
10:47:52Session AFP/Coinductive (AFP)
10:47:52Session AFP/DynamicArchitectures (AFP)
10:47:52Session AFP/Architectural_Design_Patterns (AFP)
10:47:52Session AFP/Lazy-Lists-II (AFP)
10:47:52Session AFP/Stream_Fusion_Code (AFP)
10:47:53Session AFP/Topology (AFP)
10:47:53Session AFP/Complex_Geometry (AFP)
10:47:53Session AFP/Poincare_Disc (AFP)
10:47:53Session AFP/Differential_Game_Logic (AFP)
10:47:53Session AFP/Euler_Polyhedron_Formula (AFP)
10:47:53Session AFP/First_Welfare_Theorem (AFP)
10:47:53Session AFP/Furstenberg_Topology (AFP)
10:47:53Session AFP/Green (AFP)
10:47:53Session HOL/HOL-Analysis-ex
10:47:53Session HOL/HOL-Complex_Analysis (main timing)
10:47:53Session AFP/Bernoulli (AFP)
10:47:53Session AFP/Cartan_FP (AFP)
10:47:53Session AFP/Cotangent_PFD_Formula (AFP)
10:47:53Session AFP/E_Transcendental (AFP)
10:47:54Session AFP/Error_Function (AFP)
10:47:54Session AFP/Euler_MacLaurin (AFP)
10:47:54Session HOL/HOL-Eisbach
10:47:54Session AFP/AOT (AFP)
10:47:54Session AFP/Allen_Calculus (AFP)
10:47:54Session AFP/Automatic_Refinement (AFP)
10:47:54Session AFP/Refine_Monadic (AFP)
10:47:54Session AFP/Card_Partitions (AFP)
10:47:54Session AFP/Bell_Numbers_Spivey (AFP)
10:47:54Session AFP/Card_Equiv_Relations (AFP)
10:47:54Session AFP/Equivalence_Relation_Enumeration (AFP)
10:47:54Session AFP/Falling_Factorial_Sum (AFP)
10:47:54Session AFP/Combinatorial_Enumeration_Algorithms (AFP)
10:47:55Session AFP/Case_Labeling (AFP)
10:47:55Session AFP/Clean (AFP)
10:47:55Session AFP/Combinatorics_Words (AFP)
10:47:55Session AFP/Combinatorics_Words_Graph_Lemma (AFP)
10:47:55Session AFP/Binary_Code_Imprimitive (AFP)
10:47:55Session AFP/Two_Generated_Word_Monoids_Intersection (AFP)
10:47:55Session AFP/Cook_Levin (AFP)
10:47:55Session AFP/Dependent_SIFUM_Type_Systems (AFP)
10:47:55Session AFP/Dependent_SIFUM_Refinement (AFP)
10:47:55Session Doc/Eisbach (doc)
10:47:55Session HOL/HOL-MicroJava (timing)
10:47:56Session AFP/Optics (AFP)
10:47:56Session AFP/ConcurrentHOL (AFP)
10:47:56Session AFP/UTP-Toolkit (AFP)
10:47:56Session AFP/UTP (AFP)
10:47:56Session AFP/Solidity (AFP)
10:47:56Session AFP/Twelvefold_Way (AFP)
10:47:56Session HOL/HOL-Hahn_Banach
10:47:56Session HOL/HOL-Homology (timing)
10:47:56Session HOL/HOL-Mirabelle-ex
10:47:56Session HOL/HOL-Probability (main timing)
10:47:57Session AFP/Actuarial_Mathematics (AFP)
10:47:57Session AFP/Applicative_Lifting (AFP)
10:47:57Session AFP/Free-Groups (AFP)
10:47:57Session AFP/Stern_Brocot (AFP)
10:47:57Session AFP/Buffons_Needle (AFP)
10:47:57Session AFP/Density_Compiler (AFP)
10:47:57Session AFP/DiscretePricing (AFP)
10:47:57Session AFP/Ergodic_Theory (AFP)
10:47:57Session AFP/Gromov_Hyperbolicity (AFP)
10:47:58Session AFP/Laws_of_Large_Numbers (AFP)
10:47:58Session AFP/Fisher_Yates (AFP)
10:47:58Session AFP/Girth_Chromatic (AFP)
10:47:58Session AFP/Random_Graph_Subgraph_Threshold (AFP)
10:47:58Session AFP/Szemeredi_Regularity (AFP)
10:47:58Session HOL/HOL-Probability-ex (timing)
10:47:58Session AFP/Hahn_Jordan_Decomposition (AFP)
10:47:58Session AFP/Lp (AFP)
10:47:58Session AFP/Concentration_Inequalities (AFP)
10:47:58Session AFP/Fourier (AFP)
10:47:58Session AFP/MDP-Rewards (AFP)
10:47:58Session AFP/Markov_Models (AFP)
10:47:58Session AFP/Martingales (AFP)
10:47:58Session AFP/Doob_Convergence (AFP)
10:47:58Session AFP/Monad_Normalisation (AFP)
10:47:58Session AFP/Monomorphic_Monad (AFP)
10:47:58Session AFP/Neumann_Morgenstern_Utility (AFP)
10:47:58Session AFP/Probabilistic_Noninterference (AFP)
10:47:58Session AFP/Probabilistic_Prime_Tests (AFP)
10:47:59Session AFP/Probabilistic_System_Zoo (AFP)
10:47:59Session AFP/Quasi_Borel_Spaces (AFP)
10:47:59Session AFP/Roth_Arithmetic_Progressions (AFP)
10:47:59Session AFP/Skip_Lists (AFP)
10:47:59Session AFP/Source_Coding_Theorem (AFP)
10:47:59Session AFP/Standard_Borel_Spaces (AFP)
10:47:59Session AFP/S_Finite_Measure_Monad (AFP)
10:47:59Session AFP/Disintegration (AFP)
10:47:59Session AFP/Turans_Graph_Theorem (AFP)
10:47:59Session AFP/Hyperdual (AFP)
10:48:00Session AFP/Interval_Analysis (AFP)
10:48:00Session AFP/Irrationality_J_Hancl (AFP)
10:48:00Session AFP/Kuratowski_Closure_Complement (AFP)
10:48:00Session AFP/Laplace_Transform (AFP)
10:48:00Session AFP/Lower_Semicontinuous (AFP)
10:48:00Session AFP/Minkowskis_Theorem (AFP)
10:48:00Session AFP/Octonions (AFP)
10:48:00Session AFP/Polynomial_Crit_Geometry (AFP)
10:48:00Session AFP/Prime_Harmonic_Series (AFP)
10:48:00Session AFP/Ptolemys_Theorem (AFP)
10:48:00Session AFP/Quaternions (AFP)
10:48:00Session AFP/Rank_Nullity_Theorem (AFP)
10:48:00Session AFP/Gauss_Jordan (AFP)
10:48:00Session AFP/Echelon_Form (AFP)
10:48:00Session AFP/Hermite (AFP)
10:48:00Session AFP/Safe_Distance (AFP)
10:48:01Session AFP/Tarskis_Geometry (AFP)
10:48:01Session AFP/Triangle (AFP)
10:48:01Session AFP/Ceva (AFP)
10:48:01Session AFP/Chord_Segments (AFP)
10:48:01Session AFP/Stewart_Apollonius (AFP)
10:48:01Session AFP/Winding_Number_Eval (AFP)
10:48:01Session AFP/Count_Complex_Roots (AFP)
10:48:01Session AFP/Youngs_Inequality (AFP)
10:48:01Session AFP/pGCL (AFP)
10:48:01Session HOL/HOL-Real_Asymp-Manual
10:48:01Session AFP/Sophomores_Dream (AFP)
10:48:01Session AFP/Stirling_Formula (AFP)
10:48:01Session AFP/Irrationals_From_THEBOOK (AFP)
10:48:01Session AFP/Lambert_W (AFP)
10:48:01Session HOL/HOL-SET_Protocol (timing)
10:48:01Session HOL/HOL-SMT_Examples (timing)
10:48:01Session HOL/HOL-SPARK
10:48:02Session HOL/HOL-SPARK-Examples
10:48:02Session AFP/RIPEMD-160-SPARK (AFP)
10:48:02Session HOL/HOL-SPARK-Manual
10:48:02Session HOL/HOL-Statespace
10:48:02Session HOL/HOL-TLA
10:48:02Session HOL/HOL-TLA-Buffer
10:48:02Session HOL/HOL-TLA-Inc
10:48:02Session HOL/HOL-TLA-Memory
10:48:02Session HOL/HOL-TPTP
10:48:02Session HOL/HOL-Types_To_Sets
10:48:02Session AFP/Banach_Steinhaus (AFP)
10:48:02Session AFP/Smooth_Manifolds (AFP)
10:48:02Session AFP/Types_To_Sets_Extension (AFP)
10:48:02Session HOL/HOL-Unix
10:48:02Session HOL/HOL-ZF
10:48:02Session AFP/Category2 (AFP)
10:48:02Session HOL/HOLCF (main timing)
10:48:02Session AFP/Circus (AFP)
10:48:03Session AFP/HOL-CSP (AFP)
10:48:03Session AFP/HOL-CSPM (AFP)
10:48:03Session AFP/HOL-CSP_OpSem (AFP)
10:48:03Session HOL/HOLCF-IMP
10:48:03Session HOL/HOLCF-Library
10:48:03Session AFP/CSP_RefTK (AFP)
10:48:03Session HOL/HOLCF-FOCUS
10:48:03Session HOL/HOLCF-ex
10:48:03Session AFP/PCF (AFP)
10:48:03Session AFP/HOLCF-Prelude (AFP)
10:48:03Session AFP/BirdKMP (AFP)
10:48:04Session HOL/HOLCF-Tutorial
10:48:04Session HOL/IOA (timing)
10:48:04Session HOL/IOA-ABP
10:48:04Session HOL/IOA-NTP
10:48:04Session HOL/IOA-Storage
10:48:04Session HOL/IOA-ex
10:48:04Session AFP/Shivers-CFA (AFP)
10:48:04Session AFP/Stream-Fusion (AFP)
10:48:04Session AFP/Tycon (AFP)
10:48:04Session AFP/WorkerWrapper (AFP)
10:48:04Session AFP/Hales_Jewett (AFP)
10:48:04Session Misc/Haskell
10:48:04Session AFP/Heard_Of (AFP)
10:48:04Session AFP/Consensus_Refined (AFP)
10:48:04Session AFP/Hello_World (AFP)
10:48:04Session AFP/HoareForDivergence (AFP)
10:48:04Session AFP/Hood_Melville_Queue (AFP)
10:48:04Session AFP/HotelKeyCards (AFP)
10:48:04Session Doc/How_to_Prove_it (no_doc)
10:48:04Session AFP/Huffman (AFP)
10:48:04Session AFP/Hybrid_Logic (AFP)
10:48:04Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
10:48:04Session AFP/HyperHoareLogic (AFP)
10:48:04Session AFP/IFC_Tracking (AFP)
10:48:04Session AFP/IMP2 (AFP)
10:48:05Session AFP/IMP2_Binary_Heap (AFP)
10:48:05Session AFP/IMP_Compiler (AFP)
10:48:05Session AFP/IMP_Compiler_Reuse (AFP)
10:48:05Session AFP/IMP_Noninterference (AFP)
10:48:05Session Doc/Implementation (doc)
10:48:05Session AFP/Implicational_Logic (AFP)
10:48:05Session AFP/Impossible_Geometry (AFP)
10:48:05Session AFP/Inductive_Confidentiality (AFP)
10:48:05Session AFP/Inductive_Inference (AFP)
10:48:05Session AFP/InfPathElimination (AFP)
10:48:05Session AFP/Intro_Dest_Elim (AFP)
10:48:05Session AFP/Involutions2Squares (AFP)
10:48:05Session AFP/IsaGeoCoq (AFP)
10:48:05Session AFP/IsaNet (AFP)
10:48:05Session Doc/Isar_Ref (doc)
10:48:05Session AFP/Isabelle_C (AFP)
10:48:06Session Doc/JEdit (doc)
10:48:06Session AFP/Jacobson_Basic_Algebra (AFP)
10:48:06Session AFP/Grothendieck_Schemes (AFP)
10:48:06Session AFP/Pluennecke_Ruzsa_Inequality (AFP)
10:48:06Session AFP/Khovanskii_Theorem (AFP)
10:48:06Session AFP/Kneser_Cauchy_Davenport (AFP)
10:48:06Session AFP/JiveDataStoreModel (AFP)
10:48:06Session AFP/Key_Agreement_Strong_Adversaries (AFP)
10:48:06Session AFP/Kleene_Algebra (AFP)
10:48:06Session AFP/KAD (AFP)
10:48:06Session AFP/KAT_and_DRA (AFP)
10:48:06Session AFP/Algebraic_VCs (AFP)
10:48:06Session AFP/Multirelations (AFP)
10:48:06Session AFP/Quantales (AFP)
10:48:06Session AFP/Transformer_Semantics (AFP)
10:48:06Session AFP/Regular_Algebras (AFP)
10:48:06Session AFP/Relation_Algebra (AFP)
10:48:06Session AFP/Relational_Paths (AFP)
10:48:06Session AFP/Residuated_Lattices (AFP)
10:48:06Session AFP/Knights_Tour (AFP)
10:48:07Session AFP/LambdaMu (AFP)
10:48:07Session AFP/LatticeProperties (AFP)
10:48:07Session AFP/DataRefinementIBP (AFP)
10:48:07Session AFP/GraphMarkingIBP (AFP)
10:48:07Session AFP/Lazy_Case (AFP)
10:48:07Session AFP/Lifting_Definition_Option (AFP)
10:48:07Session AFP/List-Index (AFP)
10:48:07Session AFP/Comparison_Sort_Lower_Bound (AFP)
10:48:07Session AFP/Jinja (AFP)
10:48:07Session AFP/Dominance_CHK (AFP)
10:48:07Session AFP/HRB-Slicing (AFP)
10:48:07Session AFP/InformationFlowSlicing_Inter (AFP)
10:48:07Session AFP/Slicing (AFP)
10:48:07Session AFP/InformationFlowSlicing (AFP)
10:48:07Session AFP/JinjaDCI (AFP)
10:48:07Session AFP/Regression_Test_Selection (AFP)
10:48:08Session AFP/List_Update (AFP)
10:48:08Session AFP/Quick_Sort_Cost (AFP)
10:48:08Session AFP/Random_BSTs (AFP)
10:48:08Session AFP/Randomised_BSTs (AFP)
10:48:08Session AFP/Treaps (AFP)
10:48:08Session AFP/Randomised_Social_Choice (AFP)
10:48:08Session AFP/Fishburn_Impossibility (AFP)
10:48:08Session AFP/PAPP_Impossibility (AFP)
10:48:08Session AFP/SDS_Impossibility (AFP)
10:48:08Session AFP/List_Interleaving (AFP)
10:48:08Session AFP/List_Inversions (AFP)
10:48:08Session AFP/LocalLexing (AFP)
10:48:08Session Doc/Locales (doc)
10:48:08Session AFP/Locally-Nameless-Sigma (AFP)
10:48:08Session AFP/Logging_Independent_Anonymity (AFP)
10:48:09Session AFP/Lowe_Ontological_Argument (AFP)
10:48:09Session AFP/MHComputation (AFP)
10:48:09Session AFP/MLSS_Decision_Proc (AFP)
10:48:09Session AFP/ML_Unification (AFP)
10:48:09Session Doc/Main (doc)
10:48:09Session AFP/Marriage (AFP)
10:48:09Session AFP/Latin_Square (AFP)
10:48:09Session AFP/Matroids (AFP)
10:48:09Session AFP/Max-Card-Matching (AFP)
10:48:09Session AFP/Maximum_Segment_Sum (AFP)
10:48:09Session AFP/Median_Of_Medians_Selection (AFP)
10:48:10Session AFP/KD_Tree (AFP)
10:48:10Session AFP/Menger (AFP)
10:48:10Session AFP/Mereology (AFP)
10:48:10Session AFP/Metalogic_ProofChecker (AFP)
10:48:10Session AFP/MiniML (AFP)
10:48:10Session AFP/Modular_Assembly_Kit_Security (AFP)
10:48:10Session AFP/MonoBoolTranAlgebra (AFP)
10:48:10Session AFP/Multirelations_Heterogeneous (AFP)
10:48:10Session AFP/Multitape_To_Singletape_TM (AFP)
10:48:10Session AFP/Name_Carrying_Type_Inference (AFP)
10:48:10Session AFP/Nano_JSON (AFP)
10:48:10Session AFP/Nash_Williams (AFP)
10:48:10Session AFP/No_FTL_observers (AFP)
10:48:10Session AFP/No_FTL_observers_Gen_Rel (AFP)
10:48:10Session AFP/Nominal2 (AFP)
10:48:11Session AFP/Incompleteness (AFP)
10:48:11Session AFP/Surprise_Paradox (AFP)
10:48:11Session AFP/LambdaAuth (AFP)
10:48:11Session AFP/Launchbury (AFP)
10:48:11Session AFP/Call_Arity (AFP)
10:48:11Session AFP/Modal_Logics_for_NTS (AFP)
10:48:11Session AFP/Rewriting_Z (AFP)
10:48:11Session AFP/Nominal_Myhill_Nerode (AFP)
10:48:11Session AFP/Noninterference_CSP (AFP)
10:48:11Session AFP/Noninterference_Ipurge_Unwinding (AFP)
10:48:11Session AFP/Noninterference_Generic_Unwinding (AFP)
10:48:11Session AFP/Noninterference_Inductive_Unwinding (AFP)
10:48:11Session AFP/Noninterference_Sequential_Composition (AFP)
10:48:12Session AFP/Noninterference_Concurrent_Composition (AFP)
10:48:12Session AFP/NormByEval (AFP)
10:48:12Session AFP/OpSets (AFP)
10:48:12Session AFP/Open_Induction (AFP)
10:48:12Session AFP/Well_Quasi_Orders (AFP)
10:48:12Session AFP/Decreasing-Diagrams-II (AFP)
10:48:12Session AFP/Myhill-Nerode (AFP)
10:48:12Session AFP/Ordinal (AFP)
10:48:12Session AFP/Nested_Multisets_Ordinals (AFP)
10:48:12Session AFP/Design_Theory (AFP)
10:48:12Session AFP/Lovasz_Local (AFP)
10:48:12Session AFP/Undirected_Graph_Theory (AFP)
10:48:12Session AFP/Balog_Szemeredi_Gowers (AFP)
10:48:12Session AFP/Lambda_Free_RPOs (AFP)
10:48:12Session AFP/Lambda_Free_EPO (AFP)
10:48:12Session AFP/Substitutions_Lambda_Free (AFP)
10:48:12Session AFP/Ordered_Resolution_Prover (AFP)
10:48:13Session AFP/Chandy_Lamport (AFP)
10:48:13Session AFP/Saturation_Framework (AFP)
10:48:13Session AFP/Progress_Tracking (AFP)
10:48:13Session AFP/PAL (AFP)
10:48:13Session AFP/PLM (AFP)
10:48:13Session AFP/PSemigroupsConvolution (AFP)
10:48:13Session AFP/Package_logic (AFP)
10:48:13Session AFP/Combinable_Wands (AFP)
10:48:13Session AFP/Paraconsistency (AFP)
10:48:13Session AFP/Parity_Game (AFP)
10:48:13Session AFP/GaleStewart_Games (AFP)
10:48:14Session AFP/Partial_Function_MR (AFP)
10:48:14Session AFP/Physical_Quantities (AFP)
10:48:14Session AFP/Pop_Refinement (AFP)
10:48:14Session AFP/Possibilistic_Noninterference (AFP)
10:48:14Session AFP/Priority_Search_Trees (AFP)
10:48:14Session AFP/Prim_Dijkstra_Simple (AFP)
10:48:14Session Doc/Prog_Prove (doc)
10:48:14Session AFP/Projective_Geometry (AFP)
10:48:14Session AFP/Proof_Strategy_Language (AFP)
10:48:14Session AFP/PropResPI (AFP)
10:48:14Session AFP/Propositional_Logic_Class (AFP)
10:48:14Session AFP/Propositional_Proof_Systems (AFP)
10:48:14Session AFP/PseudoHoops (AFP)
10:48:14Session AFP/Quantales_Converse (AFP)
10:48:14Session AFP/Catoids (AFP)
10:48:14Session AFP/CubicalCategories (AFP)
10:48:14Session AFP/OmegaCatoidsQuantales (AFP)
10:48:14Session AFP/Ramsey-Infinite (AFP)
10:48:14Session AFP/Real_Power (AFP)
10:48:14Session AFP/Real_Time_Deque (AFP)
10:48:15Session AFP/Recursion-Theory-I (AFP)
10:48:15Session AFP/Minsky_Machines (AFP)
10:48:15Session AFP/RefinementReactive (AFP)
10:48:15Session AFP/Regex_Equivalence (AFP)
10:48:15Session AFP/Region_Quadtrees (AFP)
10:48:15Session AFP/Relational_Method (AFP)
10:48:15Session AFP/Rensets (AFP)
10:48:15Session AFP/Robbins-Conjecture (AFP)
10:48:15Session AFP/Roy_Floyd_Warshall (AFP)
10:48:15Session AFP/SCC_Bloemen_Sequential (AFP)
10:48:15Session AFP/SIFPL (AFP)
10:48:15Session AFP/SIFUM_Type_Systems (AFP)
10:48:15Session AFP/Sauer_Shelah_Lemma (AFP)
10:48:15Session AFP/Security_Protocol_Refinement (AFP)
10:48:15Session AFP/SenSocialChoice (AFP)
10:48:15Session AFP/Separation_Algebra (AFP)
10:48:15Session AFP/Hoare_Time (AFP)
10:48:16Session AFP/Separata (AFP)
10:48:16Session AFP/Separation_Logic_Unbounded (AFP)
10:48:16Session AFP/Simpl (AFP)
10:48:16Session AFP/BDD (AFP)
10:48:16Session AFP/SimplifiedOntologicalArgument (AFP)
10:48:16Session AFP/Sliding_Window_Algorithm (AFP)
10:48:16Session AFP/Statecharts (AFP)
10:48:16Session AFP/Stellar_Quorums (AFP)
10:48:16Session AFP/Stone_Algebras (AFP)
10:48:16Session AFP/Stone_Relation_Algebras (AFP)
10:48:16Session AFP/Relational_Cardinality (AFP)
10:48:16Session AFP/Stone_Kleene_Relation_Algebras (AFP)
10:48:16Session AFP/Aggregation_Algebras (AFP)
10:48:16Session AFP/Relational_Disjoint_Set_Forests (AFP)
10:48:16Session AFP/Relational_Minimum_Spanning_Trees (AFP)
10:48:17Session AFP/Relational_Forests (AFP)
10:48:17Session AFP/Subset_Boolean_Algebras (AFP)
10:48:17Session AFP/Correctness_Algebras (AFP)
10:48:17Session AFP/Store_Buffer_Reduction (AFP)
10:48:17Session AFP/StrictOmegaCategories (AFP)
10:48:17Session AFP/Strong_Security (AFP)
10:48:17Session Doc/Sugar (doc)
10:48:17Session AFP/Sunflowers (AFP)
10:48:17Session AFP/Clique_and_Monotone_Circuits (AFP)
10:48:17Session AFP/Suppes_Theorem (AFP)
10:48:17Session AFP/Probability_Inequality_Completeness (AFP)
10:48:17Session AFP/Syntax_Independent_Logic (AFP)
10:48:17Session AFP/Goedel_Incompleteness (AFP)
10:48:17Session AFP/Goedel_HFSet_Semantic (AFP)
10:48:18Session AFP/Goedel_HFSet_Semanticless (AFP)
10:48:18Session AFP/Robinson_Arithmetic (AFP)
10:48:18Session AFP/Synthetic_Completeness (AFP)
10:48:18Session AFP/Szpilrajn (AFP)
10:48:18Session AFP/Combinatorics_Words_Lyndon (AFP)
10:48:18Session AFP/TESL_Language (AFP)
10:48:18Session AFP/TLA (AFP)
10:48:18Session AFP/Timed_Automata (AFP)
10:48:19Session AFP/Probabilistic_Timed_Automata (AFP)
10:48:19Session AFP/Top_Down_Solver (AFP)
10:48:19Session AFP/Topological_Semantics (AFP)
10:48:19Session AFP/Transitive-Closure-II (AFP)
10:48:19Session AFP/Transport (AFP)
10:48:19Session AFP/Tree_Decomposition (AFP)
10:48:19Session AFP/Tree_Enumeration (AFP)
10:48:19Session Doc/Tutorial (doc)
10:48:19Session Doc/Typeclass_Hierarchy (doc)
10:48:20Session AFP/Types_Tableaus_and_Goedels_God (AFP)
10:48:20Session AFP/UPF (AFP)
10:48:20Session AFP/UPF_Firewall (AFP)
10:48:20Session AFP/Universal_Turing_Machine (AFP)
10:48:20Session AFP/Van_der_Waerden (AFP)
10:48:20Session AFP/VeriComp (AFP)
10:48:20Session AFP/Interpreter_Optimizations (AFP)
10:48:20Session AFP/Verified-Prover (AFP)
10:48:20Session AFP/VolpanoSmith (AFP)
10:48:20Session AFP/WHATandWHERE_Security (AFP)
10:48:20Session AFP/Weight_Balanced_Trees (AFP)
10:48:20Session AFP/Weighted_Arithmetic_Geometric_Mean (AFP)
10:48:20Session AFP/Word_Lib (AFP)
10:48:20Session AFP/AutoCorres2 (AFP)
10:48:21Session AFP/AutoCorres2_Main (AFP)
10:48:22Session AFP/AutoCorres2_Test (AFP)
10:48:22Session AFP/Complx (AFP)
10:48:22Session AFP/IEEE_Floating_Point (AFP)
10:48:22Session AFP/IP_Addresses (AFP)
10:48:23Session AFP/Simple_Firewall (AFP)
10:48:23Session AFP/Routing (AFP)
10:48:23Session AFP/Interval_Arithmetic_Word32 (AFP)
10:48:23Session AFP/LEM (AFP)
10:48:23Session AFP/Native_Word (AFP)
10:48:23Session AFP/Collections (AFP)
10:48:23Session AFP/Abstract_Completeness (AFP)
10:48:23Session AFP/Abstract_Soundness (AFP)
10:48:23Session AFP/FOL_Seq_Calc3 (AFP)
10:48:23Session AFP/Incredible_Proof_Machine (AFP)
10:48:24Session AFP/Deriving (AFP)
10:48:24Session AFP/CAVA_Base (AFP)
10:48:24Session AFP/CAVA_Automata (AFP)
10:48:24Session AFP/DFS_Framework (AFP)
10:48:24Session AFP/Gabow_SCC (AFP)
10:48:24Session AFP/LTL_to_GBA (AFP)
10:48:24Session AFP/Promela (AFP)
10:48:24Session AFP/Containers (AFP)
10:48:24Session AFP/CHERI-C_Memory_Model (AFP)
10:48:24Session AFP/Collections_Examples (AFP)
10:48:24Session AFP/Containers-Benchmarks (AFP)
10:48:25Session AFP/Eval_FO (AFP)
10:48:25Session AFP/MFOTL_Monitor (AFP)
10:48:25Session AFP/Generic_Join (AFP)
10:48:25Session AFP/MFODL_Monitor_Optimized (AFP)
10:48:25Session AFP/MFOTL_Checker (AFP)
10:48:25Session AFP/VYDRA_MDL (AFP)
10:48:25Session AFP/Formula_Derivatives (AFP)
10:48:25Session AFP/Labeled_Transition_Systems (AFP)
10:48:25Session AFP/Pushdown_Systems (AFP)
10:48:25Session AFP/MSO_Regex_Equivalence (AFP)
10:48:25Session AFP/Show (AFP)
10:48:25Session AFP/Affine_Arithmetic (AFP)
10:48:26Session AFP/Ordinary_Differential_Equations (AFP)
10:48:26Session AFP/Differential_Dynamic_Logic (AFP)
10:48:26Session AFP/Hybrid_Systems_VCs (AFP)
10:48:26Session AFP/Matrices_for_ODEs (AFP)
10:48:26Session AFP/Taylor_Models (AFP)
10:48:26Session AFP/CakeML (AFP)
10:48:27Session AFP/Certification_Monads (AFP)
10:48:27Session AFP/AI_Planning_Languages_Semantics (AFP)
10:48:27Session AFP/Verified_SAT_Based_AI_Planning (AFP)
10:48:27Session AFP/Dict_Construction (AFP)
10:48:27Session AFP/Formula_Derivatives-Examples (AFP)
10:48:27Session AFP/LL1_Parser (AFP)
10:48:27Session AFP/Monad_Memo_DP (AFP)
10:48:27Session AFP/Hidden_Markov_Models (AFP)
10:48:27Session AFP/Optimal_BST (AFP)
10:48:27Session AFP/Polynomial_Factorization (AFP)
10:48:28Session AFP/Amicable_Numbers (AFP)
10:48:28Session AFP/Continued_Fractions (AFP)
10:48:28Session AFP/Dirichlet_Series (AFP)
10:48:28Session AFP/Zeta_Function (AFP)
10:48:28Session AFP/Dirichlet_L (AFP)
10:48:28Session AFP/Gauss_Sums (AFP)
10:48:28Session AFP/Three_Squares (AFP)
10:48:29Session AFP/Polygonal_Number_Theorem (AFP)
10:48:29Session AFP/Wieferich_Kempner (AFP)
10:48:29Session AFP/Kummer_Congruence (AFP)
10:48:29Session AFP/Prime_Number_Theorem (AFP)
10:48:29Session AFP/PNT_with_Remainder (AFP)
10:48:29Session AFP/Prime_Distribution_Elementary (AFP)
10:48:29Session AFP/IMO2019 (AFP)
10:48:29Session AFP/Irrational_Series_Erdos_Straus (AFP)
10:48:29Session AFP/Transcendence_Series_Hancl_Rucki (AFP)
10:48:30Session AFP/Zeta_3_Irrational (AFP)
10:48:30Session AFP/First_Order_Terms (AFP)
10:48:30Session AFP/Resolution_FOL (AFP)
10:48:30Session AFP/Saturation_Framework_Extensions (AFP)
10:48:30Session AFP/Stateful_Protocol_Composition_and_Typing (AFP)
10:48:30Session AFP/Automated_Stateful_Protocol_Verification (AFP)
10:48:30Session AFP/Gaussian_Integers (AFP)
10:48:30Session AFP/Jordan_Normal_Form (AFP)
10:48:31Session AFP/Farkas (AFP)
10:48:31Session AFP/Isabelle_Marries_Dirac (AFP)
10:48:31Session AFP/Knuth_Bendix_Order (AFP)
10:48:31Session AFP/Functional_Ordered_Resolution_Prover (AFP)
10:48:31Session AFP/Simple_Clause_Learning (AFP)
10:48:31Session AFP/Regular_Tree_Relations (AFP)
10:48:32Session AFP/FO_Theory_Rewriting (AFP)
10:48:32Session AFP/Rewrite_Properties_Reduction (AFP)
10:48:32Session AFP/Weighted_Path_Order (AFP)
10:48:32Session AFP/Efficient_Weighted_Path_Order (AFP)
10:48:32Session AFP/Given_Clause_Loops (AFP)
10:48:32Session AFP/Multiset_Ordering_NPC (AFP)
10:48:32Session AFP/Linear_Recurrences (AFP)
10:48:32Session AFP/Polylog (AFP)
10:48:32Session AFP/Lambert_Series (AFP)
10:48:32Session AFP/Perron_Frobenius (AFP)
10:48:33Session AFP/MDP-Algorithms (AFP)
10:48:33Session AFP/Stochastic_Matrices (AFP)
10:48:33Session AFP/Subresultants (AFP)
10:48:33Session AFP/Berlekamp_Zassenhaus (AFP)
10:48:34Session AFP/Algebraic_Numbers (AFP)
10:48:34Session AFP/BenOr_Kozen_Reif (AFP)
10:48:34Session AFP/LLL_Basis_Reduction (AFP)
10:48:34Session AFP/CVP_Hardness (AFP)
10:48:34Session AFP/LLL_Factorization (AFP)
10:48:34Session AFP/Linear_Inequalities (AFP)
10:48:34Session AFP/LP_Duality (AFP)
10:48:34Session AFP/Linear_Programming (AFP)
10:48:34Session AFP/Number_Theoretic_Transform (AFP)
10:48:34Session AFP/CRYSTALS-Kyber (AFP)
10:48:34Session AFP/Perfect_Fields (AFP)
10:48:34Session AFP/Elimination_Of_Repeated_Factors (AFP)
10:48:34Session AFP/Smith_Normal_Form (AFP)
10:48:35Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP)
10:48:35Session AFP/Polynomials (AFP)
10:48:36Session AFP/Deep_Learning (AFP)
10:48:36Session AFP/QHLProver (AFP)
10:48:36Session AFP/Projective_Measurements (AFP)
10:48:36Session AFP/Commuting_Hermitian (AFP)
10:48:36Session AFP/TsirelsonBound (AFP)
10:48:36Session AFP/Uncertainty_Principle (AFP)
10:48:36Session AFP/Groebner_Bases (AFP)
10:48:37Session AFP/Fishers_Inequality (AFP)
10:48:37Session AFP/Hypergraph_Basics (AFP)
10:48:37Session AFP/Hypergraph_Colourings (AFP)
10:48:37Session AFP/Groebner_Macaulay (AFP)
10:48:37Session AFP/Nullstellensatz (AFP)
10:48:37Session AFP/Signature_Groebner (AFP)
10:48:37Session AFP/Lambda_Free_KBOs (AFP)
10:48:37Session AFP/Sumcheck_Protocol (AFP)
10:48:37Session AFP/Symmetric_Polynomials (AFP)
10:48:38Session AFP/Pi_Transcendental (AFP)
10:48:38Session AFP/Power_Sum_Polynomials (AFP)
10:48:38Session AFP/Hermite_Lindemann (AFP)
10:48:38Session AFP/Factor_Algebraic_Polynomial (AFP)
10:48:38Session AFP/Cubic_Quartic_Equations (AFP)
10:48:38Session AFP/Linear_Recurrences_Solver (AFP)
10:48:38Session AFP/Orient_Rewrite_Rule_Undecidable (AFP)
10:48:38Session AFP/Schwartz_Zippel (AFP)
10:48:39Session AFP/Virtual_Substitution (AFP)
10:48:39Session AFP/Real_Impl (AFP)
10:48:39Session AFP/Complex_Bounded_Operators_Dependencies (AFP)
10:48:40Session AFP/Complex_Bounded_Operators (AFP)
10:48:40Session AFP/Registers (AFP)
10:48:40Session AFP/QR_Decomposition (AFP)
10:48:40Session AFP/XML (AFP)
10:48:40Session AFP/Van_Emde_Boas_Trees (AFP)
10:48:40Session AFP/Dijkstra_Shortest_Path (AFP)
10:48:40Session AFP/Koenigsberg_Friendship (AFP)
10:48:41Session AFP/FOL_Seq_Calc2 (AFP)
10:48:41Session AFP/Formal_SSA (AFP)
10:48:41Session AFP/Minimal_SSA (AFP)
10:48:41Session AFP/Gale_Shapley (AFP)
10:48:41Session AFP/HOL-ODE-Numerics (AFP)
10:48:42Session AFP/HOL-ODE-ARCH-COMP (AFP)
10:48:42Session AFP/HOL-ODE-Examples (AFP large)
10:48:42Session AFP/Lorenz_Approximation (AFP)
10:48:42Session AFP/Lorenz_C0 (AFP large)
10:48:42Session AFP/Lorenz_C1 (AFP large)
10:48:42Session AFP/Poincare_Bendixson (AFP)
10:48:42Session AFP/Picks_Theorem (AFP)
10:48:42Session AFP/KnuthMorrisPratt (AFP)
10:48:42Session AFP/Safe_Range_RC (AFP)
10:48:42Session AFP/Transition_Systems_and_Automata (AFP)
10:48:42Session AFP/Adaptive_State_Counting (AFP)
10:48:42Session AFP/Buchi_Complementation (AFP)
10:48:42Session AFP/LTL_Master_Theorem (AFP)
10:48:42Session AFP/LTL_Normal_Form (AFP)
10:48:42Session AFP/Partial_Order_Reduction (AFP)
10:48:43Session AFP/SM_Base (AFP)
10:48:43Session AFP/SM (AFP)
10:48:43Session AFP/CAVA_Setup (AFP)
10:48:43Session AFP/CAVA_LTL_Modelchecker (AFP)
10:48:43Session AFP/Transitive-Closure (AFP)
10:48:43Session AFP/KBPs (AFP)
10:48:43Session AFP/LTL_to_DRA (AFP)
10:48:43Session AFP/Network_Security_Policy_Verification (AFP)
10:48:44Session AFP/Planarity_Certificates (AFP)
10:48:44Session AFP/Tree-Automata (AFP)
10:48:44Session AFP/Datatype_Order_Generator (AFP)
10:48:44Session AFP/Higher_Order_Terms (AFP)
10:48:44Session AFP/CakeML_Codegen (AFP)
10:48:44Session AFP/Old_Datatype_Show (AFP)
10:48:44Session AFP/Quantifier_Elimination_Hybrid (AFP)
10:48:45Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
10:48:45Session AFP/FSM_Tests (AFP)
10:48:45Session AFP/Iptables_Semantics (AFP)
10:48:45Session AFP/Iptables_Semantics_Examples (AFP)
10:48:45Session AFP/LOFT (AFP)
10:48:45Session AFP/Mersenne_Primes (AFP)
10:48:45Session AFP/MiniSail (AFP)
10:48:46Session AFP/Separation_Logic_Imperative_HOL (AFP)
10:48:46Session AFP/Sepref_Prereq (AFP)
10:48:46Session AFP/ROBDD (AFP)
10:48:46Session AFP/Refine_Imperative_HOL (AFP)
10:48:46Session AFP/BTree (AFP)
10:48:46Session AFP/Floyd_Warshall (AFP)
10:48:46Session AFP/Sepref_Basic (AFP)
10:48:46Session AFP/Sepref_IICF (AFP)
10:48:46Session AFP/Flow_Networks (AFP)
10:48:46Session AFP/EdmondsKarp_Maxflow (AFP)
10:48:47Session AFP/MFMC_Countable (AFP)
10:48:47Session AFP/Probabilistic_While (AFP)
10:48:47Session AFP/CryptHOL (AFP)
10:48:47Session AFP/ABY3_Protocols (AFP)
10:48:47Session AFP/Constructive_Cryptography (AFP)
10:48:47Session AFP/Game_Based_Crypto (AFP)
10:48:47Session AFP/CRYSTALS-Kyber_Security (AFP)
10:48:47Session AFP/Multi_Party_Computation (AFP)
10:48:48Session AFP/Sigma_Commit_Crypto (AFP)
10:48:48Session AFP/Constructive_Cryptography_CM (AFP)
10:48:48Session AFP/Executable_Randomized_Algorithms (AFP)
10:48:48Session AFP/Finite_Fields (AFP)
10:48:50Session AFP/Universal_Hash_Families (AFP)
10:48:50Session AFP/Expander_Graphs (AFP)
10:48:51Session AFP/Karatsuba (AFP)
10:48:51Session AFP/Median_Method (AFP)
10:48:51Session AFP/Frequency_Moments (AFP)
10:48:52Session AFP/Approximate_Model_Counting (AFP)
10:48:52Session AFP/Distributed_Distinct_Elements (AFP)
10:48:53Session AFP/Derandomization_Conditional_Expectations (AFP)
10:48:53Session AFP/Prpu_Maxflow (AFP)
10:48:53Session AFP/Knuth_Morris_Pratt (AFP)
10:48:53Session AFP/Kruskal (AFP)
10:48:53Session AFP/PAC_Checker (AFP)
10:48:53Session AFP/VerifyThis2018 (AFP)
10:48:53Session AFP/VerifyThis2019 (AFP)
10:48:53Session AFP/Simplicial_complexes_and_boolean_functions (AFP)
10:48:53Session AFP/UpDown_Scheme (AFP)
10:48:53Session AFP/WebAssembly (AFP)
10:48:53Session AFP/SPARCv8 (AFP)
10:48:54Session AFP/Schoenhage_Strassen (AFP)
10:48:54Session AFP/X86_Semantics (AFP)
10:48:54Session AFP/ZFC_in_HOL (AFP)
10:48:55Session AFP/CZH_Foundations (AFP)
10:48:55Session AFP/CZH_Elementary_Categories (AFP)
10:48:55Session AFP/CZH_Universal_Constructions (AFP)
10:48:55Session AFP/Category3 (AFP)
10:48:55Session AFP/MonoidalCategory (AFP)
10:48:56Session AFP/Ordinal_Partitions (AFP)
10:48:56Session AFP/Q0_Metatheory (AFP)
10:48:56Session AFP/Q0_Soundness (AFP)
10:48:56Session AFP/Wetzels_Problem (AFP)
10:48:56Session FOL/ZF (main timing)
10:48:56Session Doc/Logics_ZF (doc)
10:48:56Session AFP/Recursion-Addition (AFP)
10:48:56Session FOL/ZF-AC
10:48:56Session FOL/ZF-Coind
10:48:56Session FOL/ZF-Constructible
10:48:56Session AFP/Delta_System_Lemma (AFP)
10:48:56Session AFP/Transitive_Models (AFP)
10:48:56Session AFP/Independence_CH (AFP)
10:48:56Session AFP/Forcing (AFP)
10:48:57Session FOL/ZF-IMP
10:48:57Session FOL/ZF-Induct
10:48:57Session FOL/ZF-UNITY (timing)
10:48:57Session FOL/ZF-Resid
10:48:57Session FOL/ZF-ex
10:49:18Building HOL ...
10:49:18Building HOL-Proofs ...
10:49:18Running ML_Unification ...
10:49:21HOL-Proofs: theory Tools.Code_Generator
10:49:21HOL: theory Tools.Code_Generator
10:49:21ML_Unification: theory ML_Unification.ML_Code_Utils
10:49:21ML_Unification: theory ML_Unification.ML_Attribute_Utils
10:49:21ML_Unification: theory ML_Unification.ML_Conversion_Utils
10:49:21ML_Unification: theory ML_Unification.ML_General_Utils
10:49:21ML_Unification: theory ML_Unification.ML_Generic_Data_Utils
10:49:21ML_Unification: theory ML_Unification.ML_Method_Utils
10:49:21ML_Unification: theory ML_Unification.Setup_Result_Commands
10:49:21ML_Unification: theory SpecCheck.SpecCheck_Show
10:49:21ML_Unification: theory ML_Unification.ML_Normalisations
10:49:21ML_Unification: theory Tools.Code_Generator
10:49:21ML_Unification: theory ML_Unification.ML_Term_Index
10:49:21ML_Unification: theory ML_Unification.ML_Binders
10:49:21ML_Unification: theory ML_Unification.ML_Attributes
10:49:22ML_Unification: theory ML_Unification.ML_Term_Utils
10:49:22ML_Unification: theory ML_Unification.ML_Logger
10:49:22ML_Unification: theory ML_Unification.ML_Parsing_Utils
10:49:22ML_Unification: theory ML_Unification.ML_Theorem_Utils
10:49:22ML_Unification: theory ML_Unification.ML_Logger_Examples
10:49:22ML_Unification: theory ML_Unification.ML_Unification_Base
10:49:22ML_Unification: theory ML_Unification.ML_Tactic_Utils
10:49:23ML_Unification: theory ML_Unification.ML_Functor_Instances
10:49:23ML_Unification: theory ML_Unification.ML_Priorities
10:49:24ML_Unification: theory ML_Unification.ML_Unification_Parsers
10:49:25ML_Unification: theory ML_Unification.Simps_To
10:49:25ML_Unification: theory ML_Unification.Unify_Assumption_Tactic_Base
10:49:25ML_Unification: theory ML_Unification.ML_Utils
10:49:25ML_Unification: theory ML_Unification.ML_Unifiers_Base
10:49:26ML_Unification: theory ML_Unification.ML_Unification_Hints_Base
10:49:26ML_Unification: theory ML_Unification.ML_Unifiers
10:49:26ML_Unification: theory ML_Unification.Unify_Resolve_Tactics_Base
10:49:27ML_Unification: theory ML_Unification.Unify_Assumption_Tactic
10:49:30HOL: theory HOL.HOL
10:49:30ML_Unification: theory ML_Unification.Unification_Attributes_Base
10:49:30HOL-Proofs: theory HOL.HOL
10:49:31ML_Unification: theory ML_Unification.ML_Unification_Hints
10:49:33ML_Unification: theory ML_Unification.Unification_Attributes
10:49:33ML_Unification: theory ML_Unification.Unify_Fact_Tactic_Base
10:49:33ML_Unification: theory ML_Unification.Unify_Resolve_Tactics
10:49:33ML_Unification: theory ML_Unification.Unify_Fact_Tactic
10:49:33ML_Unification: theory ML_Unification.Unification_Tactics
10:49:39ML_Unification: theory HOL.HOL
10:49:40HOL: theory HOL.Argo
10:49:40HOL: theory HOL.Ctr_Sugar
10:49:40HOL: theory HOL.Orderings
10:49:41HOL-Proofs: theory HOL.Argo
10:49:41HOL-Proofs: theory HOL.Ctr_Sugar
10:49:41HOL-Proofs: theory HOL.Orderings
10:49:50HOL: theory HOL.Groups
10:49:50ML_Unification: theory HOL.Argo
10:49:50ML_Unification: theory HOL.Ctr_Sugar
10:49:50HOL-Proofs: theory HOL.Groups
10:49:51HOL: theory HOL.SAT
10:49:51HOL-Proofs: theory HOL.SAT
10:49:53HOL: theory HOL.Lattices
10:49:53HOL-Proofs: theory HOL.Lattices
10:49:53HOL: theory HOL.Boolean_Algebras
10:49:54HOL-Proofs: theory HOL.Boolean_Algebras
10:49:54HOL: theory HOL.Set
10:49:54HOL-Proofs: theory HOL.Set
10:49:55HOL: theory HOL.Fun
10:49:55HOL: theory HOL.Typedef
10:49:55HOL-Proofs: theory HOL.Fun
10:49:55HOL-Proofs: theory HOL.Typedef
10:49:56ML_Unification: theory HOL.Orderings
10:49:58HOL-Proofs: theory HOL.Complete_Lattices
10:49:58HOL-Proofs: theory HOL.Rings
10:49:58HOL: theory HOL.Complete_Lattices
10:49:58HOL: theory HOL.Rings
10:50:00HOL: theory HOL.Inductive
10:50:00ML_Unification: theory HOL.Groups
10:50:00ML_Unification: theory HOL.SAT
10:50:01ML_Unification: theory ML_Unification.ML_Unification_HOL_Setup
10:50:02ML_Unification: theory HOL.Lattices
10:50:03ML_Unification: theory HOL.Boolean_Algebras
10:50:03ML_Unification: theory HOL.Set
10:50:04HOL-Proofs: theory HOL.Inductive
10:50:05ML_Unification: theory HOL.Fun
10:50:05ML_Unification: theory HOL.Typedef
10:50:05HOL: theory HOL.Product_Type
10:50:05HOL: theory HOL.Sum_Type
10:50:07ML_Unification: theory HOL.Complete_Lattices
10:50:07ML_Unification: theory HOL.Rings
10:50:08HOL: theory HOL.Complete_Partial_Order
10:50:09ML_Unification: theory HOL.Inductive
10:50:09HOL: theory HOL.Nat
10:50:12HOL: theory HOL.Fields
10:50:12HOL: theory HOL.Meson
10:50:13HOL-Proofs: theory HOL.Product_Type
10:50:13HOL-Proofs: theory HOL.Sum_Type
10:50:16HOL-Proofs: theory HOL.Complete_Partial_Order
10:50:16HOL: theory HOL.Relation
10:50:16ML_Unification: theory HOL.Product_Type
10:50:16ML_Unification: theory HOL.Sum_Type
10:50:18HOL: theory HOL.Finite_Set
10:50:18ML_Unification: theory HOL.Complete_Partial_Order
10:50:19ML_Unification: theory HOL.Nat
10:50:20HOL: theory HOL.Transitive_Closure
10:50:21ML_Unification: theory HOL.Fields
10:50:21ML_Unification: theory HOL.Meson
10:50:22HOL: theory HOL.Wellfounded
10:50:23HOL: theory HOL.Fun_Def_Base
10:50:23HOL: theory HOL.Hilbert_Choice
10:50:23HOL: theory HOL.Wfrec
10:50:23HOL: theory HOL.Order_Relation
10:50:24ML_Unification: theory HOL.Relation
10:50:24HOL: theory HOL.BNF_Wellorder_Relation
10:50:24HOL-Proofs: theory HOL.Nat
10:50:25HOL: theory HOL.BNF_Wellorder_Embedding
10:50:25HOL: theory HOL.Zorn
10:50:25ML_Unification: theory HOL.Finite_Set
10:50:26HOL: theory HOL.BNF_Wellorder_Constructions
10:50:26HOL: theory HOL.ATP
10:50:27ML_Unification: theory HOL.Transitive_Closure
10:50:28HOL: theory HOL.BNF_Cardinal_Order_Relation
10:50:29ML_Unification: theory HOL.Wellfounded
10:50:30ML_Unification: theory HOL.Fun_Def_Base
10:50:30ML_Unification: theory HOL.Hilbert_Choice
10:50:30ML_Unification: theory HOL.Wfrec
10:50:30ML_Unification: theory HOL.Order_Relation
10:50:30HOL-Proofs: theory HOL.Fields
10:50:30HOL-Proofs: theory HOL.Meson
10:50:31HOL: theory HOL.BNF_Cardinal_Arithmetic
10:50:31ML_Unification: theory HOL.BNF_Wellorder_Relation
10:50:32ML_Unification: theory HOL.BNF_Wellorder_Embedding
10:50:32ML_Unification: theory HOL.Zorn
10:50:32ML_Unification: theory HOL.ATP
10:50:33HOL: theory HOL.BNF_Def
10:50:34ML_Unification: theory HOL.BNF_Wellorder_Constructions
10:50:35ML_Unification: theory HOL.BNF_Cardinal_Order_Relation
10:50:38HOL: theory HOL.Metis
10:50:38ML_Unification: theory HOL.BNF_Cardinal_Arithmetic
10:50:39ML_Unification: theory HOL.BNF_Def
10:50:41HOL-Proofs: theory HOL.Relation
10:50:43ML_Unification: theory HOL.Metis
10:50:44HOL: theory HOL.BNF_Composition
10:50:44HOL: theory HOL.Basic_BNFs
10:50:46HOL-Proofs: theory HOL.Finite_Set
10:50:47HOL: theory HOL.BNF_Fixpoint_Base
10:50:50ML_Unification: theory HOL.BNF_Composition
10:50:50ML_Unification: theory HOL.Basic_BNFs
10:50:53ML_Unification: theory HOL.BNF_Fixpoint_Base
10:50:58HOL: theory HOL.BNF_Least_Fixpoint
10:51:02HOL: theory HOL.Basic_BNF_LFPs
10:51:02HOL: theory HOL.Equiv_Relations
10:51:03HOL: theory HOL.Transfer
10:51:04ML_Unification: theory HOL.BNF_Least_Fixpoint
10:51:05HOL: theory HOL.Lifting
10:51:05HOL: theory HOL.Num
10:51:08HOL: theory HOL.Option
10:51:08HOL: theory HOL.Quotient
10:51:08HOL: theory HOL.Extraction
10:51:09ML_Unification: theory HOL.Basic_BNF_LFPs
10:51:09ML_Unification: theory HOL.Equiv_Relations
10:51:10ML_Unification: theory HOL.Transfer
10:51:10HOL: theory HOL.Partial_Function
10:51:11HOL: theory HOL.Fun_Def
10:51:12ML_Unification: theory HOL.Lifting
10:51:12ML_Unification: theory HOL.Num
10:51:14HOL: theory HOL.Power
10:51:15ML_Unification: theory HOL.Option
10:51:15ML_Unification: theory HOL.Extraction
10:51:15ML_Unification: theory HOL.Partial_Function
10:51:16ML_Unification: theory HOL.Fun_Def
10:51:17ML_Unification: theory HOL.Quotient
10:51:18HOL: theory HOL.Groups_Big
10:51:18HOL-Proofs: theory HOL.Transitive_Closure
10:51:20ML_Unification: theory HOL.Power
10:51:21HOL: theory HOL.Int
10:51:21HOL: theory HOL.Lattices_Big
10:51:21HOL: theory HOL.Lifting_Set
10:51:22ML_Unification: theory HOL.Groups_Big
10:51:23HOL: theory HOL.Euclidean_Rings
10:51:27ML_Unification: theory HOL.Int
10:51:27HOL: theory HOL.Parity
10:51:27HOL-Proofs: theory HOL.Wellfounded
10:51:28ML_Unification: theory HOL.Lattices_Big
10:51:29ML_Unification: theory HOL.Lifting_Set
10:51:29ML_Unification: theory HOL.Euclidean_Rings
10:51:31ML_Unification: theory HOL.Parity
10:51:31HOL-Proofs: theory HOL.Fun_Def_Base
10:51:31HOL-Proofs: theory HOL.Hilbert_Choice
10:51:31HOL-Proofs: theory HOL.Wfrec
10:51:32ML_Unification: theory HOL.Divides
10:51:32ML_Unification: theory HOL.Numeral_Simprocs
10:51:32HOL-Proofs: theory HOL.Order_Relation
10:51:34HOL-Proofs: theory HOL.BNF_Wellorder_Relation
10:51:34ML_Unification: theory HOL.SMT
10:51:35ML_Unification: theory HOL.Semiring_Normalization
10:51:36HOL: theory HOL.Divides
10:51:36HOL: theory HOL.Numeral_Simprocs
10:51:36HOL: theory HOL.Set_Interval
10:51:37HOL-Proofs: theory HOL.BNF_Wellorder_Embedding
10:51:37HOL-Proofs: theory HOL.ATP
10:51:37HOL-Proofs: theory HOL.Zorn
10:51:37HOL: theory HOL.SMT
10:51:38HOL: theory HOL.Semiring_Normalization
10:51:39ML_Unification: theory HOL.Groebner_Basis
10:51:43ML_Unification: theory HOL.Set_Interval
10:51:47HOL: theory HOL.Groebner_Basis
10:51:48ML_Unification: theory HOL.Conditionally_Complete_Lattices
10:51:48ML_Unification: theory HOL.Presburger
10:51:48ML_Unification: theory HOL.Filter
10:51:49HOL-Proofs: theory HOL.Metis
10:51:52HOL: theory HOL.Conditionally_Complete_Lattices
10:51:52HOL: theory HOL.Presburger
10:51:52HOL: theory HOL.Filter
10:51:54HOL-Proofs: theory HOL.BNF_Wellorder_Constructions
10:51:55ML_Unification: theory HOL.Sledgehammer
10:52:01HOL: theory HOL.Sledgehammer
10:52:05ML_Unification: theory HOL.List
10:52:06HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation
10:52:08HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic
10:52:10HOL-Proofs: theory HOL.BNF_Def
10:52:12HOL: theory HOL.List
10:52:15ML_Unification: theory HOL.Groups_List
10:52:15ML_Unification: theory HOL.Map
10:52:15HOL-Proofs: theory HOL.BNF_Composition
10:52:15HOL-Proofs: theory HOL.Basic_BNFs
10:52:17ML_Unification: theory HOL.Bit_Operations
10:52:17ML_Unification: theory HOL.Factorial
10:52:17ML_Unification: theory HOL.Enum
10:52:18ML_Unification: theory HOL.Binomial
10:52:18HOL-Proofs: theory HOL.BNF_Fixpoint_Base
10:52:20HOL: theory HOL.Groups_List
10:52:20HOL: theory HOL.Map
10:52:22HOL: theory HOL.Bit_Operations
10:52:22HOL: theory HOL.Factorial
10:52:22HOL: theory HOL.Enum
10:52:23HOL: theory HOL.Binomial
10:52:25ML_Unification: theory HOL.Code_Numeral
10:52:25ML_Unification: theory HOL.GCD
10:52:25ML_Unification: theory HOL.String
10:52:25ML_Unification: theory HOL.Random
10:52:27HOL-Proofs: theory HOL.BNF_Least_Fixpoint
10:52:29ML_Unification: theory HOL.BNF_Greatest_Fixpoint
10:52:29ML_Unification: theory HOL.Predicate
10:52:30ML_Unification: theory HOL.Lazy_Sequence
10:52:30ML_Unification: theory HOL.Limited_Sequence
10:52:30ML_Unification: theory HOL.Typerep
10:52:31ML_Unification: theory HOL.Code_Evaluation
10:52:31HOL-Proofs: theory HOL.Basic_BNF_LFPs
10:52:31HOL-Proofs: theory HOL.Equiv_Relations
10:52:31HOL-Proofs: theory HOL.Transfer
10:52:32HOL-Proofs: theory HOL.Num
10:52:34HOL-Proofs: theory HOL.Lifting
10:52:34ML_Unification: theory HOL.Quickcheck_Random
10:52:36HOL-Proofs: theory HOL.Power
10:52:37HOL-Proofs: theory HOL.Option
10:52:37HOL-Proofs: theory HOL.Quotient
10:52:38HOL-Proofs: theory HOL.Extraction
10:52:38HOL-Proofs: theory HOL.Partial_Function
10:52:39ML_Unification: theory HOL.Quickcheck_Exhaustive
10:52:39ML_Unification: theory HOL.Quickcheck_Narrowing
10:52:39ML_Unification: theory HOL.Random_Pred
10:52:40HOL-Proofs: theory HOL.Fun_Def
10:52:40HOL: theory HOL.Code_Numeral
10:52:40ML_Unification: theory HOL.Random_Sequence
10:52:42HOL: theory HOL.String
10:52:42HOL: theory HOL.GCD
10:52:42HOL: theory HOL.Random
10:52:43HOL-Proofs: theory HOL.Groups_Big
10:52:44ML_Unification: theory HOL.Record
10:52:44ML_Unification: theory HOL.Predicate_Compile
10:52:47HOL: theory HOL.BNF_Greatest_Fixpoint
10:52:47HOL: theory HOL.Predicate
10:52:49HOL: theory HOL.Typerep
10:52:49ML_Unification: theory HOL.Nitpick
10:52:49HOL: theory HOL.Lazy_Sequence
10:52:51ML_Unification: theory HOL.Mirabelle
10:52:53HOL: theory HOL.Limited_Sequence
10:52:53HOL: theory HOL.Code_Evaluation
10:52:55HOL: theory HOL.Quickcheck_Random
10:52:58HOL: theory HOL.Quickcheck_Exhaustive
10:52:59HOL-Proofs: theory HOL.Int
10:52:59HOL-Proofs: theory HOL.Lifting_Set
10:52:59HOL-Proofs: theory HOL.Lattices_Big
10:53:01ML_Unification: theory HOL.Nunchaku
10:53:03ML_Unification: theory Main
10:53:03ML_Unification: theory HOL.Archimedean_Field
10:53:03ML_Unification: theory ML_Unification.E_Unification_Examples
10:53:03HOL: theory HOL.Quickcheck_Narrowing
10:53:05ML_Unification: theory HOL.Rat
10:53:06HOL: theory HOL.Random_Pred
10:53:06ML_Unification: theory ML_Unification.Unification_Hints_Reification_Examples
10:53:06HOL: theory HOL.Random_Sequence
10:53:07HOL: theory HOL.Record
10:53:07HOL: theory HOL.Predicate_Compile
10:53:11HOL-Proofs: theory HOL.Euclidean_Rings
10:53:12HOL: theory HOL.Nitpick
10:53:13HOL: theory HOL.Mirabelle
10:53:21HOL: theory HOL.Nunchaku
10:53:23HOL: theory Main
10:53:23HOL: theory HOL.Archimedean_Field
10:53:23HOL: theory HOL.Hull
10:53:23HOL: theory HOL.Topological_Spaces
10:53:23HOL: theory HOL.Modules
10:53:24HOL: theory HOL.Vector_Spaces
10:53:30HOL: theory HOL.Rat
10:53:33HOL: theory HOL.Real
10:53:35HOL: theory HOL.Binomial_Plus
10:53:35HOL: theory HOL.Real_Vector_Spaces
10:53:43HOL-Proofs: theory HOL.Parity
10:53:46ML_Unification: theory SpecCheck.SpecCheck_Base
10:53:46ML_Unification: theory SpecCheck.SpecCheck_Generators
10:53:46ML_Unification: theory SpecCheck.SpecCheck_Output_Style
10:53:46ML_Unification: theory SpecCheck.SpecCheck_Shrink
10:53:46ML_Unification: theory SpecCheck.SpecCheck
10:53:46ML_Unification: theory ML_Unification.ML_Unification_Tests_Base
10:53:47ML_Unification: theory ML_Unification.First_Order_ML_Unification_Tests
10:53:47ML_Unification: theory ML_Unification.Higher_Order_Pattern_ML_Unification_Tests
10:53:47ML_Unification: theory ML_Unification.Higher_Order_ML_Unification_Tests
10:53:47ML_Unification: theory ML_Unification.ML_Unification_Tests
10:54:00HOL: theory HOL.Inequalities
10:54:00HOL: theory HOL.Limits
10:54:03HOL-Proofs: theory HOL.Divides
10:54:03HOL-Proofs: theory HOL.Set_Interval
10:54:03HOL-Proofs: theory HOL.Numeral_Simprocs
10:54:04HOL-Proofs: theory HOL.SMT
10:54:04HOL-Proofs: theory HOL.Semiring_Normalization
10:54:10HOL-Proofs: theory HOL.Groebner_Basis
10:54:10HOL: theory HOL.Deriv
10:54:10HOL: theory HOL.Series
10:54:12HOL: theory HOL.NthRoot
10:54:13HOL: theory HOL.Transcendental
10:54:19HOL: theory HOL.Complex
10:54:19HOL: theory HOL.MacLaurin
10:54:22HOL: theory Complex_Main
10:54:23Preparing ML_Unification/document ...
10:54:27Finished ML_Unification/document (0:00:04 elapsed time)
10:54:27Preparing ML_Unification/outline ...
10:54:31Finished ML_Unification/outline (0:00:03 elapsed time)
10:54:31Timing ML_Unification (4 threads, 286.868s elapsed time, 836.359s cpu time, 67.330s GC time, factor 2.92)
10:54:31Finished ML_Unification (0:04:49 elapsed time, 0:14:02 cpu time, factor 2.91)
10:54:36HOL-Proofs: theory HOL.Conditionally_Complete_Lattices
10:54:36HOL-Proofs: theory HOL.Presburger
10:54:36HOL-Proofs: theory HOL.Filter
10:54:50HOL-Proofs: theory HOL.Sledgehammer
10:54:54HOL-Proofs: theory HOL.List
10:55:30Preparing HOL/document ...
10:56:19HOL-Proofs: theory HOL.Groups_List
10:56:19HOL-Proofs: theory HOL.Map
10:56:25HOL-Proofs: theory HOL.Bit_Operations
10:56:25HOL-Proofs: theory HOL.Factorial
10:56:25HOL-Proofs: theory HOL.Enum
10:56:29HOL-Proofs: theory HOL.Binomial
10:57:17Finished HOL/document (0:01:46 elapsed time)
10:57:17Preparing HOL/outline ...
10:57:21HOL-Proofs: theory HOL.Code_Numeral
10:57:34HOL-Proofs: theory HOL.GCD
10:57:34HOL-Proofs: theory HOL.Random
10:57:34HOL-Proofs: theory HOL.String
10:57:54HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint
10:57:54HOL-Proofs: theory HOL.Predicate
10:57:54HOL-Proofs: theory HOL.Typerep
10:57:57HOL-Proofs: theory HOL.Lazy_Sequence
10:57:59HOL-Proofs: theory HOL.Limited_Sequence
10:57:59HOL-Proofs: theory HOL.Code_Evaluation
10:58:01HOL-Proofs: theory HOL.Quickcheck_Random
10:58:05HOL-Proofs: theory HOL.Quickcheck_Exhaustive
10:58:05HOL-Proofs: theory HOL.Quickcheck_Narrowing
10:58:05HOL-Proofs: theory HOL.Random_Pred
10:58:05HOL-Proofs: theory HOL.Random_Sequence
10:58:09HOL-Proofs: theory HOL.Record
10:58:09HOL-Proofs: theory HOL.Predicate_Compile
10:58:12HOL-Proofs: theory HOL.Nitpick
10:58:13HOL-Proofs: theory HOL.Mirabelle
10:58:19Finished HOL/outline (0:01:01 elapsed time)
10:58:20HOL-Proofs: theory HOL.Nunchaku
10:58:20Timing HOL (4 threads, 327.403s elapsed time, 1029.851s cpu time, 59.588s GC time, factor 3.15)
10:58:20Finished HOL (0:05:59 elapsed time, 0:18:08 cpu time, factor 3.03)
10:58:20Building HOL-Analysis ...
10:58:20Building ZFC_in_HOL ...
10:58:20Building HOL-Library ...
10:58:20Building Simpl ...
10:58:20Building Bounded_Deducibility_Security ...
10:58:20Building Automatic_Refinement ...
10:58:20Building LEM ...
10:58:20Building Syntax_Independent_Logic ...
10:58:20Building Word_Lib ...
10:58:21HOL-Proofs: theory Main
10:58:22Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Abstract_BD_Security
10:58:22Bounded_Deducibility_Security: theory HOL-Library.Sublist
10:58:22Automatic_Refinement: theory HOL-Eisbach.Eisbach
10:58:22Syntax_Independent_Logic: theory HOL-Eisbach.Eisbach
10:58:22Automatic_Refinement: theory Automatic_Refinement.Foldi
10:58:22Automatic_Refinement: theory Automatic_Refinement.Prio_List
10:58:22Automatic_Refinement: theory Automatic_Refinement.Refine_Util_Bootstrap1
10:58:22ZFC_in_HOL: theory HOL-Cardinals.Fun_More
10:58:22ZFC_in_HOL: theory HOL-Cardinals.Order_Union
10:58:22Word_Lib: theory Word_Lib.Even_More_List
10:58:22Word_Lib: theory Word_Lib.Enumeration
10:58:22Word_Lib: theory HOL-Library.Phantom_Type
10:58:22Word_Lib: theory HOL-Library.Sublist
10:58:22ZFC_in_HOL: theory HOL-Cardinals.Order_Relation_More
10:58:22ZFC_in_HOL: theory HOL-Library.FuncSet
10:58:22Simpl: theory HOL-Library.Old_Recdef
10:58:22Simpl: theory HOL-Library.Cancellation
10:58:22Simpl: theory HOL-Library.LaTeXsugar
10:58:22Simpl: theory HOL-Statespace.DistinctTreeProver
10:58:22HOL-Library: theory HOL-Library.README
10:58:22Automatic_Refinement: theory Automatic_Refinement.Mk_Term_Antiquot
10:58:22Word_Lib: theory Word_Lib.More_Bit_Ring
10:58:22LEM: theory HOL-Library.FuncSet
10:58:22LEM: theory HOL-Combinatorics.Transposition
10:58:22LEM: theory HOL-Library.Cancellation
10:58:22LEM: theory HOL-Library.Phantom_Type
10:58:22ZFC_in_HOL: theory HOL-Library.Infinite_Set
10:58:22Automatic_Refinement: theory Automatic_Refinement.Mpat_Antiquot
10:58:22Simpl: theory Simpl.Simpl_Heap
10:58:22HOL-Library: theory HOL-Library.AList
10:58:22HOL-Library: theory HOL-Library.Adhoc_Overloading
10:58:22HOL-Library: theory HOL-Library.BNF_Axiomatization
10:58:22HOL-Library: theory HOL-Library.BNF_Corec
10:58:23HOL-Proofs: theory HOL-Library.Realizers
10:58:23LEM: theory HOL-Library.Sublist
10:58:24Simpl: theory Simpl.HeapList
10:58:24ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Extension
10:58:25Word_Lib: theory Word_Lib.More_Misc
10:58:25Automatic_Refinement: theory HOL-Library.Cancellation
10:58:25Word_Lib: theory HOL-Library.Cardinality
10:58:26HOL-Library: theory HOL-Library.Cancellation
10:58:26Automatic_Refinement: theory HOL-Library.Infinite_Set
10:58:26HOL-Analysis: theory HOL-Library.BNF_Corec
10:58:26HOL-Analysis: theory HOL-Library.Cancellation
10:58:26HOL-Analysis: theory HOL-Combinatorics.Transposition
10:58:26HOL-Analysis: theory HOL-Library.FuncSet
10:58:27ZFC_in_HOL: theory HOL-Cardinals.Wellfounded_More
10:58:27Simpl: theory HOL-Library.Multiset
10:58:27HOL-Library: theory HOL-Library.Monad_Syntax
10:58:28ZFC_in_HOL: theory HOL-Library.Nat_Bijection
10:58:28ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Relation
10:58:28LEM: theory HOL-Library.Disjoint_Sets
10:58:28HOL-Library: theory HOL-Library.State_Monad
10:58:29Automatic_Refinement: theory Automatic_Refinement.Refine_Util
10:58:29HOL-Analysis: theory HOL-Library.Infinite_Set
10:58:30LEM: theory HOL-Library.Multiset
10:58:31Word_Lib: theory HOL-Library.Numeral_Type
10:58:31LEM: theory HOL-Library.Cardinality
10:58:32ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Embedding
10:58:32Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Trivia
10:58:32ZFC_in_HOL: theory HOL-Library.Old_Datatype
10:58:32Syntax_Independent_Logic: theory Syntax_Independent_Logic.Prelim
10:58:32LEM: theory HOL-Library.While_Combinator
10:58:33Syntax_Independent_Logic: theory Syntax_Independent_Logic.Syntax
10:58:33Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Filtermap
10:58:33Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Transition_System
10:58:34Word_Lib: theory Word_Lib.More_Sublist
10:58:34ZFC_in_HOL: theory HOL-Cardinals.Wellorder_Constructions
10:58:36HOL-Analysis: theory HOL-Library.Nat_Bijection
10:58:36HOL-Analysis: theory HOL-Library.Disjoint_Sets
10:58:36Word_Lib: theory HOL-Library.Type_Length
10:58:36HOL-Analysis: theory HOL-Library.Multiset
10:58:36Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_TS
10:58:36Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.IO_Automaton
10:58:36HOL-Library: theory HOL-Library.Multiset
10:58:37Word_Lib: theory HOL-Library.Word
10:58:37Word_Lib: theory Word_Lib.More_Arithmetic
10:58:37Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_Triggers
10:58:38LEM: theory LEM.Lem_bool
10:58:38HOL-Library: theory HOL-Library.Case_Converter
10:58:39LEM: theory LEM.Lem_basic_classes
10:58:39HOL-Library: theory HOL-Library.DAList
10:58:39LEM: theory HOL-Library.Numeral_Type
10:58:40Simpl: theory Simpl.Language
10:58:40ZFC_in_HOL: theory HOL-Library.Countable
10:58:40Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_IO
10:58:41Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.BD_Security_Unwinding
10:58:41Simpl: theory Simpl.Generalise
10:58:41Simpl: theory HOL-Statespace.StateFun
10:58:42HOL-Analysis: theory HOL-Library.Old_Datatype
10:58:42ZFC_in_HOL: theory HOL-Cardinals.Cardinal_Order_Relation
10:58:42ZFC_in_HOL: theory HOL-Cardinals.Ordinal_Arithmetic
10:58:42HOL-Analysis: theory HOL-Library.Phantom_Type
10:58:42Automatic_Refinement: theory Automatic_Refinement.Anti_Unification
10:58:42Automatic_Refinement: theory Automatic_Refinement.Attr_Comb
10:58:43Simpl: theory HOL-Statespace.StateSpaceLocale
10:58:43Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Compositional_Reasoning
10:58:43Automatic_Refinement: theory Automatic_Refinement.Indep_Vars
10:58:44LEM: theory Word_Lib.Even_More_List
10:58:44Automatic_Refinement: theory Automatic_Refinement.Named_Sorted_Thms
10:58:44LEM: theory Word_Lib.More_Bit_Ring
10:58:44Automatic_Refinement: theory Automatic_Refinement.Mk_Record_Simp
10:58:44HOL-Library: theory HOL-Library.Code_Lazy
10:58:45Syntax_Independent_Logic: theory Syntax_Independent_Logic.Deduction
10:58:45Bounded_Deducibility_Security: theory Bounded_Deducibility_Security.Bounded_Deducibility_Security
10:58:45Syntax_Independent_Logic: theory Syntax_Independent_Logic.Syntax_Arith
10:58:45Automatic_Refinement: theory Automatic_Refinement.Tagged_Solver
10:58:45Automatic_Refinement: theory Automatic_Refinement.Select_Solve
10:58:45Automatic_Refinement: theory HOL-Library.Multiset
10:58:45Automatic_Refinement: theory HOL-Library.Option_ord
10:58:46LEM: theory HOL-Library.Type_Length
10:58:47HOL-Analysis: theory HOL-Library.Product_Plus
10:58:47HOL-Analysis: theory HOL-Library.Product_Order
10:58:48HOL-Analysis: theory HOL-Library.Cardinality
10:58:49HOL-Library: theory HOL-Library.Simps_Case_Conv
10:58:49HOL-Analysis: theory HOL-Library.Set_Algebras
10:58:49HOL-Library: theory HOL-Library.Extended
10:58:49HOL-Library: theory HOL-Library.Centered_Division
10:58:50HOL-Library: theory HOL-Library.Char_ord
10:58:50LEM: theory HOL-Library.Word
10:58:50LEM: theory Word_Lib.More_Arithmetic
10:58:51HOL-Analysis: theory HOL-Real_Asymp.Inst_Existentials
10:58:51HOL-Library: theory HOL-Library.Code_Abstract_Char
10:58:51HOL-Analysis: theory HOL-Library.Countable
10:58:52Simpl: theory HOL-Statespace.StateSpaceSyntax
10:58:53ZFC_in_HOL: theory HOL-Cardinals.Cardinal_Arithmetic
10:58:54HOL-Analysis: theory HOL-Library.Numeral_Type
10:58:56ZFC_in_HOL: theory HOL-Library.Countable_Set
10:58:57ZFC_in_HOL: theory HOL-Cardinals.Cardinals
10:58:59HOL-Library: theory HOL-Library.Code_Abstract_Nat
10:58:59HOL-Library: theory HOL-Library.Code_Binary_Nat
10:59:00HOL-Library: theory HOL-Library.Code_Target_Nat
10:59:00ZFC_in_HOL: theory HOL-Library.Equipollence
10:59:00ZFC_in_HOL: theory HOL-Analysis.Continuum_Not_Denumerable
10:59:00Syntax_Independent_Logic: theory Syntax_Independent_Logic.Natural_Deduction
10:59:01Syntax_Independent_Logic: theory Syntax_Independent_Logic.Standard_Model
10:59:01Word_Lib: theory Word_Lib.Legacy_Aliases
10:59:01Word_Lib: theory Word_Lib.More_Divides
10:59:02HOL-Analysis: theory HOL-Analysis.Metric_Arith
10:59:02HOL-Analysis: theory HOL-Library.Countable_Set
10:59:03Word_Lib: theory Word_Lib.More_Word
10:59:03LEM: theory HOL-Combinatorics.Permutations
10:59:04ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Library
10:59:04HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices
10:59:04LEM: theory LEM.Lem_function
10:59:04Preparing Bounded_Deducibility_Security/document ...
10:59:04ZFC_in_HOL: theory ZFC_in_HOL.ZFC_in_HOL
10:59:04LEM: theory LEM.Lem_tuple
10:59:05LEM: theory LEM.Lem_maybe
10:59:08ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Cardinals
10:59:08LEM: theory HOL-Combinatorics.List_Permutation
10:59:08LEM: theory LEM.LemExtraDefs
10:59:09Word_Lib: theory Word_Lib.Strict_part_mono
10:59:09Automatic_Refinement: theory HOL-ex.Quicksort
10:59:10Finished Bounded_Deducibility_Security/document (0:00:05 elapsed time)
10:59:10Preparing Bounded_Deducibility_Security/outline ...
10:59:10Automatic_Refinement: theory Automatic_Refinement.Misc
10:59:12Word_Lib: theory Word_Lib.Bit_Comprehension
10:59:12Word_Lib: theory Word_Lib.Bit_Shifts_Infix_Syntax
10:59:12Word_Lib: theory Word_Lib.Least_significant_bit
10:59:12Word_Lib: theory HOL-Library.Signed_Division
10:59:13Word_Lib: theory Word_Lib.Signed_Division_Word
10:59:14Word_Lib: theory Word_Lib.Aligned
10:59:14Word_Lib: theory Word_Lib.Most_significant_bit
10:59:14ZFC_in_HOL: theory ZFC_in_HOL.Kirby
10:59:15Finished Bounded_Deducibility_Security/outline (0:00:04 elapsed time)
10:59:15Timing Bounded_Deducibility_Security (4 threads, 29.800s elapsed time, 58.678s cpu time, 1.722s GC time, factor 1.97)
10:59:15Finished Bounded_Deducibility_Security (0:00:43 elapsed time, 0:01:19 cpu time, factor 1.81)
10:59:15Building BD_Security_Compositional ...
10:59:15Word_Lib: theory Word_Lib.Generic_set_bit
10:59:16ZFC_in_HOL: theory ZFC_in_HOL.ZFC_Typeclasses
10:59:17Word_Lib: theory Word_Lib.Next_and_Prev
10:59:17Word_Lib: theory Word_Lib.Bits_Int
10:59:17ZFC_in_HOL: theory ZFC_in_HOL.Ordinal_Exp
10:59:17BD_Security_Compositional: theory BD_Security_Compositional.Composing_Security
10:59:17BD_Security_Compositional: theory BD_Security_Compositional.Trivial_Security
10:59:17BD_Security_Compositional: theory BD_Security_Compositional.Independent_Secrets
10:59:17BD_Security_Compositional: theory BD_Security_Compositional.Transporting_Security
10:59:18Simpl: theory Simpl.Semantic
10:59:18ZFC_in_HOL: theory ZFC_in_HOL.Cantor_NF
10:59:22ZFC_in_HOL: theory ZFC_in_HOL.General_Cardinals
10:59:25Syntax_Independent_Logic: theory Syntax_Independent_Logic.Pseudo_Term
10:59:25Word_Lib: theory Word_Lib.Singleton_Bit_Shifts
10:59:25Word_Lib: theory Word_Lib.Many_More
10:59:25Word_Lib: theory Word_Lib.Typedef_Morphisms
10:59:25Automatic_Refinement: theory Automatic_Refinement.Refine_Lib
10:59:25LEM: theory Word_Lib.Bit_Comprehension
10:59:25LEM: theory Word_Lib.Legacy_Aliases
10:59:25LEM: theory Word_Lib.More_Divides
10:59:26Syntax_Independent_Logic: theory Syntax_Independent_Logic.Deduction_Q
10:59:26LEM: theory LEM.Lem_num
10:59:26LEM: theory Word_Lib.More_Word
10:59:29Word_Lib: theory HOL-Eisbach.Eisbach
10:59:29Word_Lib: theory Word_Lib.Bit_Comprehension_Int
10:59:29Word_Lib: theory Word_Lib.Hex_Words
10:59:29Word_Lib: theory Word_Lib.Signed_Words
10:59:30HOL-Library: theory HOL-Library.Code_Prolog
10:59:30Word_Lib: theory Word_Lib.Syntax_Bundles
10:59:31Word_Lib: theory Word_Lib.Type_Syntax
10:59:31Word_Lib: theory Word_Lib.Word_Syntax
10:59:31Word_Lib: theory Word_Lib.Norm_Words
10:59:31Word_Lib: theory Word_Lib.Word_Names
10:59:32BD_Security_Compositional: theory BD_Security_Compositional.Composing_Security_Network
10:59:33Word_Lib: theory Word_Lib.Enumeration_Word
10:59:33Word_Lib: theory Word_Lib.Sgn_Abs
10:59:33Automatic_Refinement: theory Automatic_Refinement.Param_Chapter
10:59:33Automatic_Refinement: theory Automatic_Refinement.Relators
10:59:35LEM: theory Word_Lib.Bit_Shifts_Infix_Syntax
10:59:35LEM: theory Word_Lib.Least_significant_bit
10:59:35HOL-Analysis: theory HOL-Library.Equipollence
10:59:35Word_Lib: theory Word_Lib.Rsplit
10:59:35Word_Lib: theory Word_Lib.Word_16
10:59:35Word_Lib: theory Word_Lib.Reversed_Bit_Lists
10:59:37LEM: theory Word_Lib.Aligned
10:59:37LEM: theory Word_Lib.Singleton_Bit_Shifts
10:59:37LEM: theory Word_Lib.Most_significant_bit
10:59:38Simpl: theory Simpl.HoarePartialDef
10:59:38Automatic_Refinement: theory Automatic_Refinement.Param_Tool
10:59:39LEM: theory Word_Lib.Generic_set_bit
10:59:39Simpl: theory Simpl.HoarePartialProps
10:59:40Automatic_Refinement: theory Automatic_Refinement.Param_HOL
10:59:40LEM: theory Word_Lib.Bits_Int
10:59:41HOL-Library: theory HOL-Library.Code_Target_Int
10:59:43HOL-Library: theory HOL-Library.Code_Target_Numeral
10:59:43Automatic_Refinement: theory Automatic_Refinement.Parametricity
10:59:43Automatic_Refinement: theory Automatic_Refinement.Autoref_Data
10:59:43Automatic_Refinement: theory Automatic_Refinement.Autoref_Phases
10:59:43Automatic_Refinement: theory Automatic_Refinement.Autoref_Tagging
10:59:43Word_Lib: theory HOL-Eisbach.Eisbach_Tools
10:59:43HOL-Analysis: theory HOL-Library.Set_Idioms
10:59:43Word_Lib: theory Word_Lib.Word_EqI
10:59:43HOL-Library: theory HOL-Library.Code_Test
10:59:45LEM: theory LEM.Lem_set_helpers
10:59:45Simpl: theory Simpl.HoarePartial
10:59:46Automatic_Refinement: theory Automatic_Refinement.Autoref_Id_Ops
10:59:46Simpl: theory Simpl.Termination
10:59:48Automatic_Refinement: theory Automatic_Refinement.Autoref_Fix_Rel
10:59:48HOL-Analysis: theory HOL-Analysis.Abstract_Topology
10:59:50LEM: theory Word_Lib.Typedef_Morphisms
10:59:50HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring
10:59:51LEM: theory Word_Lib.Reversed_Bit_Lists
10:59:51Automatic_Refinement: theory Automatic_Refinement.Autoref_Translate
10:59:51Automatic_Refinement: theory Automatic_Refinement.Autoref_Relator_Interface
10:59:51Word_Lib: theory Word_Lib.Bitwise
10:59:52Automatic_Refinement: theory Automatic_Refinement.Autoref_Gen_Algo
10:59:52Automatic_Refinement: theory Automatic_Refinement.Autoref_Chapter
10:59:52Automatic_Refinement: theory Automatic_Refinement.Autoref_Tool
10:59:53Automatic_Refinement: theory Automatic_Refinement.Autoref_Bindings_HOL
10:59:53Word_Lib: theory Word_Lib.Bitwise_Signed
10:59:53Word_Lib: theory Word_Lib.Boolean_Inequalities
10:59:54Word_Lib: theory Word_Lib.Word_Lemmas
10:59:56Automatic_Refinement: theory Automatic_Refinement.Automatic_Refinement
10:59:56Simpl: theory Simpl.HoareTotalDef
10:59:57Simpl: theory Simpl.SmallStep
10:59:58LEM: theory LEM.Lem
10:59:58Simpl: theory Simpl.AlternativeSmallStep
10:59:58LEM: theory LEM.Lem_assert_extra
10:59:58LEM: theory LEM.Lem_function_extra
10:59:58LEM: theory LEM.Lem_maybe_extra
10:59:58LEM: theory LEM.Lem_list
10:59:59Word_Lib: theory Word_Lib.Word_8
10:59:59Word_Lib: theory Word_Lib.More_Word_Operations
11:00:00LEM: theory LEM.Lem_either
11:00:00LEM: theory LEM.Lem_list_extra
11:00:00LEM: theory LEM.Lem_string
11:00:00LEM: theory LEM.Lem_word
11:00:00LEM: theory LEM.Lem_num_extra
11:00:00LEM: theory LEM.Lem_show
11:00:00Word_Lib: theory Word_Lib.Word_32
11:00:00Word_Lib: theory Word_Lib.Word_64
11:00:00LEM: theory LEM.Lem_machine_word
11:00:01LEM: theory LEM.Lem_string_extra
11:00:01HOL-Library: theory HOL-Library.Combine_PER
11:00:01LEM: theory LEM.Lem_set
11:00:01HOL-Library: theory HOL-Library.DAList_Multiset
11:00:01HOL-Library: theory HOL-Library.Multiset_Order
11:00:01Word_Lib: theory Word_Lib.Machine_Word_32_Basics
11:00:01LEM: theory LEM.Lem_map
11:00:01Word_Lib: theory Word_Lib.Machine_Word_32
11:00:01Word_Lib: theory Word_Lib.Word_Lib_Sumo
11:00:01Word_Lib: theory Word_Lib.Machine_Word_64_Basics
11:00:01LEM: theory LEM.Lem_map_extra
11:00:01LEM: theory LEM.Lem_relation
11:00:01Word_Lib: theory Word_Lib.Machine_Word_64
11:00:02LEM: theory LEM.Lem_sorting
11:00:02Word_Lib: theory Word_Lib.Guide
11:00:02HOL-Library: theory HOL-Library.Comparator
11:00:02LEM: theory LEM.Lem_set_extra
11:00:02Simpl: theory Simpl.HoareTotalProps
11:00:02LEM: theory LEM.Lem_show_extra
11:00:04LEM: theory LEM.Lem_pervasives
11:00:04HOL-Library: theory HOL-Library.Complete_Partial_Order2
11:00:04HOL-Library: theory HOL-Library.Conditional_Parametricity
11:00:05LEM: theory LEM.Lem_pervasives_extra
11:00:05HOL-Analysis: theory HOL-Combinatorics.Permutations
11:00:05Word_Lib: theory Word_Lib.Examples
11:00:06HOL-Library: theory HOL-Library.Confluence
11:00:07HOL-Library: theory HOL-Library.Datatype_Records
11:00:07HOL-Library: theory HOL-Library.Confluent_Quotient
11:00:08HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable
11:00:08HOL-Library: theory HOL-Library.Dlist
11:00:08Simpl: theory Simpl.Compose
11:00:09Simpl: theory Simpl.HoareTotal
11:00:10HOL-Library: theory HOL-Library.Debug
11:00:10HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
11:00:10Preparing Automatic_Refinement/document ...
11:00:11HOL-Analysis: theory HOL-Analysis.Inner_Product
11:00:11HOL-Library: theory HOL-Library.Fun_Lexorder
11:00:11HOL-Library: theory HOL-Library.FuncSet
11:00:11HOL-Library: theory HOL-Library.Function_Algebras
11:00:11HOL-Analysis: theory HOL-Analysis.L2_Norm
11:00:12HOL-Analysis: theory HOL-Analysis.Operator_Norm
11:00:12HOL-Library: theory HOL-Library.Function_Division
11:00:13HOL-Analysis: theory HOL-Analysis.Poly_Roots
11:00:13HOL-Library: theory HOL-Library.Groups_Big_Fun
11:00:13Preparing ZFC_in_HOL/document ...
11:00:13HOL-Analysis: theory HOL-Analysis.Product_Vector
11:00:15Finished Automatic_Refinement/document (0:00:04 elapsed time)
11:00:15Preparing Automatic_Refinement/outline ...
11:00:15HOL-Library: theory HOL-Library.Disjoint_Sets
11:00:15HOL-Library: theory HOL-Library.IArray
11:00:16HOL-Library: theory HOL-Library.Infinite_Set
11:00:16HOL-Analysis: theory HOL-Analysis.Abstract_Limits
11:00:16HOL-Analysis: theory HOL-Analysis.FSigma
11:00:17HOL-Analysis: theory HOL-Analysis.Sum_Topology
11:00:17HOL-Library: theory HOL-Library.Omega_Words_Fun
11:00:17HOL-Analysis: theory HOL-Library.Complex_Order
11:00:17HOL-Analysis: theory HOL-Library.Discrete
11:00:17HOL-Analysis: theory HOL-Library.Indicator_Function
11:00:17HOL-Library: theory HOL-Library.LaTeXsugar
11:00:17Simpl: theory Simpl.Hoare
11:00:18HOL-Library: theory HOL-Library.Lattice_Constructions
11:00:18HOL-Library: theory HOL-Library.ListVector
11:00:18HOL-Analysis: theory HOL-Library.Landau_Symbols
11:00:18Simpl: theory Simpl.Closure
11:00:18Simpl: theory Simpl.StateSpace
11:00:19HOL-Library: theory HOL-Library.List_Lenlexorder
11:00:19Finished Automatic_Refinement/outline (0:00:03 elapsed time)
11:00:19HOL-Library: theory HOL-Library.List_Lexorder
11:00:19HOL-Library: theory HOL-Library.Mapping
11:00:19HOL-Analysis: theory HOL-Library.Liminf_Limsup
11:00:19HOL-Analysis: theory HOL-Analysis.Elementary_Topology
11:00:19Timing Automatic_Refinement (4 threads, 52.354s elapsed time, 153.585s cpu time, 4.907s GC time, factor 2.93)
11:00:19Finished Automatic_Refinement (0:01:48 elapsed time, 0:02:59 cpu time, factor 1.65)
11:00:19HOL-Library: theory HOL-Library.More_List
11:00:19Building Refine_Monadic ...
11:00:20Simpl: theory Simpl.Vcg
11:00:20HOL-Library: theory HOL-Library.Poly_Mapping
11:00:21HOL-Analysis: theory HOL-Analysis.Euclidean_Space
11:00:21Refine_Monadic: theory HOL-Library.Phantom_Type
11:00:21Refine_Monadic: theory Refine_Monadic.Example_Chapter
11:00:21Refine_Monadic: theory HOL-Library.Adhoc_Overloading
11:00:21Refine_Monadic: theory HOL-Library.While_Combinator
11:00:21Refine_Monadic: theory Refine_Monadic.Refine_Chapter
11:00:21Refine_Monadic: theory Refine_Monadic.Refine_Mono_Prover
11:00:22HOL-Library: theory HOL-Library.AList_Mapping
11:00:22Refine_Monadic: theory HOL-Library.Monad_Syntax
11:00:23HOL-Library: theory HOL-Library.NList
11:00:23Refine_Monadic: theory Refine_Monadic.Refine_Misc
11:00:23HOL-Library: theory HOL-Library.Nat_Bijection
11:00:23Refine_Monadic: theory HOL-Library.Cardinality
11:00:24HOL-Library: theory HOL-Library.Old_Datatype
11:00:24HOL-Library: theory HOL-Library.Old_Recdef
11:00:24Refine_Monadic: theory Refine_Monadic.RefineG_Domain
11:00:25Refine_Monadic: theory Refine_Monadic.RefineG_Transfer
11:00:26Preparing Word_Lib/document ...
11:00:26Refine_Monadic: theory Refine_Monadic.RefineG_Assert
11:00:26Refine_Monadic: theory HOL-Library.Numeral_Type
11:00:27Finished ZFC_in_HOL/document (0:00:13 elapsed time)
11:00:27Preparing ZFC_in_HOL/outline ...
11:00:27HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2
11:00:27HOL-Library: theory HOL-Library.Stream
11:00:27Refine_Monadic: theory Refine_Monadic.RefineG_Recursion
11:00:27HOL-Analysis: theory HOL-Library.Nonpos_Ints
11:00:27HOL-Library: theory HOL-Library.Open_State_Syntax
11:00:27HOL-Library: theory HOL-Library.Option_ord
11:00:28HOL-Analysis: theory HOL-Library.Order_Continuity
11:00:28HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product
11:00:28HOL-Library: theory HOL-Library.Parallel
11:00:28Refine_Monadic: theory Refine_Monadic.RefineG_While
11:00:28Refine_Monadic: theory HOL-Library.Type_Length
11:00:28Refine_Monadic: theory Refine_Monadic.Refine_Basic
11:00:29HOL-Analysis: theory HOL-Analysis.Linear_Algebra
11:00:29Refine_Monadic: theory Refine_Monadic.Refine_Det
11:00:29Refine_Monadic: theory HOL-Library.Word
11:00:30HOL-Analysis: theory HOL-Analysis.Connected
11:00:33HOL-Library: theory HOL-Library.Pattern_Aliases
11:00:33HOL-Library: theory HOL-Library.Phantom_Type
11:00:33HOL-Analysis: theory HOL-Analysis.Function_Topology
11:00:34Finished ZFC_in_HOL/outline (0:00:06 elapsed time)
11:00:34HOL-Analysis: theory HOL-Analysis.Affine
11:00:34Timing ZFC_in_HOL (4 threads, 92.818s elapsed time, 310.023s cpu time, 5.187s GC time, factor 3.34)
11:00:34Finished ZFC_in_HOL (0:01:51 elapsed time, 0:05:37 cpu time, factor 3.03)
11:00:34Building CZH_Foundations ...
11:00:35HOL-Analysis: theory HOL-Analysis.Cartesian_Space
11:00:35Refine_Monadic: theory Refine_Monadic.Refine_Heuristics
11:00:35Refine_Monadic: theory Refine_Monadic.Refine_Leof
11:00:35Refine_Monadic: theory Refine_Monadic.Refine_Pfun
11:00:35Refine_Monadic: theory Refine_Monadic.Refine_While
11:00:35Refine_Monadic: theory Refine_Monadic.Refine_More_Comb
11:00:35HOL-Library: theory HOL-Library.Power_By_Squaring
11:00:35Simpl: theory Simpl.ProcParEx
11:00:35HOL-Analysis: theory HOL-Analysis.Convex
11:00:35HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
11:00:35Simpl: theory Simpl.ProcParExSP
11:00:35HOL-Library: theory HOL-Library.Preorder
11:00:35Simpl: theory Simpl.XVcg
11:00:35Simpl: theory Simpl.ClosureEx
11:00:35Simpl: theory Simpl.XVcgEx
11:00:36Simpl: theory Simpl.ComposeEx
11:00:36HOL-Library: theory HOL-Library.Cardinality
11:00:36CZH_Foundations: theory CZH_Foundations.CZH_Utilities
11:00:36CZH_Foundations: theory CZH_Foundations.CZH_Sets_MIF
11:00:36HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
11:00:36HOL-Analysis: theory HOL-Analysis.Product_Topology
11:00:36CZH_Foundations: theory HOL-Eisbach.Eisbach
11:00:36CZH_Foundations: theory Conditional_Simplification.CS_Tools
11:00:36CZH_Foundations: theory Cardinality_Continuum.Cardinality_Continuum_Library
11:00:36CZH_Foundations: theory HOL-Library.Rewrite
11:00:36Simpl: theory Simpl.Quicksort
11:00:36Simpl: theory Simpl.SyntaxTest
11:00:36CZH_Foundations: theory Conditional_Simplification.IHOL_CS
11:00:36Simpl: theory Simpl.UserGuide
11:00:36HOL-Library: theory HOL-Library.Product_Lexorder
11:00:37Simpl: theory Simpl.VcgEx
11:00:37Simpl: theory Simpl.VcgExSP
11:00:37Simpl: theory Simpl.VcgExTotal
11:00:37HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm
11:00:37HOL-Analysis: theory HOL-Analysis.T1_Spaces
11:00:38Finished Word_Lib/document (0:00:11 elapsed time)
11:00:38Preparing Word_Lib/outline ...
11:00:39HOL-Library: theory HOL-Library.Product_Plus
11:00:39Refine_Monadic: theory Refine_Monadic.Refine_Transfer
11:00:39HOL-Library: theory HOL-Library.Quotient_Syntax
11:00:39HOL-Library: theory HOL-Library.Product_Order
11:00:39HOL-Library: theory HOL-Library.Quotient_Option
11:00:39Refine_Monadic: theory Refine_Monadic.Autoref_Monadic
11:00:39HOL-Library: theory HOL-Library.Quotient_Product
11:00:39Refine_Monadic: theory Refine_Monadic.Refine_Automation
11:00:40HOL-Library: theory HOL-Library.Quotient_Set
11:00:40HOL-Library: theory HOL-Library.Finite_Lattice
11:00:40HOL-Library: theory HOL-Library.Quotient_List
11:00:40HOL-Library: theory HOL-Library.Code_Cardinality
11:00:40Refine_Monadic: theory Refine_Monadic.Refine_Foreach
11:00:40HOL-Library: theory HOL-Library.Numeral_Type
11:00:40HOL-Library: theory HOL-Library.Quotient_Sum
11:00:40HOL-Analysis: theory HOL-Analysis.Lindelof_Spaces
11:00:41HOL-Library: theory HOL-Library.Quotient_Type
11:00:41HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces
11:00:41HOL-Library: theory HOL-Library.RBT_Impl
11:00:41Simpl: theory Simpl.Simpl
11:00:42HOL-Library: theory HOL-Library.Type_Length
11:00:42CZH_Foundations: theory CZH_Foundations.CZH_Introduction
11:00:42HOL-Library: theory HOL-Library.Saturated
11:00:42HOL-Analysis: theory HOL-Library.Extended_Nat
11:00:42HOL-Library: theory HOL-Library.Word
11:00:43CZH_Foundations: theory Cardinality_Continuum.Cardinality_Continuum
11:00:43CZH_Foundations: theory Intro_Dest_Elim.IHOL_IDE
11:00:43HOL-Analysis: theory HOL-Analysis.Determinants
11:00:43HOL-Library: theory HOL-Library.Realizers
11:00:46Finished Word_Lib/outline (0:00:08 elapsed time)
11:00:46HOL-Analysis: theory HOL-Library.Extended_Real
11:00:46Timing Word_Lib (4 threads, 105.290s elapsed time, 344.801s cpu time, 8.234s GC time, factor 3.27)
11:00:46Finished Word_Lib (0:02:04 elapsed time, 0:06:16 cpu time, factor 3.03)
11:00:47Running CoCon ...
11:00:47Refine_Monadic: theory Refine_Monadic.Refine_Monadic
11:00:47CZH_Foundations: theory CZH_Foundations.CZH_Sets_Introduction
11:00:48HOL-Library: theory HOL-Library.Reflection
11:00:48HOL-Library: theory HOL-Library.Refute
11:00:48CoCon: theory Fresh_Identifiers.Fresh
11:00:49HOL-Analysis: theory HOL-Library.Periodic_Fun
11:00:49CZH_Foundations: theory CZH_Foundations.CZH_Sets_Sets
11:00:49CoCon: theory Fresh_Identifiers.Fresh_String
11:00:49Timing LEM (4 threads, 120.686s elapsed time, 369.152s cpu time, 11.311s GC time, factor 3.06)
11:00:49Finished LEM (0:02:26 elapsed time, 0:06:55 cpu time, factor 2.84)
11:00:49Building CakeML ...
11:00:50CoCon: theory CoCon.Prelim
11:00:50Refine_Monadic: theory Refine_Monadic.Breadth_First_Search
11:00:50HOL-Analysis: theory HOL-Library.Sum_of_Squares
11:00:51HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces
11:00:51CZH_Foundations: theory CZH_Foundations.CZH_Sets_BRelations
11:00:52CakeML: theory HOL-Eisbach.Eisbach
11:00:52CakeML: theory CakeML.Doc_Generated
11:00:52CakeML: theory CakeML.Doc_Proofs
11:00:52CakeML: theory Deriving.Derive_Manager
11:00:52CakeML: theory Deriving.Generator_Aux
11:00:52CakeML: theory HOL-Library.Case_Converter
11:00:52Refine_Monadic: theory Refine_Monadic.WordRefine
11:00:53Refine_Monadic: theory Refine_Monadic.Examples
11:00:53CakeML: theory HOL-Library.Complete_Partial_Order2
11:00:56HOL-Analysis: theory HOL-Analysis.Function_Metric
11:00:56Preparing BD_Security_Compositional/document ...
11:00:56CZH_Foundations: theory CZH_Foundations.CZH_Sets_IF
11:00:57HOL-Library: theory HOL-Library.Rewrite
11:00:57HOL-Analysis: theory HOL-Analysis.Isolated
11:00:57CakeML: theory HOL-Library.Datatype_Records
11:00:58CZH_Foundations: theory CZH_Foundations.CZH_Sets_Equipollence
11:00:58CZH_Foundations: theory CZH_Foundations.CZH_Sets_Nat
11:00:58CZH_Foundations: theory CZH_Foundations.CZH_Sets_Cardinality
11:00:58HOL-Analysis: theory HOL-Real_Asymp.Eventuallize
11:00:58CZH_Foundations: theory CZH_Foundations.CZH_Sets_FSequences
11:00:58HOL-Analysis: theory HOL-Real_Asymp.Lazy_Eval
11:00:59HOL-Library: theory HOL-Library.Set_Algebras
11:01:00CakeML: theory HOL-Library.Simps_Case_Conv
11:01:00CoCon: theory CoCon.System_Specification
11:01:00CZH_Foundations: theory CZH_Foundations.CZH_Sets_FBRelations
11:01:01HOL-Library: theory HOL-Library.Signed_Division
11:01:01CakeML: theory HOL-Library.Infinite_Set
11:01:01HOL-Library: theory HOL-Library.Sorting_Algorithms
11:01:02HOL-Library: theory HOL-Library.Sublist
11:01:03Finished BD_Security_Compositional/document (0:00:06 elapsed time)
11:01:03Preparing BD_Security_Compositional/outline ...
11:01:03CZH_Foundations: theory CZH_Foundations.CZH_Sets_NOP
11:01:04CZH_Foundations: theory CZH_Foundations.CZH_Sets_Ordinals
11:01:04CZH_Foundations: theory CZH_Foundations.CZH_Sets_VNHS
11:01:04HOL-Analysis: theory HOL-Real_Asymp.Multiseries_Expansion
11:01:04HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real
11:01:05CZH_Foundations: theory CZH_Foundations.CZH_DG_Introduction
11:01:05CZH_Foundations: theory CZH_Foundations.CZH_DG_Digraph
11:01:06CZH_Foundations: theory CZH_Foundations.CZH_DG_DGHM
11:01:06HOL-Library: theory HOL-Library.Prefix_Order
11:01:06CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_Digraph
11:01:06CakeML: theory HOL-Library.Nat_Bijection
11:01:06HOL-Library: theory HOL-Library.Subseq_Order
11:01:06CakeML: theory HOL-Eisbach.Eisbach_Tools
11:01:07HOL-Library: theory HOL-Library.Transitive_Closure_Table
11:01:07CZH_Foundations: theory CZH_Foundations.CZH_SMC_Introduction
11:01:07HOL-Analysis: theory HOL-Analysis.Norm_Arith
11:01:07CakeML: theory HOL-Library.Old_Datatype
11:01:07CZH_Foundations: theory CZH_Foundations.CZH_Sets_ZQR
11:01:07CakeML: theory Word_Lib.Signed_Words
11:01:08Finished BD_Security_Compositional/outline (0:00:04 elapsed time)
11:01:08HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space
11:01:08Timing BD_Security_Compositional (4 threads, 79.173s elapsed time, 252.789s cpu time, 6.425s GC time, factor 3.19)
11:01:08Finished BD_Security_Compositional (0:01:40 elapsed time, 0:04:48 cpu time, factor 2.87)
11:01:08HOL-Library: theory HOL-Library.Tree
11:01:08Running CoSMeDis ...
11:01:08CakeML: theory Word_Lib.Word_Names
11:01:08CZH_Foundations: theory CZH_Foundations.CZH_SMC_Semicategory
11:01:08CakeML: theory Word_Lib.Type_Syntax
11:01:10CakeML: theory Word_Lib.Word_Syntax
11:01:10CoSMeDis: theory Fresh_Identifiers.Fresh
11:01:10CakeML: theory HOL-Library.Signed_Division
11:01:11CoSMeDis: theory Fresh_Identifiers.Fresh_String
11:01:12CoSMeDis: theory CoSMeDis.Prelim
11:01:12HOL-Library: theory HOL-Library.Uprod
11:01:12CakeML: theory HOL-Library.Countable
11:01:12CakeML: theory HOL-Library.Lattice_Algebras
11:01:13HOL-Library: theory HOL-Library.While_Combinator
11:01:13HOL-Analysis: theory HOL-Analysis.Infinite_Sum
11:01:14HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
11:01:15CakeML: theory Word_Lib.Signed_Division_Word
11:01:15HOL-Library: theory HOL-Library.Z2
11:01:15HOL-Library: theory HOL-Library.Tree_Multiset
11:01:15HOL-Library: theory HOL-Library.Countable
11:01:15HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
11:01:16HOL-Library: theory HOL-Library.Complex_Order
11:01:16HOL-Library: theory HOL-Library.Diagonal_Subsequence
11:01:16CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_Semicategory
11:01:16HOL-Library: theory HOL-Library.Discrete
11:01:16CakeML: theory HOL-Library.Log_Nat
11:01:16HOL-Analysis: theory HOL-Analysis.Sigma_Algebra
11:01:18CakeML: theory Show.Show
11:01:18CakeML: theory HOL-Library.Countable_Set
11:01:18HOL-Library: theory HOL-Library.Going_To_Filter
11:01:18HOL-Library: theory HOL-Library.Countable_Set
11:01:18CZH_Foundations: theory CZH_Foundations.CZH_EX_Replacement
11:01:18HOL-Library: theory HOL-Library.FSet
11:01:18CZH_Foundations: theory CZH_Foundations.CZH_EX_TS
11:01:19CZH_Foundations: theory CZH_Foundations.CZH_EX_Algebra
11:01:19CakeML: theory HOL-Library.Countable_Complete_Lattices
11:01:19HOL-Library: theory HOL-Library.Countable_Complete_Lattices
11:01:20CakeML: theory Word_Lib.Enumeration
11:01:21CoSMeDis: theory CoSMeDis.System_Specification
11:01:21HOL-Analysis: theory HOL-Analysis.Measurable
11:01:21CakeML: theory Show.Show_Instances
11:01:22CakeML: theory Word_Lib.Enumeration_Word
11:01:22CZH_Foundations: theory CZH_Foundations.CZH_Sets_Conclusions
11:01:23CakeML: theory Word_Lib.Many_More
11:01:23CakeML: theory Word_Lib.Rsplit
11:01:23HOL-Library: theory HOL-Library.Countable_Set_Type
11:01:23HOL-Analysis: theory HOL-Analysis.Measure_Space
11:01:23CakeML: theory Word_Lib.Word_EqI
11:01:25CZH_Foundations: theory CZH_Foundations.CZH_DG_TDGHM
11:01:25CakeML: theory Word_Lib.More_Misc
11:01:25CakeML: theory CakeML.Namespace
11:01:25HOL-Library: theory HOL-Library.Equipollence
11:01:25CakeML: theory HOL-Library.Order_Continuity
11:01:25CZH_Foundations: theory CZH_Foundations.CZH_DG_GRPH
11:01:25CZH_Foundations: theory CZH_Foundations.CZH_DG_Subdigraph
11:01:25CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_DGHM
11:01:26CakeML: theory HOL-Library.Extended_Nat
11:01:26CakeML: theory HOL-Library.Float
11:01:26HOL-Library: theory HOL-Library.Ramsey
11:01:26CakeML: theory Word_Lib.Boolean_Inequalities
11:01:27CZH_Foundations: theory CZH_Foundations.CZH_SMC_Semifunctor
11:01:27CakeML: theory Coinductive.Coinductive_Nat
11:01:27HOL-Library: theory HOL-Library.Set_Idioms
11:01:28HOL-Analysis: theory HOL-Computational_Algebra.Primes
11:01:28CoCon: theory CoCon.Automation_Setup
11:01:28CoCon: theory CoCon.Safety_Properties
11:01:29HOL-Library: theory HOL-Library.Finite_Map
11:01:29HOL-Library: theory HOL-Library.Indicator_Function
11:01:30HOL-Library: theory HOL-Library.Infinite_Typeclass
11:01:30HOL-Library: theory HOL-Library.Landau_Symbols
11:01:30HOL-Library: theory HOL-Library.Lattice_Algebras
11:01:30CZH_Foundations: theory CZH_Foundations.CZH_DG_Rel
11:01:31CakeML: theory Coinductive.Coinductive_List
11:01:32HOL-Analysis: theory HOL-Analysis.Caratheodory
11:01:32CakeML: theory CakeML.Tokens
11:01:33CoCon: theory CoCon.Decision_Intro
11:01:33CoCon: theory CoCon.Decision_Value_Setup
11:01:33CakeML: theory Word_Lib.Word_Lemmas
11:01:33CoCon: theory CoCon.Discussion_Intro
11:01:33CoCon: theory CoCon.Observation_Setup
11:01:33CoCon: theory CoCon.Discussion_Value_Setup
11:01:33CakeML: theory CakeML.NamespaceAuxiliary
11:01:33HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits
11:01:33CoCon: theory CoCon.Paper_Intro
11:01:34CoCon: theory CoCon.Paper_Value_Setup
11:01:34CoCon: theory CoCon.Review_Intro
11:01:34CoCon: theory CoCon.Review_Value_Setup
11:01:35HOL-Analysis: theory HOL-Analysis.Summation_Tests
11:01:36CoCon: theory CoCon.Discussion_NCPC
11:01:36CoCon: theory CoCon.Decision_NCPC
11:01:36HOL-Analysis: theory HOL-Analysis.Line_Segment
11:01:36CZH_Foundations: theory CZH_Foundations.CZH_DG_Par
11:01:37CZH_Foundations: theory CZH_Foundations.CZH_DG_Simple
11:01:37CoCon: theory CoCon.Decision_NCPC_Aut
11:01:37CZH_Foundations: theory CZH_Foundations.CZH_DG_PDigraph
11:01:37CZH_Foundations: theory CZH_Foundations.CZH_DG_Small_TDGHM
11:01:37CoCon: theory CoCon.Discussion_All
11:01:37CoCon: theory CoCon.Paper_Aut
11:01:37CoCon: theory CoCon.Paper_Aut_PC
11:01:39CZH_Foundations: theory CZH_Foundations.CZH_DG_Set
11:01:39HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space
11:01:39CoCon: theory CoCon.Review_RAut
11:01:40CoCon: theory CoCon.Review_RAut_NCPC
11:01:41CZH_Foundations: theory CZH_Foundations.CZH_SMC_GRPH
11:01:41HOL-Library: theory HOL-Library.Liminf_Limsup
11:01:41CoCon: theory CoCon.Decision_All
11:01:41CakeML: theory IEEE_Floating_Point.IEEE
11:01:41CoCon: theory CoCon.Paper_All
11:01:41CoCon: theory CoCon.Review_RAut_NCPC_PAut
11:01:42CoCon: theory CoCon.Reviewer_Assignment_Intro
11:01:42CoCon: theory CoCon.Reviewer_Assignment_Value_Setup
11:01:42HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space
11:01:42HOL-Library: theory HOL-Library.Log_Nat
11:01:43CakeML: theory Word_Lib.More_Word_Operations
11:01:43HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series
11:01:43HOL-Library: theory HOL-Library.Lub_Glb
11:01:43HOL-Library: theory HOL-Library.Nonpos_Ints
11:01:44HOL-Library: theory HOL-Library.OptionalSugar
11:01:44HOL-Library: theory HOL-Library.Order_Continuity
11:01:45CoCon: theory CoCon.Traceback_Properties
11:01:45HOL-Library: theory HOL-Library.Extended_Nat
11:01:45Preparing Refine_Monadic/document ...
11:01:45HOL-Analysis: theory HOL-Analysis.Starlike
11:01:46CZH_Foundations: theory CZH_Foundations.CZH_DG_Conclusions
11:01:46HOL-Library: theory HOL-Library.Interval
11:01:47HOL-Library: theory HOL-Library.Float
11:01:47CoCon: theory CoCon.Review_All
11:01:47CoCon: theory CoCon.Reviewer_Assignment_NCPC
11:01:47CoCon: theory CoCon.Reviewer_Assignment_NCPC_Aut
11:01:48CakeML: theory Word_Lib.Word_64
11:01:50CoCon: theory CoCon.Reviewer_Assignment_All
11:01:50CoSMeDis: theory CoSMeDis.API_Network
11:01:50CoSMeDis: theory CoSMeDis.Automation_Setup
11:01:50CoSMeDis: theory CoSMeDis.Safety_Properties
11:01:51HOL-Library: theory HOL-Library.Extended_Real
11:01:51CoSMeDis: theory CoSMeDis.Friend_Intro
11:01:51CoSMeDis: theory CoSMeDis.Friend_Observation_Setup
11:01:51CoSMeDis: theory CoSMeDis.Friend_State_Indistinguishability
11:01:51HOL-Library: theory HOL-Library.Code_Target_Numeral_Float
11:01:51HOL-Library: theory HOL-Library.Interval_Float
11:01:52CakeML: theory IEEE_Floating_Point.FP64
11:01:52CoSMeDis: theory CoSMeDis.Friend_Openness
11:01:52CZH_Foundations: theory CZH_Foundations.CZH_DG_SemiCAT
11:01:53CakeML: theory CakeML.Lib
11:01:53CoSMeDis: theory CoSMeDis.Friend_Value_Setup
11:01:53CoSMeDis: theory CoSMeDis.Friend_Request_Intro
11:01:53CoSMeDis: theory CoSMeDis.Friend_Request_Value_Setup
11:01:53HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
11:01:53CZH_Foundations: theory CZH_Foundations.CZH_SMC_NTSMCF
11:01:53CZH_Foundations: theory CZH_Foundations.CZH_SMC_Subsemicategory
11:01:54CZH_Foundations: theory CZH_Foundations.CZH_SMC_PSemicategory
11:01:54CakeML: theory CakeML.LibAuxiliary
11:01:54CakeML: theory CakeML.Ffi
11:01:54CakeML: theory CakeML.FpSem
11:01:54CakeML: theory CakeML.Ast
11:01:54CakeML: theory CakeML.SimpleIO
11:01:55CoSMeDis: theory CoSMeDis.Outer_Friend_Intro
11:01:55CoSMeDis: theory CoSMeDis.Outer_Friend
11:01:56CoSMeDis: theory CoSMeDis.Friend
11:01:56CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_Observation_Setup
11:01:58CoSMeDis: theory CoSMeDis.Friend_Request
11:01:58HOL-Analysis: theory HOL-Analysis.Continuous_Extension
11:01:58CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver_Observation_Setup
11:01:58Timing HOL-Proofs (4 threads, 564.463s elapsed time, 938.444s cpu time, 137.652s GC time, factor 1.66)
11:01:58Finished HOL-Proofs (0:12:20 elapsed time, 0:21:27 cpu time, factor 1.74)
11:01:58Running X86_Semantics ...
11:01:59HOL-Library: theory HOL-Library.Periodic_Fun
11:01:59CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_State_Indistinguishability
11:01:59HOL-Analysis: theory HOL-Analysis.Path_Connected
11:01:59CakeML: theory CakeML.CakeML_Compiler
11:01:59CakeML: theory CakeML.AstAuxiliary
11:01:59CakeML: theory CakeML.SemanticPrimitives
11:01:59HOL-Library: theory HOL-Library.Quadratic_Discriminant
11:01:59HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
11:02:00HOL-Library: theory HOL-Library.Real_Mod
11:02:00CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_Openness
11:02:00CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer_Value_Setup
11:02:00HOL-Library: theory HOL-Library.Sum_of_Squares
11:02:00CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver_State_Indistinguishability
11:02:00X86_Semantics: theory HOL-Eisbach.Eisbach
11:02:00X86_Semantics: theory HOL-Library.Phantom_Type
11:02:00X86_Semantics: theory Word_Lib.Even_More_List
11:02:00X86_Semantics: theory HOL-Library.Sublist
11:02:01Finished Refine_Monadic/document (0:00:15 elapsed time)
11:02:01Preparing Refine_Monadic/outline ...
11:02:02X86_Semantics: theory Word_Lib.More_Bit_Ring
11:02:02CoSMeDis: theory CoSMeDis.Post_Intro
11:02:03CoSMeDis: theory CoSMeDis.Post_Observation_Setup_ISSUER
11:02:03CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver_Value_Setup
11:02:03HOL-Analysis: theory HOL-Analysis.Tagged_Division
11:02:04CoSMeDis: theory CoSMeDis.Independent_Post_Observation_Setup_ISSUER
11:02:04CoSMeDis: theory CoSMeDis.Friend_Network
11:02:04CoSMeDis: theory CoSMeDis.Friend_Request_Network
11:02:04HOL-Library: theory HOL-Library.Tree_Real
11:02:05CoSMeDis: theory CoSMeDis.Outer_Friend_Issuer
11:02:05CoSMeDis: theory CoSMeDis.Outer_Friend_Receiver
11:02:06CoSMeDis: theory CoSMeDis.Post_Unwinding_Helper_ISSUER
11:02:09CoSMeDis: theory CoSMeDis.Outer_Friend_Network
11:02:09CZH_Foundations: theory CZH_Foundations.CZH_SMC_Rel
11:02:09CZH_Foundations: theory CZH_Foundations.CZH_SMC_Simple
11:02:09CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_Semifunctor
11:02:09CoSMeDis: theory CoSMeDis.DYNAMIC_Post_Value_Setup_ISSUER
11:02:10CoSMeDis: theory CoSMeDis.Friend_All
11:02:10CoSMeDis: theory CoSMeDis.Independent_DYNAMIC_Post_Value_Setup_ISSUER
11:02:10CZH_Foundations: theory CZH_Foundations.CZH_SMC_Par
11:02:11CZH_Foundations: theory CZH_Foundations.CZH_SMC_SemiCAT
11:02:11CoSMeDis: theory CoSMeDis.Friend_Request_All
11:02:11CoSMeDis: theory CoSMeDis.Post_Observation_Setup_RECEIVER
11:02:11X86_Semantics: theory HOL-Library.Cardinality
11:02:13CoSMeDis: theory CoSMeDis.Independent_Post_Observation_Setup_RECEIVER
11:02:13CZH_Foundations: theory CZH_Foundations.CZH_SMC_Set
11:02:13X86_Semantics: theory HOL-Library.Numeral_Type
11:02:13Finished Refine_Monadic/outline (0:00:12 elapsed time)
11:02:13Timing Refine_Monadic (4 threads, 66.980s elapsed time, 184.934s cpu time, 4.863s GC time, factor 2.76)
11:02:13Finished Refine_Monadic (0:01:25 elapsed time, 0:03:33 cpu time, factor 2.51)
11:02:13Building Collections ...
11:02:14CoSMeDis: theory CoSMeDis.Outer_Friend_All
11:02:14CoSMeDis: theory CoSMeDis.Post_Unwinding_Helper_RECEIVER
11:02:15CoSMeDis: theory CoSMeDis.Post_Value_Setup_ISSUER
11:02:15Preparing Simpl/document ...
11:02:15CoSMeDis: theory CoSMeDis.Independent_Post_Value_Setup_RECEIVER
11:02:16X86_Semantics: theory HOL-Library.Type_Length
11:02:16X86_Semantics: theory HOL-Library.Word
11:02:16X86_Semantics: theory Word_Lib.More_Arithmetic
11:02:17Collections: theory Collections.ICF_Tools
11:02:17Collections: theory Collections.Partial_Equivalence_Relation
11:02:17Collections: theory Finger-Trees.FingerTree
11:02:17Collections: theory HOL-Library.AList
11:02:17Collections: theory Binomial-Heaps.BinomialHeap
11:02:18HOL-Analysis: theory HOL-Analysis.Arcwise_Connected
11:02:18HOL-Analysis: theory HOL-Analysis.Locally
11:02:18HOL-Library: theory HOL-Library.RBT
11:02:18CoSMeDis: theory CoSMeDis.DYNAMIC_Post_ISSUER
11:02:18Collections: theory Collections.Ord_Code_Preproc
11:02:18HOL-Library: theory HOL-Library.RBT_Mapping
11:02:18CoCon: theory CoCon.All_BD_Security_Instances_for_CoCon
11:02:18CZH_Foundations: theory CZH_Foundations.CZH_SMC_Small_NTSMCF
11:02:18Collections: theory Collections.Locale_Code
11:02:19HOL-Library: theory HOL-Library.RBT_Set
11:02:19HOL-Analysis: theory HOL-Analysis.Uncountable_Sets
11:02:19CoSMeDis: theory CoSMeDis.Independent_Post_RECEIVER
11:02:19HOL-Analysis: theory HOL-Analysis.Homotopy
11:02:19Collections: theory Collections.Record_Intf
11:02:21Collections: theory Binomial-Heaps.SkewBinomialHeap
11:02:23Collections: theory HOL-Library.Code_Abstract_Nat
11:02:23CoSMeDis: theory CoSMeDis.Post_Value_Setup_RECEIVER
11:02:23CoSMeDis: theory CoSMeDis.Independent_DYNAMIC_Post_ISSUER
11:02:23Collections: theory HOL-Library.Code_Target_Nat
11:02:24Collections: theory HOL-Library.Code_Target_Int
11:02:25Collections: theory HOL-Library.Code_Target_Numeral
11:02:25Collections: theory HOL-Library.Confluence
11:02:26Collections: theory HOL-Library.Confluent_Quotient
11:02:26CoSMeDis: theory CoSMeDis.Independent_DYNAMIC_Post_Network
11:02:27CoSMeDis: theory CoSMeDis.Post_ISSUER
11:02:27CoSMeDis: theory CoSMeDis.Post_RECEIVER
11:02:27Collections: theory HOL-Library.Dlist
11:02:28CoSMeDis: theory CoSMeDis.DYNAMIC_Post_COMPOSE2
11:02:30Collections: theory Collections.SetIterator
11:02:30X86_Semantics: theory Word_Lib.Bit_Comprehension
11:02:30X86_Semantics: theory Word_Lib.Legacy_Aliases
11:02:30X86_Semantics: theory Word_Lib.More_Divides
11:02:30X86_Semantics: theory Word_Lib.Syntax_Bundles
11:02:31X86_Semantics: theory Word_Lib.More_Word
11:02:31CoSMeDis: theory CoSMeDis.DYNAMIC_Post_Network
11:02:32CZH_Foundations: theory CZH_Foundations.CZH_SMC_Conclusions
11:02:33CoSMeDis: theory CoSMeDis.Independent_Posts_Network
11:02:33Collections: theory Collections.Sorted_List_Operations
11:02:33CoSMeDis: theory CoSMeDis.Post_COMPOSE2
11:02:34Collections: theory Collections.Idx_Iterator
11:02:35X86_Semantics: theory Word_Lib.Bit_Shifts_Infix_Syntax
11:02:35X86_Semantics: theory Word_Lib.Least_significant_bit
11:02:35Collections: theory Collections.SetAbstractionIterator
11:02:35Collections: theory Collections.SetIteratorOperations
11:02:36X86_Semantics: theory Word_Lib.Aligned
11:02:36X86_Semantics: theory Word_Lib.Singleton_Bit_Shifts
11:02:36X86_Semantics: theory Word_Lib.Most_significant_bit
11:02:38X86_Semantics: theory Word_Lib.Generic_set_bit
11:02:38HOL-Analysis: theory HOL-Analysis.Abstract_Euclidean_Space
11:02:38HOL-Analysis: theory HOL-Analysis.Homeomorphism
11:02:38Collections: theory Word_Lib.Bit_Comprehension
11:02:39X86_Semantics: theory Word_Lib.Bits_Int
11:02:40HOL-Analysis: theory HOL-Analysis.Abstract_Topological_Spaces
11:02:41CoSMeDis: theory CoSMeDis.Post_Network
11:02:41HOL-Analysis: theory HOL-Analysis.Sparse_In
11:02:42Collections: theory Word_Lib.More_Divides
11:02:42X86_Semantics: theory Word_Lib.Typedef_Morphisms
11:02:42X86_Semantics: theory Word_Lib.Reversed_Bit_Lists
11:02:42Collections: theory HOL-Library.RBT_Impl
11:02:43Collections: theory Collections.Assoc_List
11:02:43Collections: theory Collections.Diff_Array
11:02:44HOL-Analysis: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
11:02:46X86_Semantics: theory Word_Lib.Bitwise
11:02:47X86_Semantics: theory X86_Semantics.BitByte
11:02:48X86_Semantics: theory X86_Semantics.Memory
11:02:48CakeML: theory CakeML.CakeML_Quickcheck
11:02:48CakeML: theory CakeML.Evaluate
11:02:48Collections: theory Collections.Dlist_add
11:02:48CakeML: theory CakeML.SmallStep
11:02:48CakeML: theory CakeML.TypeSystem
11:02:48Collections: theory Collections.Proper_Iterator
11:02:48X86_Semantics: theory X86_Semantics.State
11:02:48Collections: theory Collections.SetIteratorGA
11:02:50Collections: theory Collections.It_to_It
11:02:50Collections: theory HOL-Library.Signed_Division
11:02:50Collections: theory Collections.DatRef
11:02:51Collections: theory Word_Lib.Signed_Division_Word
11:02:51HOL-Library: theory HOL-Library.Disjoint_FSets
11:02:51Collections: theory Native_Word.Code_Int_Integer_Conversion
11:02:51Collections: theory Collections.Gen_Iterator
11:02:51Collections: theory Word_Lib.More_Arithmetic
11:02:52Collections: theory Word_Lib.More_Bit_Ring
11:02:52HOL-Library: theory HOL-Library.Library
11:02:52Collections: theory Collections.Iterator
11:02:52Collections: theory Collections.ICF_Spec_Base
11:02:52Collections: theory Word_Lib.More_Word
11:02:52Collections: theory Collections.MapSpec
11:02:53X86_Semantics: theory X86_Semantics.StateCleanUp
11:02:53X86_Semantics: theory X86_Semantics.X86_InstructionSemantics
11:02:56HOL-Analysis: theory HOL-Real_Asymp.Real_Asymp
11:02:56HOL-Analysis: theory HOL-Analysis.Abstract_Metric_Spaces
11:02:58Collections: theory Native_Word.Code_Target_Word_Base
11:02:58CakeML: theory CakeML.BigStep
11:02:58Collections: theory Word_Lib.Bit_Shifts_Infix_Syntax
11:02:59Collections: theory Collections.Robdd
11:02:59Collections: theory Word_Lib.Least_significant_bit
11:02:59CakeML: theory CakeML.PrimTypes
11:03:00Collections: theory Word_Lib.Most_significant_bit
11:03:00Collections: theory Word_Lib.Generic_set_bit
11:03:02Collections: theory Native_Word.Code_Target_Integer_Bit
11:03:04Collections: theory Native_Word.Word_Type_Copies
11:03:07CakeML: theory CakeML.BigSmallInvariants
11:03:08CakeML: theory CakeML.SemanticPrimitivesAuxiliary
11:03:09CakeML: theory CakeML.Semantic_Extras
11:03:14X86_Semantics: theory X86_Semantics.SymbolicExecution
11:03:15X86_Semantics: theory X86_Semantics.X86_Parse
11:03:15Finished Simpl/document (0:01:00 elapsed time)
11:03:15Preparing Simpl/outline ...
11:03:16X86_Semantics: theory X86_Semantics.Examples
11:03:17X86_Semantics: theory X86_Semantics.Example_WC
11:03:24HOL-Analysis: theory HOL-Analysis.Uniform_Limit
11:03:24HOL-Analysis: theory HOL-Analysis.Urysohn
11:03:25HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function
11:03:25HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function
11:03:26Collections: theory Native_Word.Code_Target_Int_Bit
11:03:26Collections: theory Native_Word.Uint32
11:03:26Collections: theory Collections.Code_Target_ICF
11:03:27Collections: theory Collections.Locale_Code_Ex
11:03:29HOL-Analysis: theory HOL-Analysis.Derivative
11:03:29CakeML: theory CakeML.TypeSystemAuxiliary
11:03:29Collections: theory Collections.HashCode
11:03:31HOL-Analysis: theory HOL-Analysis.Borel_Space
11:03:31HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space
11:03:31HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics
11:03:31HOL-Analysis: theory HOL-Analysis.Lipschitz
11:03:32HOL-Analysis: theory HOL-Analysis.Cross3
11:03:33HOL-Analysis: theory HOL-Analysis.Polytope
11:03:34HOL-Analysis: theory HOL-Analysis.Multivariate_Analysis
11:03:34HOL-Analysis: theory HOL-Analysis.Complex_Transcendental
11:03:36CakeML: theory CakeML.Big_Step_Determ
11:03:36CakeML: theory CakeML.Big_Step_Total
11:03:36HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
11:03:36CakeML: theory CakeML.Big_Step_Clocked
11:03:37HOL-Analysis: theory HOL-Analysis.Regularity
11:03:38HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint
11:03:39CakeML: theory CakeML.Big_Step_Unclocked
11:03:40HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems
11:03:40CakeML: theory CakeML.Evaluate_Termination
11:03:41CakeML: theory CakeML.Evaluate_Clock
11:03:41CakeML: theory CakeML.Big_Step_Fun_Equiv
11:03:42HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem
11:03:43HOL-Analysis: theory HOL-Analysis.FPS_Convergence
11:03:43CakeML: theory CakeML.Evaluate_Single
11:03:44HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers
11:03:44HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure
11:03:45HOL-Analysis: theory HOL-Analysis.Infinite_Products
11:03:45HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem
11:03:47CakeML: theory CakeML.Big_Step_Unclocked_Single
11:03:47HOL-Analysis: theory HOL-Analysis.Retracts
11:03:47Finished Simpl/outline (0:00:31 elapsed time)
11:03:47HOL-Analysis: theory HOL-Analysis.Embed_Measure
11:03:47HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure
11:03:48Timing Simpl (4 threads, 198.730s elapsed time, 427.446s cpu time, 19.813s GC time, factor 2.15)
11:03:48Finished Simpl (0:03:49 elapsed time, 0:08:03 cpu time, factor 2.11)
11:03:48Building AutoCorres2_Main ...
11:03:50HOL-Analysis: theory HOL-Analysis.Smooth_Paths
11:03:51AutoCorres2_Main: theory AutoCorres2.MkTermAntiquote
11:03:51AutoCorres2_Main: theory AutoCorres2.TermPatternAntiquote
11:03:51AutoCorres2_Main: theory AutoCorres2.ML_Fun_Cache
11:03:51AutoCorres2_Main: theory HOL-Eisbach.Eisbach
11:03:51CakeML: theory CakeML.Matching
11:03:51HOL-Analysis: theory HOL-Analysis.Bochner_Integration
11:03:52AutoCorres2_Main: theory AutoCorres2.Introduction_AutoCorres2
11:03:52AutoCorres2_Main: theory AutoCorres2.ML_Infer_Instantiate
11:03:52AutoCorres2_Main: theory AutoCorres2.ML_Record_Antiquotation
11:03:52AutoCorres2_Main: theory AutoCorres2.MapExtra
11:03:53AutoCorres2_Main: theory AutoCorres2.Option_Scanner
11:03:53AutoCorres2_Main: theory AutoCorres2.Misc_Antiquotation
11:03:54AutoCorres2_Main: theory AutoCorres2.Named_Rules
11:03:55AutoCorres2_Main: theory AutoCorres2.Padding
11:03:55AutoCorres2_Main: theory AutoCorres2.Print_Annotated
11:03:55AutoCorres2_Main: theory AutoCorres2.StaticFun
11:03:55AutoCorres2_Main: theory AutoCorres2.MapExtraTrans
11:03:55AutoCorres2_Main: theory AutoCorres2.AutoCorres_Utils
11:03:55AutoCorres2_Main: theory AutoCorres2.Subgoals
11:03:55HOL-Analysis: theory HOL-Analysis.Complete_Measure
11:03:55HOL-Analysis: theory HOL-Analysis.Radon_Nikodym
11:03:56AutoCorres2_Main: theory AutoCorres2.Target_Architecture
11:03:56AutoCorres2_Main: theory HOL-Eisbach.Eisbach_Tools
11:03:57AutoCorres2_Main: theory AutoCorres2.Tagging
11:03:57AutoCorres2_Main: theory AutoCorres2.Cong_Tactic
11:03:57AutoCorres2_Main: theory AutoCorres2.Tuple_Tools
11:03:57HOL-Analysis: theory HOL-Analysis.Set_Integral
11:03:58HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure
11:03:59AutoCorres2_Main: theory AutoCorres2.Basic_Runs_To_VCG
11:03:59AutoCorres2_Main: theory AutoCorres2.Match_Cterm
11:03:59HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum
11:03:59AutoCorres2_Main: theory AutoCorres2.Simp_Trace
11:04:01AutoCorres2_Main: theory HOL-Library.Adhoc_Overloading
11:04:01AutoCorres2_Main: theory HOL-Library.Code_Abstract_Nat
11:04:01AutoCorres2_Main: theory HOL-Library.Monad_Syntax
11:04:01AutoCorres2_Main: theory HOL-Library.Code_Binary_Nat
11:04:01AutoCorres2_Main: theory AutoCorres2.Less_Monad_Syntax
11:04:01AutoCorres2_Main: theory HOL-Library.Complete_Partial_Order2
11:04:01AutoCorres2_Main: theory HOL-Library.Phantom_Type
11:04:03HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration
11:04:03AutoCorres2_Main: theory AutoCorres2.Runs_To_VCG
11:04:03AutoCorres2_Main: theory HOL-Library.Signed_Division
11:04:03AutoCorres2_Main: theory HOL-Library.Cardinality
11:04:04AutoCorres2_Main: theory HOL-Library.Numeral_Type
11:04:04AutoCorres2_Main: theory HOL-Library.Sublist
11:04:06AutoCorres2_Main: theory AutoCorres2.Arrays
11:04:07AutoCorres2_Main: theory HOL-Library.Type_Length
11:04:07AutoCorres2_Main: theory AutoCorres2.Mutual_CCPO_Recursion
11:04:08CakeML: theory CakeML.CakeML_Code
11:04:09AutoCorres2_Main: theory AutoCorres2.Spec_Monad
11:04:09AutoCorres2_Main: theory HOL-Library.Word
11:04:10HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
11:04:10HOL-Analysis: theory HOL-Analysis.Integral_Test
11:04:10HOL-Analysis: theory HOL-Analysis.Kronecker_Approximation_Theorem
11:04:13AutoCorres2_Main: theory HOL-Library.Prefix_Order
11:04:13AutoCorres2_Main: theory Word_Lib.More_Sublist
11:04:13AutoCorres2_Main: theory AutoCorres2.PrettyProgs
11:04:13AutoCorres2_Main: theory AutoCorres2.IndirectCalls
11:04:13AutoCorres2_Main: theory Word_Lib.Enumeration
11:04:14AutoCorres2_Main: theory Word_Lib.Even_More_List
11:04:14AutoCorres2_Main: theory Word_Lib.More_Arithmetic
11:04:14AutoCorres2_Main: theory Word_Lib.More_Bit_Ring
11:04:14HOL-Analysis: theory HOL-Analysis.Further_Topology
11:04:14HOL-Analysis: theory HOL-Analysis.Gamma_Function
11:04:14HOL-Analysis: theory HOL-Analysis.Improper_Integral
11:04:14HOL-Analysis: theory HOL-Analysis.Interval_Integral
11:04:15AutoCorres2_Main: theory Word_Lib.More_Misc
11:04:16HOL-Analysis: theory HOL-Analysis.Equivalence_Measurable_On_Borel
11:04:16HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution
11:04:17HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem
11:04:19AutoCorres2_Main: theory AutoCorres2.Synthesize
11:04:22Collections: theory Collections.RBT_add
11:04:23HOL-Analysis: theory HOL-Analysis.Change_Of_Vars
11:04:23HOL-Analysis: theory HOL-Analysis.Jordan_Curve
11:04:27HOL-Analysis: theory HOL-Analysis.Simplex_Content
11:04:30HOL-Analysis: theory HOL-Analysis.Ball_Volume
11:04:30HOL-Analysis: theory HOL-Analysis.Analysis
11:04:32AutoCorres2_Main: theory AutoCorres2.Reaches
11:04:33AutoCorres2_Main: theory Word_Lib.Bit_Comprehension
11:04:33AutoCorres2_Main: theory Word_Lib.Hex_Words
11:04:33AutoCorres2_Main: theory Word_Lib.Legacy_Aliases
11:04:33AutoCorres2_Main: theory Word_Lib.More_Divides
11:04:34AutoCorres2_Main: theory Word_Lib.Signed_Words
11:04:34AutoCorres2_Main: theory Word_Lib.Norm_Words
11:04:34AutoCorres2_Main: theory Word_Lib.Word_Names
11:04:34AutoCorres2_Main: theory Word_Lib.Syntax_Bundles
11:04:34AutoCorres2_Main: theory Word_Lib.Type_Syntax
11:04:34AutoCorres2_Main: theory Word_Lib.Word_Syntax
11:04:34AutoCorres2_Main: theory Word_Lib.Signed_Division_Word
11:04:34AutoCorres2_Main: theory Word_Lib.Bit_Comprehension_Int
11:04:34AutoCorres2_Main: theory Word_Lib.More_Word
11:04:36AutoCorres2_Main: theory Word_Lib.Bit_Shifts_Infix_Syntax
11:04:36AutoCorres2_Main: theory Word_Lib.Enumeration_Word
11:04:36AutoCorres2_Main: theory Word_Lib.Least_significant_bit
11:04:36AutoCorres2_Main: theory Word_Lib.Many_More
11:04:36AutoCorres2_Main: theory Word_Lib.Strict_part_mono
11:04:36AutoCorres2_Main: theory Word_Lib.Word_16
11:04:37AutoCorres2_Main: theory AutoCorres2.Distinct_Prop
11:04:37AutoCorres2_Main: theory AutoCorres2.Lens
11:04:37AutoCorres2_Main: theory Word_Lib.Aligned
11:04:37AutoCorres2_Main: theory Word_Lib.Singleton_Bit_Shifts
11:04:37AutoCorres2_Main: theory Word_Lib.Most_significant_bit
11:04:38AutoCorres2_Main: theory Word_Lib.Generic_set_bit
11:04:39AutoCorres2_Main: theory Word_Lib.Sgn_Abs
11:04:39AutoCorres2_Main: theory Word_Lib.Next_and_Prev
11:04:39AutoCorres2_Main: theory Word_Lib.Word_EqI
11:04:40AutoCorres2_Main: theory Word_Lib.Bits_Int
11:04:40AutoCorres2_Main: theory Word_Lib.Boolean_Inequalities
11:04:43AutoCorres2_Main: theory Word_Lib.Rsplit
11:04:43AutoCorres2_Main: theory Word_Lib.Typedef_Morphisms
11:04:44AutoCorres2_Main: theory Word_Lib.Reversed_Bit_Lists
11:04:46AutoCorres2_Main: theory Word_Lib.Word_Lemmas
11:04:48AutoCorres2_Main: theory Word_Lib.Bitwise
11:04:49AutoCorres2_Main: theory Word_Lib.Bitwise_Signed
11:04:49Preparing Syntax_Independent_Logic/document ...
11:04:50AutoCorres2_Main: theory Word_Lib.Word_8
11:04:50AutoCorres2_Main: theory Word_Lib.More_Word_Operations
11:04:52AutoCorres2_Main: theory AutoCorres2.Word_Lemmas_Internal
11:04:52AutoCorres2_Main: theory Word_Lib.Word_32
11:04:52AutoCorres2_Main: theory Word_Lib.Word_64
11:04:53CoSMeDis: theory CoSMeDis.Post_All
11:04:54AutoCorres2_Main: theory Word_Lib.Machine_Word_64_Basics
11:04:54AutoCorres2_Main: theory Word_Lib.Machine_Word_32_Basics
11:04:54AutoCorres2_Main: theory Word_Lib.Machine_Word_64
11:04:54AutoCorres2_Main: theory Word_Lib.Machine_Word_32
11:04:54AutoCorres2_Main: theory Word_Lib.Word_Lib_Sumo
11:04:57AutoCorres2_Main: theory AutoCorres2.More_Lib
11:04:58AutoCorres2_Main: theory AutoCorres2.Word_Lemmas_32_Internal
11:04:58AutoCorres2_Main: theory AutoCorres2.Word_Lemmas_64_Internal
11:04:59AutoCorres2_Main: theory AutoCorres2.WordSetup
11:05:00AutoCorres2_Main: theory AutoCorres2.Addr_Type_ARM
11:05:00AutoCorres2_Main: theory AutoCorres2.Addr_Type_ARM64
11:05:00AutoCorres2_Main: theory AutoCorres2.Addr_Type_ARM_HYP
11:05:00AutoCorres2_Main: theory AutoCorres2.Addr_Type_RISCV64
11:05:01AutoCorres2_Main: theory AutoCorres2.Addr_Type_X64
11:05:01AutoCorres2_Main: theory AutoCorres2.NatBitwise
11:05:02AutoCorres2_Main: theory AutoCorres2.Reader_Monad
11:05:02AutoCorres2_Main: theory AutoCorres2.Addr_Type
11:05:03AutoCorres2_Main: theory AutoCorres2.Option_MonadND
11:05:03AutoCorres2_Main: theory AutoCorres2.CTypesBase
11:05:06Finished Syntax_Independent_Logic/document (0:00:17 elapsed time)
11:05:06Preparing Syntax_Independent_Logic/outline ...
11:05:08AutoCorres2_Main: theory AutoCorres2.CTypesDefs
11:05:18Finished Syntax_Independent_Logic/outline (0:00:11 elapsed time)
11:05:18Timing Syntax_Independent_Logic (4 threads, 367.028s elapsed time, 1307.689s cpu time, 7.409s GC time, factor 3.56)
11:05:18Finished Syntax_Independent_Logic (0:06:27 elapsed time, 0:22:22 cpu time, factor 3.46)
11:05:18Running AutoCorres2 ...
11:05:21AutoCorres2: theory AutoCorres2.TermPatternAntiquote
11:05:21AutoCorres2: theory AutoCorres2.ML_Fun_Cache
11:05:21AutoCorres2: theory AutoCorres2.MkTermAntiquote
11:05:21AutoCorres2: theory HOL-Eisbach.Eisbach
11:05:21AutoCorres2: theory AutoCorres2.Apply_Trace
11:05:21AutoCorres2: theory AutoCorres2.Introduction_AutoCorres2
11:05:21AutoCorres2: theory AutoCorres2.ML_Infer_Instantiate
11:05:21AutoCorres2: theory AutoCorres2.ML_Record_Antiquotation
11:05:22AutoCorres2: theory AutoCorres2.Option_Scanner
11:05:22AutoCorres2: theory AutoCorres2.Apply_Trace_Cmd
11:05:22AutoCorres2: theory AutoCorres2.MapExtra
11:05:24AutoCorres2: theory AutoCorres2.Misc_Antiquotation
11:05:24AutoCorres2: theory AutoCorres2.MkTermAntiquote_Tests
11:05:25AutoCorres2: theory HOL-Eisbach.Eisbach_Tools
11:05:25AutoCorres2: theory AutoCorres2.Cong_Tactic
11:05:25AutoCorres2: theory AutoCorres2.Named_Rules
11:05:25AutoCorres2: theory AutoCorres2.MapExtraTrans
11:05:25AutoCorres2: theory AutoCorres2.Padding
11:05:25AutoCorres2: theory AutoCorres2.Print_Annotated
11:05:25AutoCorres2: theory AutoCorres2.Rule_By_Method
11:05:25AutoCorres2: theory AutoCorres2.StaticFun
11:05:25AutoCorres2: theory AutoCorres2.Subgoal_Methods
11:05:25AutoCorres2: theory AutoCorres2.AutoCorres_Utils
11:05:25AutoCorres2: theory AutoCorres2.Subgoals
11:05:25AutoCorres2: theory AutoCorres2.Tagging
11:05:26AutoCorres2: theory AutoCorres2.Eisbach_Methods
11:05:27AutoCorres2: theory AutoCorres2.Basic_Runs_To_VCG
11:05:27AutoCorres2: theory AutoCorres2.Match_Cterm
11:05:27AutoCorres2: theory AutoCorres2.Simp_Trace
11:05:27AutoCorres2: theory AutoCorres2.Target_Architecture
11:05:28AutoCorres2: theory AutoCorres2.TermPatternAntiquote_Tests
11:05:28AutoCorres2: theory AutoCorres2.Tuple_Tools
11:05:28AutoCorres2: theory HOL-Library.Adhoc_Overloading
11:05:28AutoCorres2: theory HOL-Library.Monad_Syntax
11:05:28AutoCorres2: theory AutoCorres2.Less_Monad_Syntax
11:05:28AutoCorres2: theory HOL-Library.Code_Abstract_Nat
11:05:28AutoCorres2: theory HOL-Library.Complete_Partial_Order2
11:05:28AutoCorres2: theory HOL-Library.Code_Binary_Nat
11:05:28AutoCorres2: theory HOL-Library.Phantom_Type
11:05:29AutoCorres2: theory AutoCorres2.Runs_To_VCG
11:05:29AutoCorres2: theory HOL-Library.Signed_Division
11:05:29AutoCorres2: theory HOL-Library.Cardinality
11:05:29AutoCorres2_Main: theory AutoCorres2.CTypes
11:05:31AutoCorres2: theory HOL-Library.Sublist
11:05:31AutoCorres2: theory HOL-Library.Numeral_Type
11:05:35AutoCorres2: theory AutoCorres2.Arrays
11:05:35AutoCorres2_Main: theory AutoCorres2.HeapRawState
11:05:35AutoCorres2_Main: theory AutoCorres2.Vanilla32_Preliminaries
11:05:35AutoCorres2: theory HOL-Library.Type_Length
11:05:35AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_ARM
11:05:36AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_ARM64
11:05:36AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_ARM_HYP
11:05:36AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_RISCV64
11:05:36AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding_X64
11:05:36AutoCorres2_Main: theory AutoCorres2.Word_Mem_Encoding
11:05:36AutoCorres2: theory AutoCorres2.Mutual_CCPO_Recursion
11:05:36AutoCorres2: theory AutoCorres2.Spec_Monad
11:05:36AutoCorres2_Main: theory AutoCorres2.Vanilla32
11:05:36AutoCorres2: theory HOL-Library.Word
11:05:37AutoCorres2: theory HOL-Library.Prefix_Order
11:05:37AutoCorres2: theory Word_Lib.More_Sublist
11:05:37AutoCorres2: theory AutoCorres2.PrettyProgs
11:05:37AutoCorres2: theory AutoCorres2.IndirectCalls
11:05:37AutoCorres2: theory Word_Lib.Enumeration
11:05:38AutoCorres2_Main: theory AutoCorres2.CompoundCTypes
11:05:38AutoCorres2: theory Word_Lib.Even_More_List
11:05:38AutoCorres2: theory Word_Lib.More_Arithmetic
11:05:39AutoCorres2: theory Word_Lib.More_Bit_Ring
11:05:41AutoCorres2: theory Word_Lib.More_Misc
11:05:46AutoCorres2_Main: theory AutoCorres2.ArraysMemInstance
11:05:49AutoCorres2_Main: theory AutoCorres2.ArchArraysMemInstance
11:05:49AutoCorres2: theory AutoCorres2.Synthesize
11:05:53AutoCorres2_Main: theory AutoCorres2.TypHeap
11:05:57AutoCorres2: theory Word_Lib.Bit_Comprehension
11:05:57AutoCorres2: theory AutoCorres2.Reaches
11:05:57AutoCorres2: theory Word_Lib.Hex_Words
11:05:57AutoCorres2: theory Word_Lib.Legacy_Aliases
11:05:58AutoCorres2: theory Word_Lib.More_Divides
11:05:58AutoCorres2: theory Word_Lib.Signed_Words
11:05:58AutoCorres2: theory Word_Lib.Norm_Words
11:05:58Preparing CZH_Foundations/document ...
11:05:58AutoCorres2: theory Word_Lib.Word_Names
11:05:58AutoCorres2: theory Word_Lib.Syntax_Bundles
11:05:59AutoCorres2: theory Word_Lib.Type_Syntax
11:05:59AutoCorres2: theory Word_Lib.Word_Syntax
11:05:59AutoCorres2: theory Word_Lib.Signed_Division_Word
11:05:59AutoCorres2: theory Word_Lib.Bit_Comprehension_Int
11:05:59AutoCorres2: theory Word_Lib.More_Word
11:06:02AutoCorres2: theory Word_Lib.Bit_Shifts_Infix_Syntax
11:06:02AutoCorres2: theory Word_Lib.Enumeration_Word
11:06:02AutoCorres2: theory Word_Lib.Least_significant_bit
11:06:02AutoCorres2: theory Word_Lib.Many_More
11:06:03AutoCorres2: theory Word_Lib.Strict_part_mono
11:06:03AutoCorres2: theory Word_Lib.Word_16
11:06:03AutoCorres2: theory AutoCorres2.Distinct_Prop
11:06:03AutoCorres2: theory AutoCorres2.Lens
11:06:04AutoCorres2: theory Word_Lib.Aligned
11:06:04AutoCorres2: theory Word_Lib.Singleton_Bit_Shifts
11:06:04AutoCorres2: theory Word_Lib.Most_significant_bit
11:06:04AutoCorres2_Main: theory AutoCorres2.Separation_UMM
11:06:04AutoCorres2: theory Word_Lib.Generic_set_bit
11:06:04AutoCorres2: theory Word_Lib.Sgn_Abs
11:06:05AutoCorres2: theory Word_Lib.Next_and_Prev
11:06:05AutoCorres2: theory Word_Lib.Word_EqI
11:06:05AutoCorres2: theory Word_Lib.Bits_Int
11:06:07AutoCorres2_Main: theory AutoCorres2.SepCode
11:06:07AutoCorres2: theory Word_Lib.Boolean_Inequalities
11:06:09AutoCorres2_Main: theory AutoCorres2.SepInv
11:06:09AutoCorres2: theory Word_Lib.Rsplit
11:06:09AutoCorres2: theory Word_Lib.Typedef_Morphisms
11:06:10AutoCorres2: theory Word_Lib.Reversed_Bit_Lists
11:06:11AutoCorres2: theory Word_Lib.Word_Lemmas
11:06:11AutoCorres2_Main: theory AutoCorres2.SepTactic
11:06:11AutoCorres2_Main: theory AutoCorres2.StructSupport
11:06:11AutoCorres2_Main: theory AutoCorres2.SepFrame
11:06:12AutoCorres2_Main: theory AutoCorres2.ArrayAssertion
11:06:15AutoCorres2_Main: theory AutoCorres2.CProof
11:06:16AutoCorres2: theory Word_Lib.Word_8
11:06:16AutoCorres2: theory Word_Lib.Bitwise
11:06:16AutoCorres2: theory Word_Lib.More_Word_Operations
11:06:16AutoCorres2: theory Word_Lib.Bitwise_Signed
11:06:17AutoCorres2: theory AutoCorres2.Word_Lemmas_Internal
11:06:17AutoCorres2: theory Word_Lib.Word_32
11:06:17AutoCorres2: theory Word_Lib.Word_64
11:06:18AutoCorres2: theory Word_Lib.Machine_Word_64_Basics
11:06:18AutoCorres2: theory Word_Lib.Machine_Word_64
11:06:18AutoCorres2: theory Word_Lib.Machine_Word_32_Basics
11:06:18AutoCorres2: theory Word_Lib.Word_Lib_Sumo
11:06:18AutoCorres2: theory Word_Lib.Machine_Word_32
11:06:21AutoCorres2: theory AutoCorres2.More_Lib
11:06:22AutoCorres2: theory AutoCorres2.Word_Lemmas_32_Internal
11:06:22AutoCorres2: theory AutoCorres2.Word_Lemmas_64_Internal
11:06:23AutoCorres2: theory AutoCorres2.WordSetup
11:06:24AutoCorres2: theory AutoCorres2.Addr_Type_ARM
11:06:24AutoCorres2: theory AutoCorres2.Addr_Type_ARM64
11:06:24AutoCorres2: theory AutoCorres2.Addr_Type_ARM_HYP
11:06:24AutoCorres2: theory AutoCorres2.Addr_Type_RISCV64
11:06:24AutoCorres2: theory AutoCorres2.Addr_Type_X64
11:06:26AutoCorres2: theory AutoCorres2.Addr_Type
11:06:26AutoCorres2_Main: theory AutoCorres2.CLanguage
11:06:26AutoCorres2_Main: theory AutoCorres2.Padding_Equivalence
11:06:26AutoCorres2_Main: theory AutoCorres2.PackedTypes
11:06:27AutoCorres2: theory AutoCorres2.NatBitwise
11:06:27AutoCorres2: theory AutoCorres2.Reader_Monad
11:06:27AutoCorres2: theory AutoCorres2.CTypesBase
11:06:27AutoCorres2: theory AutoCorres2.Option_MonadND
11:06:31AutoCorres2: theory AutoCorres2.CTypesDefs
11:06:35AutoCorres2_Main: theory AutoCorres2.ModifiesProofs
11:06:40AutoCorres2_Main: theory AutoCorres2.UMM
11:06:46Collections: theory Collections.GenCF_Gen_Chapter
11:06:46Collections: theory Collections.GenCF_Chapter
11:06:46Collections: theory Collections.GenCF_Impl_Chapter
11:06:46Collections: theory Collections.GenCF_Intf_Chapter
11:06:46Collections: theory Collections.Intf_Comp
11:06:46Collections: theory Collections.Impl_Array_Stack
11:06:46Collections: theory HOL-Library.Product_Lexorder
11:06:46Collections: theory Collections.Array_Iterator
11:06:46Collections: theory Collections.Intf_Map
11:06:47Collections: theory Collections.Intf_Set
11:06:48Collections: theory Collections.Gen_Map
11:06:48Collections: theory Collections.Gen_Set
11:06:48Collections: theory Collections.Impl_Cfun_Set
11:06:48Collections: theory Collections.Impl_List_Set
11:06:49Collections: theory Collections.Gen_Comp
11:06:49Collections: theory Collections.Impl_RBT_Map
11:06:49AutoCorres2: theory AutoCorres2.CTypes
11:06:49AutoCorres2_Main: theory AutoCorres2.CLocals
11:06:49Collections: theory Collections.Gen_Map2Set
11:06:49Collections: theory Collections.Impl_Array_Map
11:06:50Collections: theory Collections.Impl_List_Map
11:06:51Collections: theory Collections.Intf_Hash
11:06:52Collections: theory Collections.Impl_Array_Hash_Map
11:06:54AutoCorres2_Main: theory AutoCorres2.CTranslationSetup
11:06:55AutoCorres2: theory AutoCorres2.HeapRawState
11:06:55AutoCorres2: theory AutoCorres2.Vanilla32_Preliminaries
11:06:55AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_ARM
11:06:55AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_ARM64
11:06:55AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_ARM_HYP
11:06:55AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_RISCV64
11:06:55AutoCorres2: theory AutoCorres2.Word_Mem_Encoding_X64
11:06:55AutoCorres2: theory AutoCorres2.Word_Mem_Encoding
11:06:56AutoCorres2: theory AutoCorres2.Vanilla32
11:06:57AutoCorres2: theory AutoCorres2.CompoundCTypes
11:07:07AutoCorres2: theory AutoCorres2.ArraysMemInstance
11:07:08AutoCorres2: theory AutoCorres2.ArchArraysMemInstance
11:07:12AutoCorres2: theory AutoCorres2.TypHeap
11:07:22AutoCorres2: theory AutoCorres2.Separation_UMM
11:07:23Collections: theory Native_Word.Uint
11:07:23Collections: theory Collections.Impl_Bit_Set
11:07:23Collections: theory Collections.Gen_Hash
11:07:23AutoCorres2: theory AutoCorres2.SepCode
11:07:26Collections: theory Collections.Impl_Uv_Set
11:07:28AutoCorres2: theory AutoCorres2.SepInv
11:07:28AutoCorres2: theory AutoCorres2.SepTactic
11:07:29AutoCorres2: theory AutoCorres2.StructSupport
11:07:29AutoCorres2: theory AutoCorres2.SepFrame
11:07:30AutoCorres2: theory AutoCorres2.ArrayAssertion
11:07:32AutoCorres2: theory AutoCorres2.CProof
11:07:36AutoCorres2_Main: theory AutoCorres2.Array_Selectors
11:07:36AutoCorres2_Main: theory AutoCorres2.CTranslation
11:07:37AutoCorres2_Main: theory AutoCorres2.TypHeapLib
11:07:37AutoCorres2_Main: theory AutoCorres2.AbstractArrays
11:07:37AutoCorres2_Main: theory AutoCorres2.LemmaBucket_C
11:07:38AutoCorres2_Main: theory AutoCorres2.AutoCorres_Base
11:07:38AutoCorres2_Main: theory AutoCorres2.SimplBucket
11:07:38AutoCorres2_Main: theory AutoCorres2.AutoCorresSimpset
11:07:39AutoCorres2_Main: theory AutoCorres2.CCorresE
11:07:39AutoCorres2_Main: theory AutoCorres2.CorresXF
11:07:39AutoCorres2_Main: theory AutoCorres2.L1Defs
11:07:39AutoCorres2_Main: theory AutoCorres2.TypHeapSimple
11:07:43AutoCorres2_Main: theory AutoCorres2.L1Peephole
11:07:43AutoCorres2_Main: theory AutoCorres2.ExceptionRewrite
11:07:44AutoCorres2: theory AutoCorres2.CLanguage
11:07:45AutoCorres2_Main: theory AutoCorres2.SimplConv
11:07:45AutoCorres2_Main: theory AutoCorres2.L1Valid
11:07:46AutoCorres2: theory AutoCorres2.Padding_Equivalence
11:07:46AutoCorres2: theory AutoCorres2.PackedTypes
11:07:46AutoCorres2_Main: theory AutoCorres2.L2Defs
11:07:47Collections: theory Collections.GenCF
11:07:51AutoCorres2_Main: theory AutoCorres2.Split_Heap
11:07:52Collections: theory Collections.ICF_Chapter
11:07:52Collections: theory Collections.ICF_Gen_Algo_Chapter
11:07:52Collections: theory Collections.ICF_Impl_Chapter
11:07:52Collections: theory Collections.ICF_Spec_Chapter
11:07:52Collections: theory Trie.Trie
11:07:52Collections: theory Collections.AnnotatedListSpec
11:07:52Collections: theory HOL-Library.RBT
11:07:52Collections: theory Collections.ListSpec
11:07:53AutoCorres2: theory AutoCorres2.ModifiesProofs
11:07:54Collections: theory Collections.PrioSpec
11:07:54Finished CZH_Foundations/document (0:01:55 elapsed time)
11:07:54Preparing CZH_Foundations/outline ...
11:07:55Collections: theory Collections.ListGA
11:07:55AutoCorres2_Main: theory AutoCorres2.L2ExceptionRewrite
11:07:55Collections: theory Collections.BinoPrioImpl
11:07:56Collections: theory Collections.FTAnnotatedListImpl
11:07:56Collections: theory Collections.Trie_Impl
11:07:56AutoCorres2_Main: theory AutoCorres2.L2Peephole
11:07:56Collections: theory Collections.Fifo
11:07:57Collections: theory Collections.Trie2
11:07:57Collections: theory Collections.PrioByAnnotatedList
11:07:59AutoCorres2: theory AutoCorres2.UMM
11:07:59AutoCorres2_Main: theory AutoCorres2.WordAbstract
11:07:59AutoCorres2_Main: theory AutoCorres2.Refines_Spec
11:08:01Collections: theory Collections.SkewPrioImpl
11:08:02Collections: theory Collections.PrioUniqueSpec
11:08:02AutoCorres2_Main: theory AutoCorres2.LocalVarExtract
11:08:02AutoCorres2_Main: theory AutoCorres2.Stack_Typing
11:08:02AutoCorres2_Main: theory AutoCorres2.WordPolish
11:08:03Collections: theory Collections.SetSpec
11:08:03Collections: theory Collections.PrioUniqueByAnnotatedList
11:08:04Collections: theory Collections.FTPrioImpl
11:08:06AutoCorres2_Main: theory AutoCorres2.In_Out_Parameters
11:08:07Collections: theory Collections.FTPrioUniqueImpl
11:08:08Collections: theory Collections.Algos
11:08:08Collections: theory Collections.SetIndex
11:08:09AutoCorres2: theory AutoCorres2.CLocals
11:08:10Collections: theory Collections.SetIteratorCollectionsGA
11:08:10Collections: theory Collections.MapGA
11:08:10Collections: theory Collections.SetGA
11:08:13AutoCorres2: theory AutoCorres2.CTranslationSetup
11:08:14Collections: theory Collections.ArrayMapImpl
11:08:14Collections: theory Collections.ListMapImpl
11:08:14Collections: theory Collections.ListMapImpl_Invar
11:08:18Collections: theory Collections.TrieMapImpl
11:08:22Collections: theory Collections.ListSetImpl
11:08:23AutoCorres2_Main: theory AutoCorres2.TypeStrengthen
11:08:24Collections: theory Collections.ListSetImpl_Invar
11:08:24Collections: theory Collections.ListSetImpl_NotDist
11:08:25Collections: theory Collections.ListSetImpl_Sorted
11:08:29AutoCorres2_Main: theory AutoCorres2.HeapLift
11:08:30Collections: theory Collections.SetByMap
11:08:31Collections: theory Collections.RBTMapImpl
11:08:32Collections: theory Collections.ArrayHashMap_Impl
11:08:34Collections: theory Collections.ArraySetImpl
11:08:35Collections: theory Collections.TrieSetImpl
11:08:37Collections: theory Collections.ArrayHashMap
11:08:37Preparing HOL-Library/document ...
11:08:41Collections: theory Collections.RBTSetImpl
11:08:43Collections: theory Collections.HashMap_Impl
11:08:45Collections: theory Collections.ArrayHashSet
11:08:46Collections: theory Collections.HashMap
11:08:49AutoCorres2: theory AutoCorres2.Array_Selectors
11:08:49AutoCorres2: theory AutoCorres2.CTranslation
11:08:49AutoCorres2: theory AutoCorres2.CTranslationInfrastructure
11:08:49AutoCorres2: theory AutoCorres2.TypHeapLib
11:08:50AutoCorres2: theory AutoCorres2.AbstractArrays
11:08:50AutoCorres2: theory AutoCorres2.LemmaBucket_C
11:08:51AutoCorres2: theory AutoCorres2.AutoCorres_Base
11:08:54Collections: theory Collections.HashSet
11:08:55Collections: theory Collections.MapStdImpl
11:08:56AutoCorres2: theory AutoCorres2.SimplBucket
11:08:56AutoCorres2: theory AutoCorres2.AutoCorresSimpset
11:08:56AutoCorres2: theory AutoCorres2.CCorresE
11:08:57AutoCorres2: theory AutoCorres2.CorresXF
11:08:58AutoCorres2: theory AutoCorres2.L1Defs
11:08:58AutoCorres2: theory AutoCorres2.TypHeapSimple
11:08:58AutoCorres2_Main: theory AutoCorres2.Runs_To_VCG_StackPointer
11:08:58AutoCorres2_Main: theory AutoCorres2.Polish
11:09:01AutoCorres2: theory AutoCorres2.L1Peephole
11:09:02AutoCorres2: theory AutoCorres2.ExceptionRewrite
11:09:02Collections: theory Collections.SetStdImpl
11:09:03AutoCorres2: theory AutoCorres2.SimplConv
11:09:03AutoCorres2: theory AutoCorres2.L1Valid
11:09:04Finished CZH_Foundations/outline (0:01:09 elapsed time)
11:09:04Timing CZH_Foundations (4 threads, 304.077s elapsed time, 1047.105s cpu time, 75.338s GC time, factor 3.44)
11:09:04Finished CZH_Foundations (0:05:20 elapsed time, 0:17:55 cpu time, factor 3.35)
11:09:04Building CZH_Elementary_Categories ...
11:09:04AutoCorres2: theory AutoCorres2.L2Defs
11:09:07CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Introduction
11:09:08CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Category
11:09:09AutoCorres2: theory AutoCorres2.Split_Heap
11:09:12AutoCorres2: theory AutoCorres2.L2ExceptionRewrite
11:09:14AutoCorres2: theory AutoCorres2.L2Peephole
11:09:15AutoCorres2: theory AutoCorres2.Refines_Spec
11:09:15AutoCorres2: theory AutoCorres2.WordAbstract
11:09:18CakeML: theory CakeML.Compiler_Test
11:09:19AutoCorres2: theory AutoCorres2.WordPolish
11:09:19CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Functor
11:09:19AutoCorres2: theory AutoCorres2.LocalVarExtract
11:09:19AutoCorres2: theory AutoCorres2.Stack_Typing
11:09:20CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Category
11:09:22AutoCorres2: theory AutoCorres2.In_Out_Parameters
11:09:24Collections: theory Collections.ICF_Impl
11:09:24CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_GRPH
11:09:25AutoCorres2_Main: theory AutoCorres2.AutoCorres
11:09:29Collections: theory Collections.ICF_Refine_Monadic
11:09:29CakeML: theory CakeML.Code_Test_Haskell
11:09:30Collections: theory Collections.ICF_Autoref
11:09:37Collections: theory Collections.ICF_Entrypoints_Chapter
11:09:37Collections: theory Collections.Collections_Entrypoints_Chapter
11:09:37Collections: theory Collections.Userguides_Chapter
11:09:37Collections: theory Collections.Collections
11:09:37Collections: theory Collections.Refine_Dflt
11:09:38AutoCorres2: theory AutoCorres2.TypeStrengthen
11:09:38Collections: theory Collections.CollectionsV1
11:09:38Collections: theory Collections.ICF_Userguide
11:09:38Collections: theory Collections.Refine_Dflt_Only_ICF
11:09:39Collections: theory Collections.Refine_Monadic_Userguide
11:09:39Collections: theory Collections.Refine_Dflt_ICF
11:09:44AutoCorres2: theory AutoCorres2.HeapLift
11:09:56AutoCorres2_Main: theory AutoCorres2_Main.AutoCorres_Main
11:09:56AutoCorres2_Main: theory AutoCorres2_Main.AutoCorres_Nondet_Syntax
11:09:56CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Order
11:09:56CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_NTCF
11:09:57CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Subcategory
11:09:57CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_DG_CAT
11:09:58CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Rel
11:10:00CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Functor
11:10:08Finished HOL-Library/document (0:01:30 elapsed time)
11:10:08Preparing HOL-Library/outline ...
11:10:10AutoCorres2: theory AutoCorres2.Polish
11:10:11AutoCorres2: theory AutoCorres2.Runs_To_VCG_StackPointer
11:10:15CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Parallel
11:10:16CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_SS
11:10:24CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Par
11:10:26CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Order
11:10:31CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_PCategory
11:10:31CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Simple
11:10:33CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Ordinal
11:10:34CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_CSimplicial
11:10:34CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Comma
11:10:34CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Discrete
11:10:35CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_SemiCAT
11:10:37AutoCorres2: theory AutoCorres2.AutoCorres
11:10:37CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_SMC_CAT
11:10:38CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_CAT
11:10:39CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_NTCF
11:10:54CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Set
11:11:00CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Hom
11:11:00CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Structure_Example
11:11:01Preparing CakeML/document ...
11:11:01Finished HOL-Library/outline (0:00:53 elapsed time)
11:11:02CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_DG_FUNCT
11:11:02Timing HOL-Library (4 threads, 553.235s elapsed time, 1529.639s cpu time, 65.434s GC time, factor 2.76)
11:11:02Finished HOL-Library (0:10:10 elapsed time, 0:27:16 cpu time, factor 2.68)
11:11:02Building HOL-Computational_Algebra ...
11:11:05HOL-Computational_Algebra: theory HOL-Computational_Algebra.Factorial_Ring
11:11:05HOL-Computational_Algebra: theory HOL-Computational_Algebra.Group_Closure
11:11:05HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fraction_Field
11:11:09AutoCorres2: theory AutoCorres2.AutoCorresInfrastructure
11:11:09AutoCorres2: theory AutoCorres2.Chapter1_MinMax
11:11:09AutoCorres2: theory AutoCorres2.Chapter2_HoareHeap
11:11:12Finished CakeML/document (0:00:11 elapsed time)
11:11:12Preparing CakeML/outline ...
11:11:19Finished CakeML/outline (0:00:07 elapsed time)
11:11:20AutoCorres2: theory AutoCorres2.Chapter3_HoareHeap
11:11:20Timing CakeML (4 threads, 552.266s elapsed time, 1511.007s cpu time, 113.872s GC time, factor 2.74)
11:11:20Finished CakeML (0:10:08 elapsed time, 0:26:55 cpu time, factor 2.66)
11:11:20Building Core_SC_DOM ...
11:11:22AutoCorres2: theory AutoCorres2.In_Out_Parameters_Ex
11:11:22HOL-Computational_Algebra: theory HOL-Computational_Algebra.Euclidean_Algorithm
11:11:24CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_SMC_FUNCT
11:11:28CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_FUNCT
11:11:29AutoCorres2: theory AutoCorres2.fnptr
11:11:29AutoCorres2: theory AutoCorres2.open_struct
11:11:42HOL-Computational_Algebra: theory HOL-Computational_Algebra.Normalized_Fraction
11:11:42HOL-Computational_Algebra: theory HOL-Computational_Algebra.Primes
11:11:42HOL-Computational_Algebra: theory HOL-Computational_Algebra.Field_as_Ring
11:11:44CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Cone
11:11:46Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Basic_Datatypes
11:11:46Core_SC_DOM: theory Core_SC_DOM.Hiding_Type_Variables
11:11:46Core_SC_DOM: theory Core_SC_DOM.Testing_Utils
11:11:48Core_SC_DOM: theory Core_SC_DOM.Ref
11:11:48Core_SC_DOM: theory Core_SC_DOM.Heap_Error_Monad
11:11:48Core_SC_DOM: theory Core_SC_DOM.ObjectPointer
11:11:48Core_SC_DOM: theory Core_SC_DOM.BaseClass
11:11:49Core_SC_DOM: theory Core_SC_DOM.NodePointer
11:11:49Core_SC_DOM: theory Core_SC_DOM.ObjectClass
11:11:49Core_SC_DOM: theory Core_SC_DOM.ElementPointer
11:11:51Core_SC_DOM: theory Core_SC_DOM.CharacterDataPointer
11:11:52Core_SC_DOM: theory Core_SC_DOM.NodeClass
11:11:52Core_SC_DOM: theory Core_SC_DOM.DocumentPointer
11:11:52Core_SC_DOM: theory Core_SC_DOM.BaseMonad
11:11:53AutoCorres2: theory AutoCorres2.pointers_to_locals
11:11:54Core_SC_DOM: theory Core_SC_DOM.ShadowRootPointer
11:11:55HOL-Computational_Algebra: theory HOL-Computational_Algebra.Nth_Powers
11:11:55HOL-Computational_Algebra: theory HOL-Computational_Algebra.Squarefree
11:11:55HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Power_Series
11:11:55Core_SC_DOM: theory Core_SC_DOM.ObjectMonad
11:11:55HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial
11:11:55Core_SC_DOM: theory Core_SC_DOM.ElementClass
11:11:56Preparing Collections/document ...
11:11:56CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Yoneda
11:11:56Core_SC_DOM: theory Core_SC_DOM.NodeMonad
11:11:58Core_SC_DOM: theory Core_SC_DOM.CharacterDataClass
11:11:59Core_SC_DOM: theory Core_SC_DOM.ElementMonad
11:12:00Core_SC_DOM: theory Core_SC_DOM.DocumentClass
11:12:01Core_SC_DOM: theory Core_SC_DOM.CharacterDataMonad
11:12:03Core_SC_DOM: theory Core_SC_DOM.DocumentMonad
11:12:05Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Functions
11:12:06CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Small_Cone
11:12:10HOL-Computational_Algebra: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
11:12:10HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_FPS
11:12:10HOL-Computational_Algebra: theory HOL-Computational_Algebra.Polynomial_Factorial
11:12:12HOL-Computational_Algebra: theory HOL-Computational_Algebra.Formal_Laurent_Series
11:12:14AutoCorres2: theory AutoCorres2.union_ac
11:12:17HOL-Computational_Algebra: theory HOL-Computational_Algebra.Computational_Algebra
11:12:26Finished Collections/document (0:00:30 elapsed time)
11:12:26Preparing Collections/outline ...
11:12:33Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Heap_WF
11:12:44CZH_Elementary_Categories: theory CZH_Elementary_Categories.CZH_ECAT_Conclusions
11:12:46Finished Collections/outline (0:00:20 elapsed time)
11:12:46Preparing Collections/userguide ...
11:12:52Finished Collections/userguide (0:00:06 elapsed time)
11:12:53Timing Collections (4 threads, 477.792s elapsed time, 1335.308s cpu time, 84.657s GC time, factor 2.79)
11:12:53Finished Collections (0:09:36 elapsed time, 0:25:28 cpu time, factor 2.65)
11:12:53Building Abstract-Rewriting ...
11:13:02Abstract-Rewriting: theory Abstract-Rewriting.Seq
11:13:02Abstract-Rewriting: theory Regular-Sets.Regular_Set
11:13:06Core_SC_DOM: theory Core_SC_DOM.Core_DOM
11:13:06Core_SC_DOM: theory Core_SC_DOM.Core_DOM_BaseTest
11:13:08Abstract-Rewriting: theory Regular-Sets.Regular_Exp
11:13:14Abstract-Rewriting: theory Regular-Sets.NDerivative
11:13:14Abstract-Rewriting: theory Regular-Sets.Relation_Interpretation
11:13:17Core_SC_DOM: theory Core_SC_DOM.Document_adoptNode
11:13:18Core_SC_DOM: theory Core_SC_DOM.Document_getElementById
11:13:19Abstract-Rewriting: theory Regular-Sets.Equivalence_Checking
11:13:19Abstract-Rewriting: theory Regular-Sets.Regexp_Method
11:13:21Abstract-Rewriting: theory Abstract-Rewriting.Abstract_Rewriting
11:13:22Core_SC_DOM: theory Core_SC_DOM.Node_insertBefore
11:13:23Core_SC_DOM: theory Core_SC_DOM.Node_removeChild
11:13:23Core_SC_DOM: theory Core_SC_DOM.Core_DOM_Tests
11:13:24Abstract-Rewriting: theory Abstract-Rewriting.Relative_Rewriting
11:13:24Abstract-Rewriting: theory Abstract-Rewriting.SN_Orders
11:13:27Preparing HOL-Computational_Algebra/document ...
11:13:28Abstract-Rewriting: theory Abstract-Rewriting.SN_Order_Carrier
11:13:59Preparing Abstract-Rewriting/document ...
11:14:03Finished HOL-Computational_Algebra/document (0:00:36 elapsed time)
11:14:03Preparing HOL-Computational_Algebra/outline ...
11:14:10Finished Abstract-Rewriting/document (0:00:10 elapsed time)
11:14:10Preparing Abstract-Rewriting/outline ...
11:14:15Finished Abstract-Rewriting/outline (0:00:05 elapsed time)
11:14:15Timing Abstract-Rewriting (4 threads, 42.604s elapsed time, 116.209s cpu time, 2.956s GC time, factor 2.73)
11:14:15Finished Abstract-Rewriting (0:01:04 elapsed time, 0:02:30 cpu time, factor 2.33)
11:14:15Building First_Order_Terms ...
11:14:18First_Order_Terms: theory First_Order_Terms.Transitive_Closure_More
11:14:18First_Order_Terms: theory Fresh_Identifiers.Fresh
11:14:19First_Order_Terms: theory First_Order_Terms.Lists_are_Infinite
11:14:19First_Order_Terms: theory First_Order_Terms.Renaming2
11:14:19First_Order_Terms: theory First_Order_Terms.Renaming2_String
11:14:20First_Order_Terms: theory First_Order_Terms.Option_Monad
11:14:20First_Order_Terms: theory First_Order_Terms.Seq_More
11:14:20First_Order_Terms: theory First_Order_Terms.Fun_More
11:14:20Finished HOL-Computational_Algebra/outline (0:00:17 elapsed time)
11:14:20Timing HOL-Computational_Algebra (4 threads, 115.501s elapsed time, 333.802s cpu time, 6.929s GC time, factor 2.89)
11:14:20Finished HOL-Computational_Algebra (0:02:21 elapsed time, 0:06:15 cpu time, factor 2.65)
11:14:20Building HOL-Number_Theory ...
11:14:21First_Order_Terms: theory First_Order_Terms.Term
11:14:24HOL-Number_Theory: theory HOL-Number_Theory.Cong
11:14:24HOL-Number_Theory: theory HOL-Algebra.Congruence
11:14:24HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes
11:14:24HOL-Number_Theory: theory HOL-Number_Theory.Fib
11:14:24HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers
11:14:25First_Order_Terms: theory First_Order_Terms.Unifiers
11:14:25First_Order_Terms: theory First_Order_Terms.Term_Pair_Multiset
11:14:25First_Order_Terms: theory First_Order_Terms.Subsumption
11:14:25First_Order_Terms: theory First_Order_Terms.Subterm_and_Context
11:14:25First_Order_Terms: theory First_Order_Terms.Abstract_Matching
11:14:25First_Order_Terms: theory First_Order_Terms.Abstract_Unification
11:14:26HOL-Number_Theory: theory HOL-Algebra.Order
11:14:27HOL-Number_Theory: theory HOL-Number_Theory.Mod_Exp
11:14:27First_Order_Terms: theory First_Order_Terms.Unification
11:14:27HOL-Number_Theory: theory HOL-Number_Theory.Totient
11:14:28HOL-Number_Theory: theory HOL-Algebra.Lattice
11:14:29First_Order_Terms: theory First_Order_Terms.Matching
11:14:29First_Order_Terms: theory First_Order_Terms.Unification_String
11:14:30HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice
11:14:32HOL-Number_Theory: theory HOL-Algebra.Group
11:14:35HOL-Number_Theory: theory HOL-Algebra.Coset
11:14:36HOL-Number_Theory: theory HOL-Algebra.FiniteProduct
11:14:37HOL-Number_Theory: theory HOL-Algebra.Ring
11:14:38First_Order_Terms: theory Deriving.Generator_Aux
11:14:38First_Order_Terms: theory Deriving.Derive_Manager
11:14:38First_Order_Terms: theory Matrix.Utility
11:14:39First_Order_Terms: theory Show.Show
11:14:39First_Order_Terms: theory Polynomial_Factorization.Missing_List
11:14:39HOL-Number_Theory: theory HOL-Algebra.Generated_Groups
11:14:41HOL-Number_Theory: theory HOL-Algebra.Elementary_Groups
11:14:41First_Order_Terms: theory Show.Show_Instances
11:14:43First_Order_Terms: theory Show.Shows_Literal
11:14:43First_Order_Terms: theory First_Order_Terms.Position
11:14:43HOL-Number_Theory: theory HOL-Algebra.AbelCoset
11:14:43HOL-Number_Theory: theory HOL-Algebra.Module
11:14:45First_Order_Terms: theory First_Order_Terms.Term_More
11:14:50HOL-Number_Theory: theory HOL-Algebra.Ideal
11:14:54HOL-Number_Theory: theory HOL-Algebra.RingHom
11:14:57HOL-Number_Theory: theory HOL-Algebra.UnivPoly
11:15:17HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group
11:15:23HOL-Number_Theory: theory HOL-Number_Theory.Residues
11:15:27HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion
11:15:27HOL-Number_Theory: theory HOL-Number_Theory.Pocklington
11:15:27Preparing First_Order_Terms/document ...
11:15:27HOL-Number_Theory: theory HOL-Number_Theory.Gauss
11:15:28HOL-Number_Theory: theory HOL-Number_Theory.Residue_Primitive_Roots
11:15:28HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity
11:15:29HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory
11:15:41Finished First_Order_Terms/document (0:00:13 elapsed time)
11:15:41Preparing First_Order_Terms/outline ...
11:15:48Finished First_Order_Terms/outline (0:00:07 elapsed time)
11:15:48Timing First_Order_Terms (4 threads, 44.082s elapsed time, 144.498s cpu time, 4.451s GC time, factor 3.28)
11:15:48Finished First_Order_Terms (0:01:10 elapsed time, 0:03:08 cpu time, factor 2.68)
11:15:49Building HOL-Algebra ...
11:15:52HOL-Algebra: theory HOL-Algebra.README
11:15:52HOL-Algebra: theory HOL-Cardinals.Fun_More
11:15:52HOL-Algebra: theory HOL-Cardinals.Order_Union
11:15:52HOL-Algebra: theory HOL-Cardinals.Order_Relation_More
11:15:52HOL-Algebra: theory HOL-Combinatorics.Transposition
11:15:52HOL-Algebra: theory HOL-Algebra.Exponent
11:15:52HOL-Algebra: theory HOL-Algebra.Congruence
11:15:52HOL-Algebra: theory HOL-Combinatorics.Permutations
11:15:53HOL-Algebra: theory HOL-Cardinals.Wellfounded_More
11:15:53HOL-Algebra: theory HOL-Cardinals.Wellorder_Relation
11:15:53HOL-Algebra: theory HOL-Cardinals.Wellorder_Embedding
11:15:53HOL-Algebra: theory HOL-Cardinals.Wellorder_Constructions
11:15:55HOL-Algebra: theory HOL-Algebra.Order
11:15:55HOL-Algebra: theory HOL-Combinatorics.Cycles
11:15:55HOL-Algebra: theory HOL-Combinatorics.List_Permutation
11:15:55HOL-Algebra: theory HOL-Cardinals.Cardinal_Order_Relation
11:15:59HOL-Algebra: theory HOL-Algebra.Lattice
11:15:59HOL-Algebra: theory HOL-Cardinals.Cardinal_Arithmetic
11:16:00HOL-Algebra: theory HOL-Algebra.Complete_Lattice
11:16:01Timing AutoCorres2_Main (4 threads, 624.714s elapsed time, 2235.602s cpu time, 58.596s GC time, factor 3.58)
11:16:01Finished AutoCorres2_Main (0:11:55 elapsed time, 0:40:06 cpu time, factor 3.37)
11:16:01Running AutoCorres2_Test ...
11:16:01HOL-Algebra: theory HOL-Algebra.Galois_Connection
11:16:01HOL-Algebra: theory HOL-Algebra.Group
11:16:03HOL-Algebra: theory HOL-Algebra.Bij
11:16:03HOL-Algebra: theory HOL-Algebra.Coset
11:16:03HOL-Algebra: theory HOL-Algebra.FiniteProduct
11:16:04HOL-Algebra: theory HOL-Algebra.Ring
11:16:06AutoCorres2_Test: theory AutoCorres2_Test.Match_Cterm_Ex
11:16:06AutoCorres2_Test: theory AutoCorres2_Test.DataStructures
11:16:06AutoCorres2_Test: theory HOL-Computational_Algebra.Factorial_Ring
11:16:06AutoCorres2_Test: theory HOL-Library.Product_Lexorder
11:16:06AutoCorres2_Test: theory AutoCorres2_Test.AC_Rename
11:16:06AutoCorres2_Test: theory AutoCorres2_Test.Alloc_Ex
11:16:06HOL-Algebra: theory HOL-Algebra.Group_Action
11:16:06HOL-Algebra: theory HOL-Algebra.Left_Coset
11:16:06HOL-Algebra: theory HOL-Algebra.SimpleGroups
11:16:07HOL-Algebra: theory HOL-Algebra.SndIsomorphismGrp
11:16:07HOL-Algebra: theory HOL-Algebra.Sylow
11:16:07AutoCorres2_Test: theory AutoCorres2_Test.Asm_Labels
11:16:08HOL-Algebra: theory HOL-Algebra.Generated_Groups
11:16:09HOL-Algebra: theory HOL-Algebra.Zassenhaus
11:16:09HOL-Algebra: theory HOL-Algebra.Divisibility
11:16:10HOL-Algebra: theory HOL-Algebra.Solvable_Groups
11:16:10HOL-Algebra: theory HOL-Algebra.Elementary_Groups
11:16:10HOL-Algebra: theory HOL-Algebra.Sym_Groups
11:16:13HOL-Algebra: theory HOL-Algebra.AbelCoset
11:16:13HOL-Algebra: theory HOL-Algebra.Module
11:16:13HOL-Algebra: theory HOL-Algebra.Exact_Sequence
11:16:14HOL-Algebra: theory HOL-Algebra.Product_Groups
11:16:14HOL-Algebra: theory HOL-Algebra.Free_Abelian_Groups
11:16:19HOL-Algebra: theory HOL-Algebra.Ideal
11:16:20AutoCorres2_Test: theory AutoCorres2_Test.BinarySearch
11:16:20AutoCorres2_Test: theory AutoCorres2_Test.CList
11:16:24HOL-Algebra: theory HOL-Algebra.Ideal_Product
11:16:24HOL-Algebra: theory HOL-Algebra.RingHom
11:16:25AutoCorres2_Test: theory HOL-Computational_Algebra.Euclidean_Algorithm
11:16:26HOL-Algebra: theory HOL-Algebra.QuotRing
11:16:26HOL-Algebra: theory HOL-Algebra.UnivPoly
11:16:31HOL-Algebra: theory HOL-Algebra.IntRing
11:16:31HOL-Algebra: theory HOL-Algebra.Weak_Morphisms
11:16:33HOL-Algebra: theory HOL-Algebra.Chinese_Remainder
11:16:40AutoCorres2_Test: theory AutoCorres2_Test.ConditionGuard
11:16:45Preparing HOL-Number_Theory/document ...
11:16:47AutoCorres2_Test: theory HOL-Computational_Algebra.Primes
11:16:50AutoCorres2_Test: theory AutoCorres2_Test.CustomWordAbs
11:16:53HOL-Algebra: theory HOL-Algebra.Multiplicative_Group
11:16:55Finished HOL-Number_Theory/document (0:00:09 elapsed time)
11:16:55Preparing HOL-Number_Theory/outline ...
11:16:57HOL-Algebra: theory HOL-Algebra.Ring_Divisibility
11:16:57HOL-Algebra: theory HOL-Algebra.Subrings
11:16:59Finished HOL-Number_Theory/outline (0:00:04 elapsed time)
11:16:59Timing HOL-Number_Theory (4 threads, 113.228s elapsed time, 407.401s cpu time, 13.147s GC time, factor 3.60)
11:16:59Finished HOL-Number_Theory (0:02:22 elapsed time, 0:07:35 cpu time, factor 3.19)
11:16:59Running Crypto_Standards ...
11:16:59AutoCorres2_Test: theory AutoCorres2_Test.EvaluationOrder
11:17:00AutoCorres2_Test: theory AutoCorres2_Test.Exception_Rewriting
11:17:01HOL-Algebra: theory HOL-Algebra.Embedded_Algebras
11:17:01HOL-Algebra: theory HOL-Algebra.Generated_Rings
11:17:02HOL-Algebra: theory HOL-Algebra.Generated_Fields
11:17:03Crypto_Standards: theory Crypto_Standards.More_Bit_Operations_Nat
11:17:03Crypto_Standards: theory HOL-Decision_Procs.Conversions
11:17:03Crypto_Standards: theory HOL-Decision_Procs.Algebra_Aux
11:17:03Crypto_Standards: theory Crypto_Standards.Words
11:17:04AutoCorres2_Test: theory AutoCorres2_Test.FactorialTest
11:17:06Crypto_Standards: theory HOL-Decision_Procs.Commutative_Ring
11:17:06Crypto_Standards: theory Crypto_Standards.More_Residues
11:17:08Crypto_Standards: theory Crypto_Standards.FIPS180_4
11:17:09Crypto_Standards: theory Crypto_Standards.PKCS1v2_2
11:17:14HOL-Algebra: theory HOL-Algebra.Polynomials
11:17:15AutoCorres2_Test: theory AutoCorres2_Test.FibProof
11:17:18AutoCorres2_Test: theory AutoCorres2_Test.FunctionInfoDemo
11:17:18Crypto_Standards: theory Crypto_Standards.FIPS180_4_Test_Vectors
11:17:24Crypto_Standards: theory HOL-Decision_Procs.Reflective_Field
11:17:24Crypto_Standards: theory Crypto_Standards.Efficient_Mod_Exp
11:17:25Crypto_Standards: theory Crypto_Standards.PKCS1v2_2_Interpretations
11:17:29Crypto_Standards: theory Crypto_Standards.FIPS198_1
11:17:31Crypto_Standards: theory Crypto_Standards.FIPS198_1_Test_Vectors
11:17:32AutoCorres2_Test: theory AutoCorres2_Test.Global_Structs
11:17:33AutoCorres2_Test: theory AutoCorres2_Test.Guard_Simp
11:17:39Crypto_Standards: theory Crypto_Standards.PKCS1v2_2_Test_Vectors
11:17:39HOL-Algebra: theory HOL-Algebra.Polynomial_Divisibility
11:17:40Crypto_Standards: theory Elliptic_Curves_Group_Law.Elliptic_Locale
11:17:47AutoCorres2_Test: theory AutoCorres2_Test.HeapWrap
11:17:47Crypto_Standards: theory Elliptic_Curves_Group_Law.Elliptic_Test
11:17:54AutoCorres2_Test: theory AutoCorres2_Test.In_Out_Parameters_Slow
11:17:55Crypto_Standards: theory Crypto_Standards.EC_Common
11:18:09Crypto_Standards: theory Crypto_Standards.SEC1v2_0
11:18:21HOL-Algebra: theory HOL-Algebra.Finite_Extensions
11:18:21HOL-Algebra: theory HOL-Algebra.Indexed_Polynomials
11:18:30Crypto_Standards: theory Crypto_Standards.Crypto_Standards
11:18:30Crypto_Standards: theory Crypto_Standards.Efficient_SEC1
11:18:34Preparing Core_SC_DOM/document ...
11:18:36FATAL: Unable to delete script file /tmp/jenkins4015888800386434878.sh
11:18:36Command Close created at
11:18:36 at hudson.remoting.Command.<init>(Command.java:70)
11:18:36 at hudson.remoting.Channel$CloseCommand.<init>(Channel.java:1309)
11:18:36 at hudson.remoting.Channel.close(Channel.java:1483)
11:18:36 at hudson.remoting.Channel.close(Channel.java:1450)
11:18:36 at hudson.remoting.Channel$CloseCommand.execute(Channel.java:1315)
11:18:36 at hudson.remoting.Channel$1.handle(Channel.java:609)
11:18:36 at hudson.remoting.SynchronousCommandTransport$ReaderThread.run(SynchronousCommandTransport.java:81)
11:18:36Caused: hudson.remoting.Channel$OrderlyShutdown
11:18:36 at hudson.remoting.Channel$CloseCommand.execute(Channel.java:1316)
11:18:36 at hudson.remoting.Channel$1.handle(Channel.java:609)
11:18:36 at hudson.remoting.SynchronousCommandTransport$ReaderThread.run(SynchronousCommandTransport.java:81)
11:18:36Caused: hudson.remoting.ChannelClosedException: Channel "hudson.remoting.Channel@2ae79fc2:workermta1": Remote call on workermta1 failed. The channel is closing down or has closed down
11:18:36 at hudson.remoting.Channel.call(Channel.java:996)
11:18:36 at hudson.FilePath.act(FilePath.java:1230)
11:18:36 at hudson.FilePath.act(FilePath.java:1219)
11:18:36 at hudson.FilePath.delete(FilePath.java:1766)
11:18:36 at hudson.tasks.CommandInterpreter.perform(CommandInterpreter.java:163)
11:18:36 at hudson.tasks.CommandInterpreter.perform(CommandInterpreter.java:92)
11:18:36 at hudson.tasks.BuildStepMonitor$1.perform(BuildStepMonitor.java:20)
11:18:36 at hudson.model.AbstractBuild$AbstractBuildExecution.perform(AbstractBuild.java:818)
11:18:36 at hudson.model.Build$BuildExecution.build(Build.java:199)
11:18:36 at hudson.model.Build$BuildExecution.doRun(Build.java:164)
11:18:36 at hudson.model.AbstractBuild$AbstractBuildExecution.run(AbstractBuild.java:526)
11:18:36 at hudson.model.Run.execute(Run.java:1895)
11:18:36 at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44)
11:18:36 at hudson.model.ResourceController.execute(ResourceController.java:101)
11:18:36 at hudson.model.Executor.run(Executor.java:442)
11:18:36Build was aborted
11:18:38ERROR: Failed to evaluate groovy script.
11:18:38java.lang.NullPointerException: Cannot invoke method child() on null object
11:18:38 at org.codehaus.groovy.runtime.NullObject.invokeMethod(NullObject.java:91)
11:18:38 at org.codehaus.groovy.runtime.callsite.PogoMetaClassSite.call(PogoMetaClassSite.java:47)
11:18:38 at org.codehaus.groovy.runtime.callsite.CallSiteArray.defaultCall(CallSiteArray.java:47)
11:18:38 at org.codehaus.groovy.runtime.callsite.NullCallSite.call(NullCallSite.java:34)
11:18:38 at org.codehaus.groovy.runtime.callsite.CallSiteArray.defaultCall(CallSiteArray.java:47)
11:18:38 at org.codehaus.groovy.runtime.callsite.AbstractCallSite.call(AbstractCallSite.java:116)
11:18:38 at org.codehaus.groovy.runtime.callsite.AbstractCallSite.call(AbstractCallSite.java:128)
11:18:38 at Script1.run(Script1.groovy:4)
11:18:38 at groovy.lang.GroovyShell.evaluate(GroovyShell.java:574)
11:18:38 at groovy.lang.GroovyShell.evaluate(GroovyShell.java:612)
11:18:38 at groovy.lang.GroovyShell.evaluate(GroovyShell.java:583)
11:18:38 at org.jenkinsci.plugins.scriptsecurity.sandbox.groovy.SecureGroovyScript.evaluate(SecureGroovyScript.java:373)
11:18:38 at org.jenkinsci.plugins.scriptsecurity.sandbox.groovy.SecureGroovyScript.evaluate(SecureGroovyScript.java:310)
11:18:38 at org.jvnet.hudson.plugins.groovypostbuild.GroovyPostbuildRecorder.perform(GroovyPostbuildRecorder.java:434)
11:18:38 at hudson.tasks.BuildStepMonitor$1.perform(BuildStepMonitor.java:20)
11:18:38 at hudson.model.AbstractBuild$AbstractBuildExecution.perform(AbstractBuild.java:818)
11:18:38 at hudson.model.AbstractBuild$AbstractBuildExecution.performAllBuildSteps(AbstractBuild.java:767)
11:18:38 at hudson.model.Build$BuildExecution.post2(Build.java:179)
11:18:38 at hudson.model.AbstractBuild$AbstractBuildExecution.post(AbstractBuild.java:711)
11:18:38 at hudson.model.Run.execute(Run.java:1918)
11:18:38 at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44)
11:18:38 at hudson.model.ResourceController.execute(ResourceController.java:101)
11:18:38 at hudson.model.Executor.run(Executor.java:442)
11:18:39FATAL: Expected 1 instance of hudson.model.User$AllUsers but got 0
11:18:39java.lang.IllegalStateException: Expected 1 instance of hudson.model.User$AllUsers but got 0
11:18:39 at hudson.ExtensionList.lookupSingleton(ExtensionList.java:457)
11:18:39 at hudson.model.User$AllUsers.getInstance(User.java:1104)
11:18:39 at hudson.model.User$AllUsers.get(User.java:1122)
11:18:39 at hudson.model.User.getOrCreateById(User.java:541)
11:18:39 at hudson.model.User.getById(User.java:644)
11:18:39 at jenkins.scm.RunWithSCM$1$1.adapt(RunWithSCM.java:105)
11:18:39 at jenkins.scm.RunWithSCM$1$1.adapt(RunWithSCM.java:101)
11:18:39 at hudson.util.AdaptedIterator.next(AdaptedIterator.java:57)
11:18:39 at java.base/java.util.AbstractCollection.addAll(AbstractCollection.java:335)
11:18:39 at jenkins.scm.RunWithSCM.calculateCulprits(RunWithSCM.java:133)
11:18:39 at hudson.model.AbstractBuild.calculateCulprits(AbstractBuild.java:353)
11:18:39 at jenkins.scm.RunWithSCM.getCulprits(RunWithSCM.java:93)
11:18:39 at hudson.model.AbstractBuild.getCulprits(AbstractBuild.java:342)
11:18:39 at hudson.model.AbstractBuild$AbstractBuildExecution.post(AbstractBuild.java:715)
11:18:39 at hudson.model.Run.execute(Run.java:1918)
11:18:39 at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44)
11:18:39 at hudson.model.ResourceController.execute(ResourceController.java:101)
11:18:39 at hudson.model.Executor.run(Executor.java:442)
11:18:40FATAL: Jenkins.instance is missing. Read the documentation of Jenkins.getInstanceOrNull to see what you are doing wrong.
11:18:40java.lang.IllegalStateException: Jenkins.instance is missing. Read the documentation of Jenkins.getInstanceOrNull to see what you are doing wrong.
11:18:40 at jenkins.model.Jenkins.get(Jenkins.java:819)
11:18:40 at hudson.tasks.BuildTrigger.execute(BuildTrigger.java:274)
11:18:40 at hudson.model.AbstractBuild$AbstractBuildExecution.cleanUp(AbstractBuild.java:728)
11:18:40 at hudson.model.Build$BuildExecution.cleanUp(Build.java:194)
11:18:40 at hudson.model.Run.execute(Run.java:1938)
11:18:40 at hudson.model.FreeStyleBuild.run(FreeStyleBuild.java:44)
11:18:40 at hudson.model.ResourceController.execute(ResourceController.java:101)
11:18:40 at hudson.model.Executor.run(Executor.java:442)
11:18:40Finished: FAILURE