Skipping 2 KB.. Full Log

### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/stack-2.15.1"
01:37:03 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/verit-2021.06.2-rmx-1"
01:37:03 Getting "https://isabelle.sketis.net/components/javamail-20240109.tar.gz"
01:37:04 Unpacking "/media/data/jenkins/.isabelle/contrib/javamail-20240109.tar.gz"
01:37:04 Getting "https://isabelle.sketis.net/components/jdk-21.0.2.tar.gz"
01:37:12 Unpacking "/media/data/jenkins/.isabelle/contrib/jdk-21.0.2.tar.gz"
01:37:29 Getting "https://isabelle.sketis.net/components/llncs-2.23.tar.gz"
01:37:29 Unpacking "/media/data/jenkins/.isabelle/contrib/llncs-2.23.tar.gz"
01:37:29 Getting "https://isabelle.sketis.net/components/postgresql-42.7.1.tar.gz"
01:37:29 Unpacking "/media/data/jenkins/.isabelle/contrib/postgresql-42.7.1.tar.gz"
01:37:30 Getting "https://isabelle.sketis.net/components/sqlite-jdbc-3.45.0.0.tar.gz"
01:37:30 Unpacking "/media/data/jenkins/.isabelle/contrib/sqlite-jdbc-3.45.0.0.tar.gz"
01:37:31 Getting "https://isabelle.sketis.net/components/stack-2.15.1.tar.gz"
01:37:31 Unpacking "/media/data/jenkins/.isabelle/contrib/stack-2.15.1.tar.gz"
01:37:35 Getting "https://isabelle.sketis.net/components/verit-2021.06.2-rmx-1.tar.gz"
01:37:35 Unpacking "/media/data/jenkins/.isabelle/contrib/verit-2021.06.2-rmx-1.tar.gz"
01:37:35 + bin/isabelle jedit -bf
01:37:36 ### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle.jar) ...
01:38:36 ### Building Demo (/media/data/jenkins/workspace/isabelle-nightly-slow/src/Tools/Demo/lib/demo.jar) ...
01:38:37 ### Building graph browser (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle_graphbrowser.jar) ...
01:38:38 Note: Some input files use unchecked or unsafe operations.
01:38:38 Note: Recompile with -Xlint:unchecked for details.
01:38:38 ### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle_admin.jar) ...
01:38:38 ### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-nightly-slow/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
01:38:42 + bin/isabelle ocaml_setup
01:38:42 # Run eval $(opam env) to update the current shell environment
01:38:43 [NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
01:38:43        opam update
01:38:43 
01:38:44 [NOTE] Package zarith is already installed (current version is 1.12).
01:38:44 + bin/isabelle ghc_setup
01:38:46 Preparing to install GHC (tinfo6) to an isolated location. This will not interfere with any
01:38:46 system-level installation.
01:38:46 Preparing to download ghc-tinfo6-9.6.3 ...
01:38:46 ghc-tinfo6-9.6.3: download has begun
01:38:47 ghc-tinfo6-9.6.3:   67.06 MiB / 193.64 MiB ( 34.63%) downloaded...
01:38:48 ghc-tinfo6-9.6.3:  140.39 MiB / 193.64 MiB ( 72.50%) downloaded...
01:38:49 ghc-tinfo6-9.6.3:  193.64 MiB / 193.64 MiB (100.00%) downloaded...
01:38:49 Downloaded ghc-tinfo6-9.6.3.
01:38:49 Unpacking GHC into /media/data/jenkins/.stack/programs/x86_64-linux/ghc-tinfo6-9.6.3.temp/ ...
01:39:10 Configuring GHC ...
01:39:16 /media/data/jenkins/.stack/programs/x86_64-linux/ghc-tinfo6-9.6.3.temp/ghc-9.6.3-x86_64-unknown-linux/configure: line 6576: FP_PROG_LD_BUILD_ID: command not found
01:39:21 ar: conftest.a: No such file or directory
01:39:22 Installing GHC ...
01:43:08 Installed GHC.
01:43:10 Stack will use a sandboxed GHC it installed. To use this GHC and packages outside of a project,
01:43:10 consider using: stack ghc, stack ghci, stack runghc, or stack exec.
01:43:11 The Glorious Glasgow Haskell Compilation System, version 9.6.3
01:43:12 + bin/isabelle ci_build slow
01:43:15 
01:43:15 === CONFIGURATION ===
01:43:15 
01:43:15 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
01:43:15 ISABELLE_BUILD_OPTIONS=""
01:43:15 
01:43:15 ML_PLATFORM="x86_64-linux"
01:43:15 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.9.1/x86_64-linux"
01:43:15 ML_SYSTEM="polyml-5.9.1"
01:43:15 ML_OPTIONS="-H 4000 --maxheap 32G"
01:43:15 jobs = 1, threads = 8, numa = false
01:43:15 
01:43:15 === BUILD ===
01:43:15 
01:43:15 Build started at Thu, 29 Feb 2024 00:43:14 GMT
01:43:15 Isabelle id 513829904beb
01:43:15 Build for AFP id ef55afaa373b
01:43:15 
01:43:15 === LOG ===
01:43:15 
01:43:18 Session Pure/Pure
01:43:19 Session FOL/FOL
01:43:19 Session Pure/Pure-Examples
01:43:19 Session Pure/Pure-ex
01:43:19 Session Misc/Tools
01:43:19 Session HOL/HOL (main)
01:43:20 Session AFP/AWN (AFP)
01:43:20 Session AFP/AODV (AFP slow)
01:43:21 Session HOL/HOL-Cardinals (timing)
01:43:21 Session HOL/HOL-Library (main timing)
01:43:21 Session AFP/Binomial-Heaps (AFP)
01:43:21 Session AFP/ConcurrentIMP (AFP)
01:43:21 Session AFP/ConcurrentGC (AFP slow)
01:43:21 Session AFP/FinFun (AFP)
01:43:21 Session AFP/Finger-Trees (AFP)
01:43:21 Session HOL/HOL-Combinatorics (main timing)
01:43:22 Session HOL/HOL-Computational_Algebra (main timing)
01:43:22 Session HOL/HOL-Algebra (main timing)
01:43:22 Session HOL/HOL-Decision_Procs (timing)
01:43:23 Session HOL/HOL-Number_Theory (main timing)
01:43:23 Session HOL/HOL-ex (timing)
01:43:23 Session HOL/HOL-Imperative_HOL (timing)
01:43:23 Session AFP/HereditarilyFinite (AFP)
01:43:23 Session AFP/Trie (AFP)
01:43:23 Session AFP/Flyspeck-Tame (AFP)
01:43:24 Session AFP/Flyspeck-Tame-Computation (AFP slow very_slow)
01:43:24 Session HOL/HOL-Real_Asymp
01:43:24 Session HOL/HOL-Analysis (main timing)
01:43:25 Session AFP/Coinductive (AFP)
01:43:26 Session HOL/HOL-Eisbach
01:43:26 Session AFP/Automatic_Refinement (AFP)
01:43:26 Session AFP/Refine_Monadic (AFP)
01:43:26 Session AFP/Triangle (AFP)
01:43:26 Session HOL/HOL-Types_To_Sets
01:43:26 Session AFP/List-Index (AFP)
01:43:26 Session AFP/Word_Lib (AFP)
01:43:27 Session AFP/IP_Addresses (AFP)
01:43:27 Session AFP/Simple_Firewall (AFP)
01:43:27 Session AFP/Routing (AFP)
01:43:27 Session AFP/Native_Word (AFP)
01:43:27 Session AFP/Collections (AFP)
01:43:27 Session AFP/Deriving (AFP)
01:43:27 Session AFP/Show (AFP)
01:43:27 Session AFP/Affine_Arithmetic (AFP)
01:43:28 Session AFP/Ordinary_Differential_Equations (AFP)
01:43:28 Session AFP/HOL-ODE-Numerics (AFP)
01:43:29 Session AFP/Lorenz_Approximation (AFP)
01:43:29 Session AFP/Lorenz_C1 (AFP slow very_slow)
01:43:29 Session AFP/Iptables_Semantics (AFP)
01:43:29 Session AFP/Iptables_Semantics_Examples (AFP)
01:43:29 Session AFP/Iptables_Semantics_Examples_Big (AFP slow very_slow)
01:43:29 Session AFP/JinjaThreads (AFP slow)
01:43:30 Session AFP/ZFC_in_HOL (AFP)
01:43:31 Session AFP/Category3 (AFP)
01:43:31 Session AFP/MonoidalCategory (AFP)
01:43:31 Session AFP/Bicategory (AFP slow)
01:43:32 Building Pure ...
01:43:56 Pure: theory Pure
01:43:57 Pure: theory ML_Bootstrap
01:43:57 Pure: theory Pure.Sessions
01:44:00 Timing Pure (1 threads, 1.009s elapsed time, 1.073s cpu time, 0.000s GC time, factor 1.06)
01:44:00 Finished Pure (0:00:26 elapsed time, 0:00:26 cpu time, factor 0.99)
01:44:00 Building HOL ...
01:44:04 HOL: theory Tools.Code_Generator
01:44:09 HOL: theory HOL.HOL
01:44:15 HOL: theory HOL.Argo
01:44:15 HOL: theory HOL.Ctr_Sugar
01:44:15 HOL: theory HOL.Orderings
01:44:18 HOL: theory HOL.Groups
01:44:20 HOL: theory HOL.SAT
01:44:22 HOL: theory HOL.Lattices
01:44:24 HOL: theory HOL.Boolean_Algebras
01:44:25 HOL: theory HOL.Set
01:44:27 HOL: theory HOL.Fun
01:44:27 HOL: theory HOL.Typedef
01:44:29 HOL: theory HOL.Complete_Lattices
01:44:29 HOL: theory HOL.Rings
01:44:32 HOL: theory HOL.Inductive
01:44:36 HOL: theory HOL.Product_Type
01:44:36 HOL: theory HOL.Sum_Type
01:44:37 HOL: theory HOL.Complete_Partial_Order
01:44:46 HOL: theory HOL.Nat
01:44:49 HOL: theory HOL.Fields
01:44:49 HOL: theory HOL.Meson
01:44:55 HOL: theory HOL.Relation
01:44:57 HOL: theory HOL.Finite_Set
01:44:59 HOL: theory HOL.Transitive_Closure
01:45:01 HOL: theory HOL.Wellfounded
01:45:01 HOL: theory HOL.Fun_Def_Base
01:45:01 HOL: theory HOL.Hilbert_Choice
01:45:01 HOL: theory HOL.Wfrec
01:45:02 HOL: theory HOL.Order_Relation
01:45:03 HOL: theory HOL.BNF_Wellorder_Relation
01:45:03 HOL: theory HOL.BNF_Wellorder_Embedding
01:45:03 HOL: theory HOL.Zorn
01:45:03 HOL: theory HOL.ATP
01:45:05 HOL: theory HOL.BNF_Wellorder_Constructions
01:45:06 HOL: theory HOL.BNF_Cardinal_Order_Relation
01:45:08 HOL: theory HOL.BNF_Cardinal_Arithmetic
01:45:10 HOL: theory HOL.BNF_Def
01:45:10 HOL: theory HOL.Metis
01:45:15 HOL: theory HOL.BNF_Composition
01:45:15 HOL: theory HOL.Basic_BNFs
01:45:16 HOL: theory HOL.BNF_Fixpoint_Base
01:45:21 HOL: theory HOL.BNF_Least_Fixpoint
01:45:26 HOL: theory HOL.Basic_BNF_LFPs
01:45:26 HOL: theory HOL.Equiv_Relations
01:45:26 HOL: theory HOL.Transfer
01:45:27 HOL: theory HOL.Lifting
01:45:27 HOL: theory HOL.Num
01:45:30 HOL: theory HOL.Option
01:45:31 HOL: theory HOL.Quotient
01:45:31 HOL: theory HOL.Extraction
01:45:31 HOL: theory HOL.Partial_Function
01:45:32 HOL: theory HOL.Fun_Def
01:45:32 HOL: theory HOL.Power
01:45:37 HOL: theory HOL.Groups_Big
01:45:41 HOL: theory HOL.Int
01:45:41 HOL: theory HOL.Lifting_Set
01:45:41 HOL: theory HOL.Lattices_Big
01:45:46 HOL: theory HOL.Euclidean_Rings
01:45:56 HOL: theory HOL.Parity
01:46:09 HOL: theory HOL.Divides
01:46:09 HOL: theory HOL.Numeral_Simprocs
01:46:09 HOL: theory HOL.Set_Interval
01:46:11 HOL: theory HOL.SMT
01:46:11 HOL: theory HOL.Semiring_Normalization
01:46:14 HOL: theory HOL.Groebner_Basis
01:46:17 HOL: theory HOL.Conditionally_Complete_Lattices
01:46:17 HOL: theory HOL.Presburger
01:46:17 HOL: theory HOL.Filter
01:46:22 HOL: theory HOL.Sledgehammer
01:46:27 HOL: theory HOL.List
01:46:43 HOL: theory HOL.Map
01:46:43 HOL: theory HOL.Groups_List
01:46:47 HOL: theory HOL.Bit_Operations
01:46:47 HOL: theory HOL.Enum
01:46:47 HOL: theory HOL.Factorial
01:46:49 HOL: theory HOL.Binomial
01:47:21 HOL: theory HOL.Code_Numeral
01:47:23 HOL: theory HOL.GCD
01:47:23 HOL: theory HOL.String
01:47:23 HOL: theory HOL.Random
01:47:28 HOL: theory HOL.BNF_Greatest_Fixpoint
01:47:28 HOL: theory HOL.Predicate
01:47:28 HOL: theory HOL.Typerep
01:47:31 HOL: theory HOL.Lazy_Sequence
01:47:32 HOL: theory HOL.Limited_Sequence
01:47:32 HOL: theory HOL.Code_Evaluation
01:47:34 HOL: theory HOL.Quickcheck_Random
01:47:38 HOL: theory HOL.Quickcheck_Exhaustive
01:47:38 HOL: theory HOL.Random_Pred
01:47:38 HOL: theory HOL.Quickcheck_Narrowing
01:47:39 HOL: theory HOL.Random_Sequence
01:47:44 HOL: theory HOL.Record
01:47:44 HOL: theory HOL.Predicate_Compile
01:47:46 HOL: theory HOL.Nitpick
01:47:48 HOL: theory HOL.Mirabelle
01:47:55 HOL: theory HOL.Nunchaku
01:47:57 HOL: theory Main
01:47:58 HOL: theory HOL.Archimedean_Field
01:47:58 HOL: theory HOL.Hull
01:47:58 HOL: theory HOL.Topological_Spaces
01:47:58 HOL: theory HOL.Modules
01:48:00 HOL: theory HOL.Vector_Spaces
01:48:10 HOL: theory HOL.Rat
01:48:13 HOL: theory HOL.Real
01:48:16 HOL: theory HOL.Real_Vector_Spaces
01:48:40 HOL: theory HOL.Inequalities
01:48:40 HOL: theory HOL.Limits
01:48:50 HOL: theory HOL.Deriv
01:48:50 HOL: theory HOL.Series
01:48:54 HOL: theory HOL.NthRoot
01:48:55 HOL: theory HOL.Transcendental
01:49:08 HOL: theory HOL.Complex
01:49:08 HOL: theory HOL.MacLaurin
01:49:10 HOL: theory Complex_Main
01:50:35 Preparing HOL/document ...
01:52:33 Finished HOL/document (0:01:57 elapsed time)
01:52:33 Preparing HOL/outline ...
01:53:38 Finished HOL/outline (0:01:04 elapsed time)
01:53:40 Timing HOL (8 threads, 360.489s elapsed time, 1350.079s cpu time, 264.559s GC time, factor 3.75)
01:53:40 Finished HOL (0:06:24 elapsed time, 0:23:19 cpu time, factor 3.64)
01:53:40 Running JinjaThreads ...
01:53:42 JinjaThreads: theory Automatic_Refinement.Prio_List
01:53:42 JinjaThreads: theory HOL-Eisbach.Eisbach
01:53:42 JinjaThreads: theory Automatic_Refinement.Foldi
01:53:42 JinjaThreads: theory Collections.ICF_Tools
01:53:42 JinjaThreads: theory Finger-Trees.FingerTree
01:53:42 JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1
01:53:42 JinjaThreads: theory HOL-Library.Adhoc_Overloading
01:53:42 JinjaThreads: theory HOL-Library.AList
01:53:42 JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot
01:53:42 JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot
01:53:42 JinjaThreads: theory Collections.Ord_Code_Preproc
01:53:42 JinjaThreads: theory HOL-Library.Cancellation
01:53:43 JinjaThreads: theory HOL-Library.Monad_Syntax
01:53:43 JinjaThreads: theory Automatic_Refinement.Refine_Util
01:53:43 JinjaThreads: theory Collections.Locale_Code
01:53:43 JinjaThreads: theory Collections.Record_Intf
01:53:43 JinjaThreads: theory HOL-Library.Case_Converter
01:53:43 JinjaThreads: theory HOL-Library.Code_Abstract_Nat
01:53:43 JinjaThreads: theory HOL-Library.Code_Target_Int
01:53:43 JinjaThreads: theory HOL-Library.Code_Target_Nat
01:53:43 JinjaThreads: theory HOL-Library.Complete_Partial_Order2
01:53:44 JinjaThreads: theory Automatic_Refinement.Anti_Unification
01:53:44 JinjaThreads: theory Automatic_Refinement.Attr_Comb
01:53:44 JinjaThreads: theory Automatic_Refinement.Autoref_Data
01:53:44 JinjaThreads: theory Automatic_Refinement.Indep_Vars
01:53:44 JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp
01:53:44 JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms
01:53:44 JinjaThreads: theory Automatic_Refinement.Tagged_Solver
01:53:44 JinjaThreads: theory Automatic_Refinement.Select_Solve
01:53:44 JinjaThreads: theory HOL-Library.Simps_Case_Conv
01:53:44 JinjaThreads: theory HOL-Library.Code_Target_Numeral
01:53:44 JinjaThreads: theory HOL-Library.Multiset
01:53:44 JinjaThreads: theory HOL-Library.Confluence
01:53:44 JinjaThreads: theory HOL-Library.Infinite_Set
01:53:44 JinjaThreads: theory HOL-Library.Nat_Bijection
01:53:44 JinjaThreads: theory HOL-Library.Old_Datatype
01:53:45 JinjaThreads: theory HOL-Library.Confluent_Quotient
01:53:45 JinjaThreads: theory HOL-Library.Dlist
01:53:46 JinjaThreads: theory HOL-Library.Option_ord
01:53:46 JinjaThreads: theory HOL-Library.Phantom_Type
01:53:46 JinjaThreads: theory Trie.Trie
01:53:46 JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs
01:53:46 JinjaThreads: theory HOL-Library.RBT_Impl
01:53:46 JinjaThreads: theory HOL-Library.Signed_Division
01:53:46 JinjaThreads: theory HOL-Library.Sublist
01:53:47 JinjaThreads: theory HOL-Library.Cardinality
01:53:48 JinjaThreads: theory HOL-Library.Transitive_Closure_Table
01:53:48 JinjaThreads: theory FinFun.FinFun
01:53:49 JinjaThreads: theory HOL-Library.Numeral_Type
01:53:49 JinjaThreads: theory HOL-Library.While_Combinator
01:53:49 JinjaThreads: theory Collections.DatRef
01:53:49 JinjaThreads: theory HOL-Library.Countable
01:53:50 JinjaThreads: theory HOL-Library.Type_Length
01:53:50 JinjaThreads: theory JinjaThreads.Set_Monad
01:53:50 JinjaThreads: theory JinjaThreads.Set_without_equal
01:53:50 JinjaThreads: theory Native_Word.Code_Int_Integer_Conversion
01:53:50 JinjaThreads: theory Refine_Monadic.Refine_Chapter
01:53:50 JinjaThreads: theory Word_Lib.More_Bit_Ring
01:53:50 JinjaThreads: theory JinjaThreads.Auxiliary
01:53:50 JinjaThreads: theory HOL-Library.Word
01:53:50 JinjaThreads: theory Word_Lib.More_Arithmetic
01:53:51 JinjaThreads: theory HOL-Library.Countable_Set
01:53:52 JinjaThreads: theory HOL-Library.Countable_Complete_Lattices
01:53:52 JinjaThreads: theory Binomial-Heaps.BinomialHeap
01:53:52 JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap
01:53:52 JinjaThreads: theory HOL-ex.Quicksort
01:53:53 JinjaThreads: theory Automatic_Refinement.Misc
01:53:55 JinjaThreads: theory HOL-Library.Order_Continuity
01:53:56 JinjaThreads: theory HOL-Library.Extended_Nat
01:53:57 JinjaThreads: theory Coinductive.Coinductive_Nat
01:53:59 JinjaThreads: theory Coinductive.Coinductive_List
01:54:00 JinjaThreads: theory Automatic_Refinement.Refine_Lib
01:54:00 JinjaThreads: theory Collections.SetIterator
01:54:00 JinjaThreads: theory Collections.Sorted_List_Operations
01:54:00 JinjaThreads: theory Word_Lib.Bit_Comprehension
01:54:00 JinjaThreads: theory Word_Lib.More_Divides
01:54:01 JinjaThreads: theory Word_Lib.Signed_Division_Word
01:54:01 JinjaThreads: theory Word_Lib.More_Word
01:54:01 JinjaThreads: theory Automatic_Refinement.Autoref_Phases
01:54:01 JinjaThreads: theory Automatic_Refinement.Autoref_Tagging
01:54:01 JinjaThreads: theory Automatic_Refinement.Relators
01:54:01 JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover
01:54:02 JinjaThreads: theory Collections.SetIteratorOperations
01:54:03 JinjaThreads: theory Automatic_Refinement.Param_Tool
01:54:03 JinjaThreads: theory Native_Word.Code_Target_Word_Base
01:54:03 JinjaThreads: theory Word_Lib.Bit_Shifts_Infix_Syntax
01:54:03 JinjaThreads: theory Word_Lib.Least_significant_bit
01:54:04 JinjaThreads: theory Automatic_Refinement.Param_HOL
01:54:06 JinjaThreads: theory Automatic_Refinement.Parametricity
01:54:06 JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops
01:54:06 JinjaThreads: theory Collections.Assoc_List
01:54:06 JinjaThreads: theory Collections.Dlist_add
01:54:06 JinjaThreads: theory Collections.Proper_Iterator
01:54:07 JinjaThreads: theory Collections.SetIteratorGA
01:54:07 JinjaThreads: theory Collections.Diff_Array
01:54:07 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel
01:54:07 JinjaThreads: theory Collections.Trie_Impl
01:54:07 JinjaThreads: theory Collections.It_to_It
01:54:08 JinjaThreads: theory Word_Lib.Most_significant_bit
01:54:08 JinjaThreads: theory Word_Lib.Generic_set_bit
01:54:08 JinjaThreads: theory Automatic_Refinement.Autoref_Translate
01:54:08 JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface
01:54:08 JinjaThreads: theory Collections.Trie2
01:54:08 JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo
01:54:08 JinjaThreads: theory Automatic_Refinement.Autoref_Tool
01:54:09 JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL
01:54:09 JinjaThreads: theory Native_Word.Code_Target_Integer_Bit
01:54:09 JinjaThreads: theory Native_Word.Word_Type_Copies
01:54:09 JinjaThreads: theory Coinductive.Lazy_LList
01:54:09 JinjaThreads: theory Coinductive.TLList
01:54:13 JinjaThreads: theory Coinductive.Lazy_TLList
01:54:14 JinjaThreads: theory Automatic_Refinement.Automatic_Refinement
01:54:14 JinjaThreads: theory Collections.Idx_Iterator
01:54:14 JinjaThreads: theory Refine_Monadic.Refine_Misc
01:54:16 JinjaThreads: theory Refine_Monadic.RefineG_Domain
01:54:16 JinjaThreads: theory Refine_Monadic.RefineG_Transfer
01:54:16 JinjaThreads: theory Refine_Monadic.RefineG_Assert
01:54:17 JinjaThreads: theory Refine_Monadic.RefineG_Recursion
01:54:18 JinjaThreads: theory Refine_Monadic.RefineG_While
01:54:18 JinjaThreads: theory Refine_Monadic.Refine_Basic
01:54:18 JinjaThreads: theory Refine_Monadic.Refine_Det
01:54:23 JinjaThreads: theory Refine_Monadic.Refine_Heuristics
01:54:23 JinjaThreads: theory Refine_Monadic.Refine_Leof
01:54:23 JinjaThreads: theory Refine_Monadic.Refine_Pfun
01:54:24 JinjaThreads: theory Refine_Monadic.Refine_More_Comb
01:54:24 JinjaThreads: theory Refine_Monadic.Refine_While
01:54:27 JinjaThreads: theory Refine_Monadic.Refine_Transfer
01:54:27 JinjaThreads: theory Native_Word.Code_Target_Int_Bit
01:54:27 JinjaThreads: theory Native_Word.Uint32
01:54:28 JinjaThreads: theory Refine_Monadic.Autoref_Monadic
01:54:28 JinjaThreads: theory Refine_Monadic.Refine_Automation
01:54:28 JinjaThreads: theory Refine_Monadic.Refine_Foreach
01:54:28 JinjaThreads: theory Collections.Code_Target_ICF
01:54:30 JinjaThreads: theory Collections.HashCode
01:54:32 JinjaThreads: theory Refine_Monadic.Refine_Monadic
01:54:33 JinjaThreads: theory Collections.Gen_Iterator
01:54:33 JinjaThreads: theory Collections.Intf_Map
01:54:33 JinjaThreads: theory Collections.Intf_Set
01:54:34 JinjaThreads: theory Collections.Iterator
01:54:35 JinjaThreads: theory Collections.Array_Iterator
01:54:35 JinjaThreads: theory Collections.ICF_Spec_Base
01:54:36 JinjaThreads: theory Collections.AnnotatedListSpec
01:54:36 JinjaThreads: theory Collections.ListSpec
01:54:36 JinjaThreads: theory Collections.MapSpec
01:54:36 JinjaThreads: theory Collections.PrioSpec
01:54:38 JinjaThreads: theory Collections.PrioUniqueSpec
01:54:38 JinjaThreads: theory Collections.SetSpec
01:54:39 JinjaThreads: theory Collections.BinoPrioImpl
01:54:39 JinjaThreads: theory Collections.SkewPrioImpl
01:54:40 JinjaThreads: theory Collections.ListGA
01:54:40 JinjaThreads: theory Collections.FTAnnotatedListImpl
01:54:40 JinjaThreads: theory Collections.PrioByAnnotatedList
01:54:41 JinjaThreads: theory Collections.Fifo
01:54:44 JinjaThreads: theory Collections.PrioUniqueByAnnotatedList
01:54:47 JinjaThreads: theory Collections.Algos
01:54:47 JinjaThreads: theory Collections.SetIndex
01:54:48 JinjaThreads: theory Collections.SetIteratorCollectionsGA
01:54:49 JinjaThreads: theory Collections.MapGA
01:54:49 JinjaThreads: theory Collections.SetGA
01:54:49 JinjaThreads: theory Collections.FTPrioImpl
01:54:49 JinjaThreads: theory Collections.FTPrioUniqueImpl
01:54:52 JinjaThreads: theory Collections.ArrayMapImpl
01:54:52 JinjaThreads: theory Collections.ListMapImpl
01:54:52 JinjaThreads: theory Collections.ListMapImpl_Invar
01:54:53 JinjaThreads: theory Collections.TrieMapImpl
01:54:58 JinjaThreads: theory Collections.ListSetImpl
01:54:58 JinjaThreads: theory Collections.ListSetImpl_Invar
01:54:58 JinjaThreads: theory Collections.ListSetImpl_NotDist
01:54:59 JinjaThreads: theory Collections.ListSetImpl_Sorted
01:55:02 JinjaThreads: theory Collections.SetByMap
01:55:04 JinjaThreads: theory Collections.ArrayHashMap_Impl
01:55:07 JinjaThreads: theory Collections.TrieSetImpl
01:55:07 JinjaThreads: theory Collections.ArraySetImpl
01:55:10 JinjaThreads: theory Collections.ArrayHashMap
01:55:11 JinjaThreads: theory HOL-Library.RBT
01:55:11 JinjaThreads: theory Collections.RBT_add
01:55:14 JinjaThreads: theory Collections.RBTMapImpl
01:55:17 JinjaThreads: theory Collections.ArrayHashSet
01:55:23 JinjaThreads: theory Collections.RBTSetImpl
01:55:23 JinjaThreads: theory Collections.HashMap_Impl
01:55:25 JinjaThreads: theory Collections.HashMap
01:55:33 JinjaThreads: theory Collections.HashSet
01:55:33 JinjaThreads: theory Collections.MapStdImpl
01:55:42 JinjaThreads: theory Collections.SetStdImpl
01:55:47 JinjaThreads: theory Collections.ICF_Impl
01:55:57 JinjaThreads: theory Collections.ICF_Refine_Monadic
01:56:53 JinjaThreads: theory Collections.ICF_Autoref
01:56:58 JinjaThreads: theory Collections.Collections
01:56:59 JinjaThreads: theory Collections.CollectionsV1
01:57:06 JinjaThreads: theory JinjaThreads.JT_ICF
01:57:06 JinjaThreads: theory JinjaThreads.Basic_Main
01:58:47 JinjaThreads FAILED (see also "isabelle build_log -H Error JinjaThreads")
01:58:47 *** quickcheck expected to find a counterexample but did not find one
01:58:47 *** At command "quickcheck" (line 79 of "$AFP/Coinductive/TLList.thy")
01:58:47 Building Flyspeck-Tame ...
01:58:49 Flyspeck-Tame: theory Flyspeck-Tame.ListAux
01:58:49 Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order
01:58:49 Flyspeck-Tame: theory Flyspeck-Tame.RTranCl
01:58:49 Flyspeck-Tame: theory HOL-Library.AList
01:58:49 Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat
01:58:49 Flyspeck-Tame: theory HOL-Library.Code_Target_Int
01:58:49 Flyspeck-Tame: theory HOL-Library.IArray
01:58:49 Flyspeck-Tame: theory HOL-Library.While_Combinator
01:58:49 Flyspeck-Tame: theory HOL-Library.Code_Target_Nat
01:58:49 Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso
01:58:50 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral
01:58:50 Flyspeck-Tame: theory Flyspeck-Tame.Arch
01:58:50 Flyspeck-Tame: theory Flyspeck-Tame.Worklist
01:58:51 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax
01:58:51 Flyspeck-Tame: theory Flyspeck-Tame.ListSum
01:58:51 Flyspeck-Tame: theory Flyspeck-Tame.Rotation
01:58:51 Flyspeck-Tame: theory Flyspeck-Tame.Maps
01:58:51 Flyspeck-Tame: theory Flyspeck-Tame.Graph
01:58:52 Flyspeck-Tame: theory Trie.Trie
01:58:54 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision
01:58:54 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps
01:58:55 Flyspeck-Tame: theory Flyspeck-Tame.Tame
01:58:55 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator
01:58:56 Flyspeck-Tame: theory Trie.Tries
01:58:56 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps
01:58:56 Flyspeck-Tame: theory Flyspeck-Tame.TameProps
01:58:56 Flyspeck-Tame: theory Flyspeck-Tame.Plane
01:58:57 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps
01:58:57 Flyspeck-Tame: theory Flyspeck-Tame.Plane1
01:58:57 Flyspeck-Tame: theory Flyspeck-Tame.Generator
01:58:58 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum
01:59:01 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux
01:59:02 Flyspeck-Tame: theory Flyspeck-Tame.Invariants
01:59:03 Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps
01:59:03 Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps
01:59:03 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props
01:59:04 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound
01:59:04 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps
01:59:04 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps
01:59:04 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps
01:59:05 Flyspeck-Tame: theory Flyspeck-Tame.Relative_Completeness
02:00:41 Preparing Flyspeck-Tame/document ...
02:00:59 Finished Flyspeck-Tame/document (0:00:18 elapsed time)
02:00:59 Preparing Flyspeck-Tame/outline ...
02:01:08 Finished Flyspeck-Tame/outline (0:00:08 elapsed time)
02:01:09 Timing Flyspeck-Tame (8 threads, 79.134s elapsed time, 420.227s cpu time, 33.636s GC time, factor 5.31)
02:01:09 Finished Flyspeck-Tame (0:01:52 elapsed time, 0:08:05 cpu time, factor 4.33)
02:01:09 Running Flyspeck-Tame-Computation ...
02:01:10 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.ArchComp
02:01:11 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.Completeness
07:08:00 Timing Flyspeck-Tame-Computation (8 threads, 18406.871s elapsed time, 27598.935s cpu time, 1265.709s GC time, factor 1.50)
07:08:00 Finished Flyspeck-Tame-Computation (5:06:48 elapsed time, 7:40:00 cpu time, factor 1.50)
07:08:00 Building AWN ...
07:08:01 AWN: theory AWN.Lib
07:08:01 AWN: theory AWN.TransitionSystems
07:08:01 AWN: theory AWN.AWN
07:08:02 AWN: theory AWN.Invariants
07:08:03 AWN: theory AWN.OInvariants
07:08:15 AWN: theory AWN.AWN_Cterms
07:08:15 AWN: theory AWN.AWN_SOS
07:08:16 AWN: theory AWN.OAWN_SOS
07:08:18 AWN: theory AWN.AWN_Labels
07:08:20 AWN: theory AWN.Pnet
07:08:20 AWN: theory AWN.Inv_Cterms
07:08:20 AWN: theory AWN.AWN_Invariants
07:08:21 AWN: theory AWN.Closed
07:08:22 AWN: theory AWN.AWN_SOS_Labels
07:08:22 AWN: theory AWN.Qmsg
07:08:23 AWN: theory AWN.OAWN_Invariants
07:08:23 AWN: theory AWN.OPnet
07:08:23 AWN: theory AWN.ONode_Lifting
07:08:23 AWN: theory AWN.OAWN_SOS_Labels
07:08:24 AWN: theory AWN.OPnet_Lifting
07:08:24 AWN: theory AWN.OClosed_Lifting
07:08:25 AWN: theory AWN.OClosed_Transfer
07:08:25 AWN: theory AWN.OAWN_Convert
07:08:25 AWN: theory AWN.Qmsg_Lifting
07:08:26 AWN: theory AWN.AWN_Main
07:08:26 AWN: theory AWN.Toy
07:08:41 AWN: theory AWN.AWN_Term_Graph
07:09:05 Preparing AWN/document ...
07:09:18 Finished AWN/document (0:00:12 elapsed time)
07:09:18 Preparing AWN/outline ...
07:09:25 Finished AWN/outline (0:00:07 elapsed time)
07:09:25 Timing AWN (8 threads, 43.747s elapsed time, 213.995s cpu time, 7.221s GC time, factor 4.89)
07:09:25 Finished AWN (0:01:04 elapsed time, 0:04:14 cpu time, factor 3.96)
07:09:25 Running AODV ...
07:09:27 AODV: theory AODV.Aodv_Basic
07:09:29 AODV: theory AODV.A_Norreqid
07:09:29 AODV: theory AODV.Aodv_Data
07:09:29 AODV: theory AODV.Aodv_Message
07:09:29 AODV: theory AODV.B_Fwdrreps
07:09:29 AODV: theory AODV.C_Gtobcast
07:09:29 AODV: theory AODV.D_Fwdrreqs
07:09:29 AODV: theory AODV.E_All_ABCD
07:09:29 AODV: theory AODV.B_Aodv_Data
07:09:29 AODV: theory AODV.B_Aodv_Message
07:09:29 AODV: theory AODV.D_Aodv_Data
07:09:29 AODV: theory AODV.A_Aodv_Data
07:09:29 AODV: theory AODV.A_Aodv_Message
07:09:29 AODV: theory AODV.C_Aodv_Data
07:09:31 AODV: theory AODV.C_Aodv_Message
07:09:31 AODV: theory AODV.C_Fresher
07:09:32 AODV: theory AODV.D_Aodv_Message
07:09:32 AODV: theory AODV.Fresher
07:09:32 AODV: theory AODV.E_Aodv_Data
07:09:32 AODV: theory AODV.B_Fresher
07:09:32 AODV: theory AODV.D_Fresher
07:09:32 AODV: theory AODV.A_Fresher
07:09:33 AODV: theory AODV.E_Aodv_Message
07:09:34 AODV: theory AODV.A_Aodv
07:09:34 AODV: theory AODV.Aodv
07:09:34 AODV: theory AODV.B_Aodv
07:09:34 AODV: theory AODV.E_Fresher
07:09:34 AODV: theory AODV.C_Aodv
07:09:34 AODV: theory AODV.D_Aodv
07:09:35 AODV: theory AODV.E_Aodv
07:10:30 AODV: theory AODV.A_Aodv_Predicates
07:10:30 AODV: theory AODV.A_OAodv
07:10:30 AODV: theory AODV.A_Loop_Freedom
07:10:30 AODV: theory AODV.A_Quality_Increases
07:10:30 AODV: theory AODV.A_Seq_Invariants
07:10:31 AODV: theory AODV.A_Global_Invariants
07:10:31 AODV: theory AODV.A_Aodv_Loop_Freedom
07:10:38 AODV: theory AODV.B_Aodv_Predicates
07:10:39 AODV: theory AODV.B_Loop_Freedom
07:10:39 AODV: theory AODV.B_Quality_Increases
07:10:39 AODV: theory AODV.B_Seq_Invariants
07:10:39 AODV: theory AODV.B_OAodv
07:10:40 AODV: theory AODV.B_Global_Invariants
07:10:41 AODV: theory AODV.B_Aodv_Loop_Freedom
07:10:49 AODV: theory AODV.C_Aodv_Predicates
07:10:49 AODV: theory AODV.C_OAodv
07:10:49 AODV: theory AODV.C_Loop_Freedom
07:10:49 AODV: theory AODV.C_Quality_Increases
07:10:49 AODV: theory AODV.C_Seq_Invariants
07:10:50 AODV: theory AODV.C_Global_Invariants
07:10:50 AODV: theory AODV.Aodv_Predicates
07:10:51 AODV: theory AODV.OAodv
07:10:51 AODV: theory AODV.Loop_Freedom
07:10:51 AODV: theory AODV.Quality_Increases
07:10:51 AODV: theory AODV.Seq_Invariants
07:10:51 AODV: theory AODV.C_Aodv_Loop_Freedom
07:10:52 AODV: theory AODV.Global_Invariants
07:10:52 AODV: theory AODV.Aodv_Loop_Freedom
07:10:56 AODV: theory AODV.E_Aodv_Predicates
07:10:56 AODV: theory AODV.E_OAodv
07:10:56 AODV: theory AODV.E_Loop_Freedom
07:10:56 AODV: theory AODV.E_Quality_Increases
07:10:56 AODV: theory AODV.E_Seq_Invariants
07:10:57 AODV: theory AODV.E_Global_Invariants
07:10:58 AODV: theory AODV.E_Aodv_Loop_Freedom
07:11:01 AODV: theory AODV.D_Aodv_Predicates
07:11:01 AODV: theory AODV.D_OAodv
07:11:01 AODV: theory AODV.D_Loop_Freedom
07:11:01 AODV: theory AODV.D_Quality_Increases
07:11:01 AODV: theory AODV.D_Seq_Invariants
07:11:02 AODV: theory AODV.D_Global_Invariants
07:11:03 AODV: theory AODV.D_Aodv_Loop_Freedom
07:11:08 AODV: theory AODV.All
08:43:56 Preparing AODV/document ...
08:44:21 Finished AODV/document (0:00:25 elapsed time)
08:44:21 Preparing AODV/outline ...
08:44:36 Finished AODV/outline (0:00:14 elapsed time)
08:44:39 Timing AODV (8 threads, 5662.662s elapsed time, 33977.598s cpu time, 1387.741s GC time, factor 6.00)
08:44:39 Finished AODV (1:34:24 elapsed time, 9:26:22 cpu time, factor 6.00)
08:44:39 Building Word_Lib ...
08:44:41 Word_Lib: theory Word_Lib.Enumeration
08:44:41 Word_Lib: theory Word_Lib.Even_More_List
08:44:41 Word_Lib: theory Word_Lib.More_Bit_Ring
08:44:41 Word_Lib: theory HOL-Library.Sublist
08:44:41 Word_Lib: theory Word_Lib.More_Misc
08:44:41 Word_Lib: theory HOL-Library.Phantom_Type
08:44:42 Word_Lib: theory HOL-Library.Cardinality
08:44:43 Word_Lib: theory HOL-Library.Numeral_Type
08:44:44 Word_Lib: theory Word_Lib.More_Sublist
08:44:44 Word_Lib: theory HOL-Library.Type_Length
08:44:45 Word_Lib: theory HOL-Library.Word
08:44:45 Word_Lib: theory Word_Lib.More_Arithmetic
08:44:54 Word_Lib: theory Word_Lib.Legacy_Aliases
08:44:54 Word_Lib: theory Word_Lib.More_Divides
08:44:55 Word_Lib: theory Word_Lib.More_Word
08:44:56 Word_Lib: theory Word_Lib.Strict_part_mono
08:45:01 Word_Lib: theory HOL-Library.Signed_Division
08:45:01 Word_Lib: theory Word_Lib.Bit_Shifts_Infix_Syntax
08:45:01 Word_Lib: theory Word_Lib.Bit_Comprehension
08:45:01 Word_Lib: theory Word_Lib.Least_significant_bit
08:45:02 Word_Lib: theory Word_Lib.Signed_Division_Word
08:45:03 Word_Lib: theory Word_Lib.Aligned
08:45:03 Word_Lib: theory Word_Lib.Most_significant_bit
08:45:04 Word_Lib: theory Word_Lib.Generic_set_bit
08:45:04 Word_Lib: theory Word_Lib.Next_and_Prev
08:45:04 Word_Lib: theory Word_Lib.Bits_Int
08:45:09 Word_Lib: theory Word_Lib.Singleton_Bit_Shifts
08:45:09 Word_Lib: theory Word_Lib.Many_More
08:45:09 Word_Lib: theory Word_Lib.Typedef_Morphisms
08:45:11 Word_Lib: theory Word_Lib.Signed_Words
08:45:11 Word_Lib: theory HOL-Eisbach.Eisbach
08:45:11 Word_Lib: theory Word_Lib.Hex_Words
08:45:11 Word_Lib: theory Word_Lib.Syntax_Bundles
08:45:11 Word_Lib: theory Word_Lib.Type_Syntax
08:45:11 Word_Lib: theory Word_Lib.Word_Syntax
08:45:11 Word_Lib: theory Word_Lib.Enumeration_Word
08:45:11 Word_Lib: theory Word_Lib.Bit_Comprehension_Int
08:45:11 Word_Lib: theory Word_Lib.Sgn_Abs
08:45:11 Word_Lib: theory Word_Lib.Rsplit
08:45:11 Word_Lib: theory Word_Lib.Reversed_Bit_Lists
08:45:11 Word_Lib: theory Word_Lib.Norm_Words
08:45:11 Word_Lib: theory Word_Lib.Word_Names
08:45:11 Word_Lib: theory Word_Lib.Word_16
08:45:12 Word_Lib: theory HOL-Eisbach.Eisbach_Tools
08:45:12 Word_Lib: theory Word_Lib.Word_EqI
08:45:14 Word_Lib: theory Word_Lib.Boolean_Inequalities
08:45:15 Word_Lib: theory Word_Lib.Bitwise
08:45:15 Word_Lib: theory Word_Lib.Bitwise_Signed
08:45:17 Word_Lib: theory Word_Lib.Word_Lemmas
08:45:19 Word_Lib: theory Word_Lib.Word_8
08:45:19 Word_Lib: theory Word_Lib.More_Word_Operations
08:45:23 Word_Lib: theory Word_Lib.Word_32
08:45:23 Word_Lib: theory Word_Lib.Word_64
08:45:24 Word_Lib: theory Word_Lib.Machine_Word_64_Basics
08:45:24 Word_Lib: theory Word_Lib.Machine_Word_64
08:45:24 Word_Lib: theory Word_Lib.Machine_Word_32_Basics
08:45:24 Word_Lib: theory Word_Lib.Word_Lib_Sumo
08:45:24 Word_Lib: theory Word_Lib.Machine_Word_32
08:45:27 Word_Lib: theory Word_Lib.Guide
08:45:29 Word_Lib: theory Word_Lib.Examples
08:45:45 Preparing Word_Lib/document ...
08:45:56 Finished Word_Lib/document (0:00:10 elapsed time)
08:45:56 Preparing Word_Lib/outline ...
08:46:04 Finished Word_Lib/outline (0:00:08 elapsed time)
08:46:04 Timing Word_Lib (8 threads, 50.481s elapsed time, 261.446s cpu time, 12.134s GC time, factor 5.18)
08:46:04 Finished Word_Lib (0:01:03 elapsed time, 0:04:47 cpu time, factor 4.55)
08:46:04 Building IP_Addresses ...
08:46:07 IP_Addresses: theory HOL-Library.Cancellation
08:46:07 IP_Addresses: theory HOL-Library.Infinite_Set
08:46:07 IP_Addresses: theory IP_Addresses.NumberWang_IPv4
08:46:07 IP_Addresses: theory IP_Addresses.NumberWang_IPv6
08:46:07 IP_Addresses: theory HOL-Library.Option_ord
08:46:08 IP_Addresses: theory HOL-Library.Multiset
08:46:14 IP_Addresses: theory HOL-ex.Quicksort
08:46:15 IP_Addresses: theory Automatic_Refinement.Misc
08:46:23 IP_Addresses: theory HOL-Library.Product_Lexorder
08:46:23 IP_Addresses: theory IP_Addresses.Hs_Compat
08:46:23 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
08:46:23 IP_Addresses: theory IP_Addresses.WordInterval
08:46:23 IP_Addresses: theory HOL-Library.Code_Abstract_Nat
08:46:23 IP_Addresses: theory IP_Addresses.Lib_List_toString
08:46:23 IP_Addresses: theory HOL-Library.Code_Target_Nat
08:46:23 IP_Addresses: theory IP_Addresses.Lib_Word_toString
08:46:27 IP_Addresses: theory IP_Addresses.WordInterval_Sorted
08:46:27 IP_Addresses: theory IP_Addresses.IP_Address
08:46:33 IP_Addresses: theory IP_Addresses.IPv4
08:46:34 IP_Addresses: theory IP_Addresses.Prefix_Match
08:46:34 IP_Addresses: theory IP_Addresses.IPv6
08:46:35 IP_Addresses: theory IP_Addresses.CIDR_Split
08:47:29 IP_Addresses: theory IP_Addresses.IP_Address_Parser
08:47:29 IP_Addresses: theory IP_Addresses.IP_Address_toString
08:47:30 IP_Addresses: theory IP_Addresses.Prefix_Match_toString
08:50:24 Preparing IP_Addresses/document ...
08:50:28 Finished IP_Addresses/document (0:00:04 elapsed time)
08:50:28 Preparing IP_Addresses/outline ...
08:50:32 Finished IP_Addresses/outline (0:00:03 elapsed time)
08:50:32 Timing IP_Addresses (8 threads, 241.746s elapsed time, 785.616s cpu time, 43.090s GC time, factor 3.25)
08:50:32 Finished IP_Addresses (0:04:18 elapsed time, 0:13:39 cpu time, factor 3.18)
08:50:33 Building Simple_Firewall ...
08:50:35 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
08:50:35 Simple_Firewall: theory Simple_Firewall.GroupF
08:50:35 Simple_Firewall: theory Simple_Firewall.List_Product_More
08:50:35 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
08:50:35 Simple_Firewall: theory Simple_Firewall.Option_Helpers
08:50:35 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
08:50:35 Simple_Firewall: theory HOL-Library.Char_ord
08:50:35 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
08:50:35 Simple_Firewall: theory Simple_Firewall.Iface
08:50:35 Simple_Firewall: theory Simple_Firewall.L4_Protocol
08:50:38 Simple_Firewall: theory Simple_Firewall.Simple_Packet
08:50:39 Simple_Firewall: theory Simple_Firewall.Primitives_toString
08:50:41 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax
08:50:44 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics
08:50:44 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString
08:50:46 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw
08:50:46 Simple_Firewall: theory Simple_Firewall.Shadowed
08:50:46 Simple_Firewall: theory Simple_Firewall.Service_Matrix
08:51:09 Preparing Simple_Firewall/document ...
08:51:18 Finished Simple_Firewall/document (0:00:09 elapsed time)
08:51:18 Preparing Simple_Firewall/outline ...
08:51:25 Finished Simple_Firewall/outline (0:00:07 elapsed time)
08:51:27 Timing Simple_Firewall (8 threads, 19.693s elapsed time, 83.596s cpu time, 3.132s GC time, factor 4.24)
08:51:27 Finished Simple_Firewall (0:00:33 elapsed time, 0:01:50 cpu time, factor 3.29)
08:51:27 Building Routing ...
08:51:29 Routing: theory Pure-ex.Guess
08:51:29 Routing: theory Routing.Linorder_Helper
08:51:29 Routing: theory HOL-Library.Adhoc_Overloading
08:51:30 Routing: theory HOL-Library.Monad_Syntax
08:51:31 Routing: theory Routing.Routing_Table
08:51:34 Routing: theory Routing.IpRoute_Parser
08:51:34 Routing: theory Routing.Linux_Router
08:51:50 Preparing Routing/document ...
08:51:52 Finished Routing/document (0:00:02 elapsed time)
08:51:52 Preparing Routing/outline ...
08:51:54 Finished Routing/outline (0:00:02 elapsed time)
08:51:56 Timing Routing (8 threads, 9.883s elapsed time, 31.538s cpu time, 0.738s GC time, factor 3.19)
08:51:56 Finished Routing (0:00:20 elapsed time, 0:00:50 cpu time, factor 2.53)
08:51:56 Building Iptables_Semantics ...
08:51:59 Iptables_Semantics: theory Iptables_Semantics.List_Misc
08:51:59 Iptables_Semantics: theory Iptables_Semantics.Negation_Type
08:52:01 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
08:52:02 Iptables_Semantics: theory Iptables_Semantics.Ternary
08:52:02 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
08:52:02 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
08:52:02 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
08:52:02 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
08:52:02 Iptables_Semantics: theory Native_Word.Code_Int_Integer_Conversion
08:52:02 Iptables_Semantics: theory HOL-Library.Code_Target_Int
08:52:02 Iptables_Semantics: theory HOL-Library.LaTeXsugar
08:52:02 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
08:52:02 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
08:52:02 Iptables_Semantics: theory Native_Word.Code_Target_Integer_Bit
08:52:02 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
08:52:02 Iptables_Semantics: theory Iptables_Semantics.Word_Upto
08:52:03 Iptables_Semantics: theory Iptables_Semantics.IpAddresses
08:52:03 Iptables_Semantics: theory Iptables_Semantics.Ports
08:52:04 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
08:52:05 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
08:52:17 Iptables_Semantics: theory Native_Word.Code_Target_Int_Bit
08:52:18 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
08:52:18 Iptables_Semantics: theory Iptables_Semantics.Semantics
08:52:18 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
08:52:20 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics
08:52:20 Iptables_Semantics: theory Iptables_Semantics.Matching
08:52:20 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
08:52:20 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
08:52:21 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
08:52:21 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
08:52:21 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
08:52:22 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
08:52:22 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
08:52:23 Iptables_Semantics: theory Iptables_Semantics.Optimizing
08:52:23 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
08:52:23 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
08:52:24 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
08:52:25 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
08:52:27 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
08:52:28 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
08:52:28 Iptables_Semantics: theory Iptables_Semantics.Ipassmt
08:52:31 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
08:53:04 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
08:53:04 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
08:53:04 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
08:53:04 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
08:53:04 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
08:53:04 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
08:53:04 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
08:53:04 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
08:53:04 Iptables_Semantics: theory Iptables_Semantics.No_Spoof
08:53:09 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
08:53:10 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
08:53:13 Iptables_Semantics: theory Iptables_Semantics.Transform
08:53:16 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
08:53:18 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
08:53:22 Iptables_Semantics: theory Iptables_Semantics.Code_Interface
08:53:22 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
08:53:23 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings
08:53:23 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
08:53:24 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
08:53:29 Iptables_Semantics: theory Iptables_Semantics.Parser
08:53:29 Iptables_Semantics: theory Iptables_Semantics.Parser6
08:53:29 Iptables_Semantics: theory Iptables_Semantics.Documentation
08:53:30 Iptables_Semantics: theory Iptables_Semantics.Code_haskell
08:54:25 Preparing Iptables_Semantics/document ...
08:54:50 Finished Iptables_Semantics/document (0:00:25 elapsed time)
08:54:50 Preparing Iptables_Semantics/outline ...
08:55:04 Finished Iptables_Semantics/outline (0:00:13 elapsed time)
08:55:05 Timing Iptables_Semantics (8 threads, 113.239s elapsed time, 542.729s cpu time, 41.930s GC time, factor 4.79)
08:55:05 Finished Iptables_Semantics (0:02:25 elapsed time, 0:10:08 cpu time, factor 4.18)
08:55:05 Building Iptables_Semantics_Examples ...
08:55:07 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall
08:55:07 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test
08:55:07 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company
08:55:07 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example
08:55:07 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com
08:55:07 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof
08:55:07 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing
08:55:07 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test
08:55:11 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail
08:55:11 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples
08:55:11 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed
08:55:11 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation
08:59:22 Preparing Iptables_Semantics_Examples/document ...
08:59:27 Finished Iptables_Semantics_Examples/document (0:00:05 elapsed time)
08:59:27 Preparing Iptables_Semantics_Examples/outline ...
08:59:33 Finished Iptables_Semantics_Examples/outline (0:00:05 elapsed time)
08:59:33 Timing Iptables_Semantics_Examples (8 threads, 240.995s elapsed time, 1343.504s cpu time, 133.372s GC time, factor 5.57)
08:59:33 Finished Iptables_Semantics_Examples (0:04:16 elapsed time, 0:22:52 cpu time, factor 5.36)
08:59:33 Running Iptables_Semantics_Examples_Big ...
08:59:35 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern
08:59:35 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated
08:59:35 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall
08:59:35 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3
08:59:35 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small
09:02:04 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large
09:23:22 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW
10:08:40 Preparing Iptables_Semantics_Examples_Big/document ...
10:08:45 Finished Iptables_Semantics_Examples_Big/document (0:00:05 elapsed time)
10:08:45 Preparing Iptables_Semantics_Examples_Big/outline ...
10:08:49 Finished Iptables_Semantics_Examples_Big/outline (0:00:04 elapsed time)
10:08:50 Timing Iptables_Semantics_Examples_Big (8 threads, 4141.062s elapsed time, 24952.071s cpu time, 6431.702s GC time, factor 6.03)
10:08:50 Finished Iptables_Semantics_Examples_Big (1:09:06 elapsed time, 6:56:02 cpu time, factor 6.02)
10:08:50 Building HOL-Analysis ...
10:09:02 HOL-Analysis: theory HOL-Library.BNF_Corec
10:09:02 HOL-Analysis: theory HOL-Library.Cancellation
10:09:02 HOL-Analysis: theory HOL-Library.FuncSet
10:09:02 HOL-Analysis: theory HOL-Library.Nat_Bijection
10:09:02 HOL-Analysis: theory HOL-Library.Old_Datatype
10:09:02 HOL-Analysis: theory HOL-Library.Infinite_Set
10:09:02 HOL-Analysis: theory HOL-Combinatorics.Transposition
10:09:02 HOL-Analysis: theory HOL-Library.Phantom_Type
10:09:02 HOL-Analysis: theory HOL-Library.Product_Plus
10:09:03 HOL-Analysis: theory HOL-Library.Set_Algebras
10:09:03 HOL-Analysis: theory HOL-Library.Product_Order
10:09:03 HOL-Analysis: theory HOL-Real_Asymp.Inst_Existentials
10:09:03 HOL-Analysis: theory HOL-Analysis.Metric_Arith
10:09:04 HOL-Analysis: theory HOL-Library.Disjoint_Sets
10:09:04 HOL-Analysis: theory HOL-Analysis.Inner_Product
10:09:04 HOL-Analysis: theory HOL-Library.Multiset
10:09:04 HOL-Analysis: theory HOL-Library.Cardinality
10:09:04 HOL-Analysis: theory HOL-Library.Countable
10:09:04 HOL-Analysis: theory HOL-Analysis.L2_Norm
10:09:04 HOL-Analysis: theory HOL-Analysis.Operator_Norm
10:09:04 HOL-Analysis: theory HOL-Analysis.Poly_Roots
10:09:04 HOL-Analysis: theory HOL-Analysis.Product_Vector
10:09:04 HOL-Analysis: theory HOL-Library.Complex_Order
10:09:04 HOL-Analysis: theory HOL-Library.Discrete
10:09:05 HOL-Analysis: theory HOL-Library.Indicator_Function
10:09:05 HOL-Analysis: theory HOL-Library.Landau_Symbols
10:09:05 HOL-Analysis: theory HOL-Library.Numeral_Type
10:09:05 HOL-Analysis: theory HOL-Library.Liminf_Limsup
10:09:05 HOL-Analysis: theory HOL-Library.Countable_Set
10:09:05 HOL-Analysis: theory HOL-Library.Nonpos_Ints
10:09:06 HOL-Analysis: theory HOL-Library.Periodic_Fun
10:09:06 HOL-Analysis: theory HOL-Library.Sum_of_Squares
10:09:07 HOL-Analysis: theory HOL-Real_Asymp.Eventuallize
10:09:07 HOL-Analysis: theory HOL-Real_Asymp.Lazy_Eval
10:09:07 HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices
10:09:07 HOL-Analysis: theory HOL-Library.Equipollence
10:09:08 HOL-Analysis: theory HOL-Library.Set_Idioms
10:09:08 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable
10:09:08 HOL-Analysis: theory HOL-Analysis.Euclidean_Space
10:09:08 HOL-Analysis: theory HOL-Analysis.Abstract_Topology
10:09:08 HOL-Analysis: theory HOL-Analysis.Elementary_Topology
10:09:12 HOL-Analysis: theory HOL-Library.Order_Continuity
10:09:12 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product
10:09:12 HOL-Analysis: theory HOL-Analysis.Linear_Algebra
10:09:13 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring
10:09:14 HOL-Analysis: theory HOL-Combinatorics.Permutations
10:09:14 HOL-Analysis: theory HOL-Analysis.Norm_Arith
10:09:15 HOL-Analysis: theory HOL-Library.Extended_Nat
10:09:16 HOL-Analysis: theory HOL-Analysis.Affine
10:09:18 HOL-Analysis: theory HOL-Library.Extended_Real
10:09:18 HOL-Analysis: theory HOL-Real_Asymp.Multiseries_Expansion
10:09:18 HOL-Analysis: theory HOL-Analysis.Abstract_Limits
10:09:18 HOL-Analysis: theory HOL-Analysis.FSigma
10:09:18 HOL-Analysis: theory HOL-Analysis.Sum_Topology
10:09:18 HOL-Analysis: theory HOL-Analysis.Convex
10:09:18 HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2
10:09:19 HOL-Analysis: theory HOL-Analysis.Cartesian_Space
10:09:21 HOL-Analysis: theory HOL-Analysis.Connected
10:09:21 HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces
10:09:21 HOL-Analysis: theory HOL-Analysis.Determinants
10:09:22 HOL-Analysis: theory HOL-Analysis.Function_Topology
10:09:24 HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real
10:09:24 HOL-Analysis: theory HOL-Analysis.Product_Topology
10:09:24 HOL-Analysis: theory HOL-Analysis.T1_Spaces
10:09:25 HOL-Analysis: theory HOL-Analysis.Lindelof_Spaces
10:09:25 HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces
10:09:25 HOL-Analysis: theory HOL-Analysis.Function_Metric
10:09:25 HOL-Analysis: theory HOL-Analysis.Isolated
10:09:26 HOL-Analysis: theory HOL-Analysis.Infinite_Sum
10:09:26 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra
10:09:26 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space
10:09:28 HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm
10:09:28 HOL-Analysis: theory HOL-Analysis.Measurable
10:09:29 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits
10:09:29 HOL-Analysis: theory HOL-Analysis.Line_Segment
10:09:29 HOL-Analysis: theory HOL-Analysis.Tagged_Division
10:09:29 HOL-Analysis: theory HOL-Analysis.Measure_Space
10:09:31 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space
10:09:31 HOL-Analysis: theory HOL-Analysis.Summation_Tests
10:09:32 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space
10:09:32 HOL-Analysis: theory HOL-Analysis.Starlike
10:09:33 HOL-Analysis: theory HOL-Analysis.Caratheodory
10:09:35 HOL-Analysis: theory HOL-Analysis.Continuous_Extension
10:09:35 HOL-Analysis: theory HOL-Analysis.Path_Connected
10:09:38 HOL-Analysis: theory HOL-Analysis.Uniform_Limit
10:09:38 HOL-Analysis: theory HOL-Analysis.Locally
10:09:38 HOL-Analysis: theory HOL-Analysis.Uncountable_Sets
10:09:38 HOL-Analysis: theory HOL-Analysis.Homotopy
10:09:39 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function
10:09:39 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function
10:09:41 HOL-Analysis: theory HOL-Analysis.Abstract_Euclidean_Space
10:09:41 HOL-Analysis: theory HOL-Analysis.Homeomorphism
10:09:41 HOL-Analysis: theory HOL-Analysis.Abstract_Topological_Spaces
10:09:42 HOL-Analysis: theory HOL-Analysis.Derivative
10:09:43 HOL-Analysis: theory HOL-Computational_Algebra.Primes
10:09:43 HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series
10:09:44 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected
10:09:47 HOL-Analysis: theory HOL-Analysis.Borel_Space
10:09:47 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space
10:09:47 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics
10:09:49 HOL-Analysis: theory HOL-Analysis.Abstract_Metric_Spaces
10:09:49 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint
10:09:49 HOL-Analysis: theory HOL-Analysis.Cross3
10:09:50 HOL-Analysis: theory HOL-Analysis.Polytope
10:09:52 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems
10:09:52 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental
10:09:53 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem
10:09:54 HOL-Analysis: theory HOL-Analysis.Retracts
10:09:55 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
10:09:56 HOL-Analysis: theory HOL-Analysis.Regularity
10:09:59 HOL-Analysis: theory HOL-Analysis.Smooth_Paths
10:09:59 HOL-Analysis: theory HOL-Analysis.Lipschitz
10:09:59 HOL-Analysis: theory HOL-Analysis.Urysohn
10:10:00 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem
10:10:00 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers
10:10:00 HOL-Analysis: theory HOL-Analysis.Infinite_Products
10:10:00 HOL-Analysis: theory HOL-Analysis.FPS_Convergence
10:10:01 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure
10:10:01 HOL-Analysis: theory HOL-Analysis.Multivariate_Analysis
10:10:02 HOL-Analysis: theory HOL-Analysis.Embed_Measure
10:10:02 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure
10:10:05 HOL-Analysis: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
10:10:05 HOL-Analysis: theory HOL-Analysis.Bochner_Integration
10:10:07 HOL-Analysis: theory HOL-Analysis.Complete_Measure
10:10:07 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym
10:10:07 HOL-Analysis: theory HOL-Real_Asymp.Real_Asymp
10:10:08 HOL-Analysis: theory HOL-Analysis.Set_Integral
10:10:08 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure
10:10:09 HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum
10:10:10 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration
10:10:13 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
10:10:13 HOL-Analysis: theory HOL-Analysis.Integral_Test
10:10:13 HOL-Analysis: theory HOL-Analysis.Kronecker_Approximation_Theorem
10:10:15 HOL-Analysis: theory HOL-Analysis.Further_Topology
10:10:15 HOL-Analysis: theory HOL-Analysis.Gamma_Function
10:10:16 HOL-Analysis: theory HOL-Analysis.Improper_Integral
10:10:16 HOL-Analysis: theory HOL-Analysis.Interval_Integral
10:10:17 HOL-Analysis: theory HOL-Analysis.Equivalence_Measurable_On_Borel
10:10:17 HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem
10:10:17 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution
10:10:18 HOL-Analysis: theory HOL-Analysis.Change_Of_Vars
10:10:20 HOL-Analysis: theory HOL-Analysis.Jordan_Curve
10:10:20 HOL-Analysis: theory HOL-Analysis.Simplex_Content
10:10:21 HOL-Analysis: theory HOL-Analysis.Ball_Volume
10:10:21 HOL-Analysis: theory HOL-Analysis.Analysis
10:21:26 Preparing HOL-Analysis/document ...
10:24:42 Finished HOL-Analysis/document (0:03:16 elapsed time)
10:24:42 Preparing HOL-Analysis/manual ...
10:25:07 Finished HOL-Analysis/manual (0:00:24 elapsed time)
10:25:11 Timing HOL-Analysis (8 threads, 671.620s elapsed time, 3984.156s cpu time, 596.009s GC time, factor 5.93)
10:25:11 Finished HOL-Analysis (0:12:14 elapsed time, 1:08:24 cpu time, factor 5.59)
10:25:11 Building Ordinary_Differential_Equations ...
10:25:16 Ordinary_Differential_Equations: theory HOL-Library.Code_Abstract_Nat
10:25:16 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Dense_Linear_Order
10:25:16 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Int
10:25:16 Ordinary_Differential_Equations: theory HOL-Library.Code_Cardinality
10:25:16 Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence
10:25:16 Ordinary_Differential_Equations: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
10:25:16 Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras
10:25:16 Ordinary_Differential_Equations: theory HOL-Library.Log_Nat
10:25:16 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Nat
10:25:16 Ordinary_Differential_Equations: theory Triangle.Angles
10:25:17 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator
10:25:17 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Vector_Derivative_On
10:25:17 Ordinary_Differential_Equations: theory List-Index.List_Index
10:25:17 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral
10:25:17 Ordinary_Differential_Equations: theory Triangle.Triangle
10:25:18 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Gronwall
10:25:18 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Interval_Integral_HK
10:25:24 Ordinary_Differential_Equations: theory HOL-Library.Interval
10:25:24 Ordinary_Differential_Equations: theory HOL-Library.Float
10:25:28 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral_Float
10:25:28 Ordinary_Differential_Equations: theory Affine_Arithmetic.Executable_Euclidean_Space
10:25:28 Ordinary_Differential_Equations: theory HOL-Library.Interval_Float
10:25:30 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation_Bounds
10:25:32 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities
10:25:34 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Cones
10:25:34 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem
10:25:34 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor
10:25:36 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation
10:25:37 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
10:25:38 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow
10:25:44 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Poincare_Map
10:25:44 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution
10:25:44 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE
10:25:47 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis
10:25:50 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow_Congs
10:26:29 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex
10:26:32 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis
10:28:18 Preparing Ordinary_Differential_Equations/document ...
10:28:38 Finished Ordinary_Differential_Equations/document (0:00:19 elapsed time)
10:28:38 Preparing Ordinary_Differential_Equations/outline ...
10:28:46 Finished Ordinary_Differential_Equations/outline (0:00:08 elapsed time)
10:28:46 Timing Ordinary_Differential_Equations (8 threads, 145.204s elapsed time, 726.988s cpu time, 21.027s GC time, factor 5.01)
10:28:46 Finished Ordinary_Differential_Equations (0:03:03 elapsed time, 0:13:10 cpu time, factor 4.31)
10:28:46 Building HOL-ODE-Numerics ...
10:28:52 HOL-ODE-Numerics: theory Automatic_Refinement.Prio_List
10:28:52 HOL-ODE-Numerics: theory Automatic_Refinement.Foldi
10:28:52 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util_Bootstrap1
10:28:52 HOL-ODE-Numerics: theory Deriving.Comparator
10:28:52 HOL-ODE-Numerics: theory HOL-Eisbach.Eisbach
10:28:52 HOL-ODE-Numerics: theory Deriving.Derive_Manager
10:28:52 HOL-ODE-Numerics: theory Deriving.Generator_Aux
10:28:52 HOL-ODE-Numerics: theory HOL-Library.AList
10:28:52 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot
10:28:52 HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot
10:28:52 HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading
10:28:53 HOL-ODE-Numerics: theory HOL-ex.Quicksort
10:28:53 HOL-ODE-Numerics: theory HOL-Library.Char_ord
10:28:53 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util
10:28:53 HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax
10:28:53 HOL-ODE-Numerics: theory Deriving.Equality_Generator
10:28:53 HOL-ODE-Numerics: theory HOL-Combinatorics.List_Permutation
10:28:53 HOL-ODE-Numerics: theory HOL-Library.Option_ord
10:28:53 HOL-ODE-Numerics: theory HOL-Library.Parallel
10:28:54 HOL-ODE-Numerics: theory HOL-Library.Type_Length
10:28:55 HOL-ODE-Numerics: theory Deriving.Equality_Instances
10:28:55 HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification
10:28:55 HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb
10:28:55 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data
10:28:55 HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms
10:28:55 HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars
10:28:55 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp
10:28:55 HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver
10:28:55 HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve
10:28:55 HOL-ODE-Numerics: theory Automatic_Refinement.Misc
10:28:55 HOL-ODE-Numerics: theory HOL-Library.RBT_Impl
10:28:55 HOL-ODE-Numerics: theory HOL-Library.Signed_Division
10:28:55 HOL-ODE-Numerics: theory Deriving.Compare
10:28:56 HOL-ODE-Numerics: theory Deriving.Comparator_Generator
10:28:56 HOL-ODE-Numerics: theory HOL-Library.While_Combinator
10:28:56 HOL-ODE-Numerics: theory HOL-Library.Word
10:28:56 HOL-ODE-Numerics: theory HOL-Library.Mapping
10:28:56 HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets
10:28:56 HOL-ODE-Numerics: theory Deriving.Countable_Generator
10:28:57 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer
10:28:57 HOL-ODE-Numerics: theory Deriving.Compare_Generator
10:28:57 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise
10:28:57 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis
10:28:57 HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float
10:28:57 HOL-ODE-Numerics: theory Deriving.Compare_Instances
10:28:58 HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real
10:28:58 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form
10:28:58 HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression
10:28:58 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector
10:28:59 HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
10:28:59 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
10:28:59 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict
10:29:01 HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
10:29:01 HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
10:29:02 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
10:29:02 HOL-ODE-Numerics: theory Native_Word.Code_Int_Integer_Conversion
10:29:02 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
10:29:02 HOL-ODE-Numerics: theory Show.Show
10:29:02 HOL-ODE-Numerics: theory Word_Lib.More_Arithmetic
10:29:02 HOL-ODE-Numerics: theory Word_Lib.More_Bit_Ring
10:29:05 HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
10:29:05 HOL-ODE-Numerics: theory Show.Show_Instances
10:29:05 HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib
10:29:05 HOL-ODE-Numerics: theory Collections.SetIterator
10:29:05 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases
10:29:06 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging
10:29:06 HOL-ODE-Numerics: theory Automatic_Refinement.Relators
10:29:06 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
10:29:06 HOL-ODE-Numerics: theory Collections.SetIteratorOperations
10:29:08 HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
10:29:08 HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
10:29:11 HOL-ODE-Numerics: theory Collections.Assoc_List
10:29:11 HOL-ODE-Numerics: theory Collections.Proper_Iterator
10:29:11 HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
10:29:11 HOL-ODE-Numerics: theory Collections.SetIteratorGA
10:29:11 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
10:29:11 HOL-ODE-Numerics: theory Word_Lib.Bit_Comprehension
10:29:11 HOL-ODE-Numerics: theory Word_Lib.More_Divides
10:29:11 HOL-ODE-Numerics: theory Collections.Diff_Array
10:29:12 HOL-ODE-Numerics: theory Collections.It_to_It
10:29:12 HOL-ODE-Numerics: theory Word_Lib.Signed_Division_Word
10:29:12 HOL-ODE-Numerics: theory Word_Lib.More_Word
10:29:12 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
10:29:13 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
10:29:13 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
10:29:14 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
10:29:14 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
10:29:15 HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
10:29:15 HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
10:29:15 HOL-ODE-Numerics: theory Word_Lib.Bit_Shifts_Infix_Syntax
10:29:15 HOL-ODE-Numerics: theory Word_Lib.Least_significant_bit
10:29:20 HOL-ODE-Numerics: theory Word_Lib.Most_significant_bit
10:29:21 HOL-ODE-Numerics: theory Word_Lib.Generic_set_bit
10:29:23 HOL-ODE-Numerics: theory Native_Word.Code_Target_Integer_Bit
10:29:24 HOL-ODE-Numerics: theory Native_Word.Word_Type_Copies
10:29:25 HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
10:29:25 HOL-ODE-Numerics: theory Collections.Intf_Comp
10:29:25 HOL-ODE-Numerics: theory Collections.Idx_Iterator
10:29:25 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
10:29:27 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
10:29:27 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
10:29:27 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
10:29:28 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
10:29:29 HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
10:29:29 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
10:29:29 HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
10:29:30 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
10:29:35 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
10:29:35 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
10:29:35 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
10:29:35 HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
10:29:36 HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
10:29:39 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
10:29:40 HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
10:29:40 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
10:29:40 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
10:29:45 HOL-ODE-Numerics: theory Native_Word.Code_Target_Int_Bit
10:29:45 HOL-ODE-Numerics: theory Native_Word.Uint
10:29:45 HOL-ODE-Numerics: theory Native_Word.Uint32
10:29:45 HOL-ODE-Numerics: theory Collections.Code_Target_ICF
10:29:45 HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
10:29:47 HOL-ODE-Numerics: theory Collections.Gen_Iterator
10:29:47 HOL-ODE-Numerics: theory Collections.Intf_Map
10:29:47 HOL-ODE-Numerics: theory Collections.Intf_Set
10:29:48 HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
10:29:48 HOL-ODE-Numerics: theory Collections.HashCode
10:29:48 HOL-ODE-Numerics: theory Collections.Iterator
10:29:49 HOL-ODE-Numerics: theory Collections.Intf_Hash
10:29:49 HOL-ODE-Numerics: theory Deriving.Hash_Generator
10:29:49 HOL-ODE-Numerics: theory Collections.Array_Iterator
10:29:49 HOL-ODE-Numerics: theory Collections.Gen_Map
10:29:49 HOL-ODE-Numerics: theory Collections.Gen_Map2Set
10:29:50 HOL-ODE-Numerics: theory Collections.Gen_Set
10:29:50 HOL-ODE-Numerics: theory Collections.Impl_List_Set
10:29:51 HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
10:29:51 HOL-ODE-Numerics: theory Collections.Impl_Array_Map
10:29:51 HOL-ODE-Numerics: theory Collections.Impl_List_Map
10:29:52 HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
10:29:52 HOL-ODE-Numerics: theory Collections.Gen_Hash
10:29:52 HOL-ODE-Numerics: theory Deriving.Hash_Instances
10:29:52 HOL-ODE-Numerics: theory Deriving.Derive
10:29:53 HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
10:30:28 HOL-ODE-Numerics: theory HOL-Library.RBT
10:30:28 HOL-ODE-Numerics: theory Collections.RBT_add
10:30:30 HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
10:30:30 HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
10:30:31 HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
10:30:40 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
10:30:42 HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
10:30:50 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
10:30:50 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
10:30:51 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
10:30:56 HOL-ODE-Numerics: theory Affine_Arithmetic.Print
10:30:59 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
10:30:59 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
10:30:59 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
10:31:00 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation
10:31:00 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs
10:31:00 HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter
10:31:01 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
10:31:14 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
10:31:15 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
10:31:15 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
10:31:15 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
10:31:24 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
10:31:24 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
10:31:26 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
10:31:31 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
10:31:31 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
10:31:31 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
10:31:34 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
10:31:45 HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
10:32:32 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
10:32:32 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
10:32:55 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
10:32:57 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
10:32:57 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
10:33:00 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
10:33:21 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
10:33:21 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
10:33:36 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
10:34:16 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
10:35:56 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
10:47:21 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver
10:48:06 HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities
10:50:00 HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics
10:52:16 Timing HOL-ODE-Numerics (8 threads, 1295.985s elapsed time, 6396.364s cpu time, 421.962s GC time, factor 4.94)
10:52:16 Finished HOL-ODE-Numerics (0:23:18 elapsed time, 1:49:54 cpu time, factor 4.71)
10:52:16 Building Lorenz_Approximation ...
10:52:20 Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
10:52:26 Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
10:53:00 Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
10:58:16 Timing Lorenz_Approximation (8 threads, 317.871s elapsed time, 729.017s cpu time, 63.118s GC time, factor 2.29)
10:58:16 Finished Lorenz_Approximation (0:05:59 elapsed time, 0:13:15 cpu time, factor 2.22)
10:58:16 Running Lorenz_C1 ...
10:58:20 Lorenz_C1: theory Lorenz_C1.Lorenz_C1
19:03:06 Timing Lorenz_C1 (8 threads, 29082.474s elapsed time, 189624.309s cpu time, 13625.401s GC time, factor 6.52)
19:03:06 Finished Lorenz_C1 (8:04:46 elapsed time, 52:40:28 cpu time, factor 6.52)
19:03:06 Building HOL-Library ...
19:03:07 HOL-Library: theory HOL-Library.README
19:03:08 HOL-Library: theory HOL-Library.AList
19:03:08 HOL-Library: theory HOL-Library.Adhoc_Overloading
19:03:08 HOL-Library: theory HOL-Library.BNF_Axiomatization
19:03:08 HOL-Library: theory HOL-Library.BNF_Corec
19:03:08 HOL-Library: theory HOL-Library.Cancellation
19:03:08 HOL-Library: theory HOL-Library.Case_Converter
19:03:08 HOL-Library: theory HOL-Library.Centered_Division
19:03:08 HOL-Library: theory HOL-Library.Char_ord
19:03:08 HOL-Library: theory HOL-Library.Code_Abstract_Char
19:03:08 HOL-Library: theory HOL-Library.Monad_Syntax
19:03:08 HOL-Library: theory HOL-Library.Code_Abstract_Nat
19:03:08 HOL-Library: theory HOL-Library.Code_Prolog
19:03:08 HOL-Library: theory HOL-Library.State_Monad
19:03:08 HOL-Library: theory HOL-Library.Code_Binary_Nat
19:03:09 HOL-Library: theory HOL-Library.Code_Lazy
19:03:09 HOL-Library: theory HOL-Library.Simps_Case_Conv
19:03:09 HOL-Library: theory HOL-Library.Extended
19:03:09 HOL-Library: theory HOL-Library.Multiset
19:03:10 HOL-Library: theory HOL-Library.Code_Target_Nat
19:03:10 HOL-Library: theory HOL-Library.Code_Target_Int
19:03:10 HOL-Library: theory HOL-Library.Code_Test
19:03:10 HOL-Library: theory HOL-Library.Code_Target_Numeral
19:03:10 HOL-Library: theory HOL-Library.Combine_PER
19:03:11 HOL-Library: theory HOL-Library.Comparator
19:03:11 HOL-Library: theory HOL-Library.Complete_Partial_Order2
19:03:11 HOL-Library: theory HOL-Library.DAList
19:03:11 HOL-Library: theory HOL-Library.Conditional_Parametricity
19:03:11 HOL-Library: theory HOL-Library.Confluence
19:03:11 HOL-Library: theory HOL-Library.Datatype_Records
19:03:11 HOL-Library: theory HOL-Library.Confluent_Quotient
19:03:12 HOL-Library: theory HOL-Library.Dlist
19:03:12 HOL-Library: theory HOL-Library.Debug
19:03:12 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
19:03:12 HOL-Library: theory HOL-Library.Fun_Lexorder
19:03:12 HOL-Library: theory HOL-Library.FuncSet
19:03:12 HOL-Library: theory HOL-Library.Function_Algebras
19:03:13 HOL-Library: theory HOL-Library.Function_Division
19:03:13 HOL-Library: theory HOL-Library.Groups_Big_Fun
19:03:13 HOL-Library: theory HOL-Library.IArray
19:03:14 HOL-Library: theory HOL-Library.Infinite_Set
19:03:14 HOL-Library: theory HOL-Library.Disjoint_Sets
19:03:14 HOL-Library: theory HOL-Library.LaTeXsugar
19:03:14 HOL-Library: theory HOL-Library.Lattice_Constructions
19:03:14 HOL-Library: theory HOL-Library.Omega_Words_Fun
19:03:14 HOL-Library: theory HOL-Library.ListVector
19:03:15 HOL-Library: theory HOL-Library.List_Lenlexorder
19:03:15 HOL-Library: theory HOL-Library.List_Lexorder
19:03:15 HOL-Library: theory HOL-Library.Mapping
19:03:15 HOL-Library: theory HOL-Library.More_List
19:03:15 HOL-Library: theory HOL-Library.NList
19:03:15 HOL-Library: theory HOL-Library.Nat_Bijection
19:03:15 HOL-Library: theory HOL-Library.Poly_Mapping
19:03:16 HOL-Library: theory HOL-Library.Stream
19:03:18 HOL-Library: theory HOL-Library.Old_Datatype
19:03:19 HOL-Library: theory HOL-Library.AList_Mapping
19:03:19 HOL-Library: theory HOL-Library.Old_Recdef
19:03:19 HOL-Library: theory HOL-Library.Open_State_Syntax
19:03:19 HOL-Library: theory HOL-Library.Option_ord
19:03:19 HOL-Library: theory HOL-Library.Parallel
19:03:20 HOL-Library: theory HOL-Library.Pattern_Aliases
19:03:20 HOL-Library: theory HOL-Library.Phantom_Type
19:03:20 HOL-Library: theory HOL-Library.DAList_Multiset
19:03:20 HOL-Library: theory HOL-Library.Multiset_Order
19:03:20 HOL-Library: theory HOL-Library.Power_By_Squaring
19:03:20 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
19:03:21 HOL-Library: theory HOL-Library.Preorder
19:03:22 HOL-Library: theory HOL-Library.Product_Lexorder
19:03:22 HOL-Library: theory HOL-Library.Product_Plus
19:03:22 HOL-Library: theory HOL-Library.Quotient_Syntax
19:03:22 HOL-Library: theory HOL-Library.Quotient_Option
19:03:22 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
19:03:22 HOL-Library: theory HOL-Library.Quotient_Product
19:03:22 HOL-Library: theory HOL-Library.Quotient_Set
19:03:22 HOL-Library: theory HOL-Library.Product_Order
19:03:22 HOL-Library: theory HOL-Library.Quotient_Sum
19:03:22 HOL-Library: theory HOL-Library.Quotient_Type
19:03:22 HOL-Library: theory HOL-Library.Cardinality
19:03:22 HOL-Library: theory HOL-Library.RBT_Impl
19:03:22 HOL-Library: theory HOL-Library.Quotient_List
19:03:22 HOL-Library: theory HOL-Library.Realizers
19:03:22 HOL-Library: theory HOL-Library.Finite_Lattice
19:03:22 HOL-Library: theory HOL-Library.Reflection
19:03:22 HOL-Library: theory HOL-Library.Refute
19:03:23 HOL-Library: theory HOL-Library.Rewrite
19:03:23 HOL-Library: theory HOL-Library.Set_Algebras
19:03:23 HOL-Library: theory HOL-Library.Signed_Division
19:03:24 HOL-Library: theory HOL-Library.Sorting_Algorithms
19:03:24 HOL-Library: theory HOL-Library.Sublist
19:03:24 HOL-Library: theory HOL-Library.Code_Cardinality
19:03:24 HOL-Library: theory HOL-Library.Numeral_Type
19:03:24 HOL-Library: theory HOL-Library.Transitive_Closure_Table
19:03:24 HOL-Library: theory HOL-Library.Tree
19:03:25 HOL-Library: theory HOL-Library.Uprod
19:03:25 HOL-Library: theory HOL-Library.While_Combinator
19:03:25 HOL-Library: theory HOL-Library.Z2
19:03:25 HOL-Library: theory HOL-Library.Type_Length
19:03:26 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
19:03:26 HOL-Library: theory HOL-Library.Countable
19:03:26 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
19:03:26 HOL-Library: theory HOL-Library.Prefix_Order
19:03:26 HOL-Library: theory HOL-Library.Subseq_Order
19:03:26 HOL-Library: theory HOL-Library.Saturated
19:03:26 HOL-Library: theory HOL-Library.Word
19:03:26 HOL-Library: theory HOL-Library.Complex_Order
19:03:26 HOL-Library: theory HOL-Library.Diagonal_Subsequence
19:03:26 HOL-Library: theory HOL-Library.Discrete
19:03:26 HOL-Library: theory HOL-Library.Going_To_Filter
19:03:26 HOL-Library: theory HOL-Library.Indicator_Function
19:03:26 HOL-Library: theory HOL-Library.Infinite_Typeclass
19:03:26 HOL-Library: theory HOL-Library.Landau_Symbols
19:03:27 HOL-Library: theory HOL-Library.Countable_Set
19:03:27 HOL-Library: theory HOL-Library.Tree_Multiset
19:03:27 HOL-Library: theory HOL-Library.FSet
19:03:27 HOL-Library: theory HOL-Library.Lattice_Algebras
19:03:27 HOL-Library: theory HOL-Library.Countable_Complete_Lattices
19:03:27 HOL-Library: theory HOL-Library.Countable_Set_Type
19:03:29 HOL-Library: theory HOL-Library.Equipollence
19:03:29 HOL-Library: theory HOL-Library.Set_Idioms
19:03:29 HOL-Library: theory HOL-Library.Liminf_Limsup
19:03:30 HOL-Library: theory HOL-Library.Ramsey
19:03:30 HOL-Library: theory HOL-Library.Log_Nat
19:03:30 HOL-Library: theory HOL-Library.Lub_Glb
19:03:30 HOL-Library: theory HOL-Library.Nonpos_Ints
19:03:30 HOL-Library: theory HOL-Library.OptionalSugar
19:03:30 HOL-Library: theory HOL-Library.Order_Continuity
19:03:30 HOL-Library: theory HOL-Library.Finite_Map
19:03:30 HOL-Library: theory HOL-Library.Periodic_Fun
19:03:30 HOL-Library: theory HOL-Library.Quadratic_Discriminant
19:03:30 HOL-Library: theory HOL-Library.Sum_of_Squares
19:03:31 HOL-Library: theory HOL-Library.Tree_Real
19:03:31 HOL-Library: theory HOL-Library.Extended_Nat
19:03:32 HOL-Library: theory HOL-Library.Extended_Real
19:03:32 HOL-Library: theory HOL-Library.Interval
19:03:32 HOL-Library: theory HOL-Library.Float
19:03:33 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
19:03:35 HOL-Library: theory HOL-Library.Code_Target_Numeral_Float
19:03:35 HOL-Library: theory HOL-Library.Interval_Float
19:03:36 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
19:03:44 HOL-Library: theory HOL-Library.Disjoint_FSets
19:03:44 HOL-Library: theory HOL-Library.Library
19:04:21 HOL-Library: theory HOL-Library.RBT
19:04:24 HOL-Library: theory HOL-Library.RBT_Mapping
19:04:24 HOL-Library: theory HOL-Library.RBT_Set
19:06:17 Preparing HOL-Library/document ...
19:07:18 Finished HOL-Library/document (0:01:01 elapsed time)
19:07:18 Preparing HOL-Library/outline ...
19:07:55 Finished HOL-Library/outline (0:00:36 elapsed time)
19:07:56 Timing HOL-Library (8 threads, 153.406s elapsed time, 942.368s cpu time, 58.183s GC time, factor 6.14)
19:07:56 Finished HOL-Library (0:03:06 elapsed time, 0:16:51 cpu time, factor 5.44)
19:07:56 Building Category3 ...
19:07:59 Category3: theory HOL-Cardinals.Fun_More
19:07:59 Category3: theory Category3.Category
19:07:59 Category3: theory HereditarilyFinite.HF
19:07:59 Category3: theory HOL-Cardinals.Order_Relation_More
19:07:59 Category3: theory HOL-Cardinals.Order_Union
19:08:00 Category3: theory HOL-Cardinals.Wellorder_Extension
19:08:00 Category3: theory HOL-Cardinals.Wellfounded_More
19:08:00 Category3: theory HOL-Cardinals.Wellorder_Relation
19:08:00 Category3: theory Category3.ConcreteCategory
19:08:00 Category3: theory Category3.DiscreteCategory
19:08:00 Category3: theory Category3.EpiMonoIso
19:08:01 Category3: theory HOL-Cardinals.Wellorder_Embedding
19:08:01 Category3: theory HOL-Cardinals.Wellorder_Constructions
19:08:01 Category3: theory Category3.DualCategory
19:08:01 Category3: theory Category3.InitialTerminal
19:08:01 Category3: theory Category3.ProductCategory
19:08:02 Category3: theory HOL-Cardinals.Cardinal_Order_Relation
19:08:02 Category3: theory HOL-Cardinals.Ordinal_Arithmetic
19:08:03 Category3: theory Category3.FreeCategory
19:08:03 Category3: theory Category3.Functor
19:08:03 Category3: theory HOL-Cardinals.Cardinal_Arithmetic
19:08:04 Category3: theory HOL-Cardinals.Cardinals
19:08:04 Category3: theory ZFC_in_HOL.ZFC_Library
19:08:05 Category3: theory ZFC_in_HOL.ZFC_in_HOL
19:08:06 Category3: theory ZFC_in_HOL.ZFC_Cardinals
19:08:08 Category3: theory Category3.NaturalTransformation
19:08:09 Category3: theory Category3.Subcategory
19:08:11 Category3: theory Category3.SetCategory
19:08:11 Category3: theory Category3.BinaryFunctor
19:08:14 Category3: theory Category3.SetCat
19:08:16 Category3: theory Category3.FunctorCategory
19:08:29 Category3: theory Category3.Yoneda
19:08:52 Category3: theory Category3.Adjunction
19:09:47 Category3: theory Category3.EquivalenceOfCategories
19:09:47 Category3: theory Category3.Limit
19:12:05 Category3: theory Category3.CategoryWithPullbacks
19:12:05 Category3: theory Category3.ZFC_SetCat
19:12:21 Category3: theory Category3.ZFC_SetCat_Interp
19:12:22 Category3: theory Category3.CartesianCategory
19:12:44 Category3: theory Category3.CartesianClosedCategory
19:12:45 Category3: theory Category3.CategoryWithFiniteLimits
19:12:46 Category3: theory Category3.HF_SetCat
19:12:52 Category3: theory Category3.HF_SetCat_Interp
19:14:33 Preparing Category3/document ...
19:15:04 Finished Category3/document (0:00:30 elapsed time)
19:15:04 Preparing Category3/outline ...
19:15:16 Finished Category3/outline (0:00:12 elapsed time)
19:15:16 Timing Category3 (8 threads, 367.490s elapsed time, 1826.247s cpu time, 329.975s GC time, factor 4.97)
19:15:16 Finished Category3 (0:06:32 elapsed time, 0:31:18 cpu time, factor 4.78)
19:15:17 Building MonoidalCategory ...
19:15:19 MonoidalCategory: theory MonoidalCategory.MonoidalCategory
19:16:23 MonoidalCategory: theory MonoidalCategory.MonoidalFunctor
19:16:26 MonoidalCategory: theory MonoidalCategory.CartesianMonoidalCategory
19:16:35 MonoidalCategory: theory MonoidalCategory.FreeMonoidalCategory
19:19:04 Preparing MonoidalCategory/document ...
19:19:18 Finished MonoidalCategory/document (0:00:14 elapsed time)
19:19:18 Preparing MonoidalCategory/outline ...
19:19:24 Finished MonoidalCategory/outline (0:00:06 elapsed time)
19:19:25 Timing MonoidalCategory (8 threads, 205.845s elapsed time, 753.484s cpu time, 57.531s GC time, factor 3.66)
19:19:25 Finished MonoidalCategory (0:03:45 elapsed time, 0:13:13 cpu time, factor 3.51)
19:19:25 Running Bicategory ...
19:19:37 Bicategory: theory Bicategory.IsomorphismClass
19:19:37 Bicategory: theory Bicategory.Prebicategory
19:20:03 Bicategory: theory Bicategory.Bicategory
19:20:35 Bicategory: theory Bicategory.Coherence
19:20:44 Bicategory: theory Bicategory.ConcreteBicategory
19:20:44 Bicategory: theory Bicategory.InternalEquivalence
19:20:44 Bicategory: theory Bicategory.Subbicategory
19:21:53 Bicategory: theory Bicategory.CanonicalIsos
19:21:53 Bicategory: theory Bicategory.Pseudofunctor
19:24:27 Bicategory: theory Bicategory.Strictness
19:26:57 Bicategory: theory Bicategory.CatBicat
19:27:20 Bicategory: theory Bicategory.InternalAdjunction
19:31:07 Bicategory: theory Bicategory.PseudonaturalTransformation
19:32:13 Bicategory: theory Bicategory.Tabulation
19:32:13 Bicategory: theory Bicategory.SpanBicategory
19:34:36 Bicategory: theory Bicategory.EquivalenceOfBicategories
19:34:39 Bicategory: theory Bicategory.Modification
19:52:52 Bicategory: theory Bicategory.BicategoryOfSpans
20:06:27 Preparing Bicategory/document ...
20:08:12 Finished Bicategory/document (0:01:44 elapsed time)
20:08:12 Preparing Bicategory/outline ...
20:08:32 Finished Bicategory/outline (0:00:20 elapsed time)
20:08:33 Timing Bicategory (8 threads, 2809.347s elapsed time, 9982.983s cpu time, 1437.626s GC time, factor 3.55)
20:08:33 Finished Bicategory (0:46:55 elapsed time, 2:46:46 cpu time, factor 3.55)
20:08:33 Building ConcurrentIMP ...
20:08:35 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred
20:08:36 ConcurrentIMP: theory ConcurrentIMP.Infinite_Sequences
20:08:36 ConcurrentIMP: theory ConcurrentIMP.LTL
20:08:38 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang
20:08:44 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg
20:08:50 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg_rules
20:08:50 ConcurrentIMP: theory ConcurrentIMP.CIMP
20:08:51 ConcurrentIMP: theory ConcurrentIMP.CIMP_locales
20:08:51 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer
20:08:51 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer
20:09:12 Preparing ConcurrentIMP/document ...
20:09:18 Finished ConcurrentIMP/document (0:00:06 elapsed time)
20:09:18 Preparing ConcurrentIMP/outline ...
20:09:23 Finished ConcurrentIMP/outline (0:00:05 elapsed time)
20:09:23 Timing ConcurrentIMP (8 threads, 21.763s elapsed time, 74.587s cpu time, 2.784s GC time, factor 3.43)
20:09:23 Finished ConcurrentIMP (0:00:37 elapsed time, 0:01:47 cpu time, factor 2.83)
20:09:23 Running ConcurrentGC ...
20:09:26 ConcurrentGC: theory ConcurrentGC.Model
20:09:44 ConcurrentGC: theory ConcurrentGC.Proofs_Basis
20:09:54 ConcurrentGC: theory ConcurrentGC.Global_Invariants
20:09:54 ConcurrentGC: theory ConcurrentGC.Local_Invariants
20:09:54 ConcurrentGC: theory ConcurrentGC.Tactics
20:09:54 ConcurrentGC: theory ConcurrentGC.Concrete_heap
20:09:54 ConcurrentGC: theory ConcurrentGC.Global_Invariants_Lemmas
20:09:55 ConcurrentGC: theory ConcurrentGC.Concrete
20:09:57 ConcurrentGC: theory ConcurrentGC.Global_Noninterference
20:11:26 ConcurrentGC: theory ConcurrentGC.Local_Invariants_Lemmas
20:11:27 ConcurrentGC: theory ConcurrentGC.Initial_Conditions
20:11:27 ConcurrentGC: theory ConcurrentGC.MarkObject
20:11:27 ConcurrentGC: theory ConcurrentGC.Noninterference
20:11:28 ConcurrentGC: theory ConcurrentGC.Phases
20:11:28 ConcurrentGC: theory ConcurrentGC.StrongTricolour
20:11:28 ConcurrentGC: theory ConcurrentGC.TSO
20:11:28 ConcurrentGC: theory ConcurrentGC.Valid_Refs
20:11:29 ConcurrentGC: theory ConcurrentGC.Worklists
20:11:31 ConcurrentGC: theory ConcurrentGC.Proofs
20:27:57 Preparing ConcurrentGC/document ...
20:28:08 Finished ConcurrentGC/document (0:00:11 elapsed time)
20:28:08 Preparing ConcurrentGC/outline ...
20:28:16 Finished ConcurrentGC/outline (0:00:07 elapsed time)
20:28:17 Timing ConcurrentGC (8 threads, 1109.838s elapsed time, 6155.671s cpu time, 338.360s GC time, factor 5.55)
20:28:17 Finished ConcurrentGC (0:18:32 elapsed time, 1:42:41 cpu time, factor 5.54)
20:28:17 Presentation in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info"
20:28:28 Presenting HOL in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL" ...
20:28:28 Presenting AWN in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN" ...
20:28:28 Presenting Flyspeck-Tame in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame" ...
20:28:28 Presenting Flyspeck-Tame-Computation in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame-Computation" ...
20:28:28 Presenting HOL-Analysis in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Analysis" ...
20:28:28 Presenting AODV in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV" ...
20:28:28 Presenting Ordinary_Differential_Equations in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Ordinary_Differential_Equations" ...
20:28:28 Presenting HOL-ODE-Numerics in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/HOL-ODE-Numerics" ...
20:28:28 Presenting Pure in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure" ...
20:28:28 Presenting document Ordinary_Differential_Equations/document
20:28:28 Presenting document Ordinary_Differential_Equations/outline
20:28:28 Presenting document AWN/document
20:28:28 Presenting document AWN/outline
20:28:28 Presenting document Flyspeck-Tame/document
20:28:28 Presenting document Flyspeck-Tame/outline
20:28:28 Presenting document AODV/document
20:28:28 Presenting document AODV/outline
20:28:28 Presenting theory "AWN.Lib"
20:28:28 Presenting theory "AODV.Aodv_Basic"
20:28:28 Presenting theory "Flyspeck-Tame-Computation.ArchComp"
20:28:28 Presenting theory "HOL-Library.Parallel"
20:28:28 Presenting theory "AWN.TransitionSystems"
20:28:29 Presenting document HOL/document
20:28:29 Presenting theory "Flyspeck-Tame-Computation.Completeness"
20:28:29 Presenting document HOL-Analysis/document
20:28:29 Presenting document HOL/outline
20:28:29 Presenting theory "Refine_Monadic.Refine_Chapter"
20:28:29 Presenting document HOL-Analysis/manual
20:28:29 Presenting Lorenz_Approximation in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Lorenz_Approximation" ...
20:28:29 Presenting theory "HOL-Analysis.L2_Norm"
20:28:29 Presenting theory "HOL-Library.Lattice_Algebras"
20:28:29 Presenting theory "Lorenz_Approximation.Result_Elements"
20:28:29 Presenting theory "AWN.Invariants"
20:28:29 Presenting theory "HOL-Library.Adhoc_Overloading"
20:28:29 Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
20:28:29 Presenting theory "HOL-Library.Monad_Syntax"
20:28:29 Presenting theory "Automatic_Refinement.Refine_Util_Bootstrap1"
20:28:29 Presenting theory "HOL-Analysis.Inner_Product"
20:28:29 Presenting theory "HOL-Library.Product_Plus"
20:28:29 Presenting theory "Automatic_Refinement.Mpat_Antiquot"
20:28:30 Presenting theory "Automatic_Refinement.Mk_Term_Antiquot"
20:28:31 Presenting theory "Flyspeck-Tame.ListAux"
20:28:31 Presenting theory "HOL-Library.Interval"
20:28:31 Presenting theory "Flyspeck-Tame.Quasi_Order"
20:28:31 Presenting theory "HOL-Library.Log_Nat"
20:28:32 Presenting theory "HOL-Analysis.Product_Vector"
20:28:32 Presenting theory "Automatic_Refinement.Refine_Util"
20:28:32 Presenting theory "HOL-Analysis.Euclidean_Space"
20:28:32 Presenting theory "AWN.OInvariants"
20:28:32 Presenting theory "Automatic_Refinement.Attr_Comb"
20:28:32 Presenting theory "Automatic_Refinement.Named_Sorted_Thms"
20:28:32 Presenting theory "Automatic_Refinement.Prio_List"
20:28:32 Presenting theory "Pure"
20:28:32 Presenting file "~~/src/Pure/ROOT0.ML"
20:28:32 Presenting file "~~/src/Pure/ROOT.ML"
20:28:33 Presenting theory "ML_Bootstrap"
20:28:33 Presenting theory "Pure.Sessions"
20:28:33 Presenting theory "Automatic_Refinement.Tagged_Solver"
20:28:33 Presenting theory "AODV.Aodv_Data"
20:28:33 Presenting theory "Flyspeck-Tame.PlaneGraphIso"
20:28:33 Presenting theory "HOL-Library.Infinite_Set"
20:28:33 Presenting theory "AODV.Aodv_Message"
20:28:34 Presenting theory "Automatic_Refinement.Anti_Unification"
20:28:34 Presenting theory "Flyspeck-Tame.Rotation"
20:28:34 Presenting theory "HOL-ex.Quicksort"
20:28:34 Presenting theory "Flyspeck-Tame.Graph"
20:28:34 Presenting theory "Lorenz_Approximation.Result_File_Coarse"
20:28:34 Presenting theory "HOL-Library.IArray"
20:28:35 Presenting theory "Flyspeck-Tame.IArray_Syntax"
20:28:35 Presenting theory "Flyspeck-Tame.Enumerator"
20:28:35 Presenting theory "HOL-Library.Option_ord"
20:28:35 Presenting theory "AWN.AWN"
20:28:35 Presenting theory "Flyspeck-Tame.FaceDivision"
20:28:35 Presenting theory "Flyspeck-Tame.RTranCl"
20:28:35 Presenting theory "Flyspeck-Tame.Plane"
20:28:35 Presenting theory "Flyspeck-Tame.Plane1"
20:28:36 Presenting theory "AODV.Aodv"
20:28:36 Presenting theory "HOL-Library.Float"
20:28:36 Presenting theory "AODV.Aodv_Predicates"
20:28:36 Presenting theory "HOL-Analysis.Linear_Algebra"
20:28:36 Presenting theory "HOL-Library.Interval_Float"
20:28:37 Presenting theory "Flyspeck-Tame.GraphProps"
20:28:37 Presenting theory "AWN.AWN_SOS"
20:28:37 Presenting theory "Flyspeck-Tame.EnumeratorProps"
20:28:39 Presenting theory "HOL-Analysis.Affine"
20:28:40 Presenting theory "HOL-Library.Set_Algebras"
20:28:40 Presenting theory "AODV.Fresher"
20:28:41 Presenting theory "HOL-Eisbach.Eisbach"
20:28:41 Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
20:28:41 Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
20:28:41 Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
20:28:41 Presenting file "~~/src/HOL/Eisbach/match_method.ML"
20:28:41 Presenting theory "HOL-Decision_Procs.Dense_Linear_Order"
20:28:41 Presenting file "~~/src/HOL/Decision_Procs/langford_data.ML"
20:28:41 Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff_data.ML"
20:28:41 Presenting file "~~/src/HOL/Decision_Procs/langford.ML"
20:28:41 Presenting file "~~/src/HOL/Decision_Procs/ferrante_rackoff.ML"
20:28:42 Presenting theory "HOL-Library.FuncSet"
20:28:43 Presenting theory "AWN.AWN_Cterms"
20:28:44 Presenting theory "AWN.AWN_Labels"
20:28:44 Presenting theory "AWN.Inv_Cterms"
20:28:44 Presenting theory "AWN.AWN_SOS_Labels"
20:28:44 Presenting theory "AODV.Seq_Invariants"
20:28:46 Presenting theory "Lorenz_Approximation.Lorenz_Approximation"
20:28:46 Presenting theory "HOL-Analysis.Convex"
20:28:46 Presenting Lorenz_C1 in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Lorenz_C1" ...
20:28:46 Presenting theory "AWN.Pnet"
20:28:46 Presenting theory "Lorenz_C1.Lorenz_C1"
20:28:46 Presenting theory "AODV.Quality_Increases"
20:28:46 Presenting HOL-Library in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library" ...
20:28:46 Presenting theory "AODV.OAodv"
20:28:47 Presenting theory "AWN.Closed"
20:28:47 Presenting theory "HOL-Library.Cancellation"
20:28:47 Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
20:28:47 Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
20:28:47 Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
20:28:47 Presenting document HOL-Library/document
20:28:47 Presenting document HOL-Library/outline
20:28:47 Presenting theory "HOL-Library.README"
20:28:47 Presenting theory "HOL-Decision_Procs.Approximation_Bounds"
20:28:47 Presenting theory "Automatic_Refinement.Misc"
20:28:47 Presenting theory "HOL-Library.Code_Target_Int"
20:28:48 Presenting theory "HOL-Library.Code_Abstract_Nat"
20:28:48 Presenting theory "HOL-Library.Code_Target_Nat"
20:28:48 Presenting theory "HOL-Library.Code_Target_Numeral"
20:28:48 Presenting theory "Automatic_Refinement.Foldi"
20:28:48 Presenting theory "HOL-Library.Code_Target_Numeral_Float"
20:28:48 Presenting theory "HOL-Library.AList"
20:28:48 Presenting theory "Automatic_Refinement.Indep_Vars"
20:28:48 Presenting theory "Automatic_Refinement.Select_Solve"
20:28:48 Presenting theory "AWN.OAWN_SOS"
20:28:48 Presenting theory "Automatic_Refinement.Mk_Record_Simp"
20:28:48 Presenting theory "Flyspeck-Tame.FaceDivisionProps"
20:28:48 Presenting theory "Automatic_Refinement.Refine_Lib"
20:28:48 Presenting file "$AFP/Automatic_Refinement/Lib/Cond_Rewr_Conv.ML"
20:28:48 Presenting file "$AFP/Automatic_Refinement/Lib/Revert_Abbrev.ML"
20:28:48 Presenting theory "HOL-Library.Adhoc_Overloading"
20:28:48 Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
20:28:48 Presenting theory "AWN.OAWN_SOS_Labels"
20:28:48 Presenting theory "AWN.OPnet"
20:28:48 Presenting theory "Automatic_Refinement.Autoref_Phases"
20:28:49 Presenting theory "Automatic_Refinement.Autoref_Data"
20:28:49 Presenting theory "HOL-Library.BNF_Axiomatization"
20:28:49 Presenting file "~~/src/HOL/Tools/BNF/bnf_axiomatization.ML"
20:28:49 Presenting theory "Automatic_Refinement.Autoref_Tagging"
20:28:51 Presenting theory "AWN.ONode_Lifting"
20:28:51 Presenting theory "Automatic_Refinement.Relators"
20:28:51 Presenting theory "AODV.Global_Invariants"
20:28:52 Presenting theory "AODV.Loop_Freedom"
20:28:52 Presenting theory "HOL-Decision_Procs.Approximation"
20:28:52 Presenting file "~~/src/HOL/Decision_Procs/approximation.ML"
20:28:52 Presenting file "~~/src/HOL/Decision_Procs/approximation_generator.ML"
20:28:52 Presenting theory "Automatic_Refinement.Param_Tool"
20:28:53 Presenting theory "HOL-Library.Multiset"
20:28:53 Presenting theory "List-Index.List_Index"
20:28:53 Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
20:28:54 Presenting theory "Affine_Arithmetic.Affine_Arithmetic_Auxiliarities"
20:28:54 Presenting theory "Automatic_Refinement.Param_HOL"
20:28:54 Presenting theory "Automatic_Refinement.Parametricity"
20:28:54 Presenting theory "HOL-Library.Code_Cardinality"
20:28:54 Presenting theory "Flyspeck-Tame.Invariants"
20:28:55 Presenting theory "HOL-Library.Disjoint_Sets"
20:28:55 Presenting theory "AODV.Aodv_Loop_Freedom"
20:28:55 Presenting theory "AODV.A_Norreqid"
20:28:55 Presenting theory "Automatic_Refinement.Autoref_Id_Ops"
20:28:55 Presenting theory "HOL-Combinatorics.Transposition"
20:28:55 Presenting theory "Affine_Arithmetic.Executable_Euclidean_Space"
20:28:55 Presenting theory "Flyspeck-Tame.PlaneProps"
20:28:56 Presenting theory "Flyspeck-Tame.ListSum"
20:28:56 Presenting theory "AWN.OPnet_Lifting"
20:28:56 Presenting theory "Flyspeck-Tame.Tame"
20:28:56 Presenting theory "Flyspeck-Tame.Plane1Props"
20:28:56 Presenting theory "AWN.OClosed_Lifting"
20:28:56 Presenting theory "Flyspeck-Tame.Generator"
20:28:56 Presenting theory "Flyspeck-Tame.TameProps"
20:28:56 Presenting theory "Flyspeck-Tame.TameEnum"
20:28:57 Presenting theory "Ordinary_Differential_Equations.ODE_Auxiliarities"
20:28:57 Presenting theory "Automatic_Refinement.Autoref_Fix_Rel"
20:28:57 Presenting theory "Ordinary_Differential_Equations.MVT_Ex"
20:28:58 Presenting theory "Automatic_Refinement.Autoref_Translate"
20:28:58 Presenting theory "Automatic_Refinement.Autoref_Gen_Algo"
20:28:58 Presenting theory "Ordinary_Differential_Equations.Vector_Derivative_On"
20:28:58 Presenting theory "Automatic_Refinement.Autoref_Relator_Interface"
20:28:58 Presenting theory "Automatic_Refinement.Autoref_Tool"
20:28:59 Presenting theory "Ordinary_Differential_Equations.Interval_Integral_HK"
20:28:59 Presenting theory "HOL-Combinatorics.Permutations"
20:28:59 Presenting theory "HOL-Library.Phantom_Type"
20:28:59 Presenting theory "Flyspeck-Tame.ScoreProps"
20:28:59 Presenting theory "Automatic_Refinement.Autoref_Bindings_HOL"
20:28:59 Presenting theory "Ordinary_Differential_Equations.Gronwall"
20:29:00 Presenting theory "AWN.AWN_Invariants"
20:29:00 Presenting theory "Automatic_Refinement.Automatic_Refinement"
20:29:00 Presenting theory "HOL-Library.Cardinality"
20:29:00 Presenting theory "AODV.A_Aodv_Data"
20:29:00 Presenting theory "Flyspeck-Tame.LowerBound"
20:29:00 Presenting theory "AODV.A_Aodv_Message"
20:29:00 Presenting theory "Refine_Monadic.Refine_Mono_Prover"
20:29:00 Presenting file "$AFP/Refine_Monadic/refine_mono_prover.ML"
20:29:00 Presenting theory "HOL-Library.Numeral_Type"
20:29:01 Presenting theory "Refine_Monadic.Refine_Misc"
20:29:01 Presenting theory "Flyspeck-Tame.GeneratorProps"
20:29:02 Presenting theory "Refine_Monadic.RefineG_Transfer"
20:29:02 Presenting theory "Flyspeck-Tame.TameEnumProps"
20:29:02 Presenting theory "AODV.A_Aodv"
20:29:02 Presenting theory "Refine_Monadic.RefineG_Domain"
20:29:03 Presenting theory "HOL-Library.Old_Datatype"
20:29:03 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
20:29:03 Presenting theory "AODV.A_Aodv_Predicates"
20:29:03 Presenting theory "HOL-Library.Nat_Bijection"
20:29:04 Presenting theory "Refine_Monadic.RefineG_Recursion"
20:29:04 Presenting theory "Refine_Monadic.RefineG_Assert"
20:29:04 Presenting theory "Ordinary_Differential_Equations.Initial_Value_Problem"
20:29:04 Presenting theory "HOL-Library.AList"
20:29:04 Presenting theory "Tools.Code_Generator"
20:29:04 Presenting theory "HOL-Library.Countable"
20:29:04 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
20:29:04 Presenting file "~~/src/Tools/cache_io.ML"
20:29:04 Presenting file "~~/src/Tools/Code/code_preproc.ML"
20:29:04 Presenting file "~~/src/Tools/Code/code_symbol.ML"
20:29:04 Presenting file "~~/src/Tools/Code/code_thingol.ML"
20:29:04 Presenting file "~~/src/Tools/Code/code_simp.ML"
20:29:04 Presenting file "~~/src/Tools/Code/code_printer.ML"
20:29:04 Presenting file "~~/src/Tools/Code/code_target.ML"
20:29:05 Presenting file "~~/src/Tools/Code/code_namespace.ML"
20:29:05 Presenting file "~~/src/Tools/Code/code_ml.ML"
20:29:05 Presenting file "~~/src/Tools/Code/code_haskell.ML"
20:29:05 Presenting file "~~/src/Tools/Code/code_scala.ML"
20:29:05 Presenting file "~~/src/Tools/Code/code_runtime.ML"
20:29:05 Presenting file "~~/src/Tools/nbe.ML"
20:29:05 Presenting theory "AWN.OAWN_Invariants"
20:29:05 Presenting theory "HOL-Library.Countable_Set"
20:29:05 Presenting theory "Trie.Trie"
20:29:06 Presenting theory "Trie.Tries"
20:29:07 Presenting theory "AODV.A_Fresher"
20:29:07 Presenting theory "AWN.OAWN_Convert"
20:29:07 Presenting theory "Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative"
20:29:07 Presenting theory "AWN.Qmsg"
20:29:07 Presenting theory "HOL-Library.While_Combinator"
20:29:07 Presenting theory "HOL-Library.Diagonal_Subsequence"
20:29:08 Presenting theory "Ordinary_Differential_Equations.Bounded_Linear_Operator"
20:29:08 Presenting theory "HOL-Analysis.Finite_Cartesian_Product"
20:29:08 Presenting theory "Flyspeck-Tame.Worklist"
20:29:08 Presenting theory "Flyspeck-Tame.Maps"
20:29:09 Presenting theory "HOL-Library.Code_Target_Int"
20:29:09 Presenting theory "Refine_Monadic.Refine_Basic"
20:29:09 Presenting theory "HOL-Library.Code_Abstract_Nat"
20:29:09 Presenting theory "HOL-Library.Code_Target_Nat"
20:29:09 Presenting theory "HOL-Library.Code_Target_Numeral"
20:29:09 Presenting theory "Flyspeck-Tame.Arch"
20:29:09 Presenting theory "Ordinary_Differential_Equations.Multivariate_Taylor"
20:29:09 Presenting theory "Refine_Monadic.Refine_Leof"
20:29:09 Presenting theory "Flyspeck-Tame.ArchCompAux"
20:29:10 Presenting theory "Refine_Monadic.Refine_Heuristics"
20:29:10 Presenting theory "Flyspeck-Tame.ArchCompProps"
20:29:10 Presenting theory "Flyspeck-Tame.Relative_Completeness"
20:29:10 Presenting Category3 in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Category3" ...
20:29:10 Presenting theory "Refine_Monadic.Refine_More_Comb"
20:29:10 Presenting document Category3/document
20:29:10 Presenting document Category3/outline
20:29:10 Presenting theory "AWN.Qmsg_Lifting"
20:29:11 Presenting theory "Category3.Category"
20:29:11 Presenting theory "AODV.A_Seq_Invariants"
20:29:11 Presenting theory "HOL-Library.While_Combinator"
20:29:11 Presenting theory "Category3.EpiMonoIso"
20:29:12 Presenting theory "Category3.DualCategory"
20:29:12 Presenting theory "Refine_Monadic.RefineG_While"
20:29:12 Presenting theory "HOL-Analysis.Cartesian_Space"
20:29:13 Presenting theory "Category3.ConcreteCategory"
20:29:13 Presenting theory "Category3.InitialTerminal"
20:29:14 Presenting theory "AODV.A_Quality_Increases"
20:29:14 Presenting theory "AODV.A_OAodv"
20:29:15 Presenting theory "Category3.Functor"
20:29:16 Presenting theory "Category3.Subcategory"
20:29:16 Presenting theory "Refine_Monadic.Refine_While"
20:29:16 Presenting theory "HOL-Analysis.Determinants"
20:29:17 Presenting theory "Refine_Monadic.Refine_Det"
20:29:18 Presenting theory "Refine_Monadic.Refine_Pfun"
20:29:18 Presenting theory "HOL-Library.Set_Idioms"
20:29:18 Presenting theory "Refine_Monadic.Refine_Transfer"
20:29:20 Presenting theory "Ordinary_Differential_Equations.Flow"
20:29:21 Presenting theory "Category3.SetCategory"
20:29:22 Presenting theory "Ordinary_Differential_Equations.Upper_Lower_Solution"
20:29:23 Presenting theory "HOL-Library.BNF_Corec"
20:29:23 Presenting theory "AWN.OClosed_Transfer"
20:29:23 Presenting theory "AODV.A_Global_Invariants"
20:29:23 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML"
20:29:23 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML"
20:29:23 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML"
20:29:23 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML"
20:29:23 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML"
20:29:23 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
20:29:23 Presenting theory "AWN.AWN_Main"
20:29:23 Presenting theory "Refine_Monadic.Refine_Foreach"
20:29:24 Presenting theory "AODV.A_Loop_Freedom"
20:29:24 Presenting theory "HOL-Library.While_Combinator"
20:29:25 Presenting theory "Refine_Monadic.Refine_Automation"
20:29:25 Presenting theory "Refine_Monadic.Autoref_Monadic"
20:29:25 Presenting theory "Refine_Monadic.Refine_Monadic"
20:29:25 Presenting theory "HOL-Library.Bourbaki_Witt_Fixpoint"
20:29:25 Presenting theory "HOL-Library.Centered_Division"
20:29:25 Presenting theory "HOL-Library.Char_ord"
20:29:25 Presenting theory "HOL-Library.Phantom_Type"
20:29:26 Presenting theory "HOL-Library.Cardinality"
20:29:26 Presenting theory "HOL-Library.Code_Cardinality"
20:29:27 Presenting theory "AODV.A_Aodv_Loop_Freedom"
20:29:27 Presenting theory "AODV.B_Fwdrreps"
20:29:27 Presenting theory "AWN.Toy"
20:29:27 Presenting theory "Category3.SetCat"
20:29:28 Presenting theory "Collections.SetIterator"
20:29:28 Presenting theory "AWN.AWN_Term_Graph"
20:29:28 Presenting MonoidalCategory in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/MonoidalCategory" ...
20:29:28 Presenting document MonoidalCategory/document
20:29:28 Presenting document MonoidalCategory/outline
20:29:28 Presenting theory "Ordinary_Differential_Equations.Poincare_Map"
20:29:28 Presenting theory "Category3.ProductCategory"
20:29:28 Presenting theory "HOL-Library.Case_Converter"
20:29:28 Presenting file "~~/src/HOL/Library/case_converter.ML"
20:29:28 Presenting theory "HOL-Analysis.Abstract_Topology"
20:29:29 Presenting theory "HOL-Analysis.FSigma"
20:29:30 Presenting theory "HOL-Analysis.Sum_Topology"
20:29:30 Presenting theory "Category3.NaturalTransformation"
20:29:30 Presenting theory "Collections.SetIteratorOperations"
20:29:30 Presenting theory "HOL-Library.Code_Lazy"
20:29:30 Presenting file "~~/src/HOL/Library/code_lazy.ML"
20:29:31 Presenting theory "AODV.B_Aodv_Data"
20:29:31 Presenting theory "AODV.B_Aodv_Message"
20:29:31 Presenting theory "Ordinary_Differential_Equations.Reachability_Analysis"
20:29:31 Presenting theory "Category3.BinaryFunctor"
20:29:31 Presenting theory "Collections.Proper_Iterator"
20:29:32 Presenting theory "Collections.It_to_It"
20:29:32 Presenting theory "HOL-Library.Code_Test"
20:29:32 Presenting file "~~/src/HOL/Library/code_test.ML"
20:29:32 Presenting theory "HOL-Library.Combine_PER"
20:29:32 Presenting theory "Ordinary_Differential_Equations.Flow_Congs"
20:29:33 Presenting theory "Triangle.Angles"
20:29:33 Presenting theory "AODV.B_Aodv"
20:29:33 Presenting theory "Collections.SetIteratorGA"
20:29:33 Presenting theory "Triangle.Triangle"
20:29:34 Presenting theory "AODV.B_Aodv_Predicates"
20:29:35 Presenting theory "HOL-Analysis.Elementary_Topology"
20:29:35 Presenting theory "Ordinary_Differential_Equations.Cones"
20:29:35 Presenting theory "Collections.Gen_Iterator"
20:29:35 Presenting theory "Category3.FunctorCategory"
20:29:35 Presenting theory "Ordinary_Differential_Equations.Linear_ODE"
20:29:35 Presenting theory "Ordinary_Differential_Equations.ODE_Analysis"
20:29:35 Presenting Bicategory in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Bicategory" ...
20:29:35 Presenting theory "Collections.Idx_Iterator"
20:29:35 Presenting document Bicategory/document
20:29:35 Presenting document Bicategory/outline
20:29:35 Presenting theory "Collections.Iterator"
20:29:35 Presenting theory "Bicategory.IsomorphismClass"
20:29:36 Presenting theory "Collections.Intf_Set"
20:29:36 Presenting theory "HOL-Analysis.Abstract_Limits"
20:29:37 Presenting theory "HOL-Analysis.Continuum_Not_Denumerable"
20:29:37 Presenting theory "HOL-Library.Indicator_Function"
20:29:37 Presenting theory "Collections.Impl_List_Set"
20:29:38 Presenting theory "MonoidalCategory.MonoidalCategory"
20:29:38 Presenting theory "Collections.Intf_Map"
20:29:38 Presenting theory "Category3.Yoneda"
20:29:38 Presenting theory "AODV.B_Fresher"
20:29:38 Presenting theory "HOL-Library.Equipollence"
20:29:38 Presenting theory "HOL-Library.Complete_Partial_Order2"
20:29:38 Presenting theory "Collections.Gen_Map"
20:29:40 Presenting theory "Bicategory.Prebicategory"
20:29:40 Presenting theory "Collections.Intf_Comp"
20:29:40 Presenting theory "HOL-Library.Conditional_Parametricity"
20:29:40 Presenting file "~~/src/HOL/Library/conditional_parametricity.ML"
20:29:40 Presenting theory "HOL-Library.Confluence"
20:29:41 Presenting theory "MonoidalCategory.MonoidalFunctor"
20:29:41 Presenting theory "HOL-Library.Confluent_Quotient"
20:29:41 Presenting theory "HOL.HOL"
20:29:41 Presenting file "~~/src/Tools/misc_legacy.ML"
20:29:41 Presenting file "~~/src/Tools/try.ML"
20:29:41 Presenting file "~~/src/Tools/quickcheck.ML"
20:29:41 Presenting file "~~/src/Tools/solve_direct.ML"
20:29:41 Presenting file "~~/src/Tools/IsaPlanner/zipper.ML"
20:29:41 Presenting file "~~/src/Tools/IsaPlanner/isand.ML"
20:29:41 Presenting file "~~/src/Tools/IsaPlanner/rw_inst.ML"
20:29:42 Presenting file "~~/src/Provers/hypsubst.ML"
20:29:42 Presenting file "~~/src/Provers/splitter.ML"
20:29:42 Presenting file "~~/src/Provers/classical.ML"
20:29:42 Presenting file "~~/src/Provers/blast.ML"
20:29:42 Presenting file "~~/src/Provers/clasimp.ML"
20:29:42 Presenting file "~~/src/Tools/eqsubst.ML"
20:29:42 Presenting file "~~/src/Provers/quantifier1.ML"
20:29:42 Presenting file "~~/src/Tools/atomize_elim.ML"
20:29:42 Presenting file "~~/src/Tools/cong_tac.ML"
20:29:42 Presenting file "~~/src/Tools/intuitionistic.ML"
20:29:42 Presenting file "~~/src/Tools/project_rule.ML"
20:29:42 Presenting file "~~/src/Tools/subtyping.ML"
20:29:42 Presenting file "~~/src/Tools/case_product.ML"
20:29:42 Presenting file "~~/src/HOL/Tools/hologic.ML"
20:29:42 Presenting file "~~/src/HOL/Tools/rewrite_hol_proof.ML"
20:29:42 Presenting file "~~/src/HOL/Tools/simpdata.ML"
20:29:42 Presenting file "~~/src/Tools/induct.ML"
20:29:42 Presenting file "~~/src/Tools/induction.ML"
20:29:42 Presenting file "~~/src/Tools/induct_tacs.ML"
20:29:42 Presenting file "~~/src/Tools/coherent.ML"
20:29:42 Presenting file "~~/src/HOL/Tools/cnf.ML"
20:29:42 Presenting theory "Collections.Impl_List_Map"
20:29:42 Presenting theory "AODV.B_Seq_Invariants"
20:29:42 Presenting theory "HOL-Analysis.Abstract_Topology_2"
20:29:43 Presenting theory "HOL-Library.Old_Datatype"
20:29:43 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
20:29:43 Presenting theory "HOL-Library.Nat_Bijection"
20:29:44 Presenting theory "HOL-Analysis.Connected"
20:29:45 Presenting theory "HOL-Library.Countable"
20:29:45 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
20:29:45 Presenting theory "AODV.B_Quality_Increases"
20:29:46 Presenting theory "AODV.B_OAodv"
20:29:46 Presenting theory "HOL-Library.Infinite_Set"
20:29:46 Presenting theory "Bicategory.Bicategory"
20:29:47 Presenting theory "HOL-Library.Countable_Set"
20:29:48 Presenting theory "HOL-Library.Countable_Complete_Lattices"
20:29:49 Presenting theory "HOL-Library.Countable_Set_Type"
20:29:49 Presenting theory "HOL-Library.Debug"
20:29:49 Presenting theory "HOL-Analysis.Function_Topology"
20:29:49 Presenting theory "MonoidalCategory.FreeMonoidalCategory"
20:29:49 Presenting theory "HOL-Library.Diagonal_Subsequence"
20:29:50 Presenting theory "HOL-Library.Discrete"
20:29:50 Presenting theory "HOL.Orderings"
20:29:50 Presenting file "~~/src/Provers/order_procedure.ML"
20:29:50 Presenting file "~~/src/Provers/order_tac.ML"
20:29:51 Presenting theory "HOL-Analysis.Product_Topology"
20:29:52 Presenting theory "MonoidalCategory.CartesianMonoidalCategory"
20:29:52 Presenting theory "HOL-Library.FuncSet"
20:29:52 Presenting ConcurrentIMP in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP" ...
20:29:52 Presenting document ConcurrentIMP/document
20:29:52 Presenting document ConcurrentIMP/outline
20:29:52 Presenting theory "HOL.Groups"
20:29:52 Presenting file "~~/src/HOL/Tools/group_cancel.ML"
20:29:52 Presenting theory "ConcurrentIMP.CIMP_pred"
20:29:53 Presenting theory "ConcurrentIMP.Infinite_Sequences"
20:29:53 Presenting theory "HOL-Analysis.T1_Spaces"
20:29:53 Presenting theory "Category3.Adjunction"
20:29:53 Presenting theory "HOL.Lattices"
20:29:53 Presenting theory "HOL-Library.Disjoint_Sets"
20:29:53 Presenting theory "AODV.B_Global_Invariants"
20:29:54 Presenting theory "ConcurrentIMP.LTL"
20:29:54 Presenting theory "HOL.Boolean_Algebras"
20:29:54 Presenting file "~~/src/HOL/Tools/boolean_algebra_cancel.ML"
20:29:54 Presenting theory "AODV.B_Loop_Freedom"
20:29:55 Presenting theory "ConcurrentIMP.CIMP_lang"
20:29:55 Presenting theory "HOL-Library.RBT_Impl"
20:29:55 Presenting theory "HOL-Analysis.Lindelof_Spaces"
20:29:56 Presenting theory "Category3.EquivalenceOfCategories"
20:29:56 Presenting theory "HOL-Analysis.Metric_Arith"
20:29:56 Presenting file "~~/src/HOL/Analysis/metric_arith.ML"
20:29:56 Presenting theory "Collections.RBT_add"
20:29:57 Presenting theory "HOL-Library.FSet"
20:29:57 Presenting theory "HOL.Set"
20:29:57 Presenting theory "Category3.FreeCategory"
20:29:57 Presenting theory "AODV.B_Aodv_Loop_Freedom"
20:29:57 Presenting theory "AODV.C_Gtobcast"
20:29:57 Presenting theory "Category3.DiscreteCategory"
20:29:57 Presenting theory "ConcurrentIMP.CIMP_vcg"
20:29:58 Presenting theory "Bicategory.Coherence"
20:29:58 Presenting theory "ConcurrentIMP.CIMP_vcg_rules"
20:29:58 Presenting theory "HOL.Typedef"
20:29:58 Presenting file "~~/src/HOL/Tools/typedef.ML"
20:29:59 Presenting theory "ConcurrentIMP.CIMP"
20:29:59 Presenting file "$AFP/ConcurrentIMP/cimp.ML"
20:29:59 Presenting theory "ConcurrentIMP.CIMP_locales"
20:29:59 Presenting theory "ConcurrentIMP.CIMP_one_place_buffer"
20:29:59 Presenting theory "ConcurrentIMP.CIMP_unbounded_buffer"
20:29:59 Presenting ConcurrentGC in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC" ...
20:29:59 Presenting document ConcurrentGC/document
20:29:59 Presenting document ConcurrentGC/outline
20:30:00 Presenting theory "Collections.Impl_RBT_Map"
20:30:00 Presenting theory "Bicategory.CanonicalIsos"
20:30:00 Presenting theory "HOL-Library.Finite_Map"
20:30:00 Presenting theory "HOL-Library.Disjoint_FSets"
20:30:01 Presenting theory "AODV.C_Aodv_Data"
20:30:01 Presenting theory "HOL-Library.Dlist"
20:30:01 Presenting theory "AODV.C_Aodv_Message"
20:30:01 Presenting theory "ConcurrentGC.Model"
20:30:01 Presenting theory "HOL-Library.Dual_Ordered_Lattice"
20:30:01 Presenting theory "HOL-Analysis.Elementary_Metric_Spaces"
20:30:02 Presenting theory "HOL-Library.AList"
20:30:02 Presenting theory "HOL.Fun"
20:30:02 Presenting file "~~/src/HOL/Tools/functor.ML"
20:30:02 Presenting theory "Collections.Assoc_List"
20:30:02 Presenting theory "AODV.C_Aodv"
20:30:03 Presenting theory "HOL-Library.Equipollence"
20:30:03 Presenting theory "Bicategory.Subbicategory"
20:30:03 Presenting theory "AODV.C_Aodv_Predicates"
20:30:03 Presenting theory "HOL-Library.Simps_Case_Conv"
20:30:03 Presenting file "~~/src/HOL/Library/simps_case_conv.ML"
20:30:04 Presenting theory "ConcurrentGC.Proofs_Basis"
20:30:04 Presenting theory "HOL-Library.Extended"
20:30:04 Presenting theory "Collections.Diff_Array"
20:30:04 Presenting theory "ConcurrentGC.Global_Invariants"
20:30:05 Presenting theory "HOL-Library.Order_Continuity"
20:30:05 Presenting theory "HOL.Complete_Lattices"
20:30:05 Presenting theory "Collections.Impl_Array_Map"
20:30:05 Presenting theory "Collections.Array_Iterator"
20:30:05 Presenting theory "HOL-Library.Type_Length"
20:30:05 Presenting theory "HOL-Analysis.Elementary_Normed_Spaces"
20:30:06 Presenting theory "HOL-Library.Extended_Nat"
20:30:07 Presenting theory "Bicategory.InternalEquivalence"
20:30:07 Presenting theory "ConcurrentGC.Local_Invariants"
20:30:07 Presenting theory "AODV.C_Fresher"
20:30:07 Presenting theory "HOL-Library.Liminf_Limsup"
20:30:10 Presenting theory "ConcurrentGC.Tactics"
20:30:11 Presenting theory "AODV.C_Seq_Invariants"
20:30:12 Presenting theory "HOL-Library.Sum_of_Squares"
20:30:12 Presenting file "~~/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML"
20:30:12 Presenting file "~~/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML"
20:30:12 Presenting file "~~/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML"
20:30:12 Presenting file "~~/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML"
20:30:13 Presenting theory "AODV.C_Quality_Increases"
20:30:13 Presenting theory "HOL-Analysis.Norm_Arith"
20:30:13 Presenting file "~~/src/HOL/Analysis/normarith.ML"
20:30:13 Presenting theory "AODV.C_OAodv"
20:30:15 Presenting theory "HOL-Library.Word"
20:30:15 Presenting theory "HOL-Library.Extended_Real"
20:30:15 Presenting theory "ConcurrentGC.Global_Invariants_Lemmas"
20:30:15 Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
20:30:15 Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
20:30:15 Presenting theory "Word_Lib.More_Arithmetic"
20:30:16 Presenting theory "ConcurrentGC.Local_Invariants_Lemmas"
20:30:16 Presenting theory "HOL.Ctr_Sugar"
20:30:16 Presenting theory "HOL-Library.Indicator_Function"
20:30:16 Presenting theory "Word_Lib.More_Divides"
20:30:16 Presenting file "~~/src/HOL/Tools/Ctr_Sugar/case_translation.ML"
20:30:16 Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML"
20:30:16 Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
20:30:16 Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML"
20:30:16 Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML"
20:30:16 Presenting theory "Bicategory.Pseudofunctor"
20:30:16 Presenting file "~~/src/HOL/Tools/coinduction.ML"
20:30:16 Presenting theory "Word_Lib.More_Bit_Ring"
20:30:16 Presenting theory "ConcurrentGC.Initial_Conditions"
20:30:17 Presenting theory "ConcurrentGC.Noninterference"
20:30:18 Presenting theory "HOL-Analysis.Topology_Euclidean_Space"
20:30:18 Presenting theory "ConcurrentGC.Global_Noninterference"
20:30:19 Presenting theory "HOL-Library.Extended_Nonnegative_Real"
20:30:19 Presenting theory "Word_Lib.More_Word"
20:30:19 Presenting theory "ConcurrentGC.MarkObject"
20:30:20 Presenting theory "HOL-Analysis.Line_Segment"
20:30:20 Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"
20:30:20 Presenting theory "Category3.Limit"
20:30:20 Presenting theory "HOL-Library.Log_Nat"
20:30:20 Presenting theory "Word_Lib.Most_significant_bit"
20:30:20 Presenting theory "Word_Lib.Least_significant_bit"
20:30:20 Presenting theory "ConcurrentGC.Phases"
20:30:21 Presenting theory "Word_Lib.Generic_set_bit"
20:30:21 Presenting theory "Word_Lib.Bit_Comprehension"
20:30:21 Presenting theory "AODV.C_Global_Invariants"
20:30:21 Presenting theory "HOL-Library.Lattice_Algebras"
20:30:21 Presenting theory "HOL-Library.Signed_Division"
20:30:21 Presenting theory "AODV.C_Loop_Freedom"
20:30:21 Presenting theory "Word_Lib.Signed_Division_Word"
20:30:22 Presenting theory "ConcurrentGC.StrongTricolour"
20:30:22 Presenting theory "Native_Word.Code_Target_Word_Base"
20:30:22 Presenting theory "ConcurrentGC.TSO"
20:30:22 Presenting theory "ConcurrentGC.Valid_Refs"
20:30:22 Presenting theory "Category3.CategoryWithPullbacks"
20:30:23 Presenting theory "Native_Word.Word_Type_Copies"
20:30:23 Presenting theory "Native_Word.Code_Int_Integer_Conversion"
20:30:23 Presenting theory "ConcurrentGC.Worklists"
20:30:23 Presenting theory "ConcurrentGC.Proofs"
20:30:23 Presenting theory "ConcurrentGC.Concrete_heap"
20:30:23 Presenting theory "ConcurrentGC.Concrete"
20:30:23 Presenting Word_Lib in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib" ...
20:30:23 Presenting theory "Native_Word.Code_Target_Integer_Bit"
20:30:23 Presenting document Word_Lib/document
20:30:23 Presenting document Word_Lib/outline
20:30:23 Presenting theory "HOL-Analysis.Convex_Euclidean_Space"
20:30:24 Presenting theory "Word_Lib.Enumeration"
20:30:24 Presenting theory "AODV.C_Aodv_Loop_Freedom"
20:30:24 Presenting theory "Word_Lib.Even_More_List"
20:30:24 Presenting theory "AODV.D_Fwdrreqs"
20:30:24 Presenting theory "HOL-Library.Phantom_Type"
20:30:24 Presenting theory "Native_Word.Uint32"
20:30:24 Presenting theory "Collections.HashCode"
20:30:24 Presenting theory "Native_Word.Code_Target_Int_Bit"
20:30:24 Presenting theory "Collections.Code_Target_ICF"
20:30:25 Presenting theory "Collections.Intf_Hash"
20:30:25 Presenting theory "HOL-Library.Float"
20:30:25 Presenting theory "HOL-Library.Cardinality"
20:30:25 Presenting theory "HOL-Library.Function_Algebras"
20:30:25 Presenting theory "HOL-Library.Function_Division"
20:30:26 Presenting theory "HOL-Library.Numeral_Type"
20:30:26 Presenting theory "HOL-Library.Type_Length"
20:30:26 Presenting theory "HOL-Library.Fun_Lexorder"
20:30:26 Presenting theory "HOL-Library.Going_To_Filter"
20:30:27 Presenting theory "HOL-Library.Groups_Big_Fun"
20:30:27 Presenting theory "HOL-Library.Infinite_Typeclass"
20:30:27 Presenting theory "HOL-Library.Set_Algebras"
20:30:28 Presenting theory "Category3.CartesianCategory"
20:30:29 Presenting theory "HOL-Library.Interval"
20:30:29 Presenting theory "Category3.CategoryWithFiniteLimits"
20:30:29 Presenting theory "AODV.D_Aodv_Data"
20:30:29 Presenting theory "AODV.D_Aodv_Message"
20:30:30 Presenting theory "HOL-Library.Interval_Float"
20:30:30 Presenting theory "Category3.CartesianClosedCategory"
20:30:30 Presenting theory "HOL-Library.IArray"
20:30:30 Presenting theory "Collections.Impl_Array_Hash_Map"
20:30:31 Presenting theory "Collections.Impl_Array_Stack"
20:30:31 Presenting theory "Collections.Impl_Cfun_Set"
20:30:32 Presenting theory "Collections.Impl_Bit_Set"
20:30:32 Presenting theory "AODV.D_Aodv"
20:30:32 Presenting theory "HereditarilyFinite.HF"
20:30:32 Presenting theory "Native_Word.Uint"
20:30:32 Presenting theory "AODV.D_Aodv_Predicates"
20:30:33 Presenting theory "Collections.Impl_Uv_Set"
20:30:35 Presenting theory "HOL-Library.Word"
20:30:35 Presenting theory "Collections.Gen_Set"
20:30:36 Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
20:30:36 Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
20:30:36 Presenting theory "Word_Lib.Legacy_Aliases"
20:30:36 Presenting theory "Word_Lib.More_Arithmetic"
20:30:36 Presenting theory "Collections.Gen_Map2Set"
20:30:36 Presenting theory "Collections.Gen_Hash"
20:30:36 Presenting theory "HOL-ODE-Numerics.GenCF_No_Comp"
20:30:36 Presenting theory "HOL-Analysis.Starlike"
20:30:36 Presenting theory "Word_Lib.More_Divides"
20:30:36 Presenting theory "Word_Lib.More_Misc"
20:30:37 Presenting theory "AODV.D_Fresher"
20:30:37 Presenting theory "HOL-Library.Landau_Symbols"
20:30:37 Presenting theory "Bicategory.Strictness"
20:30:37 Presenting theory "HOL-ODE-Numerics.Refine_Dflt_No_Comp"
20:30:37 Presenting theory "HOL.Inductive"
20:30:37 Presenting file "~~/src/HOL/Tools/inductive.ML"
20:30:37 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML"
20:30:37 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML"
20:30:37 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_data.ML"
20:30:37 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML"
20:30:37 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML"
20:30:37 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML"
20:30:37 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_primrec.ML"
20:30:38 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML"
20:30:38 Presenting theory "HOL-Library.Lattice_Constructions"
20:30:38 Presenting theory "HOL-ODE-Numerics.Autoref_Misc"
20:30:39 Presenting theory "HOL-Library.Sublist"
20:30:39 Presenting theory "HOL-Library.Stream"
20:30:39 Presenting theory "Word_Lib.More_Sublist"
20:30:39 Presenting theory "Word_Lib.More_Bit_Ring"
20:30:40 Presenting theory "AODV.D_Seq_Invariants"
20:30:41 Presenting theory "HOL-ODE-Numerics.Weak_Set"
20:30:43 Presenting theory "HOL-Library.Sublist"
20:30:43 Presenting theory "Word_Lib.More_Word"
20:30:43 Presenting theory "AODV.D_Quality_Increases"
20:30:44 Presenting theory "AODV.D_OAodv"
20:30:44 Presenting theory "Word_Lib.Strict_part_mono"
20:30:44 Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"
20:30:44 Presenting theory "HOL-Library.Mapping"
20:30:44 Presenting theory "Word_Lib.Most_significant_bit"
20:30:44 Presenting theory "HOL-Combinatorics.List_Permutation"
20:30:44 Presenting theory "Word_Lib.Least_significant_bit"
20:30:45 Presenting theory "Word_Lib.Generic_set_bit"
20:30:45 Presenting theory "Word_Lib.Bit_Comprehension"
20:30:45 Presenting theory "HOL-Library.Linear_Temporal_Logic_on_Streams"
20:30:45 Presenting theory "HOL-Analysis.Path_Connected"
20:30:45 Presenting theory "HOL.Product_Type"
20:30:45 Presenting theory "HOL-Library.ListVector"
20:30:45 Presenting file "~~/src/HOL/Tools/split_rule.ML"
20:30:45 Presenting file "~~/src/HOL/Tools/set_comprehension_pointfree.ML"
20:30:45 Presenting file "~~/src/HOL/Tools/inductive_set.ML"
20:30:45 Presenting theory "HOL-Library.Lub_Glb"
20:30:46 Presenting theory "Category3.HF_SetCat"
20:30:46 Presenting theory "HOL.Sum_Type"
20:30:46 Presenting theory "Category3.HF_SetCat_Interp"
20:30:46 Presenting theory "HOL-Cardinals.Fun_More"
20:30:47 Presenting theory "Bicategory.InternalAdjunction"
20:30:47 Presenting theory "Word_Lib.Bits_Int"
20:30:47 Presenting theory "HOL-Cardinals.Order_Relation_More"
20:30:47 Presenting theory "HOL-Cardinals.Wellfounded_More"
20:30:47 Presenting theory "HOL-Cardinals.Wellorder_Relation"
20:30:48 Presenting theory "HOL-Library.Mapping"
20:30:48 Presenting theory "HOL-Analysis.Locally"
20:30:48 Presenting theory "HOL-Cardinals.Wellorder_Embedding"
20:30:48 Presenting theory "HOL-Library.Monad_Syntax"
20:30:48 Presenting theory "Affine_Arithmetic.Affine_Form"
20:30:48 Presenting theory "HOL-Analysis.Uncountable_Sets"
20:30:48 Presenting theory "HOL-Cardinals.Order_Union"
20:30:49 Presenting theory "HOL-Library.More_List"
20:30:49 Presenting theory "HOL.Rings"
20:30:49 Presenting theory "Word_Lib.Aligned"
20:30:49 Presenting file "~~/src/HOL/Tools/arith_data.ML"
20:30:49 Presenting file "~~/src/Provers/Arith/cancel_div_mod.ML"
20:30:49 Presenting theory "Word_Lib.Next_and_Prev"
20:30:49 Presenting theory "HOL-Library.Cancellation"
20:30:49 Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
20:30:49 Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
20:30:49 Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
20:30:49 Presenting theory "HOL-Library.Signed_Division"
20:30:50 Presenting theory "Word_Lib.Signed_Division_Word"
20:30:50 Presenting theory "HOL-Cardinals.Wellorder_Constructions"
20:30:51 Presenting theory "Word_Lib.Many_More"
20:30:51 Presenting theory "AODV.D_Global_Invariants"
20:30:51 Presenting theory "Word_Lib.Singleton_Bit_Shifts"
20:30:52 Presenting theory "Word_Lib.Typedef_Morphisms"
20:30:52 Presenting theory "AODV.D_Loop_Freedom"
20:30:53 Presenting theory "HOL.Nat"
20:30:53 Presenting file "~~/src/HOL/Tools/nat_arith.ML"
20:30:54 Presenting theory "Affine_Arithmetic.Floatarith_Expression"
20:30:55 Presenting theory "AODV.D_Aodv_Loop_Freedom"
20:30:55 Presenting theory "AODV.E_All_ABCD"
20:30:56 Presenting theory "HOL-Cardinals.Ordinal_Arithmetic"
20:30:56 Presenting theory "Word_Lib.Reversed_Bit_Lists"
20:30:56 Presenting theory "Deriving.Generator_Aux"
20:30:56 Presenting file "$AFP/Deriving/bnf_access.ML"
20:30:56 Presenting file "$AFP/Deriving/generator_aux.ML"
20:30:56 Presenting theory "Deriving.Derive_Manager"
20:30:56 Presenting file "$AFP/Deriving/derive_manager.ML"
20:30:56 Presenting theory "Deriving.Comparator"
20:30:58 Presenting theory "Word_Lib.Bitwise"
20:30:58 Presenting theory "Word_Lib.Bit_Comprehension_Int"
20:30:58 Presenting theory "Word_Lib.Signed_Words"
20:30:58 Presenting theory "Word_Lib.Bitwise_Signed"
20:30:58 Presenting theory "AODV.E_Aodv_Data"
20:30:59 Presenting theory "HOL-Library.Multiset"
20:30:59 Presenting theory "Word_Lib.Enumeration_Word"
20:30:59 Presenting theory "AODV.E_Aodv_Message"
20:30:59 Presenting theory "Word_Lib.Hex_Words"
20:30:59 Presenting theory "Deriving.Comparator_Generator"
20:30:59 Presenting file "$AFP/Deriving/Comparator_Generator/comparator_generator.ML"
20:30:59 Presenting theory "Word_Lib.Norm_Words"
20:30:59 Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
20:30:59 Presenting theory "HOL-Cardinals.Cardinal_Order_Relation"
20:30:59 Presenting theory "Word_Lib.Rsplit"
20:30:59 Presenting theory "Word_Lib.Syntax_Bundles"
20:30:59 Presenting theory "Word_Lib.Sgn_Abs"
20:30:59 Presenting theory "Deriving.Compare"
20:30:59 Presenting file "$AFP/Deriving/Comparator_Generator/compare_code.ML"
20:30:59 Presenting theory "Word_Lib.Type_Syntax"
20:31:00 Presenting theory "Deriving.Compare_Generator"
20:31:00 Presenting file "$AFP/Deriving/Comparator_Generator/compare_generator.ML"
20:31:00 Presenting theory "HOL-Library.Char_ord"
20:31:00 Presenting theory "Deriving.Compare_Instances"
20:31:00 Presenting theory "HOL-Cardinals.Cardinal_Arithmetic"
20:31:01 Presenting theory "HOL.Fields"
20:31:01 Presenting theory "AODV.E_Aodv"
20:31:01 Presenting file "~~/src/Provers/Arith/fast_lin_arith.ML"
20:31:01 Presenting file "~~/src/HOL/Tools/lin_arith.ML"
20:31:01 Presenting theory "HOL-Library.Multiset_Order"
20:31:01 Presenting theory "HOL-Cardinals.Wellorder_Extension"
20:31:01 Presenting theory "HOL-Cardinals.Cardinals"
20:31:01 Presenting theory "ZFC_in_HOL.ZFC_Library"
20:31:01 Presenting theory "AODV.E_Aodv_Predicates"
20:31:01 Presenting theory "HOL-Library.NList"
20:31:02 Presenting theory "HOL-Library.Nonpos_Ints"
20:31:02 Presenting theory "Deriving.Equality_Generator"
20:31:02 Presenting file "$AFP/Deriving/Equality_Generator/equality_generator.ML"
20:31:02 Presenting theory "Deriving.Equality_Instances"
20:31:02 Presenting theory "HOL-Library.Numeral_Type"
20:31:03 Presenting theory "HOL-Analysis.Homotopy"
20:31:03 Presenting theory "ZFC_in_HOL.ZFC_in_HOL"
20:31:03 Presenting theory "Deriving.Hash_Generator"
20:31:03 Presenting file "$AFP/Deriving/Hash_Generator/hash_generator.ML"
20:31:03 Presenting theory "Deriving.Hash_Instances"
20:31:03 Presenting theory "Deriving.Countable_Generator"
20:31:03 Presenting theory "Deriving.Derive"
20:31:04 Presenting theory "HOL.Relation"
20:31:04 Presenting theory "HOL-Library.RBT"
20:31:04 Presenting theory "HOL-Library.Omega_Words_Fun"
20:31:04 Presenting theory "HOL-Library.RBT_Mapping"
20:31:04 Presenting theory "HOL-Library.Open_State_Syntax"
20:31:04 Presenting theory "AODV.E_Fresher"
20:31:05 Presenting theory "HOL-Library.Option_ord"
20:31:05 Presenting theory "HOL-Library.Parallel"
20:31:05 Presenting theory "HOL-Analysis.Abstract_Euclidean_Space"
20:31:06 Presenting theory "HOL-Eisbach.Eisbach"
20:31:06 Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
20:31:06 Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
20:31:06 Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
20:31:06 Presenting file "~~/src/HOL/Eisbach/match_method.ML"
20:31:06 Presenting theory "HOL-Library.Pattern_Aliases"
20:31:06 Presenting theory "HOL-Eisbach.Eisbach_Tools"
20:31:06 Presenting theory "Word_Lib.Word_EqI"
20:31:06 Presenting theory "HOL-Library.Periodic_Fun"
20:31:06 Presenting theory "Word_Lib.Boolean_Inequalities"
20:31:07 Presenting theory "Affine_Arithmetic.Straight_Line_Program"
20:31:08 Presenting theory "AODV.E_Seq_Invariants"
20:31:09 Presenting theory "ZFC_in_HOL.ZFC_Cardinals"
20:31:09 Presenting theory "HOL.Finite_Set"
20:31:10 Presenting theory "Word_Lib.Word_Lemmas"
20:31:10 Presenting theory "HOL-Library.Poly_Mapping"
20:31:10 Presenting theory "HOL-Library.Power_By_Squaring"
20:31:11 Presenting theory "Word_Lib.Word_8"
20:31:11 Presenting theory "Word_Lib.Word_16"
20:31:11 Presenting theory "Word_Lib.Word_Syntax"
20:31:11 Presenting theory "Word_Lib.Word_Names"
20:31:11 Presenting theory "AODV.E_Quality_Increases"
20:31:11 Presenting theory "AODV.E_OAodv"
20:31:11 Presenting theory "HOL-Library.Preorder"
20:31:11 Presenting file "~~/src/Provers/preorder.ML"
20:31:11 Presenting theory "HOL-Library.Product_Plus"
20:31:12 Presenting theory "HOL-Library.Quadratic_Discriminant"
20:31:12 Presenting theory "HOL-Library.Quotient_Syntax"
20:31:12 Presenting theory "HOL-Library.Quotient_Set"
20:31:12 Presenting theory "Word_Lib.More_Word_Operations"
20:31:12 Presenting theory "HOL-Library.Quotient_Product"
20:31:12 Presenting theory "HOL-Library.Quotient_Option"
20:31:13 Presenting theory "Word_Lib.Word_32"
20:31:13 Presenting theory "Word_Lib.Word_Lib_Sumo"
20:31:13 Presenting theory "Word_Lib.Machine_Word_32_Basics"
20:31:13 Presenting theory "Word_Lib.Machine_Word_32"
20:31:13 Presenting theory "Word_Lib.Word_64"
20:31:13 Presenting theory "Word_Lib.Machine_Word_64_Basics"
20:31:13 Presenting theory "HOL-Library.Quotient_List"
20:31:13 Presenting theory "Word_Lib.Machine_Word_64"
20:31:13 Presenting theory "HOL.Transitive_Closure"
20:31:13 Presenting file "~~/src/Provers/trancl.ML"
20:31:13 Presenting theory "HOL-Library.Quotient_Sum"
20:31:13 Presenting theory "Word_Lib.Guide"
20:31:13 Presenting theory "HOL-Library.Quotient_Type"
20:31:14 Presenting theory "Category3.ZFC_SetCat"
20:31:14 Presenting theory "Word_Lib.Examples"
20:31:14 Presenting IP_Addresses in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses" ...
20:31:14 Presenting document IP_Addresses/document
20:31:14 Presenting document IP_Addresses/outline
20:31:15 Presenting theory "Category3.ZFC_SetCat_Interp"
20:31:15 Presenting Simple_Firewall in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall" ...
20:31:15 Presenting document Simple_Firewall/document
20:31:15 Presenting document Simple_Firewall/outline
20:31:15 Presenting theory "Simple_Firewall.Lib_Enum_toString"
20:31:15 Presenting theory "HOL-Library.Cancellation"
20:31:15 Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
20:31:15 Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
20:31:15 Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
20:31:15 Presenting theory "Simple_Firewall.L4_Protocol"
20:31:15 Presenting theory "Simple_Firewall.Simple_Packet"
20:31:15 Presenting theory "Simple_Firewall.Firewall_Common_Decision_State"
20:31:15 Presenting theory "HOL-Library.Char_ord"
20:31:15 Presenting theory "HOL.Wellfounded"
20:31:16 Presenting theory "HOL.Wfrec"
20:31:16 Presenting theory "HOL-Library.Ramsey"
20:31:16 Presenting theory "Simple_Firewall.Iface"
20:31:16 Presenting theory "HOL-Library.Reflection"
20:31:16 Presenting theory "Simple_Firewall.SimpleFw_Syntax"
20:31:16 Presenting file "~~/src/HOL/Tools/reflection.ML"
20:31:17 Presenting theory "HOL.Order_Relation"
20:31:17 Presenting theory "AODV.E_Global_Invariants"
20:31:17 Presenting theory "Simple_Firewall.SimpleFw_Semantics"
20:31:18 Presenting theory "Simple_Firewall.List_Product_More"
20:31:18 Presenting theory "Simple_Firewall.Option_Helpers"
20:31:18 Presenting theory "HOL-Analysis.Abstract_Topological_Spaces"
20:31:18 Presenting theory "AODV.E_Loop_Freedom"
20:31:18 Presenting theory "Affine_Arithmetic.Affine_Approximation"
20:31:18 Presenting theory "Simple_Firewall.Generic_SimpleFw"
20:31:18 Presenting theory "Simple_Firewall.Shadowed"
20:31:18 Presenting theory "HOL-Library.Rewrite"
20:31:18 Presenting file "~~/src/HOL/Library/cconv.ML"
20:31:18 Presenting file "~~/src/HOL/Library/rewrite.ML"
20:31:18 Presenting theory "HOL-Library.Type_Length"
20:31:19 Presenting theory "HOL.Hilbert_Choice"
20:31:19 Presenting theory "HOL-Library.Saturated"
20:31:19 Presenting file "~~/src/HOL/Tools/choice_specification.ML"
20:31:19 Presenting theory "Affine_Arithmetic.Counterclockwise"
20:31:19 Presenting theory "Simple_Firewall.IP_Partition_Preliminaries"
20:31:19 Presenting theory "Affine_Arithmetic.Counterclockwise_Vector"
20:31:20 Presenting theory "AODV.E_Aodv_Loop_Freedom"
20:31:20 Presenting theory "AODV.All"
20:31:20 Presenting theory "Simple_Firewall.GroupF"
20:31:20 Presenting Routing in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing" ...
20:31:20 Presenting document Routing/document
20:31:20 Presenting document Routing/outline
20:31:20 Presenting theory "Routing.Linorder_Helper"
20:31:20 Presenting theory "Simple_Firewall.IP_Addr_WordInterval_toString"
20:31:20 Presenting theory "Simple_Firewall.Primitives_toString"
20:31:20 Presenting theory "HOL-Library.Set_Idioms"
20:31:20 Presenting theory "Bicategory.PseudonaturalTransformation"
20:31:20 Presenting theory "HOL-Library.Signed_Division"
20:31:20 Presenting theory "Pure-ex.Guess"
20:31:20 Presenting theory "HOL.Zorn"
20:31:21 Presenting theory "HOL-Library.State_Monad"
20:31:21 Presenting theory "Affine_Arithmetic.Counterclockwise_2D_Strict"
20:31:21 Presenting theory "HOL-Library.Comparator"
20:31:21 Presenting theory "HOL.BNF_Wellorder_Relation"
20:31:21 Presenting theory "HOL-Library.Multiset"
20:31:21 Presenting theory "Routing.Routing_Table"
20:31:21 Presenting theory "HOL-Library.Sorting_Algorithms"
20:31:21 Presenting theory "HOL-Library.Adhoc_Overloading"
20:31:21 Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
20:31:21 Presenting theory "Affine_Arithmetic.Polygon"
20:31:21 Presenting theory "HOL-Library.Monad_Syntax"
20:31:21 Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
20:31:21 Presenting theory "Routing.Linux_Router"
20:31:22 Presenting theory "HOL-ex.Quicksort"
20:31:22 Presenting theory "Simple_Firewall.Service_Matrix"
20:31:22 Presenting theory "Simple_Firewall.SimpleFw_toString"
20:31:22 Presenting Iptables_Semantics in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics" ...
20:31:22 Presenting theory "Routing.IpRoute_Parser"
20:31:22 Presenting file "$AFP/Routing/IpRoute_Parser.ML"
20:31:22 Presenting Iptables_Semantics_Examples in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples" ...
20:31:22 Presenting document Iptables_Semantics/document
20:31:22 Presenting document Iptables_Semantics_Examples/document
20:31:22 Presenting document Iptables_Semantics_Examples/outline
20:31:22 Presenting document Iptables_Semantics/outline
20:31:22 Presenting theory "Iptables_Semantics.List_Misc"
20:31:22 Presenting theory "Iptables_Semantics.Negation_Type"
20:31:23 Presenting theory "HOL-Library.Option_ord"
20:31:23 Presenting theory "HOL.BNF_Wellorder_Embedding"
20:31:23 Presenting theory "Iptables_Semantics.WordInterval_Lists"
20:31:23 Presenting theory "Iptables_Semantics.Repeat_Stabilize"
20:31:23 Presenting theory "Iptables_Semantics.Firewall_Common"
20:31:23 Presenting theory "HOL-Library.LaTeXsugar"
20:31:23 Presenting theory "HOL-Library.Infinite_Set"
20:31:24 Presenting theory "Affine_Arithmetic.Counterclockwise_2D_Arbitrary"
20:31:26 Presenting theory "HOL-Library.Sum_of_Squares"
20:31:26 Presenting file "~~/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML"
20:31:26 Presenting file "~~/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML"
20:31:26 Presenting file "~~/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML"
20:31:26 Presenting theory "Iptables_Semantics.Semantics"
20:31:26 Presenting file "~~/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML"
20:31:27 Presenting theory "HOL-Library.Transitive_Closure_Table"
20:31:27 Presenting theory "HOL-Analysis.Abstract_Metric_Spaces"
20:31:27 Presenting theory "Iptables_Semantics.Matching"
20:31:27 Presenting theory "HOL.BNF_Wellorder_Constructions"
20:31:27 Presenting theory "HOL-Library.Tree"
20:31:27 Presenting theory "HOL-Library.Tree_Multiset"
20:31:27 Presenting theory "HOL-Library.Tree_Real"
20:31:27 Presenting theory "Iptables_Semantics.Ruleset_Update"
20:31:27 Presenting theory "Iptables_Semantics_Examples.Parser_Test"
20:31:28 Presenting theory "Iptables_Semantics_Examples.Parser6_Test"
20:31:28 Presenting theory "HOL-Library.Uprod"
20:31:28 Presenting theory "Iptables_Semantics_Examples.Small_Examples"
20:31:28 Presenting theory "Iptables_Semantics_Examples.Ports_Fail"
20:31:28 Presenting theory "HOL-Library.Countable_Complete_Lattices"
20:31:28 Presenting theory "Iptables_Semantics_Examples.Contrived_Example"
20:31:28 Presenting theory "Iptables_Semantics_Examples.iptables_Ln_tuned_parsed"
20:31:29 Presenting theory "HOL-Library.Order_Continuity"
20:31:29 Presenting theory "Iptables_Semantics.Call_Return_Unfolding"
20:31:29 Presenting theory "Iptables_Semantics.Ternary"
20:31:30 Presenting theory "HOL-Library.Extended_Nat"
20:31:30 Presenting theory "Iptables_Semantics_Examples.Analyze_Synology_Diskstation"
20:31:30 Presenting theory "Automatic_Refinement.Misc"
20:31:31 Presenting theory "HOL.BNF_Cardinal_Order_Relation"
20:31:31 Presenting theory "Iptables_Semantics.Matching_Ternary"
20:31:31 Presenting theory "HOL-Library.Liminf_Limsup"
20:31:31 Presenting theory "Iptables_Semantics_Examples.Analyze_Ringofsaturn_com"
20:31:31 Presenting theory "IP_Addresses.NumberWang_IPv4"
20:31:31 Presenting theory "IP_Addresses.NumberWang_IPv6"
20:31:32 Presenting theory "HOL.BNF_Cardinal_Arithmetic"
20:31:32 Presenting theory "Iptables_Semantics.Semantics_Ternary"
20:31:32 Presenting theory "Iptables_Semantics.Datatype_Selectors"
20:31:32 Presenting theory "Affine_Arithmetic.Intersection"
20:31:32 Presenting theory "Iptables_Semantics.IpAddresses"
20:31:33 Presenting theory "Iptables_Semantics.L4_Protocol_Flags"
20:31:33 Presenting theory "Iptables_Semantics.Ports"
20:31:33 Presenting theory "IP_Addresses.WordInterval"
20:31:33 Presenting theory "Iptables_Semantics.Conntrack_State"
20:31:33 Presenting theory "IP_Addresses.Hs_Compat"
20:31:33 Presenting theory "Iptables_Semantics.Tagged_Packet"
20:31:33 Presenting theory "Iptables_Semantics.Common_Primitive_Syntax"
20:31:33 Presenting theory "Iptables_Semantics.Unknown_Match_Tacs"
20:31:34 Presenting theory "IP_Addresses.IP_Address"
20:31:34 Presenting theory "IP_Addresses.IPv4"
20:31:34 Presenting theory "Affine_Arithmetic.Affine_Code"
20:31:34 Presenting theory "Iptables_Semantics.Common_Primitive_Matcher_Generic"
20:31:35 Presenting theory "HOL.Fun_Def_Base"
20:31:35 Presenting file "~~/src/HOL/Tools/Function/function_lib.ML"
20:31:35 Presenting file "~~/src/HOL/Tools/Function/function_common.ML"
20:31:35 Presenting file "~~/src/HOL/Tools/Function/function_context_tree.ML"
20:31:35 Presenting file "~~/src/HOL/Tools/Function/sum_tree.ML"
20:31:35 Presenting theory "Iptables_Semantics.Common_Primitive_Matcher"
20:31:36 Presenting theory "Iptables_Semantics.Example_Semantics"
20:31:36 Presenting theory "HOL-Library.Word"
20:31:36 Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
20:31:36 Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
20:31:37 Presenting theory "HOL-Library.Z2"
20:31:37 Presenting theory "HOL-Library.Library"
20:31:37 Presenting theory "Show.Show"
20:31:37 Presenting file "$AFP/Show/show_generator.ML"
20:31:37 Presenting theory "HOL-Library.Product_Order"
20:31:37 Presenting theory "HOL-Library.Extended_Real"
20:31:38 Presenting theory "Iptables_Semantics.Alternative_Semantics"
20:31:38 Presenting theory "Show.Show_Instances"
20:31:38 Presenting theory "Affine_Arithmetic.Optimize_Integer"
20:31:38 Presenting theory "HOL-Library.Finite_Lattice"
20:31:38 Presenting theory "Affine_Arithmetic.Optimize_Float"
20:31:38 Presenting theory "HOL-Library.List_Lexorder"
20:31:38 Presenting theory "HOL-Library.List_Lenlexorder"
20:31:38 Presenting theory "HOL-Library.Prefix_Order"
20:31:38 Presenting theory "Iptables_Semantics.Semantics_Stateful"
20:31:38 Presenting theory "HOL-Library.Product_Lexorder"
20:31:39 Presenting theory "IP_Addresses.IPv6"
20:31:39 Presenting theory "Affine_Arithmetic.Print"
20:31:39 Presenting theory "HOL-Library.Subseq_Order"
20:31:39 Presenting theory "HOL-ODE-Numerics.Enclosure_Operations"
20:31:39 Presenting theory "IP_Addresses.Prefix_Match"
20:31:40 Presenting theory "HOL-Library.Datatype_Records"
20:31:40 Presenting file "~~/src/HOL/Library/datatype_records.ML"
20:31:40 Presenting theory "HOL-ODE-Numerics.Refine_Vector_List"
20:31:40 Presenting theory "IP_Addresses.CIDR_Split"
20:31:40 Presenting theory "HOL-Library.AList_Mapping"
20:31:40 Presenting theory "HOL-Library.Product_Lexorder"
20:31:40 Presenting theory "IP_Addresses.WordInterval_Sorted"
20:31:40 Presenting theory "HOL-ODE-Numerics.Transfer_Analysis"
20:31:40 Presenting theory "HOL-Library.Code_Abstract_Char"
20:31:40 Presenting theory "HOL-Library.Code_Abstract_Nat"
20:31:41 Presenting theory "HOL-ODE-Numerics.Transfer_ODE"
20:31:41 Presenting theory "HOL-Library.Code_Target_Nat"
20:31:41 Presenting theory "HOL-Library.Code_Abstract_Nat"
20:31:41 Presenting theory "HOL-Library.Code_Binary_Nat"
20:31:41 Presenting theory "Iptables_Semantics_Examples.Analyze_SQRL_Shorewall"
20:31:42 Presenting theory "HOL-Library.Extended_Nonnegative_Real"
20:31:42 Presenting theory "Iptables_Semantics_Examples.SQRL_2015_nospoof"
20:31:42 Presenting theory "Iptables_Semantics.Semantics_Goto"
20:31:42 Presenting theory "HOL-Library.Complex_Order"
20:31:42 Presenting theory "HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector"
20:31:42 Presenting theory "Iptables_Semantics.Negation_Type_DNF"
20:31:42 Presenting theory "Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing"
20:31:43 Presenting theory "Iptables_Semantics.Matching_Embeddings"
20:31:43 Presenting theory "HOL-ODE-Numerics.Refine_Hyperplane"
20:31:43 Presenting theory "HOL-ODE-Numerics.Refine_Unions"
20:31:44 Presenting theory "Iptables_Semantics_Examples.Analyze_medium_sized_company"
20:31:44 Presenting Iptables_Semantics_Examples_Big in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big" ...
20:31:44 Presenting document Iptables_Semantics_Examples_Big/document
20:31:44 Presenting document Iptables_Semantics_Examples_Big/outline
20:31:44 Presenting theory "Iptables_Semantics.Fixed_Action"
20:31:44 Presenting theory "HOL-ODE-Numerics.Refine_Intersection"
20:31:44 Presenting theory "Iptables_Semantics_Examples_Big.Analyze_topos_generated"
20:31:45 Presenting theory "HOL-ODE-Numerics.Refine_Invar"
20:31:45 Presenting theory "Iptables_Semantics.Normalized_Matches"
20:31:45 Presenting theory "HOL-Library.Code_Prolog"
20:31:45 Presenting file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
20:31:46 Presenting theory "HOL-Library.Code_Target_Int"
20:31:46 Presenting theory "Iptables_Semantics.Negation_Type_Matching"
20:31:46 Presenting theory "HOL-Library.Code_Real_Approx_By_Float"
20:31:46 Presenting theory "HOL-Library.Code_Target_Nat"
20:31:46 Presenting theory "HOL-Library.Code_Target_Numeral"
20:31:46 Presenting theory "HOL-Library.Code_Target_Numeral_Float"
20:31:46 Presenting theory "HOL-Library.Complex_Order"
20:31:47 Presenting theory "HOL-Library.DAList"
20:31:47 Presenting theory "HOL-ODE-Numerics.Refine_Interval"
20:31:48 Presenting theory "HOL-Library.DAList_Multiset"
20:31:48 Presenting theory "HOL-ODE-Numerics.Refine_Info"
20:31:49 Presenting theory "HOL-ODE-Numerics.Abstract_Rigorous_Numerics"
20:31:49 Presenting theory "Iptables_Semantics.Primitive_Normalization"
20:31:49 Presenting theory "HOL-ODE-Numerics.Refine_Rigorous_Numerics"
20:31:49 Presenting theory "Iptables_Semantics.MatchExpr_Fold"
20:31:49 Presenting theory "Iptables_Semantics.Common_Primitive_Lemmas"
20:31:50 Presenting theory "IP_Addresses.IP_Address_Parser"
20:31:50 Presenting theory "IP_Addresses.Lib_Numbers_toString"
20:31:50 Presenting theory "HOL-Types_To_Sets.Types_To_Sets"
20:31:50 Presenting file "~~/src/HOL/Types_To_Sets/local_typedef.ML"
20:31:50 Presenting file "~~/src/HOL/Types_To_Sets/unoverloading.ML"
20:31:50 Presenting file "~~/src/HOL/Types_To_Sets/internalize_sort.ML"
20:31:50 Presenting file "~~/src/HOL/Types_To_Sets/unoverload_type.ML"
20:31:50 Presenting file "~~/src/HOL/Types_To_Sets/unoverload_def.ML"
20:31:50 Presenting theory "IP_Addresses.Lib_Word_toString"
20:31:50 Presenting theory "IP_Addresses.Lib_List_toString"
20:31:50 Presenting theory "IP_Addresses.IP_Address_toString"
20:31:50 Presenting theory "IP_Addresses.Prefix_Match_toString"
20:31:50 Presenting theory "HOL.BNF_Def"
20:31:50 Presenting file "~~/src/HOL/Tools/BNF/bnf_util.ML"
20:31:50 Presenting file "~~/src/HOL/Tools/BNF/bnf_tactics.ML"
20:31:50 Presenting file "~~/src/HOL/Tools/BNF/bnf_def_tactics.ML"
20:31:50 Presenting theory "HOL-Analysis.Infinite_Sum"
20:31:50 Presenting file "~~/src/HOL/Tools/BNF/bnf_def.ML"
20:31:51 Presenting theory "HOL-Library.Product_Order"
20:31:51 Presenting theory "Iptables_Semantics.Ports_Normalize"
20:31:51 Presenting theory "Bicategory.EquivalenceOfBicategories"
20:31:51 Presenting theory "HOL-Analysis.Ordered_Euclidean_Space"
20:31:51 Presenting theory "Iptables_Semantics.IpAddresses_Normalize"
20:31:51 Presenting theory "HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform"
20:31:51 Presenting theory "Iptables_Semantics.Interfaces_Normalize"
20:31:52 Presenting theory "Iptables_Semantics.Word_Upto"
20:31:52 Presenting theory "Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small"
20:31:52 Presenting theory "Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall"
20:31:52 Presenting theory "Iptables_Semantics.Protocols_Normalize"
20:31:52 Presenting theory "Iptables_Semantics.Remdups_Rev"
20:31:52 Presenting theory "Iptables_Semantics_Examples_Big.Analyze_Containern"
20:31:52 Presenting theory "HOL-Computational_Algebra.Factorial_Ring"
20:31:53 Presenting theory "HOL-ODE-Numerics.Concrete_Rigorous_Numerics"
20:31:53 Presenting theory "Iptables_Semantics.Ipassmt"
20:31:53 Presenting theory "HOL.BNF_Composition"
20:31:53 Presenting file "~~/src/HOL/Tools/BNF/bnf_comp_tactics.ML"
20:31:53 Presenting file "~~/src/HOL/Tools/BNF/bnf_comp.ML"
20:31:53 Presenting theory "Affine_Arithmetic.Float_Real"
20:31:53 Presenting theory "HOL.Basic_BNFs"
20:31:53 Presenting theory "HOL-Computational_Algebra.Euclidean_Algorithm"
20:31:53 Presenting theory "Affine_Arithmetic.Ex_Affine_Approximation"
20:31:53 Presenting theory "HOL-Library.RBT_Impl"
20:31:53 Presenting theory "Affine_Arithmetic.Ex_Ineqs"
20:31:54 Presenting theory "HOL-Computational_Algebra.Primes"
20:31:54 Presenting theory "Iptables_Semantics.No_Spoof"
20:31:54 Presenting theory "HOL-Library.RBT"
20:31:54 Presenting theory "Affine_Arithmetic.Ex_Inter"
20:31:54 Presenting theory "Iptables_Semantics.Common_Primitive_toString"
20:31:54 Presenting theory "Affine_Arithmetic.Affine_Arithmetic"
20:31:54 Presenting theory "HOL-Library.RBT_Mapping"
20:31:54 Presenting theory "HOL-ODE-Numerics.Refine_String"
20:31:54 Presenting theory "Iptables_Semantics.Routing_IpAssmt"
20:31:54 Presenting theory "Iptables_Semantics_Examples_Big.TUM_Spoofing_new3"
20:31:54 Presenting theory "HOL-ODE-Numerics.Refine_Folds"
20:31:54 Presenting theory "Iptables_Semantics.Output_Interface_Replace"
20:31:55 Presenting theory "HOL-Library.RBT_Set"
20:31:55 Presenting theory "Iptables_Semantics.Interface_Replace"
20:31:55 Presenting theory "HOL-Library.LaTeXsugar"
20:31:55 Presenting theory "HOL-Library.OptionalSugar"
20:31:55 Presenting theory "HOL-ODE-Numerics.One_Step_Method"
20:31:55 Presenting theory "Iptables_Semantics.Optimizing"
20:31:55 Presenting theory "HOL-Library.Predicate_Compile_Alternative_Defs"
20:31:55 Presenting theory "Iptables_Semantics_Examples_Big.TUM_Simple_FW"
20:31:56 Presenting theory "HOL-Library.Predicate_Compile_Quickcheck"
20:31:56 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
20:31:56 Presenting theory "Bicategory.SpanBicategory"
20:31:56 Presenting theory "HOL-Analysis.Arcwise_Connected"
20:31:56 Presenting theory "HOL-ODE-Numerics.Runge_Kutta"
20:31:57 Presenting theory "Iptables_Semantics.Transform"
20:31:57 Presenting theory "HOL-ODE-Numerics.Abstract_Reachability_Analysis"
20:31:57 Presenting theory "Iptables_Semantics.Conntrack_State_Transform"
20:31:57 Presenting theory "Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large"
20:31:58 Presenting theory "Iptables_Semantics.Primitive_Abstract"
20:31:59 Presenting theory "HOL-ODE-Numerics.Concrete_Reachability_Analysis"
20:31:59 Presenting theory "HOL-Library.Old_Recdef"
20:31:59 Presenting theory "HOL-ODE-Numerics.Refine_Parallel"
20:31:59 Presenting file "~~/src/HOL/Library/old_recdef.ML"
20:31:59 Presenting theory "HOL-ODE-Numerics.Refine_Default"
20:31:59 Presenting theory "HOL-ODE-Numerics.Refine_Phantom"
20:32:00 Presenting theory "Iptables_Semantics.SimpleFw_Compliance"
20:32:00 Presenting theory "HOL-ODE-Numerics.Refine_ScaleR2"
20:32:00 Presenting theory "Iptables_Semantics.Semantics_Embeddings"
20:32:00 Presenting theory "Iptables_Semantics.Iptables_Semantics"
20:32:01 Presenting theory "HOL-Library.Code_Target_Int"
20:32:01 Presenting theory "Native_Word.Code_Int_Integer_Conversion"
20:32:01 Presenting theory "HOL-Library.Realizers"
20:32:01 Presenting file "~~/src/HOL/Tools/datatype_realizer.ML"
20:32:01 Presenting file "~~/src/HOL/Tools/inductive_realizer.ML"
20:32:01 Presenting theory "Native_Word.Code_Target_Integer_Bit"
20:32:01 Presenting theory "Native_Word.Code_Target_Int_Bit"
20:32:01 Presenting theory "Iptables_Semantics.Code_Interface"
20:32:03 Presenting theory "Iptables_Semantics.Parser6"
20:32:04 Presenting theory "Bicategory.Tabulation"
20:32:04 Presenting theory "Iptables_Semantics.No_Spoof_Embeddings"
20:32:04 Presenting theory "HOL-Analysis.Urysohn"
20:32:04 Presenting theory "HOL-Library.Refute"
20:32:05 Presenting file "~~/src/HOL/Library/refute.ML"
20:32:05 Presenting theory "Iptables_Semantics.Parser"
20:32:05 Presenting theory "Iptables_Semantics.Code_haskell"
20:32:05 Presenting theory "Iptables_Semantics.Access_Matrix_Embeddings"
20:32:05 Presenting theory "Iptables_Semantics.Documentation"
20:32:05 Presenting theory "HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1"
20:32:05 Presenting theory "HOL.BNF_Fixpoint_Base"
20:32:05 Presenting theory "HOL-Analysis.Isolated"
20:32:05 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_util_tactics.ML"
20:32:05 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_util.ML"
20:32:05 Presenting theory "HOL-Analysis.Operator_Norm"
20:32:05 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML"
20:32:05 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML"
20:32:05 Presenting theory "HOL-Library.Discrete"
20:32:05 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML"
20:32:05 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m.ML"
20:32:05 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML"
20:32:06 Presenting theory "HOL-Analysis.Extended_Real_Limits"
20:32:07 Presenting theory "HOL-Analysis.Summation_Tests"
20:32:07 Presenting theory "HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1"
20:32:07 Presenting theory "HOL-Analysis.Uniform_Limit"
20:32:08 Presenting theory "HOL-Analysis.Bounded_Linear_Function"
20:32:08 Presenting theory "HOL-ODE-Numerics.Refine_Reachability_Analysis"
20:32:08 Presenting theory "HOL.BNF_Least_Fixpoint"
20:32:09 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_util.ML"
20:32:09 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_tactics.ML"
20:32:09 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp.ML"
20:32:09 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_compat.ML"
20:32:09 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML"
20:32:09 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_size.ML"
20:32:09 Presenting file "~~/src/HOL/Tools/datatype_simprocs.ML"
20:32:09 Presenting theory "HOL.Equiv_Relations"
20:32:09 Presenting theory "HOL-Analysis.Derivative"
20:32:09 Presenting theory "HOL.Basic_BNF_LFPs"
20:32:09 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML"
20:32:09 Presenting theory "Bicategory.BicategoryOfSpans"
20:32:10 Presenting theory "HOL.Meson"
20:32:10 Presenting file "~~/src/HOL/Tools/Meson/meson.ML"
20:32:10 Presenting file "~~/src/HOL/Tools/Meson/meson_clausify.ML"
20:32:10 Presenting file "~~/src/HOL/Tools/Meson/meson_tactic.ML"
20:32:10 Presenting theory "HOL-Analysis.Cartesian_Euclidean_Space"
20:32:10 Presenting theory "HOL-Library.Nonpos_Ints"
20:32:10 Presenting theory "HOL-ODE-Numerics.Refine_Reachability_Analysis_C1"
20:32:11 Presenting theory "HOL-Analysis.Complex_Analysis_Basics"
20:32:11 Presenting theory "HOL-Library.Periodic_Fun"
20:32:12 Presenting theory "HOL-ODE-Numerics.Init_ODE_Solver"
20:32:12 Presenting theory "Bicategory.Modification"
20:32:12 Presenting theory "HOL-Analysis.Complex_Transcendental"
20:32:14 Presenting theory "HOL-Analysis.Sigma_Algebra"
20:32:14 Presenting theory "Bicategory.ConcreteBicategory"
20:32:14 Presenting theory "HOL-ODE-Numerics.Example_Utilities"
20:32:15 Presenting theory "HOL-Analysis.Measurable"
20:32:15 Presenting theory "HOL-ODE-Numerics.ODE_Numerics"
20:32:15 Presenting file "~~/src/HOL/Analysis/measurable.ML"
20:32:15 Presenting theory "HOL.ATP"
20:32:15 Presenting file "~~/src/HOL/Tools/ATP/atp_util.ML"
20:32:15 Presenting file "~~/src/HOL/Tools/ATP/atp_problem.ML"
20:32:15 Presenting file "~~/src/HOL/Tools/ATP/atp_proof.ML"
20:32:15 Presenting file "~~/src/HOL/Tools/ATP/atp_proof_redirect.ML"
20:32:15 Presenting file "~~/src/HOL/Tools/lambda_lifting.ML"
20:32:15 Presenting file "~~/src/HOL/Tools/monomorph.ML"
20:32:15 Presenting file "~~/src/HOL/Tools/ATP/atp_problem_generate.ML"
20:32:15 Presenting file "~~/src/HOL/Tools/ATP/atp_proof_reconstruct.ML"
20:32:15 Presenting theory "Bicategory.CatBicat"
20:32:16 Presenting theory "HOL-Analysis.Measure_Space"
20:32:17 Presenting theory "HOL-Analysis.Borel_Space"
20:32:17 Presenting theory "HOL.Metis"
20:32:17 Presenting file "~~/src/Tools/Metis/metis.ML"
20:32:18 Presenting theory "HOL-Analysis.Nonnegative_Lebesgue_Integration"
20:32:18 Presenting file "~~/src/HOL/Tools/Metis/metis_generate.ML"
20:32:18 Presenting file "~~/src/HOL/Tools/Metis/metis_reconstruct.ML"
20:32:18 Presenting file "~~/src/HOL/Tools/Metis/metis_tactic.ML"
20:32:18 Presenting theory "HOL.Transfer"
20:32:18 Presenting theory "HOL-Analysis.Binary_Product_Measure"
20:32:18 Presenting file "~~/src/HOL/Tools/Transfer/transfer.ML"
20:32:18 Presenting file "~~/src/HOL/Tools/Transfer/transfer_bnf.ML"
20:32:18 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML"
20:32:19 Presenting theory "HOL-Analysis.Finite_Product_Measure"
20:32:19 Presenting theory "HOL.Lifting"
20:32:19 Presenting file "~~/src/HOL/Tools/Lifting/lifting_util.ML"
20:32:19 Presenting file "~~/src/HOL/Tools/Lifting/lifting_info.ML"
20:32:19 Presenting file "~~/src/HOL/Tools/Lifting/lifting_bnf.ML"
20:32:19 Presenting file "~~/src/HOL/Tools/Lifting/lifting_term.ML"
20:32:19 Presenting file "~~/src/HOL/Tools/Lifting/lifting_def.ML"
20:32:19 Presenting theory "HOL-Analysis.Caratheodory"
20:32:19 Presenting file "~~/src/HOL/Tools/Lifting/lifting_setup.ML"
20:32:19 Presenting file "~~/src/HOL/Tools/Lifting/lifting_def_code_dt.ML"
20:32:20 Presenting theory "HOL-Analysis.Bochner_Integration"
20:32:20 Presenting theory "HOL.Quotient"
20:32:20 Presenting file "~~/src/HOL/Tools/Quotient/quotient_info.ML"
20:32:20 Presenting file "~~/src/HOL/Tools/Quotient/quotient_term.ML"
20:32:20 Presenting file "~~/src/HOL/Tools/Quotient/quotient_type.ML"
20:32:20 Presenting file "~~/src/HOL/Tools/Quotient/quotient_def.ML"
20:32:20 Presenting file "~~/src/HOL/Tools/Quotient/quotient_tacs.ML"
20:32:20 Presenting file "~~/src/HOL/Tools/BNF/bnf_lift.ML"
20:32:21 Presenting theory "HOL-Analysis.Complete_Measure"
20:32:21 Presenting theory "HOL.Num"
20:32:21 Presenting file "~~/src/HOL/Tools/numeral.ML"
20:32:21 Presenting theory "HOL-Analysis.Regularity"
20:32:21 Presenting theory "HOL.Power"
20:32:21 Presenting theory "HOL-Analysis.Lebesgue_Measure"
20:32:21 Presenting theory "HOL.Groups_Big"
20:32:22 Presenting theory "HOL.Complete_Partial_Order"
20:32:22 Presenting theory "HOL.Option"
20:32:22 Presenting theory "HOL.Partial_Function"
20:32:22 Presenting file "~~/src/HOL/Tools/Function/partial_function.ML"
20:32:22 Presenting theory "HOL-Analysis.Tagged_Division"
20:32:23 Presenting theory "HOL.Argo"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_expr.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_term.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_lit.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_proof.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_rewr.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_cls.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_common.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_cc.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_simplex.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_thy.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_heap.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_cdcl.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_core.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_clausify.ML"
20:32:23 Presenting file "~~/src/Tools/Argo/argo_solver.ML"
20:32:23 Presenting file "~~/src/HOL/Tools/Argo/argo_tactic.ML"
20:32:23 Presenting theory "HOL.SAT"
20:32:23 Presenting file "~~/src/HOL/Tools/prop_logic.ML"
20:32:23 Presenting file "~~/src/HOL/Tools/sat_solver.ML"
20:32:23 Presenting file "~~/src/HOL/Tools/sat.ML"
20:32:23 Presenting file "~~/src/HOL/Tools/Argo/argo_sat_solver.ML"
20:32:24 Presenting theory "HOL-Analysis.Henstock_Kurzweil_Integration"
20:32:24 Presenting theory "HOL.Fun_Def"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/function_core.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/mutual.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/pattern_split.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/relation.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/function_elims.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/function.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/pat_completeness.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/fun.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/induction_schema.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/measure_functions.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/lexicographic_order.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/termination.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/scnp_solve.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/scnp_reconstruct.ML"
20:32:24 Presenting file "~~/src/HOL/Tools/Function/fun_cases.ML"
20:32:24 Presenting theory "HOL.Int"
20:32:25 Presenting file "~~/src/HOL/Tools/int_arith.ML"
20:32:25 Presenting theory "HOL.Lattices_Big"
20:32:25 Presenting theory "HOL.Euclidean_Rings"
20:32:26 Presenting theory "HOL.Parity"
20:32:26 Presenting theory "HOL.Numeral_Simprocs"
20:32:26 Presenting file "~~/src/Provers/Arith/assoc_fold.ML"
20:32:26 Presenting file "~~/src/Provers/Arith/cancel_numerals.ML"
20:32:26 Presenting file "~~/src/Provers/Arith/combine_numerals.ML"
20:32:26 Presenting file "~~/src/Provers/Arith/cancel_numeral_factor.ML"
20:32:26 Presenting file "~~/src/Provers/Arith/extract_common_term.ML"
20:32:26 Presenting file "~~/src/HOL/Tools/numeral_simprocs.ML"
20:32:26 Presenting file "~~/src/HOL/Tools/nat_numeral_simprocs.ML"
20:32:26 Presenting theory "HOL-Library.BNF_Corec"
20:32:27 Presenting theory "HOL.Semiring_Normalization"
20:32:27 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML"
20:32:27 Presenting file "~~/src/HOL/Tools/semiring_normalizer.ML"
20:32:27 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML"
20:32:27 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML"
20:32:27 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML"
20:32:27 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML"
20:32:27 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
20:32:27 Presenting theory "HOL.Groebner_Basis"
20:32:27 Presenting file "~~/src/HOL/Tools/groebner.ML"
20:32:27 Presenting theory "HOL-Library.Landau_Symbols"
20:32:27 Presenting theory "HOL.Set_Interval"
20:32:28 Presenting theory "HOL-Real_Asymp.Lazy_Eval"
20:32:28 Presenting file "~~/src/HOL/Real_Asymp/lazy_eval.ML"
20:32:28 Presenting theory "HOL-Real_Asymp.Inst_Existentials"
20:32:28 Presenting file "~~/src/HOL/Real_Asymp/inst_existentials.ML"
20:32:28 Presenting theory "HOL-Real_Asymp.Eventuallize"
20:32:29 Presenting theory "HOL.Presburger"
20:32:29 Presenting file "~~/src/HOL/Tools/Qelim/qelim.ML"
20:32:29 Presenting file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"
20:32:29 Presenting file "~~/src/HOL/Tools/Qelim/cooper.ML"
20:32:29 Presenting file "~~/src/HOL/Tools/try0.ML"
20:32:30 Presenting theory "HOL-Real_Asymp.Multiseries_Expansion"
20:32:31 Presenting file "~~/src/HOL/Real_Asymp/asymptotic_basis.ML"
20:32:31 Presenting file "~~/src/HOL/Real_Asymp/exp_log_expression.ML"
20:32:31 Presenting file "~~/src/HOL/Real_Asymp/expansion_interface.ML"
20:32:31 Presenting file "~~/src/HOL/Real_Asymp/multiseries_expansion.ML"
20:32:31 Presenting file "~~/src/HOL/Real_Asymp/real_asymp.ML"
20:32:32 Presenting theory "HOL.SMT"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smt_util.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smt_failure.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smt_config.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smt_builtin.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smt_datatypes.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smt_normalize.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smt_translate.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smtlib.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smtlib_interface.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smtlib_proof.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smtlib_isar.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/z3_proof.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/z3_isar.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smt_solver.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/cvc_interface.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/lethe_proof.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/lethe_isar.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/lethe_proof_parse.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/cvc_proof_parse.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/conj_disj_perm.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smt_replay_methods.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smt_replay.ML"
20:32:32 Presenting theory "HOL-Real_Asymp.Multiseries_Expansion_Bounds"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smt_replay_arith.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/z3_interface.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/z3_replay_rules.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/z3_replay_methods.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/z3_replay.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/lethe_replay_methods.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/cvc5_replay_methods.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/verit_replay_methods.ML"
20:32:32 Presenting file "~~/src/HOL/Real_Asymp/multiseries_expansion_bounds.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/verit_strategies.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/verit_replay.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/cvc5_replay.ML"
20:32:32 Presenting file "~~/src/HOL/Tools/SMT/smt_systems.ML"
20:32:32 Presenting theory "HOL-Real_Asymp.Real_Asymp"
20:32:32 Presenting file "~~/src/HOL/Real_Asymp/real_asymp_diag.ML"
20:32:33 Presenting theory "HOL-Analysis.Kronecker_Approximation_Theorem"
20:32:33 Presenting theory "HOL-Analysis.Weierstrass_Theorems"
20:32:34 Presenting theory "HOL.Sledgehammer"
20:32:34 Presenting theory "HOL-Analysis.Radon_Nikodym"
20:32:34 Presenting file "~~/src/HOL/Tools/ATP/system_on_tptp.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer.ML"
20:32:34 Presenting theory "HOL-Analysis.Set_Integral"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML"
20:32:34 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML"
20:32:34 Presenting theory "HOL.Lifting_Set"
20:32:35 Presenting theory "HOL-Analysis.Homeomorphism"
20:32:36 Presenting theory "HOL.List"
20:32:36 Presenting theory "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration"
20:32:37 Presenting theory "HOL.Groups_List"
20:32:37 Presenting theory "HOL-Analysis.Harmonic_Numbers"
20:32:38 Presenting theory "HOL.Bit_Operations"
20:32:38 Presenting theory "HOL-Analysis.Gamma_Function"
20:32:38 Presenting theory "HOL.Code_Numeral"
20:32:38 Presenting theory "HOL.Random"
20:32:38 Presenting theory "HOL.Map"
20:32:39 Presenting theory "HOL.Enum"
20:32:39 Presenting theory "HOL.String"
20:32:39 Presenting theory "HOL-Analysis.Interval_Integral"
20:32:39 Presenting file "~~/src/HOL/Tools/string_syntax.ML"
20:32:39 Presenting file "~~/src/HOL/Tools/literal.ML"
20:32:39 Presenting theory "HOL.Typerep"
20:32:39 Presenting theory "HOL.Predicate"
20:32:39 Presenting theory "HOL-Analysis.Lebesgue_Integral_Substitution"
20:32:39 Presenting theory "HOL.Lazy_Sequence"
20:32:39 Presenting theory "HOL.Limited_Sequence"
20:32:39 Presenting theory "HOL-Analysis.Ball_Volume"
20:32:39 Presenting theory "HOL-Analysis.Integral_Test"
20:32:39 Presenting theory "HOL.Code_Evaluation"
20:32:39 Presenting file "~~/src/HOL/Tools/code_evaluation.ML"
20:32:39 Presenting file "~~/src/HOL/Tools/value_command.ML"
20:32:39 Presenting file "~~/src/HOL/Tools/reification.ML"
20:32:40 Presenting theory "HOL.Quickcheck_Random"
20:32:40 Presenting file "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML"
20:32:40 Presenting file "~~/src/HOL/Tools/Quickcheck/random_generators.ML"
20:32:40 Presenting theory "HOL.Random_Pred"
20:32:40 Presenting theory "HOL.Random_Sequence"
20:32:40 Presenting theory "HOL-Analysis.Improper_Integral"
20:32:40 Presenting theory "HOL.Quickcheck_Exhaustive"
20:32:40 Presenting file "~~/src/HOL/Tools/Quickcheck/exhaustive_generators.ML"
20:32:41 Presenting theory "HOL-Analysis.Continuous_Extension"
20:32:41 Presenting file "~~/src/HOL/Tools/Quickcheck/abstract_generators.ML"
20:32:41 Presenting theory "HOL-Analysis.Equivalence_Measurable_On_Borel"
20:32:42 Presenting theory "HOL-Analysis.Embed_Measure"
20:32:43 Presenting theory "HOL-Analysis.Brouwer_Fixpoint"
20:32:43 Presenting theory "HOL.Predicate_Compile"
20:32:43 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML"
20:32:43 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML"
20:32:43 Presenting file "~~/src/HOL/Tools/Predicate_Compile/core_data.ML"
20:32:43 Presenting file "~~/src/HOL/Tools/Predicate_Compile/mode_inference.ML"
20:32:43 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML"
20:32:43 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML"
20:32:43 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML"
20:32:43 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML"
20:32:43 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML"
20:32:43 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML"
20:32:43 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile.ML"
20:32:43 Presenting theory "HOL-Analysis.Fashoda_Theorem"
20:32:43 Presenting theory "HOL.Quickcheck_Narrowing"
20:32:43 Presenting theory "HOL-Analysis.Cross3"
20:32:43 Presenting file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"
20:32:43 Presenting file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"
20:32:43 Presenting file "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
20:32:43 Presenting file "~~/src/HOL/Tools/Quickcheck/find_unused_assms.ML"
20:32:43 Presenting theory "HOL-Analysis.Bounded_Continuous_Function"
20:32:44 Presenting theory "HOL.Mirabelle"
20:32:44 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_util.ML"
20:32:44 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle.ML"
20:32:44 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_arith.ML"
20:32:44 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_metis.ML"
20:32:44 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML"
20:32:44 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML"
20:32:44 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML"
20:32:44 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"
20:32:44 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_try0.ML"
20:32:44 Presenting theory "HOL.Extraction"
20:32:44 Presenting theory "HOL-Analysis.Infinite_Products"
20:32:44 Presenting theory "HOL.Record"
20:32:44 Presenting file "~~/src/HOL/Tools/record.ML"
20:32:44 Presenting theory "HOL-Analysis.Infinite_Set_Sum"
20:32:45 Presenting theory "HOL.GCD"
20:32:45 Presenting theory "HOL-Analysis.Polytope"
20:32:46 Presenting theory "HOL-Analysis.Retracts"
20:32:48 Presenting theory "HOL.Nitpick"
20:32:48 Presenting theory "HOL-Analysis.Further_Topology"
20:32:48 Presenting file "~~/src/HOL/Tools/Nitpick/kodkod.ML"
20:32:48 Presenting file "~~/src/HOL/Tools/Nitpick/kodkod_sat.ML"
20:32:48 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_util.ML"
20:32:48 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_hol.ML"
20:32:48 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_mono.ML"
20:32:48 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_preproc.ML"
20:32:48 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_scope.ML"
20:32:48 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_peephole.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_rep.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_nut.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_kodkod.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_model.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_commands.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_tests.ML"
20:32:49 Presenting theory "HOL-Analysis.Jordan_Curve"
20:32:49 Presenting theory "HOL-Analysis.Poly_Roots"
20:32:49 Presenting theory "HOL-Analysis.Generalised_Binomial_Theorem"
20:32:49 Presenting theory "HOL.Nunchaku"
20:32:49 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_util.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_collect.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_problem.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_translate.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_model.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_display.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_tool.ML"
20:32:49 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku.ML"
20:32:49 Presenting theory "HOL-Analysis.Vitali_Covering_Theorem"
20:32:49 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_commands.ML"
20:32:51 Presenting theory "HOL-Analysis.Change_Of_Vars"
20:32:51 Presenting theory "HOL.BNF_Greatest_Fixpoint"
20:32:51 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_util.ML"
20:32:51 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_tactics.ML"
20:32:51 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp.ML"
20:32:52 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
20:32:52 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML"
20:32:52 Presenting theory "HOL-Analysis.Lipschitz"
20:32:52 Presenting theory "HOL-Analysis.Multivariate_Analysis"
20:32:52 Presenting theory "HOL.Filter"
20:32:52 Presenting theory "HOL-Analysis.Simplex_Content"
20:32:52 Presenting theory "HOL.Conditionally_Complete_Lattices"
20:32:53 Presenting theory "HOL.Factorial"
20:32:53 Presenting theory "HOL.Binomial"
20:32:53 Presenting theory "HOL-Computational_Algebra.Formal_Power_Series"
20:32:53 Presenting theory "HOL.Divides"
20:32:53 Presenting theory "Main"
20:32:53 Presenting theory "HOL.Archimedean_Field"
20:32:54 Presenting theory "HOL.Rat"
20:32:54 Presenting theory "HOL-Analysis.FPS_Convergence"
20:32:54 Presenting theory "HOL.Real"
20:32:55 Presenting theory "HOL-Analysis.Smooth_Paths"
20:32:55 Presenting file "~~/src/HOL/Tools/SMT/smt_real.ML"
20:32:55 Presenting file "~~/src/HOL/Tools/SMT/z3_real.ML"
20:32:55 Presenting file "~~/src/HOL/Tools/Argo/argo_real.ML"
20:32:55 Presenting theory "HOL-Analysis.Function_Metric"
20:32:55 Presenting theory "HOL-Analysis.Analysis"
20:32:55 Presenting theory "HOL.Topological_Spaces"
20:32:56 Presenting theory "HOL.Hull"
20:32:56 Presenting theory "HOL.Modules"
20:32:56 Presenting theory "HOL.Vector_Spaces"
20:32:57 Presenting theory "HOL.Real_Vector_Spaces"
20:32:58 Presenting theory "HOL.Limits"
20:32:58 Presenting theory "HOL.Inequalities"
20:32:58 Presenting theory "HOL.Series"
20:32:59 Presenting theory "HOL.Deriv"
20:32:59 Presenting theory "HOL.NthRoot"
20:33:00 Presenting theory "HOL.Transcendental"
20:33:02 Presenting theory "HOL.Complex"
20:33:02 Presenting theory "HOL.MacLaurin"
20:33:02 Presenting theory "Complex_Main"
20:33:02 Unfinished session(s): JinjaThreads
20:33:02 
20:33:02 === TIMING ===
20:33:02 
20:33:02 Group slow: 17:05:31 elapsed time, 81:38:07 cpu time, factor 4.78
20:33:02 Group AFP: 18:04:42 elapsed time, 85:47:17 cpu time, factor 4.75
20:33:02 Group main: 0:21:44 elapsed time, 1:48:36 cpu time, factor 4.99
20:33:02 Group timing: 0:15:20 elapsed time, 1:25:16 cpu time, factor 5.56
20:33:02 Group very_slow: 14:20:41 elapsed time, 67:16:31 cpu time, factor 4.69
20:33:02 Overall: 18:49:47 elapsed time, 87:36:20 cpu time, factor 4.65
20:33:02 
20:33:02 === FAILED SESSIONS ===
20:33:02 
20:33:02 Session JinjaThreads: FAILED 1
20:33:02 Build step 'Execute shell' marked build as failure
20:33:04 Archiving artifacts
20:33:24 Started calculate disk usage of build
20:33:25 Finished Calculation of disk usage of build in 0 seconds
20:35:03 Started calculate disk usage of workspace
20:35:07 Finished Calculation of disk usage of workspace in  4 second
20:35:08 No emails were triggered.
20:35:08 Finished: FAILURE