Skipping 4 KB.. Full Log

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