Skip to content
[Jenkins]Jenkins
log in
Failed

Console Output

01:35:21 Started by an SCM change


01:35:21 Running as SYSTEM


01:35:21 [EnvInject] - Loading node environment variables.


01:35:21 Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow


01:35:21 [isabelle-nightly-slow] $ hg showconfig paths.default


01:35:21 ERROR: Workspace reports paths.default as http://isabelle.in.tum.de/repos/isabelle/


01:35:21 which looks different than https://isabelle.in.tum.de/repos/isabelle/


01:35:21 so falling back to fresh clone rather than incremental update


01:35:26 $ hg clone --rev default --noupdate https://isabelle.in.tum.de/repos/isabelle/ /media/data/jenkins/workspace/isabelle-nightly-slow


01:36:15 adding changesets


01:36:15 adding manifests


01:36:15 adding file changes


01:36:17 added 79742 changesets with 215840 changes to 11707 files


01:36:17 new changesets a5a9c433f639:513829904beb


01:36:17 [isabelle-nightly-slow] $ hg update --rev default


01:36:18 3608 files updated, 0 files merged, 0 files removed, 0 files unresolved


01:36:18 [isabelle-nightly-slow] $ hg log --rev . --template {node}


01:36:18 [isabelle-nightly-slow] $ hg log --rev . --template {rev}


01:36:18 WARN: Revision data for previous build unavailable; unable to determine change log


01:36:18 $ hg clone --rev default --noupdate https://foss.heptapod.net/isa-afp/afp-devel/ /media/data/jenkins/workspace/isabelle-nightly-slow/afp


01:36:59 adding changesets


01:36:59 adding manifests


01:36:59 adding file changes


01:36:59 added 14078 changesets with 120006 changes to 20154 files


01:36:59 new changesets 86acbdb19eec:ef55afaa373b


01:36:59 [afp] $ hg update --rev default


01:37:02 16357 files updated, 0 files merged, 0 files removed, 0 files unresolved


01:37:02 [afp] $ hg log --rev . --template {node}


01:37:02 [afp] $ hg log --rev . --template {rev}


01:37:02 WARN: Revision data for previous build unavailable; unable to determine change log


01:37:02 No emails were triggered.


01:37:03 [isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins4710059513728717569.sh


01:37:03 + Admin/jenkins/run_build slow


01:37:03 + set -e


01:37:03 + PROFILE=slow


01:37:03 + shift


01:37:03 + bin/isabelle components -a


01:37:03 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/javamail-20240109"


01:37:03 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/jdk-21.0.2"


01:37:03 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/llncs-2.23"


01:37:03 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/postgresql-42.7.1"


01:37:03 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/sqlite-jdbc-3.45.0.0"


01:37:03 ### 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