Skip to content
[Jenkins]Jenkins
log in
Success

Console Output

01:33:11 Started by an SCM change


01:33:11 Running as SYSTEM


01:33:11 [EnvInject] - Loading node environment variables.


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


01:33:11 [isabelle-nightly-slow] $ hg showconfig paths.default


01:33:11 [isabelle-nightly-slow] $ hg pull --rev default


01:33:11 pulling from https://isabelle.in.tum.de/repos/isabelle/


01:33:11 no changes found


01:33:11 [isabelle-nightly-slow] $ hg update --clean --rev default


01:33:11 14 files updated, 0 files merged, 0 files removed, 0 files unresolved


01:33:11 [isabelle-nightly-slow] $ hg --config extensions.purge= clean --all


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


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


01:33:13 WARN: Revision data for previous build unavailable; unable to determine change log


01:33:13 [afp] $ hg showconfig paths.default


01:33:13 [afp] $ hg pull --rev default


01:33:13 pulling from https://foss.heptapod.net/isa-afp/afp-devel/


01:33:13 no changes found


01:33:13 [afp] $ hg update --clean --rev default


01:33:14 23 files updated, 0 files merged, 0 files removed, 0 files unresolved


01:33:14 [afp] $ hg --config extensions.purge= clean --all


01:33:14 [afp] $ hg log --rev . --template {node}


01:33:14 [afp] $ hg log --rev . --template {rev}


01:33:15 WARN: Revision data for previous build unavailable; unable to determine change log


01:33:15 No emails were triggered.


01:33:15 [isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins12914577238174036496.sh


01:33:15 + Admin/jenkins/run_build slow


01:33:15 + set -e


01:33:15 + PROFILE=slow


01:33:15 + shift


01:33:15 + bin/isabelle components -a


01:33:15 ### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/z3-4.4.0pre-4"


01:33:15 Getting "https://isabelle.sketis.net/components/z3-4.4.0pre-4.tar.gz"


01:33:16 Unpacking "/media/data/jenkins/.isabelle/contrib/z3-4.4.0pre-4.tar.gz"


01:33:16 + bin/isabelle jedit -bf


01:33:17 ### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle.jar) ...


01:34:13 ### Building Demo (/media/data/jenkins/workspace/isabelle-nightly-slow/src/Tools/Demo/lib/demo.jar) ...


01:34:13 ### Building graph browser (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle_graphbrowser.jar) ...


01:34:14 Note: Some input files use unchecked or unsafe operations.


01:34:14 Note: Recompile with -Xlint:unchecked for details.


01:34:14 ### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle_admin.jar) ...


01:34:14 ### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-nightly-slow/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...


01:34:18 + bin/isabelle ocaml_setup


01:34:18 # Run eval $(opam env) to update the current shell environment


01:34:19 [NOTE] It seems you have not updated your repositories for a while. Consider updating them with:


01:34:19        opam update


01:34:19 

01:34:20 [NOTE] Package zarith is already installed (current version is 1.12).


01:34:20 + bin/isabelle ghc_setup


01:34:21 Stack will use a sandboxed GHC it installed. To use this GHC and packages outside of a project,


01:34:21 consider using: stack ghc, stack ghci, stack runghc, or stack exec.


01:34:22 The Glorious Glasgow Haskell Compilation System, version 9.6.3


01:34:23 + bin/isabelle ci_build slow


01:34:25 

01:34:25 === CONFIGURATION ===


01:34:25 

01:34:25 ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"


01:34:25 ISABELLE_BUILD_OPTIONS=""


01:34:25 

01:34:25 ML_PLATFORM="x86_64-linux"


01:34:25 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.9.1/x86_64-linux"


01:34:25 ML_SYSTEM="polyml-5.9.1"


01:34:25 ML_OPTIONS="-H 4000 --maxheap 32G"


01:34:25 jobs = 1, threads = 8, numa = false


01:34:25 

01:34:25 === BUILD ===


01:34:25 

01:34:25 Build started at Tue, 5 Mar 2024 00:34:25 GMT


01:34:25 Isabelle id 48af00f6f110


01:34:26 Build for AFP id efe28b85919e


01:34:26 

01:34:26 === LOG ===


01:34:26 

01:34:28 Session Pure/Pure


01:34:28 Session FOL/FOL


01:34:28 Session Pure/Pure-Examples


01:34:28 Session Pure/Pure-ex


01:34:28 Session Misc/Tools


01:34:29 Session HOL/HOL (main)


01:34:29 Session AFP/AWN (AFP)


01:34:30 Session AFP/AODV (AFP slow)


01:34:30 Session HOL/HOL-Cardinals (timing)


01:34:30 Session HOL/HOL-Library (main timing)


01:34:30 Session AFP/Binomial-Heaps (AFP)


01:34:31 Session AFP/ConcurrentIMP (AFP)


01:34:31 Session AFP/ConcurrentGC (AFP slow)


01:34:31 Session AFP/FinFun (AFP)


01:34:31 Session AFP/Finger-Trees (AFP)


01:34:31 Session HOL/HOL-Combinatorics (main timing)


01:34:31 Session HOL/HOL-Computational_Algebra (main timing)


01:34:31 Session HOL/HOL-Algebra (main timing)


01:34:32 Session HOL/HOL-Decision_Procs (timing)


01:34:32 Session HOL/HOL-Number_Theory (main timing)


01:34:32 Session HOL/HOL-ex (timing)


01:34:33 Session HOL/HOL-Imperative_HOL (timing)


01:34:33 Session AFP/HereditarilyFinite (AFP)


01:34:33 Session AFP/Trie (AFP)


01:34:33 Session AFP/Flyspeck-Tame (AFP)


01:34:33 Session AFP/Flyspeck-Tame-Computation (AFP slow very_slow)


01:34:33 Session HOL/HOL-Real_Asymp


01:34:33 Session HOL/HOL-Analysis (main timing)


01:34:35 Session AFP/Coinductive (AFP)


01:34:35 Session HOL/HOL-Eisbach


01:34:35 Session AFP/Automatic_Refinement (AFP)


01:34:35 Session AFP/Refine_Monadic (AFP)


01:34:36 Session AFP/Word_Lib (AFP)


01:34:36 Session AFP/IP_Addresses (AFP)


01:34:36 Session AFP/Simple_Firewall (AFP)


01:34:36 Session AFP/Routing (AFP)


01:34:36 Session AFP/Native_Word (AFP)


01:34:36 Session AFP/Collections (AFP)


01:34:37 Session AFP/Iptables_Semantics (AFP)


01:34:37 Session AFP/Iptables_Semantics_Examples (AFP)


01:34:37 Session AFP/Iptables_Semantics_Examples_Big (AFP slow very_slow)


01:34:37 Session AFP/JinjaThreads (AFP slow)


01:34:38 Session AFP/ZFC_in_HOL (AFP)


01:34:38 Session AFP/Category3 (AFP)


01:34:39 Session AFP/MonoidalCategory (AFP)


01:34:39 Session AFP/Bicategory (AFP slow)


01:34:40 Building Pure ...


01:35:03 Pure: theory Pure


01:35:04 Pure: theory ML_Bootstrap


01:35:04 Pure: theory Pure.Sessions


01:35:07 Timing Pure (1 threads, 0.995s elapsed time, 1.042s cpu time, 0.000s GC time, factor 1.05)


01:35:07 Finished Pure (0:00:25 elapsed time, 0:00:25 cpu time, factor 0.99)


01:35:07 Building HOL ...


01:35:11 HOL: theory Tools.Code_Generator


01:35:16 HOL: theory HOL.HOL


01:35:21 HOL: theory HOL.Orderings


01:35:21 HOL: theory HOL.Ctr_Sugar


01:35:21 HOL: theory HOL.Argo


01:35:25 HOL: theory HOL.Groups


01:35:26 HOL: theory HOL.SAT


01:35:27 HOL: theory HOL.Lattices


01:35:29 HOL: theory HOL.Boolean_Algebras


01:35:30 HOL: theory HOL.Set


01:35:32 HOL: theory HOL.Fun


01:35:32 HOL: theory HOL.Typedef


01:35:33 HOL: theory HOL.Complete_Lattices


01:35:33 HOL: theory HOL.Rings


01:35:37 HOL: theory HOL.Inductive


01:35:40 HOL: theory HOL.Product_Type


01:35:40 HOL: theory HOL.Sum_Type


01:35:41 HOL: theory HOL.Complete_Partial_Order


01:35:49 HOL: theory HOL.Nat


01:35:52 HOL: theory HOL.Fields


01:35:52 HOL: theory HOL.Meson


01:35:58 HOL: theory HOL.Relation


01:36:00 HOL: theory HOL.Finite_Set


01:36:02 HOL: theory HOL.Transitive_Closure


01:36:04 HOL: theory HOL.Wellfounded


01:36:05 HOL: theory HOL.Fun_Def_Base


01:36:05 HOL: theory HOL.Hilbert_Choice


01:36:05 HOL: theory HOL.Wfrec


01:36:05 HOL: theory HOL.Order_Relation


01:36:06 HOL: theory HOL.BNF_Wellorder_Relation


01:36:06 HOL: theory HOL.BNF_Wellorder_Embedding


01:36:06 HOL: theory HOL.Zorn


01:36:06 HOL: theory HOL.ATP


01:36:07 HOL: theory HOL.BNF_Wellorder_Constructions


01:36:09 HOL: theory HOL.BNF_Cardinal_Order_Relation


01:36:11 HOL: theory HOL.BNF_Cardinal_Arithmetic


01:36:11 HOL: theory HOL.BNF_Def


01:36:14 HOL: theory HOL.Metis


01:36:19 HOL: theory HOL.BNF_Composition


01:36:19 HOL: theory HOL.Basic_BNFs


01:36:20 HOL: theory HOL.BNF_Fixpoint_Base


01:36:25 HOL: theory HOL.BNF_Least_Fixpoint


01:36:31 HOL: theory HOL.Basic_BNF_LFPs


01:36:31 HOL: theory HOL.Equiv_Relations


01:36:31 HOL: theory HOL.Transfer


01:36:32 HOL: theory HOL.Lifting


01:36:32 HOL: theory HOL.Num


01:36:34 HOL: theory HOL.Option


01:36:34 HOL: theory HOL.Quotient


01:36:35 HOL: theory HOL.Extraction


01:36:35 HOL: theory HOL.Partial_Function


01:36:37 HOL: theory HOL.Fun_Def


01:36:37 HOL: theory HOL.Power


01:36:40 HOL: theory HOL.Groups_Big


01:36:44 HOL: theory HOL.Int


01:36:44 HOL: theory HOL.Lattices_Big


01:36:44 HOL: theory HOL.Lifting_Set


01:36:49 HOL: theory HOL.Euclidean_Rings


01:36:58 HOL: theory HOL.Parity


01:37:09 HOL: theory HOL.Divides


01:37:09 HOL: theory HOL.Set_Interval


01:37:09 HOL: theory HOL.Numeral_Simprocs


01:37:10 HOL: theory HOL.SMT


01:37:10 HOL: theory HOL.Semiring_Normalization


01:37:14 HOL: theory HOL.Groebner_Basis


01:37:16 HOL: theory HOL.Conditionally_Complete_Lattices


01:37:16 HOL: theory HOL.Presburger


01:37:16 HOL: theory HOL.Filter


01:37:22 HOL: theory HOL.Sledgehammer


01:37:27 HOL: theory HOL.List


01:37:41 HOL: theory HOL.Groups_List


01:37:41 HOL: theory HOL.Map


01:37:45 HOL: theory HOL.Bit_Operations


01:37:45 HOL: theory HOL.Factorial


01:37:45 HOL: theory HOL.Enum


01:37:47 HOL: theory HOL.Binomial


01:38:15 HOL: theory HOL.Code_Numeral


01:38:17 HOL: theory HOL.GCD


01:38:17 HOL: theory HOL.String


01:38:17 HOL: theory HOL.Random


01:38:22 HOL: theory HOL.BNF_Greatest_Fixpoint


01:38:22 HOL: theory HOL.Predicate


01:38:22 HOL: theory HOL.Typerep


01:38:26 HOL: theory HOL.Lazy_Sequence


01:38:27 HOL: theory HOL.Limited_Sequence


01:38:27 HOL: theory HOL.Code_Evaluation


01:38:29 HOL: theory HOL.Quickcheck_Random


01:38:33 HOL: theory HOL.Quickcheck_Exhaustive


01:38:33 HOL: theory HOL.Random_Pred


01:38:33 HOL: theory HOL.Quickcheck_Narrowing


01:38:34 HOL: theory HOL.Random_Sequence


01:38:39 HOL: theory HOL.Record


01:38:39 HOL: theory HOL.Predicate_Compile


01:38:41 HOL: theory HOL.Nitpick


01:38:43 HOL: theory HOL.Mirabelle


01:38:49 HOL: theory HOL.Nunchaku


01:38:51 HOL: theory Main


01:38:52 HOL: theory HOL.Archimedean_Field


01:38:52 HOL: theory HOL.Hull


01:38:52 HOL: theory HOL.Topological_Spaces


01:38:53 HOL: theory HOL.Modules


01:38:54 HOL: theory HOL.Vector_Spaces


01:39:03 HOL: theory HOL.Rat


01:39:07 HOL: theory HOL.Real


01:39:09 HOL: theory HOL.Real_Vector_Spaces


01:39:33 HOL: theory HOL.Limits


01:39:33 HOL: theory HOL.Inequalities


01:39:44 HOL: theory HOL.Deriv


01:39:44 HOL: theory HOL.Series


01:39:48 HOL: theory HOL.NthRoot


01:39:49 HOL: theory HOL.Transcendental


01:39:59 HOL: theory HOL.Complex


01:40:00 HOL: theory HOL.MacLaurin


01:40:01 HOL: theory Complex_Main


01:41:26 Preparing HOL/document ...


01:43:08 Finished HOL/document (0:01:41 elapsed time)


01:43:08 Preparing HOL/outline ...


01:44:07 Finished HOL/outline (0:00:58 elapsed time)


01:44:08 Timing HOL (8 threads, 345.294s elapsed time, 1313.457s cpu time, 267.132s GC time, factor 3.80)


01:44:08 Finished HOL (0:06:07 elapsed time, 0:22:42 cpu time, factor 3.71)


01:44:08 Running JinjaThreads ...


01:44:09 JinjaThreads: theory Automatic_Refinement.Prio_List


01:44:09 JinjaThreads: theory HOL-Eisbach.Eisbach


01:44:10 JinjaThreads: theory Automatic_Refinement.Foldi


01:44:10 JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1


01:44:10 JinjaThreads: theory Collections.ICF_Tools


01:44:10 JinjaThreads: theory Finger-Trees.FingerTree


01:44:10 JinjaThreads: theory HOL-Library.Adhoc_Overloading


01:44:10 JinjaThreads: theory HOL-Library.AList


01:44:10 JinjaThreads: theory HOL-Library.Cancellation


01:44:10 JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot


01:44:10 JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot


01:44:10 JinjaThreads: theory Collections.Ord_Code_Preproc


01:44:10 JinjaThreads: theory HOL-Library.Monad_Syntax


01:44:10 JinjaThreads: theory HOL-Library.Case_Converter


01:44:10 JinjaThreads: theory Collections.Locale_Code


01:44:10 JinjaThreads: theory Collections.Record_Intf


01:44:10 JinjaThreads: theory Automatic_Refinement.Refine_Util


01:44:10 JinjaThreads: theory HOL-Library.Code_Abstract_Nat


01:44:10 JinjaThreads: theory HOL-Library.Code_Target_Int


01:44:11 JinjaThreads: theory HOL-Library.Code_Target_Nat


01:44:11 JinjaThreads: theory HOL-Library.Simps_Case_Conv


01:44:11 JinjaThreads: theory HOL-Library.Complete_Partial_Order2


01:44:11 JinjaThreads: theory HOL-Library.Confluence


01:44:11 JinjaThreads: theory HOL-Library.Multiset


01:44:11 JinjaThreads: theory HOL-Library.Code_Target_Numeral


01:44:11 JinjaThreads: theory HOL-Library.Confluent_Quotient


01:44:12 JinjaThreads: theory HOL-Library.Infinite_Set


01:44:12 JinjaThreads: theory Automatic_Refinement.Anti_Unification


01:44:12 JinjaThreads: theory Automatic_Refinement.Attr_Comb


01:44:12 JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms


01:44:12 JinjaThreads: theory Automatic_Refinement.Autoref_Data


01:44:12 JinjaThreads: theory Automatic_Refinement.Indep_Vars


01:44:12 JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp


01:44:12 JinjaThreads: theory Automatic_Refinement.Tagged_Solver


01:44:12 JinjaThreads: theory Automatic_Refinement.Select_Solve


01:44:12 JinjaThreads: theory HOL-Library.Dlist


01:44:12 JinjaThreads: theory HOL-Library.Nat_Bijection


01:44:12 JinjaThreads: theory HOL-Library.Old_Datatype


01:44:12 JinjaThreads: theory HOL-Library.Option_ord


01:44:13 JinjaThreads: theory Trie.Trie


01:44:13 JinjaThreads: theory HOL-Library.Phantom_Type


01:44:13 JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs


01:44:14 JinjaThreads: theory HOL-Library.RBT_Impl


01:44:14 JinjaThreads: theory HOL-Library.Signed_Division


01:44:14 JinjaThreads: theory HOL-Library.Sublist


01:44:15 JinjaThreads: theory HOL-Library.Cardinality


01:44:15 JinjaThreads: theory HOL-Library.Transitive_Closure_Table


01:44:16 JinjaThreads: theory HOL-Library.While_Combinator


01:44:16 JinjaThreads: theory HOL-Library.Countable


01:44:16 JinjaThreads: theory FinFun.FinFun


01:44:17 JinjaThreads: theory HOL-Library.Numeral_Type


01:44:17 JinjaThreads: theory Collections.DatRef


01:44:17 JinjaThreads: theory JinjaThreads.Set_Monad


01:44:17 JinjaThreads: theory JinjaThreads.Set_without_equal


01:44:18 JinjaThreads: theory Native_Word.Code_Int_Integer_Conversion


01:44:18 JinjaThreads: theory Refine_Monadic.Refine_Chapter


01:44:18 JinjaThreads: theory Word_Lib.More_Bit_Ring


01:44:18 JinjaThreads: theory HOL-Library.Countable_Set


01:44:18 JinjaThreads: theory JinjaThreads.Auxiliary


01:44:18 JinjaThreads: theory HOL-Library.Type_Length


01:44:18 JinjaThreads: theory HOL-Library.Countable_Complete_Lattices


01:44:19 JinjaThreads: theory HOL-Library.Word


01:44:19 JinjaThreads: theory Word_Lib.More_Arithmetic


01:44:19 JinjaThreads: theory Binomial-Heaps.BinomialHeap


01:44:19 JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap


01:44:20 JinjaThreads: theory HOL-ex.Quicksort


01:44:20 JinjaThreads: theory Automatic_Refinement.Misc


01:44:20 JinjaThreads: theory HOL-Library.Order_Continuity


01:44:21 JinjaThreads: theory HOL-Library.Extended_Nat


01:44:22 JinjaThreads: theory Coinductive.Coinductive_Nat


01:44:24 JinjaThreads: theory Coinductive.Coinductive_List


01:44:26 JinjaThreads: theory Automatic_Refinement.Refine_Lib


01:44:26 JinjaThreads: theory Collections.SetIterator


01:44:26 JinjaThreads: theory Collections.Sorted_List_Operations


01:44:28 JinjaThreads: theory Automatic_Refinement.Autoref_Phases


01:44:28 JinjaThreads: theory Automatic_Refinement.Autoref_Tagging


01:44:28 JinjaThreads: theory Automatic_Refinement.Relators


01:44:28 JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover


01:44:28 JinjaThreads: theory Collections.SetIteratorOperations


01:44:29 JinjaThreads: theory Word_Lib.Bit_Comprehension


01:44:29 JinjaThreads: theory Word_Lib.More_Divides


01:44:29 JinjaThreads: theory Word_Lib.Signed_Division_Word


01:44:29 JinjaThreads: theory Word_Lib.More_Word


01:44:30 JinjaThreads: theory Automatic_Refinement.Param_Tool


01:44:31 JinjaThreads: theory Automatic_Refinement.Param_HOL


01:44:31 JinjaThreads: theory Native_Word.Code_Target_Word_Base


01:44:31 JinjaThreads: theory Word_Lib.Bit_Shifts_Infix_Syntax


01:44:31 JinjaThreads: theory Word_Lib.Least_significant_bit


01:44:32 JinjaThreads: theory Collections.Assoc_List


01:44:32 JinjaThreads: theory Automatic_Refinement.Parametricity


01:44:32 JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops


01:44:32 JinjaThreads: theory Collections.Dlist_add


01:44:32 JinjaThreads: theory Collections.Diff_Array


01:44:32 JinjaThreads: theory Collections.Trie_Impl


01:44:32 JinjaThreads: theory Collections.Proper_Iterator


01:44:32 JinjaThreads: theory Collections.SetIteratorGA


01:44:33 JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel


01:44:33 JinjaThreads: theory Collections.Trie2


01:44:33 JinjaThreads: theory Collections.It_to_It


01:44:33 JinjaThreads: theory Coinductive.Lazy_LList


01:44:33 JinjaThreads: theory Coinductive.TLList


01:44:33 JinjaThreads: theory Word_Lib.Most_significant_bit


01:44:34 JinjaThreads: theory Word_Lib.Generic_set_bit


01:44:34 JinjaThreads: theory Automatic_Refinement.Autoref_Translate


01:44:34 JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface


01:44:34 JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo


01:44:34 JinjaThreads: theory Automatic_Refinement.Autoref_Tool


01:44:34 JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL


01:44:34 JinjaThreads: theory Native_Word.Code_Target_Integer_Bit


01:44:34 JinjaThreads: theory Native_Word.Word_Type_Copies


01:44:35 JinjaThreads: theory Coinductive.Lazy_TLList


01:44:39 JinjaThreads: theory Automatic_Refinement.Automatic_Refinement


01:44:40 JinjaThreads: theory Collections.Idx_Iterator


01:44:40 JinjaThreads: theory Refine_Monadic.Refine_Misc


01:44:41 JinjaThreads: theory Refine_Monadic.RefineG_Domain


01:44:41 JinjaThreads: theory Refine_Monadic.RefineG_Transfer


01:44:41 JinjaThreads: theory Refine_Monadic.RefineG_Assert


01:44:42 JinjaThreads: theory Refine_Monadic.RefineG_Recursion


01:44:42 JinjaThreads: theory Refine_Monadic.RefineG_While


01:44:42 JinjaThreads: theory Refine_Monadic.Refine_Basic


01:44:43 JinjaThreads: theory Refine_Monadic.Refine_Det


01:44:48 JinjaThreads: theory Refine_Monadic.Refine_Heuristics


01:44:48 JinjaThreads: theory Refine_Monadic.Refine_Leof


01:44:48 JinjaThreads: theory Refine_Monadic.Refine_Pfun


01:44:49 JinjaThreads: theory Refine_Monadic.Refine_More_Comb


01:44:49 JinjaThreads: theory Refine_Monadic.Refine_While


01:44:52 JinjaThreads: theory Native_Word.Code_Target_Int_Bit


01:44:52 JinjaThreads: theory Native_Word.Uint32


01:44:52 JinjaThreads: theory Collections.Code_Target_ICF


01:44:52 JinjaThreads: theory Refine_Monadic.Refine_Transfer


01:44:53 JinjaThreads: theory Refine_Monadic.Autoref_Monadic


01:44:53 JinjaThreads: theory Refine_Monadic.Refine_Automation


01:44:53 JinjaThreads: theory Refine_Monadic.Refine_Foreach


01:44:56 JinjaThreads: theory Collections.HashCode


01:44:59 JinjaThreads: theory Refine_Monadic.Refine_Monadic


01:45:00 JinjaThreads: theory Collections.Gen_Iterator


01:45:00 JinjaThreads: theory Collections.Intf_Map


01:45:00 JinjaThreads: theory Collections.Intf_Set


01:45:01 JinjaThreads: theory Collections.Iterator


01:45:02 JinjaThreads: theory Collections.Array_Iterator


01:45:02 JinjaThreads: theory Collections.ICF_Spec_Base


01:45:02 JinjaThreads: theory Collections.AnnotatedListSpec


01:45:02 JinjaThreads: theory Collections.ListSpec


01:45:02 JinjaThreads: theory Collections.MapSpec


01:45:02 JinjaThreads: theory Collections.PrioSpec


01:45:02 JinjaThreads: theory Collections.PrioUniqueSpec


01:45:02 JinjaThreads: theory Collections.SetSpec


01:45:05 JinjaThreads: theory Collections.BinoPrioImpl


01:45:05 JinjaThreads: theory Collections.SkewPrioImpl


01:45:06 JinjaThreads: theory Collections.ListGA


01:45:06 JinjaThreads: theory Collections.FTAnnotatedListImpl


01:45:07 JinjaThreads: theory Collections.Fifo


01:45:07 JinjaThreads: theory Collections.PrioByAnnotatedList


01:45:09 JinjaThreads: theory Collections.PrioUniqueByAnnotatedList


01:45:11 JinjaThreads: theory Collections.Algos


01:45:12 JinjaThreads: theory Collections.SetIndex


01:45:12 JinjaThreads: theory Collections.SetIteratorCollectionsGA


01:45:13 JinjaThreads: theory Collections.MapGA


01:45:13 JinjaThreads: theory Collections.SetGA


01:45:13 JinjaThreads: theory Collections.FTPrioImpl


01:45:15 JinjaThreads: theory Collections.FTPrioUniqueImpl


01:45:16 JinjaThreads: theory Collections.ArrayMapImpl


01:45:16 JinjaThreads: theory Collections.ListMapImpl


01:45:16 JinjaThreads: theory Collections.ListMapImpl_Invar


01:45:18 JinjaThreads: theory Collections.TrieMapImpl


01:45:19 JinjaThreads: theory Collections.ListSetImpl


01:45:21 JinjaThreads: theory Collections.ListSetImpl_Invar


01:45:22 JinjaThreads: theory Collections.ListSetImpl_NotDist


01:45:23 JinjaThreads: theory Collections.ListSetImpl_Sorted


01:45:25 JinjaThreads: theory Collections.SetByMap


01:45:25 JinjaThreads: theory Collections.ArrayHashMap_Impl


01:45:29 JinjaThreads: theory Collections.ArraySetImpl


01:45:29 JinjaThreads: theory Collections.TrieSetImpl


01:45:31 JinjaThreads: theory Collections.ArrayHashMap


01:45:34 JinjaThreads: theory HOL-Library.RBT


01:45:35 JinjaThreads: theory Collections.RBT_add


01:45:38 JinjaThreads: theory Collections.RBTMapImpl


01:45:38 JinjaThreads: theory Collections.ArrayHashSet


01:45:47 JinjaThreads: theory Collections.RBTSetImpl


01:45:47 JinjaThreads: theory Collections.HashMap_Impl


01:45:50 JinjaThreads: theory Collections.HashMap


01:46:00 JinjaThreads: theory Collections.HashSet


01:46:00 JinjaThreads: theory Collections.MapStdImpl


01:46:07 JinjaThreads: theory Collections.SetStdImpl


01:46:11 JinjaThreads: theory Collections.ICF_Impl


01:46:16 JinjaThreads: theory Collections.ICF_Refine_Monadic


01:46:17 JinjaThreads: theory Collections.ICF_Autoref


01:46:22 JinjaThreads: theory Collections.Collections


01:46:22 JinjaThreads: theory Collections.CollectionsV1


01:46:30 JinjaThreads: theory JinjaThreads.JT_ICF


01:46:30 JinjaThreads: theory JinjaThreads.Basic_Main


01:48:57 JinjaThreads: theory HOL-Library.Mapping


01:48:57 JinjaThreads: theory JinjaThreads.FWState


01:48:57 JinjaThreads: theory HOL-Library.Code_Cardinality


01:48:57 JinjaThreads: theory HOL-Library.Prefix_Order


01:48:57 JinjaThreads: theory JinjaThreads.LTS


01:48:57 JinjaThreads: theory JinjaThreads.Type


01:48:57 JinjaThreads: theory JinjaThreads.Orders


01:48:57 JinjaThreads: theory JinjaThreads.ListIndex


01:48:58 JinjaThreads: theory JinjaThreads.Semilat


01:48:58 JinjaThreads: theory JinjaThreads.Err


01:49:02 JinjaThreads: theory JinjaThreads.Listn


01:49:02 JinjaThreads: theory JinjaThreads.Opt


01:49:02 JinjaThreads: theory HOL-Library.AList_Mapping


01:49:02 JinjaThreads: theory JinjaThreads.Product


01:49:03 JinjaThreads: theory JinjaThreads.Decl


01:49:03 JinjaThreads: theory JinjaThreads.Semilattices


01:49:03 JinjaThreads: theory JinjaThreads.Typing_Framework


01:49:03 JinjaThreads: theory JinjaThreads.SemilatAlg


01:49:04 JinjaThreads: theory JinjaThreads.Kildall


01:49:04 JinjaThreads: theory JinjaThreads.LBVSpec


01:49:04 JinjaThreads: theory JinjaThreads.Typing_Framework_err


01:49:04 JinjaThreads: theory JinjaThreads.Bisimulation


01:49:04 JinjaThreads: theory JinjaThreads.LBVComplete


01:49:05 JinjaThreads: theory JinjaThreads.LBVCorrect


01:49:05 JinjaThreads: theory JinjaThreads.TypeRel


01:49:05 JinjaThreads: theory JinjaThreads.Abstract_BV


01:49:09 JinjaThreads: theory JinjaThreads.TypeRelRefine


01:49:09 JinjaThreads: theory JinjaThreads.Value


01:49:12 JinjaThreads: theory JinjaThreads.Exceptions


01:49:12 JinjaThreads: theory JinjaThreads.Heap


01:49:13 JinjaThreads: theory JinjaThreads.SystemClasses


01:49:14 JinjaThreads: theory JinjaThreads.MM


01:49:14 JinjaThreads: theory JinjaThreads.State


01:49:20 JinjaThreads: theory JinjaThreads.FWCondAction


01:49:20 JinjaThreads: theory JinjaThreads.FWInterrupt


01:49:20 JinjaThreads: theory JinjaThreads.FWLock


01:49:21 JinjaThreads: theory JinjaThreads.FWThread


01:49:21 JinjaThreads: theory JinjaThreads.FWWait


01:49:21 JinjaThreads: theory JinjaThreads.Observable_Events


01:49:23 JinjaThreads: theory JinjaThreads.FWLocking


01:49:23 JinjaThreads: theory JinjaThreads.FWLockingThread


01:49:23 JinjaThreads: theory JinjaThreads.FWWellform


01:49:24 JinjaThreads: theory JinjaThreads.FWLifting


01:49:24 JinjaThreads: theory JinjaThreads.FWSemantics


01:49:27 JinjaThreads: theory JinjaThreads.FWLiftingSem


01:49:27 JinjaThreads: theory JinjaThreads.FWProgressAux


01:49:28 JinjaThreads: theory JinjaThreads.JVMState


01:49:28 JinjaThreads: theory JinjaThreads.StartConfig


01:49:28 JinjaThreads: theory JinjaThreads.JMM_Spec


01:49:29 JinjaThreads: theory JinjaThreads.FWDeadlock


01:49:29 JinjaThreads: theory JinjaThreads.FWLTS


01:49:29 JinjaThreads: theory JinjaThreads.Conform


01:49:30 JinjaThreads: theory JinjaThreads.State_Refinement


01:49:32 JinjaThreads: theory JinjaThreads.ConformThreaded


01:49:32 JinjaThreads: theory JinjaThreads.ExternalCall


01:49:32 JinjaThreads: theory JinjaThreads.FWProgress


01:49:33 JinjaThreads: theory JinjaThreads.SC


01:49:33 JinjaThreads: theory JinjaThreads.SC_Collections


01:49:39 JinjaThreads: theory JinjaThreads.JMM_DRF


01:49:39 JinjaThreads: theory JinjaThreads.SC_Legal


01:49:44 JinjaThreads: theory JinjaThreads.FWBisimulation


01:49:44 JinjaThreads: theory JinjaThreads.FWInitFinLift


01:49:44 JinjaThreads: theory JinjaThreads.Non_Speculative


01:49:48 JinjaThreads: theory JinjaThreads.Scheduler


01:49:50 JinjaThreads: theory JinjaThreads.HB_Completion


01:49:50 JinjaThreads: theory JinjaThreads.SC_Completion


01:50:12 JinjaThreads: theory JinjaThreads.WellForm


01:50:12 JinjaThreads: theory JinjaThreads.ExternalCall_Execute


01:50:15 JinjaThreads: theory JinjaThreads.ExternalCallWF


01:50:15 JinjaThreads: theory JinjaThreads.JMM_Heap


01:50:15 JinjaThreads: theory JinjaThreads.SemiType


01:50:17 JinjaThreads: theory JinjaThreads.BinOp


01:50:18 JinjaThreads: theory JinjaThreads.JVM_SemiType


01:50:20 JinjaThreads: theory JinjaThreads.JMM_Type


01:50:20 JinjaThreads: theory JinjaThreads.JMM_Type2


01:50:30 JinjaThreads: theory JinjaThreads.Random_Scheduler


01:50:30 JinjaThreads: theory JinjaThreads.Round_Robin


01:52:02 JinjaThreads: theory JinjaThreads.JMM_Framework


01:52:07 JinjaThreads: theory JinjaThreads.SC_Schedulers


01:52:15 JinjaThreads: theory JinjaThreads.Expr


01:52:17 JinjaThreads: theory JinjaThreads.JVMInstructions


01:52:18 JinjaThreads: theory JinjaThreads.PCompiler


01:52:20 JinjaThreads: theory JinjaThreads.PCompilerRefine


01:52:31 JinjaThreads: theory JinjaThreads.JVMExceptions


01:52:31 JinjaThreads: theory JinjaThreads.JVMHeap


01:52:31 JinjaThreads: theory JinjaThreads.Effect


01:52:38 JinjaThreads: theory JinjaThreads.JVMExecInstr


01:52:39 JinjaThreads: theory JinjaThreads.CallExpr


01:52:39 JinjaThreads: theory JinjaThreads.DefAss


01:52:39 JinjaThreads: theory JinjaThreads.JHeap


01:52:40 JinjaThreads: theory JinjaThreads.WWellForm


01:52:40 JinjaThreads: theory JinjaThreads.WellType


01:52:41 JinjaThreads: theory JinjaThreads.JVMExec


01:52:45 JinjaThreads: theory JinjaThreads.JVMDefensive


01:52:46 JinjaThreads: theory JinjaThreads.J1State


01:52:50 JinjaThreads: theory JinjaThreads.SmallStep


01:52:50 JinjaThreads: theory JinjaThreads.JVMExec_Execute


01:52:51 JinjaThreads: theory JinjaThreads.Annotate


01:52:53 JinjaThreads: theory JinjaThreads.J1Heap


01:52:55 JinjaThreads: theory JinjaThreads.J1WellType


01:52:57 JinjaThreads: theory JinjaThreads.JWellForm


01:52:57 JinjaThreads: theory JinjaThreads.WellTypeRT


01:52:58 JinjaThreads: theory JinjaThreads.JVMThreaded


01:52:58 JinjaThreads: theory JinjaThreads.Compiler1


01:52:59 JinjaThreads: theory JinjaThreads.J1WellForm


01:52:59 JinjaThreads: theory JinjaThreads.JMM_Typesafe


01:53:00 JinjaThreads: theory JinjaThreads.Compiler2


01:53:03 JinjaThreads: theory JinjaThreads.Preprocessor


01:53:03 JinjaThreads: theory JinjaThreads.JJ1WellForm


01:53:04 JinjaThreads: theory JinjaThreads.ToString


01:53:16 JinjaThreads: theory JinjaThreads.Compiler


01:53:16 JinjaThreads: theory JinjaThreads.JMM_JVM


01:53:16 JinjaThreads: theory JinjaThreads.JVM_Main


01:53:16 JinjaThreads: theory JinjaThreads.Exception_Tables


01:53:18 JinjaThreads: theory JinjaThreads.JMM_Common


01:53:26 JinjaThreads: theory JinjaThreads.BVSpec


01:53:26 JinjaThreads: theory JinjaThreads.JMM_Typesafe2


01:53:27 JinjaThreads: theory JinjaThreads.EffectMono


01:53:27 JinjaThreads: theory JinjaThreads.TF_JVM


01:53:30 JinjaThreads: theory JinjaThreads.BVConform


01:53:31 JinjaThreads: theory JinjaThreads.FWBisimDeadlock


01:53:36 JinjaThreads: theory JinjaThreads.FWBisimLift


01:53:37 JinjaThreads: theory JinjaThreads.J1


01:53:39 JinjaThreads: theory JinjaThreads.BVExec


01:53:40 JinjaThreads: theory JinjaThreads.LBVJVM


01:53:41 JinjaThreads: theory JinjaThreads.TypeComp


01:53:47 JinjaThreads: theory JinjaThreads.BVSpecTypeSafe


01:54:01 JinjaThreads: theory JinjaThreads.BVNoTypeError


01:54:10 JinjaThreads: theory JinjaThreads.BCVExec


01:54:10 JinjaThreads: theory JinjaThreads.JVMExec_Execute2


01:54:10 JinjaThreads: theory JinjaThreads.BVProgressThreaded


01:54:11 JinjaThreads: theory JinjaThreads.Common_Main


01:54:12 JinjaThreads: theory JinjaThreads.JVMTau


01:54:26 JinjaThreads: theory JinjaThreads.J1Deadlock


01:54:42 JinjaThreads: theory JinjaThreads.Execs


01:54:49 JinjaThreads: theory JinjaThreads.DefAssPreservation


01:54:49 JinjaThreads: theory JinjaThreads.Threaded


01:54:49 JinjaThreads: theory JinjaThreads.Progress


01:54:56 JinjaThreads: theory JinjaThreads.TypeSafe


01:58:02 JinjaThreads: theory JinjaThreads.J0


01:58:03 JinjaThreads: theory JinjaThreads.JMM_J


01:58:03 JinjaThreads: theory JinjaThreads.ProgressThreaded


01:58:03 JinjaThreads: theory JinjaThreads.J_Execute


01:58:20 JinjaThreads: theory JinjaThreads.J1JVMBisim


01:58:27 JinjaThreads: theory JinjaThreads.Deadlocked


01:58:28 JinjaThreads: theory JinjaThreads.DRF_J


01:58:34 JinjaThreads: theory JinjaThreads.JVMDeadlocked


01:58:34 JinjaThreads: theory JinjaThreads.DRF_JVM


01:58:34 JinjaThreads: theory JinjaThreads.J_Main


01:58:35 JinjaThreads: theory JinjaThreads.JVM_Execute


01:58:37 JinjaThreads: theory JinjaThreads.JVM_Execute2


01:58:43 JinjaThreads: theory JinjaThreads.J0Bisim


01:58:56 JinjaThreads: theory JinjaThreads.J0J1Bisim


01:59:10 JinjaThreads: theory JinjaThreads.BV_Main


01:59:40 JinjaThreads: theory JinjaThreads.Correctness1


01:59:43 JinjaThreads: theory JinjaThreads.Correctness1Threaded


02:00:40 JinjaThreads: theory JinjaThreads.Code_Generation


02:00:49 JinjaThreads: theory JinjaThreads.ApprenticeChallenge


02:00:50 JinjaThreads: theory JinjaThreads.BufferExample


02:00:50 JinjaThreads: theory JinjaThreads.Java2Jinja


02:01:09 JinjaThreads: theory JinjaThreads.Examples_Main


02:02:02 JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe


02:02:02 JinjaThreads: theory JinjaThreads.JMM_J_Typesafe


02:02:47 JinjaThreads: theory JinjaThreads.J1JVM


02:02:49 JinjaThreads: theory JinjaThreads.JVMJ1


02:03:34 JinjaThreads: theory JinjaThreads.Execute_Main


02:04:28 JinjaThreads: theory JinjaThreads.Correctness2


02:11:22 JinjaThreads: theory JinjaThreads.Correctness


02:16:28 JinjaThreads: theory JinjaThreads.JMM_Compiler


02:16:31 JinjaThreads: theory JinjaThreads.SC_Interp


02:16:31 JinjaThreads: theory JinjaThreads.Compiler_Main


02:20:42 JinjaThreads: theory JinjaThreads.JMM_Interp


02:20:46 JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2


02:20:48 JinjaThreads: theory JinjaThreads.JMM


02:20:51 JinjaThreads: theory JinjaThreads.MM_Main


02:20:57 JinjaThreads: theory JinjaThreads.JinjaThreads


02:37:11 Preparing JinjaThreads/document ...


02:38:46 Finished JinjaThreads/document (0:01:35 elapsed time)


02:38:46 Preparing JinjaThreads/outline ...


02:39:25 Finished JinjaThreads/outline (0:00:39 elapsed time)


02:39:27 Timing JinjaThreads (8 threads, 3162.525s elapsed time, 15949.195s cpu time, 5516.684s GC time, factor 5.04)


02:39:27 Finished JinjaThreads (0:52:49 elapsed time, 4:26:18 cpu time, factor 5.04)


02:39:27 Building Flyspeck-Tame ...


02:39:28 Flyspeck-Tame: theory Flyspeck-Tame.ListAux


02:39:28 Flyspeck-Tame: theory Flyspeck-Tame.RTranCl


02:39:28 Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat


02:39:28 Flyspeck-Tame: theory HOL-Library.AList


02:39:28 Flyspeck-Tame: theory HOL-Library.Code_Target_Int


02:39:28 Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order


02:39:28 Flyspeck-Tame: theory HOL-Library.IArray


02:39:28 Flyspeck-Tame: theory HOL-Library.While_Combinator


02:39:28 Flyspeck-Tame: theory HOL-Library.Code_Target_Nat


02:39:28 Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso


02:39:29 Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral


02:39:29 Flyspeck-Tame: theory Flyspeck-Tame.Arch


02:39:29 Flyspeck-Tame: theory Flyspeck-Tame.Worklist


02:39:29 Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax


02:39:30 Flyspeck-Tame: theory Flyspeck-Tame.ListSum


02:39:30 Flyspeck-Tame: theory Flyspeck-Tame.Rotation


02:39:30 Flyspeck-Tame: theory Flyspeck-Tame.Graph


02:39:30 Flyspeck-Tame: theory Flyspeck-Tame.Maps


02:39:30 Flyspeck-Tame: theory Trie.Trie


02:39:33 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision


02:39:33 Flyspeck-Tame: theory Flyspeck-Tame.GraphProps


02:39:33 Flyspeck-Tame: theory Flyspeck-Tame.Tame


02:39:33 Flyspeck-Tame: theory Flyspeck-Tame.Enumerator


02:39:33 Flyspeck-Tame: theory Flyspeck-Tame.TameProps


02:39:33 Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps


02:39:33 Flyspeck-Tame: theory Trie.Tries


02:39:34 Flyspeck-Tame: theory Flyspeck-Tame.Plane


02:39:34 Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps


02:39:34 Flyspeck-Tame: theory Flyspeck-Tame.Plane1


02:39:34 Flyspeck-Tame: theory Flyspeck-Tame.Generator


02:39:35 Flyspeck-Tame: theory Flyspeck-Tame.TameEnum


02:39:38 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux


02:39:39 Flyspeck-Tame: theory Flyspeck-Tame.Invariants


02:39:40 Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps


02:39:40 Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps


02:39:41 Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props


02:39:41 Flyspeck-Tame: theory Flyspeck-Tame.LowerBound


02:39:42 Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps


02:39:42 Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps


02:39:42 Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps


02:39:43 Flyspeck-Tame: theory Flyspeck-Tame.Relative_Completeness


02:41:10 Preparing Flyspeck-Tame/document ...


02:41:27 Finished Flyspeck-Tame/document (0:00:16 elapsed time)


02:41:27 Preparing Flyspeck-Tame/outline ...


02:41:35 Finished Flyspeck-Tame/outline (0:00:08 elapsed time)


02:41:36 Timing Flyspeck-Tame (8 threads, 75.647s elapsed time, 403.483s cpu time, 24.282s GC time, factor 5.33)


02:41:36 Finished Flyspeck-Tame (0:01:42 elapsed time, 0:07:43 cpu time, factor 4.53)


02:41:36 Running Flyspeck-Tame-Computation ...


02:41:38 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.ArchComp


02:41:38 Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.Completeness


07:42:56 Timing Flyspeck-Tame-Computation (8 threads, 18076.139s elapsed time, 27039.916s cpu time, 1282.135s GC time, factor 1.50)


07:42:56 Finished Flyspeck-Tame-Computation (5:01:18 elapsed time, 7:30:41 cpu time, factor 1.50)


07:42:56 Building AWN ...


07:42:58 AWN: theory AWN.Lib


07:42:58 AWN: theory AWN.TransitionSystems


07:42:58 AWN: theory AWN.AWN


07:42:59 AWN: theory AWN.Invariants


07:42:59 AWN: theory AWN.OInvariants


07:43:11 AWN: theory AWN.AWN_Cterms


07:43:11 AWN: theory AWN.AWN_SOS


07:43:12 AWN: theory AWN.OAWN_SOS


07:43:15 AWN: theory AWN.AWN_Labels


07:43:16 AWN: theory AWN.Pnet


07:43:17 AWN: theory AWN.Inv_Cterms


07:43:17 AWN: theory AWN.AWN_Invariants


07:43:17 AWN: theory AWN.Closed


07:43:18 AWN: theory AWN.AWN_SOS_Labels


07:43:19 AWN: theory AWN.Qmsg


07:43:19 AWN: theory AWN.OAWN_SOS_Labels


07:43:19 AWN: theory AWN.ONode_Lifting


07:43:19 AWN: theory AWN.OAWN_Invariants


07:43:19 AWN: theory AWN.OPnet


07:43:20 AWN: theory AWN.OPnet_Lifting


07:43:21 AWN: theory AWN.OClosed_Lifting


07:43:21 AWN: theory AWN.OClosed_Transfer


07:43:21 AWN: theory AWN.OAWN_Convert


07:43:21 AWN: theory AWN.Qmsg_Lifting


07:43:22 AWN: theory AWN.AWN_Main


07:43:22 AWN: theory AWN.Toy


07:43:36 AWN: theory AWN.AWN_Term_Graph


07:43:59 Preparing AWN/document ...


07:44:11 Finished AWN/document (0:00:11 elapsed time)


07:44:11 Preparing AWN/outline ...


07:44:18 Finished AWN/outline (0:00:06 elapsed time)


07:44:18 Timing AWN (8 threads, 42.989s elapsed time, 207.228s cpu time, 6.648s GC time, factor 4.82)


07:44:18 Finished AWN (0:01:00 elapsed time, 0:04:04 cpu time, factor 4.03)


07:44:18 Running AODV ...


07:44:19 AODV: theory AODV.Aodv_Basic


07:44:21 AODV: theory AODV.A_Norreqid


07:44:21 AODV: theory AODV.C_Gtobcast


07:44:21 AODV: theory AODV.B_Fwdrreps


07:44:21 AODV: theory AODV.Aodv_Message


07:44:21 AODV: theory AODV.Aodv_Data


07:44:21 AODV: theory AODV.D_Fwdrreqs


07:44:21 AODV: theory AODV.E_All_ABCD


07:44:21 AODV: theory AODV.A_Aodv_Data


07:44:22 AODV: theory AODV.A_Aodv_Message


07:44:22 AODV: theory AODV.C_Aodv_Data


07:44:22 AODV: theory AODV.C_Aodv_Message


07:44:22 AODV: theory AODV.B_Aodv_Data


07:44:22 AODV: theory AODV.B_Aodv_Message


07:44:24 AODV: theory AODV.C_Fresher


07:44:25 AODV: theory AODV.D_Aodv_Data


07:44:25 AODV: theory AODV.A_Fresher


07:44:25 AODV: theory AODV.Fresher


07:44:25 AODV: theory AODV.D_Aodv_Message


07:44:25 AODV: theory AODV.E_Aodv_Data


07:44:25 AODV: theory AODV.B_Fresher


07:44:25 AODV: theory AODV.E_Aodv_Message


07:44:26 AODV: theory AODV.A_Aodv


07:44:27 AODV: theory AODV.Aodv


07:44:27 AODV: theory AODV.B_Aodv


07:44:27 AODV: theory AODV.C_Aodv


07:44:27 AODV: theory AODV.E_Fresher


07:44:28 AODV: theory AODV.D_Fresher


07:44:28 AODV: theory AODV.D_Aodv


07:44:28 AODV: theory AODV.E_Aodv


07:45:23 AODV: theory AODV.A_Aodv_Predicates


07:45:23 AODV: theory AODV.A_OAodv


07:45:23 AODV: theory AODV.A_Loop_Freedom


07:45:23 AODV: theory AODV.A_Quality_Increases


07:45:23 AODV: theory AODV.A_Seq_Invariants


07:45:24 AODV: theory AODV.A_Global_Invariants


07:45:25 AODV: theory AODV.A_Aodv_Loop_Freedom


07:45:28 AODV: theory AODV.C_Aodv_Predicates


07:45:28 AODV: theory AODV.C_OAodv


07:45:28 AODV: theory AODV.C_Loop_Freedom


07:45:28 AODV: theory AODV.C_Quality_Increases


07:45:28 AODV: theory AODV.C_Seq_Invariants


07:45:29 AODV: theory AODV.C_Global_Invariants


07:45:30 AODV: theory AODV.C_Aodv_Loop_Freedom


07:45:41 AODV: theory AODV.Aodv_Predicates


07:45:42 AODV: theory AODV.Loop_Freedom


07:45:42 AODV: theory AODV.Quality_Increases


07:45:42 AODV: theory AODV.Seq_Invariants


07:45:43 AODV: theory AODV.OAodv


07:45:43 AODV: theory AODV.Global_Invariants


07:45:44 AODV: theory AODV.Aodv_Loop_Freedom


07:45:46 AODV: theory AODV.E_Aodv_Predicates


07:45:46 AODV: theory AODV.E_OAodv


07:45:46 AODV: theory AODV.E_Loop_Freedom


07:45:46 AODV: theory AODV.E_Quality_Increases


07:45:47 AODV: theory AODV.E_Seq_Invariants


07:45:47 AODV: theory AODV.B_Aodv_Predicates


07:45:47 AODV: theory AODV.B_OAodv


07:45:47 AODV: theory AODV.B_Loop_Freedom


07:45:47 AODV: theory AODV.B_Quality_Increases


07:45:47 AODV: theory AODV.B_Seq_Invariants


07:45:47 AODV: theory AODV.E_Global_Invariants


07:45:48 AODV: theory AODV.B_Global_Invariants


07:45:48 AODV: theory AODV.E_Aodv_Loop_Freedom


07:45:49 AODV: theory AODV.B_Aodv_Loop_Freedom


07:45:56 AODV: theory AODV.D_Aodv_Predicates


07:45:57 AODV: theory AODV.D_OAodv


07:45:57 AODV: theory AODV.D_Loop_Freedom


07:45:57 AODV: theory AODV.D_Quality_Increases


07:45:57 AODV: theory AODV.D_Seq_Invariants


07:45:58 AODV: theory AODV.D_Global_Invariants


07:45:59 AODV: theory AODV.D_Aodv_Loop_Freedom


07:46:04 AODV: theory AODV.All


09:19:05 Preparing AODV/document ...


09:19:28 Finished AODV/document (0:00:23 elapsed time)


09:19:28 Preparing AODV/outline ...


09:19:42 Finished AODV/outline (0:00:14 elapsed time)


09:19:43 Timing AODV (8 threads, 5680.413s elapsed time, 33322.341s cpu time, 1418.452s GC time, factor 5.87)


09:19:43 Finished AODV (1:34:42 elapsed time, 9:15:27 cpu time, factor 5.86)


09:19:43 Building Word_Lib ...


09:19:45 Word_Lib: theory HOL-Library.Phantom_Type


09:19:45 Word_Lib: theory Word_Lib.Enumeration


09:19:45 Word_Lib: theory Word_Lib.More_Bit_Ring


09:19:45 Word_Lib: theory Word_Lib.Even_More_List


09:19:45 Word_Lib: theory Word_Lib.More_Misc


09:19:45 Word_Lib: theory HOL-Library.Sublist


09:19:46 Word_Lib: theory HOL-Library.Cardinality


09:19:47 Word_Lib: theory HOL-Library.Numeral_Type


09:19:48 Word_Lib: theory Word_Lib.More_Sublist


09:19:48 Word_Lib: theory HOL-Library.Type_Length


09:19:49 Word_Lib: theory HOL-Library.Word


09:19:49 Word_Lib: theory Word_Lib.More_Arithmetic


09:19:59 Word_Lib: theory Word_Lib.Legacy_Aliases


09:19:59 Word_Lib: theory Word_Lib.More_Divides


09:19:59 Word_Lib: theory Word_Lib.More_Word


09:20:01 Word_Lib: theory Word_Lib.Strict_part_mono


09:20:06 Word_Lib: theory Word_Lib.Bit_Comprehension


09:20:06 Word_Lib: theory Word_Lib.Bit_Shifts_Infix_Syntax


09:20:06 Word_Lib: theory HOL-Library.Signed_Division


09:20:06 Word_Lib: theory Word_Lib.Least_significant_bit


09:20:07 Word_Lib: theory Word_Lib.Signed_Division_Word


09:20:08 Word_Lib: theory Word_Lib.Aligned


09:20:08 Word_Lib: theory Word_Lib.Most_significant_bit


09:20:08 Word_Lib: theory Word_Lib.Generic_set_bit


09:20:08 Word_Lib: theory Word_Lib.Next_and_Prev


09:20:09 Word_Lib: theory Word_Lib.Bits_Int


09:20:14 Word_Lib: theory Word_Lib.Singleton_Bit_Shifts


09:20:14 Word_Lib: theory Word_Lib.Many_More


09:20:14 Word_Lib: theory Word_Lib.Typedef_Morphisms


09:20:15 Word_Lib: theory HOL-Eisbach.Eisbach


09:20:15 Word_Lib: theory Word_Lib.Bit_Comprehension_Int


09:20:15 Word_Lib: theory Word_Lib.Hex_Words


09:20:15 Word_Lib: theory Word_Lib.Type_Syntax


09:20:15 Word_Lib: theory Word_Lib.Syntax_Bundles


09:20:15 Word_Lib: theory Word_Lib.Enumeration_Word


09:20:15 Word_Lib: theory Word_Lib.Word_Syntax


09:20:15 Word_Lib: theory Word_Lib.Signed_Words


09:20:16 Word_Lib: theory Word_Lib.Sgn_Abs


09:20:16 Word_Lib: theory Word_Lib.Rsplit


09:20:16 Word_Lib: theory Word_Lib.Reversed_Bit_Lists


09:20:16 Word_Lib: theory Word_Lib.Norm_Words


09:20:16 Word_Lib: theory Word_Lib.Word_Names


09:20:16 Word_Lib: theory Word_Lib.Word_16


09:20:17 Word_Lib: theory HOL-Eisbach.Eisbach_Tools


09:20:17 Word_Lib: theory Word_Lib.Word_EqI


09:20:19 Word_Lib: theory Word_Lib.Boolean_Inequalities


09:20:20 Word_Lib: theory Word_Lib.Bitwise


09:20:20 Word_Lib: theory Word_Lib.Bitwise_Signed


09:20:22 Word_Lib: theory Word_Lib.Word_Lemmas


09:20:24 Word_Lib: theory Word_Lib.Word_8


09:20:24 Word_Lib: theory Word_Lib.More_Word_Operations


09:20:28 Word_Lib: theory Word_Lib.Word_32


09:20:28 Word_Lib: theory Word_Lib.Word_64


09:20:29 Word_Lib: theory Word_Lib.Machine_Word_64_Basics


09:20:29 Word_Lib: theory Word_Lib.Machine_Word_64


09:20:29 Word_Lib: theory Word_Lib.Machine_Word_32_Basics


09:20:29 Word_Lib: theory Word_Lib.Word_Lib_Sumo


09:20:29 Word_Lib: theory Word_Lib.Machine_Word_32


09:20:32 Word_Lib: theory Word_Lib.Guide


09:20:35 Word_Lib: theory Word_Lib.Examples


09:20:50 Preparing Word_Lib/document ...


09:21:01 Finished Word_Lib/document (0:00:11 elapsed time)


09:21:01 Preparing Word_Lib/outline ...


09:21:08 Finished Word_Lib/outline (0:00:07 elapsed time)


09:21:09 Timing Word_Lib (8 threads, 51.575s elapsed time, 253.996s cpu time, 11.880s GC time, factor 4.92)


09:21:09 Finished Word_Lib (0:01:04 elapsed time, 0:04:41 cpu time, factor 4.33)


09:21:09 Building IP_Addresses ...


09:21:10 IP_Addresses: theory IP_Addresses.NumberWang_IPv4


09:21:10 IP_Addresses: theory IP_Addresses.NumberWang_IPv6


09:21:10 IP_Addresses: theory HOL-Library.Infinite_Set


09:21:10 IP_Addresses: theory HOL-Library.Option_ord


09:21:10 IP_Addresses: theory HOL-Library.Cancellation


09:21:12 IP_Addresses: theory HOL-Library.Multiset


09:21:18 IP_Addresses: theory HOL-ex.Quicksort


09:21:19 IP_Addresses: theory Automatic_Refinement.Misc


09:21:26 IP_Addresses: theory IP_Addresses.Lib_Numbers_toString


09:21:26 IP_Addresses: theory IP_Addresses.Hs_Compat


09:21:26 IP_Addresses: theory HOL-Library.Code_Abstract_Nat


09:21:26 IP_Addresses: theory HOL-Library.Product_Lexorder


09:21:26 IP_Addresses: theory IP_Addresses.WordInterval


09:21:26 IP_Addresses: theory HOL-Library.Code_Target_Nat


09:21:26 IP_Addresses: theory IP_Addresses.Lib_List_toString


09:21:26 IP_Addresses: theory IP_Addresses.Lib_Word_toString


09:21:30 IP_Addresses: theory IP_Addresses.WordInterval_Sorted


09:21:30 IP_Addresses: theory IP_Addresses.IP_Address


09:21:36 IP_Addresses: theory IP_Addresses.IPv4


09:21:36 IP_Addresses: theory IP_Addresses.Prefix_Match


09:21:37 IP_Addresses: theory IP_Addresses.IPv6


09:21:37 IP_Addresses: theory IP_Addresses.CIDR_Split


09:22:30 IP_Addresses: theory IP_Addresses.IP_Address_Parser


09:22:30 IP_Addresses: theory IP_Addresses.IP_Address_toString


09:22:32 IP_Addresses: theory IP_Addresses.Prefix_Match_toString


09:25:09 Preparing IP_Addresses/document ...


09:25:13 Finished IP_Addresses/document (0:00:04 elapsed time)


09:25:13 Preparing IP_Addresses/outline ...


09:25:16 Finished IP_Addresses/outline (0:00:03 elapsed time)


09:25:17 Timing IP_Addresses (8 threads, 222.212s elapsed time, 733.493s cpu time, 31.297s GC time, factor 3.30)


09:25:17 Finished IP_Addresses (0:03:58 elapsed time, 0:12:47 cpu time, factor 3.22)


09:25:17 Building Simple_Firewall ...


09:25:18 Simple_Firewall: theory Simple_Firewall.GroupF


09:25:18 Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries


09:25:18 Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString


09:25:18 Simple_Firewall: theory HOL-Library.Char_ord


09:25:18 Simple_Firewall: theory Simple_Firewall.List_Product_More


09:25:18 Simple_Firewall: theory Simple_Firewall.Option_Helpers


09:25:18 Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State


09:25:18 Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString


09:25:19 Simple_Firewall: theory Simple_Firewall.Iface


09:25:19 Simple_Firewall: theory Simple_Firewall.L4_Protocol


09:25:22 Simple_Firewall: theory Simple_Firewall.Simple_Packet


09:25:22 Simple_Firewall: theory Simple_Firewall.Primitives_toString


09:25:24 Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax


09:25:27 Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics


09:25:27 Simple_Firewall: theory Simple_Firewall.SimpleFw_toString


09:25:30 Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw


09:25:30 Simple_Firewall: theory Simple_Firewall.Shadowed


09:25:30 Simple_Firewall: theory Simple_Firewall.Service_Matrix


09:25:49 Preparing Simple_Firewall/document ...


09:25:58 Finished Simple_Firewall/document (0:00:09 elapsed time)


09:25:58 Preparing Simple_Firewall/outline ...


09:26:05 Finished Simple_Firewall/outline (0:00:06 elapsed time)


09:26:06 Timing Simple_Firewall (8 threads, 19.260s elapsed time, 81.481s cpu time, 2.708s GC time, factor 4.23)


09:26:06 Finished Simple_Firewall (0:00:31 elapsed time, 0:01:47 cpu time, factor 3.39)


09:26:06 Building Routing ...


09:26:07 Routing: theory Routing.Linorder_Helper


09:26:07 Routing: theory HOL-Library.Adhoc_Overloading


09:26:07 Routing: theory Pure-ex.Guess


09:26:08 Routing: theory HOL-Library.Monad_Syntax


09:26:09 Routing: theory Routing.Routing_Table


09:26:12 Routing: theory Routing.IpRoute_Parser


09:26:12 Routing: theory Routing.Linux_Router


09:26:27 Preparing Routing/document ...


09:26:30 Finished Routing/document (0:00:02 elapsed time)


09:26:30 Preparing Routing/outline ...


09:26:32 Finished Routing/outline (0:00:02 elapsed time)


09:26:32 Timing Routing (8 threads, 9.512s elapsed time, 31.609s cpu time, 0.821s GC time, factor 3.32)


09:26:32 Finished Routing (0:00:21 elapsed time, 0:00:54 cpu time, factor 2.56)


09:26:32 Building Iptables_Semantics ...


09:26:33 Iptables_Semantics: theory Iptables_Semantics.List_Misc


09:26:33 Iptables_Semantics: theory Iptables_Semantics.Negation_Type


09:26:35 Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists


09:26:37 Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors


09:26:37 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF


09:26:37 Iptables_Semantics: theory HOL-Library.LaTeXsugar


09:26:37 Iptables_Semantics: theory HOL-Library.Code_Target_Int


09:26:37 Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize


09:26:37 Iptables_Semantics: theory Native_Word.Code_Int_Integer_Conversion


09:26:37 Iptables_Semantics: theory Iptables_Semantics.Ternary


09:26:37 Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev


09:26:37 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State


09:26:37 Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags


09:26:37 Iptables_Semantics: theory Native_Word.Code_Target_Integer_Bit


09:26:37 Iptables_Semantics: theory Iptables_Semantics.Word_Upto


09:26:37 Iptables_Semantics: theory Iptables_Semantics.Firewall_Common


09:26:37 Iptables_Semantics: theory Iptables_Semantics.IpAddresses


09:26:38 Iptables_Semantics: theory Iptables_Semantics.Ports


09:26:38 Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet


09:26:39 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax


09:26:52 Iptables_Semantics: theory Native_Word.Code_Target_Int_Bit


09:26:52 Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary


09:26:52 Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto


09:26:52 Iptables_Semantics: theory Iptables_Semantics.Semantics


09:26:54 Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics


09:26:54 Iptables_Semantics: theory Iptables_Semantics.Matching


09:26:54 Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful


09:26:54 Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update


09:26:54 Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding


09:26:55 Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary


09:26:55 Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs


09:26:56 Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings


09:26:56 Iptables_Semantics: theory Iptables_Semantics.Fixed_Action


09:26:56 Iptables_Semantics: theory Iptables_Semantics.Optimizing


09:26:56 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic


09:26:57 Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches


09:26:58 Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching


09:27:00 Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization


09:27:01 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher


09:27:03 Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold


09:27:03 Iptables_Semantics: theory Iptables_Semantics.Ipassmt


09:27:06 Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt


09:27:36 Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform


09:27:36 Iptables_Semantics: theory Iptables_Semantics.Example_Semantics


09:27:36 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString


09:27:36 Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas


09:27:36 Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize


09:27:36 Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize


09:27:36 Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize


09:27:36 Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize


09:27:37 Iptables_Semantics: theory Iptables_Semantics.No_Spoof


09:27:41 Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace


09:27:43 Iptables_Semantics: theory Iptables_Semantics.Interface_Replace


09:27:45 Iptables_Semantics: theory Iptables_Semantics.Transform


09:27:49 Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract


09:27:50 Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance


09:27:54 Iptables_Semantics: theory Iptables_Semantics.Code_Interface


09:27:54 Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings


09:27:55 Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings


09:27:55 Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics


09:27:55 Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings


09:28:00 Iptables_Semantics: theory Iptables_Semantics.Parser


09:28:00 Iptables_Semantics: theory Iptables_Semantics.Parser6


09:28:00 Iptables_Semantics: theory Iptables_Semantics.Documentation


09:28:01 Iptables_Semantics: theory Iptables_Semantics.Code_haskell


09:28:52 Preparing Iptables_Semantics/document ...


09:29:16 Finished Iptables_Semantics/document (0:00:23 elapsed time)


09:29:16 Preparing Iptables_Semantics/outline ...


09:29:27 Finished Iptables_Semantics/outline (0:00:11 elapsed time)


09:29:28 Timing Iptables_Semantics (8 threads, 108.352s elapsed time, 542.468s cpu time, 40.111s GC time, factor 5.01)


09:29:28 Finished Iptables_Semantics (0:02:18 elapsed time, 0:10:07 cpu time, factor 4.39)


09:29:28 Building Iptables_Semantics_Examples ...


09:29:30 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com


09:29:30 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall


09:29:30 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company


09:29:30 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example


09:29:30 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test


09:29:30 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof


09:29:30 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing


09:29:30 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test


09:29:34 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail


09:29:34 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples


09:29:34 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed


09:29:35 Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation


09:33:00 Preparing Iptables_Semantics_Examples/document ...


09:33:05 Finished Iptables_Semantics_Examples/document (0:00:05 elapsed time)


09:33:05 Preparing Iptables_Semantics_Examples/outline ...


09:33:11 Finished Iptables_Semantics_Examples/outline (0:00:05 elapsed time)


09:33:11 Timing Iptables_Semantics_Examples (8 threads, 197.879s elapsed time, 1257.055s cpu time, 99.475s GC time, factor 6.35)


09:33:11 Finished Iptables_Semantics_Examples (0:03:31 elapsed time, 0:21:23 cpu time, factor 6.08)


09:33:11 Running Iptables_Semantics_Examples_Big ...


09:33:13 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern


09:33:13 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated


09:33:13 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small


09:33:13 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3


09:33:13 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall


09:35:32 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large


09:55:52 Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW


10:36:37 Preparing Iptables_Semantics_Examples_Big/document ...


10:36:41 Finished Iptables_Semantics_Examples_Big/document (0:00:04 elapsed time)


10:36:41 Preparing Iptables_Semantics_Examples_Big/outline ...


10:36:45 Finished Iptables_Semantics_Examples_Big/outline (0:00:04 elapsed time)


10:36:46 Timing Iptables_Semantics_Examples_Big (8 threads, 3800.477s elapsed time, 23388.250s cpu time, 5582.359s GC time, factor 6.15)


10:36:46 Finished Iptables_Semantics_Examples_Big (1:03:25 elapsed time, 6:29:58 cpu time, factor 6.15)


10:36:46 Building HOL-Library ...


10:36:47 HOL-Library: theory HOL-Library.README


10:36:48 HOL-Library: theory HOL-Library.Adhoc_Overloading


10:36:48 HOL-Library: theory HOL-Library.AList


10:36:48 HOL-Library: theory HOL-Library.BNF_Axiomatization


10:36:48 HOL-Library: theory HOL-Library.BNF_Corec


10:36:48 HOL-Library: theory HOL-Library.Cancellation


10:36:48 HOL-Library: theory HOL-Library.Case_Converter


10:36:48 HOL-Library: theory HOL-Library.Char_ord


10:36:48 HOL-Library: theory HOL-Library.Centered_Division


10:36:48 HOL-Library: theory HOL-Library.Code_Abstract_Char


10:36:48 HOL-Library: theory HOL-Library.Monad_Syntax


10:36:48 HOL-Library: theory HOL-Library.Code_Abstract_Nat


10:36:48 HOL-Library: theory HOL-Library.Code_Prolog


10:36:48 HOL-Library: theory HOL-Library.State_Monad


10:36:48 HOL-Library: theory HOL-Library.Code_Binary_Nat


10:36:49 HOL-Library: theory HOL-Library.Code_Lazy


10:36:49 HOL-Library: theory HOL-Library.Simps_Case_Conv


10:36:49 HOL-Library: theory HOL-Library.Extended


10:36:49 HOL-Library: theory HOL-Library.Multiset


10:36:50 HOL-Library: theory HOL-Library.Code_Target_Nat


10:36:50 HOL-Library: theory HOL-Library.Code_Target_Int


10:36:50 HOL-Library: theory HOL-Library.Code_Test


10:36:50 HOL-Library: theory HOL-Library.Code_Target_Numeral


10:36:50 HOL-Library: theory HOL-Library.Combine_PER


10:36:50 HOL-Library: theory HOL-Library.Comparator


10:36:51 HOL-Library: theory HOL-Library.Complete_Partial_Order2


10:36:51 HOL-Library: theory HOL-Library.DAList


10:36:51 HOL-Library: theory HOL-Library.Conditional_Parametricity


10:36:51 HOL-Library: theory HOL-Library.Confluence


10:36:51 HOL-Library: theory HOL-Library.Datatype_Records


10:36:52 HOL-Library: theory HOL-Library.Confluent_Quotient


10:36:52 HOL-Library: theory HOL-Library.Debug


10:36:52 HOL-Library: theory HOL-Library.Dlist


10:36:52 HOL-Library: theory HOL-Library.Dual_Ordered_Lattice


10:36:52 HOL-Library: theory HOL-Library.Fun_Lexorder


10:36:52 HOL-Library: theory HOL-Library.FuncSet


10:36:52 HOL-Library: theory HOL-Library.Function_Algebras


10:36:53 HOL-Library: theory HOL-Library.Function_Division


10:36:53 HOL-Library: theory HOL-Library.Groups_Big_Fun


10:36:53 HOL-Library: theory HOL-Library.IArray


10:36:54 HOL-Library: theory HOL-Library.Infinite_Set


10:36:54 HOL-Library: theory HOL-Library.Disjoint_Sets


10:36:54 HOL-Library: theory HOL-Library.LaTeXsugar


10:36:54 HOL-Library: theory HOL-Library.Lattice_Constructions


10:36:55 HOL-Library: theory HOL-Library.Omega_Words_Fun


10:36:55 HOL-Library: theory HOL-Library.ListVector


10:36:55 HOL-Library: theory HOL-Library.List_Lenlexorder


10:36:55 HOL-Library: theory HOL-Library.List_Lexorder


10:36:55 HOL-Library: theory HOL-Library.Mapping


10:36:55 HOL-Library: theory HOL-Library.More_List


10:36:55 HOL-Library: theory HOL-Library.NList


10:36:55 HOL-Library: theory HOL-Library.Nat_Bijection


10:36:55 HOL-Library: theory HOL-Library.Poly_Mapping


10:36:55 HOL-Library: theory HOL-Library.Stream


10:36:56 HOL-Library: theory HOL-Library.Old_Datatype


10:36:59 HOL-Library: theory HOL-Library.Old_Recdef


10:36:59 HOL-Library: theory HOL-Library.AList_Mapping


10:37:00 HOL-Library: theory HOL-Library.Open_State_Syntax


10:37:00 HOL-Library: theory HOL-Library.Option_ord


10:37:00 HOL-Library: theory HOL-Library.Parallel


10:37:00 HOL-Library: theory HOL-Library.Pattern_Aliases


10:37:00 HOL-Library: theory HOL-Library.Phantom_Type


10:37:00 HOL-Library: theory HOL-Library.DAList_Multiset


10:37:00 HOL-Library: theory HOL-Library.Multiset_Order


10:37:00 HOL-Library: theory HOL-Library.Power_By_Squaring


10:37:01 HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs


10:37:01 HOL-Library: theory HOL-Library.Preorder


10:37:01 HOL-Library: theory HOL-Library.Product_Lexorder


10:37:01 HOL-Library: theory HOL-Library.Product_Plus


10:37:03 HOL-Library: theory HOL-Library.Quotient_Syntax


10:37:03 HOL-Library: theory HOL-Library.Quotient_Type


10:37:03 HOL-Library: theory HOL-Library.Quotient_Option


10:37:03 HOL-Library: theory HOL-Library.Product_Order


10:37:03 HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck


10:37:03 HOL-Library: theory HOL-Library.Quotient_Product


10:37:03 HOL-Library: theory HOL-Library.Quotient_Set


10:37:03 HOL-Library: theory HOL-Library.Cardinality


10:37:03 HOL-Library: theory HOL-Library.Quotient_Sum


10:37:03 HOL-Library: theory HOL-Library.Quotient_List


10:37:03 HOL-Library: theory HOL-Library.RBT_Impl


10:37:03 HOL-Library: theory HOL-Library.Realizers


10:37:03 HOL-Library: theory HOL-Library.Finite_Lattice


10:37:03 HOL-Library: theory HOL-Library.Reflection


10:37:03 HOL-Library: theory HOL-Library.Refute


10:37:03 HOL-Library: theory HOL-Library.Rewrite


10:37:04 HOL-Library: theory HOL-Library.Set_Algebras


10:37:04 HOL-Library: theory HOL-Library.Signed_Division


10:37:04 HOL-Library: theory HOL-Library.Sorting_Algorithms


10:37:04 HOL-Library: theory HOL-Library.Sublist


10:37:04 HOL-Library: theory HOL-Library.Code_Cardinality


10:37:05 HOL-Library: theory HOL-Library.Numeral_Type


10:37:05 HOL-Library: theory HOL-Library.Transitive_Closure_Table


10:37:06 HOL-Library: theory HOL-Library.Tree


10:37:06 HOL-Library: theory HOL-Library.Uprod


10:37:06 HOL-Library: theory HOL-Library.While_Combinator


10:37:06 HOL-Library: theory HOL-Library.Type_Length


10:37:06 HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint


10:37:06 HOL-Library: theory HOL-Library.Z2


10:37:07 HOL-Library: theory HOL-Library.Countable


10:37:07 HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float


10:37:07 HOL-Library: theory HOL-Library.Prefix_Order


10:37:07 HOL-Library: theory HOL-Library.Saturated


10:37:07 HOL-Library: theory HOL-Library.Word


10:37:07 HOL-Library: theory HOL-Library.Subseq_Order


10:37:07 HOL-Library: theory HOL-Library.Complex_Order


10:37:07 HOL-Library: theory HOL-Library.Diagonal_Subsequence


10:37:07 HOL-Library: theory HOL-Library.Discrete


10:37:07 HOL-Library: theory HOL-Library.Going_To_Filter


10:37:07 HOL-Library: theory HOL-Library.Indicator_Function


10:37:07 HOL-Library: theory HOL-Library.Infinite_Typeclass


10:37:07 HOL-Library: theory HOL-Library.Countable_Set


10:37:07 HOL-Library: theory HOL-Library.FSet


10:37:08 HOL-Library: theory HOL-Library.Landau_Symbols


10:37:08 HOL-Library: theory HOL-Library.Lattice_Algebras


10:37:08 HOL-Library: theory HOL-Library.Tree_Multiset


10:37:08 HOL-Library: theory HOL-Library.Countable_Complete_Lattices


10:37:08 HOL-Library: theory HOL-Library.Countable_Set_Type


10:37:10 HOL-Library: theory HOL-Library.Equipollence


10:37:10 HOL-Library: theory HOL-Library.Set_Idioms


10:37:10 HOL-Library: theory HOL-Library.Liminf_Limsup


10:37:11 HOL-Library: theory HOL-Library.Log_Nat


10:37:11 HOL-Library: theory HOL-Library.Ramsey


10:37:11 HOL-Library: theory HOL-Library.Lub_Glb


10:37:11 HOL-Library: theory HOL-Library.Nonpos_Ints


10:37:12 HOL-Library: theory HOL-Library.OptionalSugar


10:37:12 HOL-Library: theory HOL-Library.Order_Continuity


10:37:12 HOL-Library: theory HOL-Library.Finite_Map


10:37:12 HOL-Library: theory HOL-Library.Periodic_Fun


10:37:12 HOL-Library: theory HOL-Library.Quadratic_Discriminant


10:37:12 HOL-Library: theory HOL-Library.Sum_of_Squares


10:37:12 HOL-Library: theory HOL-Library.Tree_Real


10:37:12 HOL-Library: theory HOL-Library.Extended_Nat


10:37:13 HOL-Library: theory HOL-Library.Extended_Real


10:37:13 HOL-Library: theory HOL-Library.Interval


10:37:13 HOL-Library: theory HOL-Library.Float


10:37:16 HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams


10:37:17 HOL-Library: theory HOL-Library.Code_Target_Numeral_Float


10:37:17 HOL-Library: theory HOL-Library.Interval_Float


10:37:18 HOL-Library: theory HOL-Library.Extended_Nonnegative_Real


10:37:27 HOL-Library: theory HOL-Library.Disjoint_FSets


10:37:28 HOL-Library: theory HOL-Library.Library


10:38:04 HOL-Library: theory HOL-Library.RBT


10:38:05 HOL-Library: theory HOL-Library.RBT_Mapping


10:38:05 HOL-Library: theory HOL-Library.RBT_Set


10:40:22 Preparing HOL-Library/document ...


10:41:21 Finished HOL-Library/document (0:00:58 elapsed time)


10:41:21 Preparing HOL-Library/outline ...


10:41:56 Finished HOL-Library/outline (0:00:35 elapsed time)


10:41:58 Timing HOL-Library (8 threads, 168.798s elapsed time, 1045.589s cpu time, 56.839s GC time, factor 6.19)


10:41:58 Finished HOL-Library (0:03:20 elapsed time, 0:18:35 cpu time, factor 5.56)


10:41:58 Building Category3 ...


10:42:01 Category3: theory HOL-Cardinals.Order_Relation_More


10:42:01 Category3: theory Category3.Category


10:42:01 Category3: theory HOL-Cardinals.Fun_More


10:42:01 Category3: theory HOL-Cardinals.Order_Union


10:42:01 Category3: theory HereditarilyFinite.HF


10:42:02 Category3: theory HOL-Cardinals.Wellorder_Extension


10:42:02 Category3: theory HOL-Cardinals.Wellfounded_More


10:42:02 Category3: theory HOL-Cardinals.Wellorder_Relation


10:42:02 Category3: theory Category3.ConcreteCategory


10:42:02 Category3: theory Category3.DiscreteCategory


10:42:02 Category3: theory Category3.EpiMonoIso


10:42:02 Category3: theory HOL-Cardinals.Wellorder_Embedding


10:42:03 Category3: theory HOL-Cardinals.Wellorder_Constructions


10:42:03 Category3: theory Category3.DualCategory


10:42:03 Category3: theory Category3.InitialTerminal


10:42:03 Category3: theory Category3.ProductCategory


10:42:04 Category3: theory HOL-Cardinals.Cardinal_Order_Relation


10:42:04 Category3: theory HOL-Cardinals.Ordinal_Arithmetic


10:42:05 Category3: theory Category3.FreeCategory


10:42:05 Category3: theory Category3.Functor


10:42:05 Category3: theory HOL-Cardinals.Cardinal_Arithmetic


10:42:06 Category3: theory HOL-Cardinals.Cardinals


10:42:06 Category3: theory ZFC_in_HOL.ZFC_Library


10:42:06 Category3: theory ZFC_in_HOL.ZFC_in_HOL


10:42:07 Category3: theory ZFC_in_HOL.ZFC_Cardinals


10:42:10 Category3: theory Category3.NaturalTransformation


10:42:10 Category3: theory Category3.Subcategory


10:42:12 Category3: theory Category3.SetCategory


10:42:13 Category3: theory Category3.BinaryFunctor


10:42:15 Category3: theory Category3.SetCat


10:42:19 Category3: theory Category3.FunctorCategory


10:42:32 Category3: theory Category3.Yoneda


10:42:57 Category3: theory Category3.Adjunction


10:43:56 Category3: theory Category3.EquivalenceOfCategories


10:43:56 Category3: theory Category3.Limit


10:46:18 Category3: theory Category3.CategoryWithPullbacks


10:46:18 Category3: theory Category3.ZFC_SetCat


10:46:38 Category3: theory Category3.CartesianCategory


10:46:39 Category3: theory Category3.ZFC_SetCat_Interp


10:47:03 Category3: theory Category3.CartesianClosedCategory


10:47:04 Category3: theory Category3.CategoryWithFiniteLimits


10:47:05 Category3: theory Category3.HF_SetCat


10:47:11 Category3: theory Category3.HF_SetCat_Interp


10:48:58 Preparing Category3/document ...


10:49:28 Finished Category3/document (0:00:29 elapsed time)


10:49:28 Preparing Category3/outline ...


10:49:40 Finished Category3/outline (0:00:11 elapsed time)


10:49:40 Timing Category3 (8 threads, 392.398s elapsed time, 1966.612s cpu time, 379.672s GC time, factor 5.01)


10:49:40 Finished Category3 (0:06:56 elapsed time, 0:33:38 cpu time, factor 4.84)


10:49:40 Building MonoidalCategory ...


10:49:42 MonoidalCategory: theory MonoidalCategory.MonoidalCategory


10:50:45 MonoidalCategory: theory MonoidalCategory.MonoidalFunctor


10:50:51 MonoidalCategory: theory MonoidalCategory.CartesianMonoidalCategory


10:50:59 MonoidalCategory: theory MonoidalCategory.FreeMonoidalCategory


10:53:39 Preparing MonoidalCategory/document ...


10:53:54 Finished MonoidalCategory/document (0:00:14 elapsed time)


10:53:54 Preparing MonoidalCategory/outline ...


10:54:00 Finished MonoidalCategory/outline (0:00:06 elapsed time)


10:54:01 Timing MonoidalCategory (8 threads, 217.149s elapsed time, 822.736s cpu time, 80.714s GC time, factor 3.79)


10:54:01 Finished MonoidalCategory (0:03:57 elapsed time, 0:14:23 cpu time, factor 3.64)


10:54:01 Running Bicategory ...


10:54:11 Bicategory: theory Bicategory.IsomorphismClass


10:54:11 Bicategory: theory Bicategory.Prebicategory


10:54:36 Bicategory: theory Bicategory.Bicategory


10:55:10 Bicategory: theory Bicategory.Coherence


10:55:20 Bicategory: theory Bicategory.ConcreteBicategory


10:55:20 Bicategory: theory Bicategory.InternalEquivalence


10:55:20 Bicategory: theory Bicategory.Subbicategory


10:56:30 Bicategory: theory Bicategory.CanonicalIsos


10:56:35 Bicategory: theory Bicategory.Pseudofunctor


10:59:11 Bicategory: theory Bicategory.Strictness


11:01:47 Bicategory: theory Bicategory.CatBicat


11:01:49 Bicategory: theory Bicategory.InternalAdjunction


11:05:55 Bicategory: theory Bicategory.PseudonaturalTransformation


11:07:02 Bicategory: theory Bicategory.Tabulation


11:07:02 Bicategory: theory Bicategory.SpanBicategory


11:09:59 Bicategory: theory Bicategory.EquivalenceOfBicategories


11:10:00 Bicategory: theory Bicategory.Modification


11:26:50 Bicategory: theory Bicategory.BicategoryOfSpans


11:44:59 Preparing Bicategory/document ...


11:46:38 Finished Bicategory/document (0:01:38 elapsed time)


11:46:38 Preparing Bicategory/outline ...


11:46:58 Finished Bicategory/outline (0:00:20 elapsed time)


11:46:59 Timing Bicategory (8 threads, 2963.712s elapsed time, 9995.943s cpu time, 709.576s GC time, factor 3.37)


11:46:59 Finished Bicategory (0:50:53 elapsed time, 2:52:32 cpu time, factor 3.39)


11:46:59 Building ConcurrentIMP ...


11:47:01 ConcurrentIMP: theory ConcurrentIMP.CIMP_pred


11:47:01 ConcurrentIMP: theory ConcurrentIMP.Infinite_Sequences


11:47:02 ConcurrentIMP: theory ConcurrentIMP.LTL


11:47:03 ConcurrentIMP: theory ConcurrentIMP.CIMP_lang


11:47:10 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg


11:47:15 ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg_rules


11:47:15 ConcurrentIMP: theory ConcurrentIMP.CIMP


11:47:16 ConcurrentIMP: theory ConcurrentIMP.CIMP_locales


11:47:16 ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer


11:47:16 ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer


11:47:37 Preparing ConcurrentIMP/document ...


11:47:43 Finished ConcurrentIMP/document (0:00:05 elapsed time)


11:47:43 Preparing ConcurrentIMP/outline ...


11:47:48 Finished ConcurrentIMP/outline (0:00:05 elapsed time)


11:47:48 Timing ConcurrentIMP (8 threads, 21.327s elapsed time, 73.916s cpu time, 2.910s GC time, factor 3.47)


11:47:48 Finished ConcurrentIMP (0:00:37 elapsed time, 0:01:46 cpu time, factor 2.85)


11:47:48 Running ConcurrentGC ...


11:47:50 ConcurrentGC: theory ConcurrentGC.Model


11:48:08 ConcurrentGC: theory ConcurrentGC.Proofs_Basis


11:48:20 ConcurrentGC: theory ConcurrentGC.Global_Invariants


11:48:20 ConcurrentGC: theory ConcurrentGC.Local_Invariants


11:48:20 ConcurrentGC: theory ConcurrentGC.Tactics


11:48:21 ConcurrentGC: theory ConcurrentGC.Concrete_heap


11:48:21 ConcurrentGC: theory ConcurrentGC.Global_Invariants_Lemmas


11:48:21 ConcurrentGC: theory ConcurrentGC.Concrete


11:48:23 ConcurrentGC: theory ConcurrentGC.Global_Noninterference


11:50:02 ConcurrentGC: theory ConcurrentGC.Local_Invariants_Lemmas


11:50:03 ConcurrentGC: theory ConcurrentGC.Initial_Conditions


11:50:03 ConcurrentGC: theory ConcurrentGC.MarkObject


11:50:04 ConcurrentGC: theory ConcurrentGC.Noninterference


11:50:04 ConcurrentGC: theory ConcurrentGC.Phases


11:50:04 ConcurrentGC: theory ConcurrentGC.StrongTricolour


11:50:05 ConcurrentGC: theory ConcurrentGC.TSO


11:50:05 ConcurrentGC: theory ConcurrentGC.Valid_Refs


11:50:05 ConcurrentGC: theory ConcurrentGC.Worklists


11:50:07 ConcurrentGC: theory ConcurrentGC.Proofs


12:06:19 Preparing ConcurrentGC/document ...


12:06:30 Finished ConcurrentGC/document (0:00:10 elapsed time)


12:06:30 Preparing ConcurrentGC/outline ...


12:06:38 Finished ConcurrentGC/outline (0:00:07 elapsed time)


12:06:38 Timing ConcurrentGC (8 threads, 1107.449s elapsed time, 6529.771s cpu time, 340.674s GC time, factor 5.90)


12:06:38 Finished ConcurrentGC (0:18:30 elapsed time, 1:48:55 cpu time, factor 5.89)


12:06:38 Presentation in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info"


12:06:48 Presenting Pure in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure" ...


12:06:48 Presenting HOL in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL" ...


12:06:48 Presenting AWN in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN" ...


12:06:48 Presenting Flyspeck-Tame in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame" ...


12:06:48 Presenting Flyspeck-Tame-Computation in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame-Computation" ...


12:06:48 Presenting HOL-Library in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library" ...


12:06:48 Presenting MonoidalCategory in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/MonoidalCategory" ...


12:06:48 Presenting Category3 in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Category3" ...


12:06:48 Presenting AODV in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV" ...


12:06:48 Presenting document MonoidalCategory/document


12:06:48 Presenting document MonoidalCategory/outline


12:06:48 Presenting document Flyspeck-Tame/document


12:06:48 Presenting document Flyspeck-Tame/outline


12:06:48 Presenting document AWN/document


12:06:48 Presenting document AWN/outline


12:06:48 Presenting document Category3/document


12:06:48 Presenting document Category3/outline


12:06:48 Presenting theory "AWN.Lib"


12:06:48 Presenting theory "Flyspeck-Tame-Computation.ArchComp"


12:06:48 Presenting document AODV/document


12:06:48 Presenting document AODV/outline


12:06:49 Presenting document HOL/document


12:06:49 Presenting document HOL/outline


12:06:49 Presenting theory "AODV.Aodv_Basic"


12:06:49 Presenting theory "AWN.TransitionSystems"


12:06:49 Presenting theory "Flyspeck-Tame-Computation.Completeness"


12:06:49 Presenting Bicategory in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Bicategory" ...


12:06:49 Presenting document Bicategory/document


12:06:49 Presenting theory "Category3.Category"


12:06:49 Presenting document Bicategory/outline


12:06:49 Presenting theory "Bicategory.IsomorphismClass"


12:06:49 Presenting theory "AWN.Invariants"


12:06:49 Presenting document HOL-Library/document


12:06:49 Presenting document HOL-Library/outline


12:06:49 Presenting theory "HOL-Library.README"


12:06:50 Presenting theory "Category3.EpiMonoIso"


12:06:50 Presenting theory "Category3.DualCategory"


12:06:50 Presenting theory "Flyspeck-Tame.ListAux"


12:06:50 Presenting theory "Flyspeck-Tame.Quasi_Order"


12:06:51 Presenting theory "HOL-Library.AList"


12:06:51 Presenting theory "Category3.ConcreteCategory"


12:06:51 Presenting theory "HOL-Library.Adhoc_Overloading"


12:06:51 Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"


12:06:51 Presenting theory "Category3.InitialTerminal"


12:06:51 Presenting theory "AWN.OInvariants"


12:06:52 Presenting theory "Pure"


12:06:52 Presenting theory "Flyspeck-Tame.PlaneGraphIso"


12:06:52 Presenting file "~~/src/Pure/ROOT0.ML"


12:06:52 Presenting file "~~/src/Pure/ROOT.ML"


12:06:52 Presenting theory "HOL-Library.BNF_Axiomatization"


12:06:52 Presenting file "~~/src/HOL/Tools/BNF/bnf_axiomatization.ML"


12:06:52 Presenting theory "ML_Bootstrap"


12:06:52 Presenting theory "Pure.Sessions"


12:06:52 Presenting theory "Flyspeck-Tame.Rotation"


12:06:52 Presenting theory "Bicategory.Prebicategory"


12:06:52 Presenting theory "Flyspeck-Tame.Graph"


12:06:53 Presenting theory "HOL-Library.IArray"


12:06:53 Presenting theory "Category3.Functor"


12:06:53 Presenting theory "Flyspeck-Tame.IArray_Syntax"


12:06:53 Presenting theory "Flyspeck-Tame.Enumerator"


12:06:53 Presenting theory "Flyspeck-Tame.FaceDivision"


12:06:53 Presenting theory "Category3.Subcategory"


12:06:53 Presenting theory "AODV.Aodv_Data"


12:06:53 Presenting theory "Flyspeck-Tame.RTranCl"


12:06:53 Presenting theory "AWN.AWN"


12:06:53 Presenting theory "Flyspeck-Tame.Plane"


12:06:53 Presenting theory "Flyspeck-Tame.Plane1"


12:06:53 Presenting theory "AODV.Aodv_Message"


12:06:54 Presenting theory "Flyspeck-Tame.GraphProps"


12:06:55 Presenting theory "Flyspeck-Tame.EnumeratorProps"


12:06:55 Presenting theory "AODV.Aodv"


12:06:55 Presenting theory "AWN.AWN_SOS"


12:06:55 Presenting theory "AODV.Aodv_Predicates"


12:06:55 Presenting theory "MonoidalCategory.MonoidalCategory"


12:06:56 Presenting theory "Bicategory.Bicategory"


12:06:56 Presenting theory "Category3.SetCategory"


12:06:58 Presenting theory "AODV.Fresher"


12:06:58 Presenting theory "MonoidalCategory.MonoidalFunctor"


12:06:59 Presenting theory "AWN.AWN_Cterms"


12:07:00 Presenting theory "AWN.AWN_Labels"


12:07:00 Presenting theory "AWN.Inv_Cterms"


12:07:00 Presenting theory "AWN.AWN_SOS_Labels"


12:07:01 Presenting theory "AODV.Seq_Invariants"


12:07:01 Presenting theory "Category3.SetCat"


12:07:02 Presenting theory "Category3.ProductCategory"


12:07:03 Presenting theory "AWN.Pnet"


12:07:03 Presenting theory "AWN.Closed"


12:07:04 Presenting theory "AODV.Quality_Increases"


12:07:04 Presenting theory "AODV.OAodv"


12:07:05 Presenting theory "Category3.NaturalTransformation"


12:07:05 Presenting theory "MonoidalCategory.FreeMonoidalCategory"


12:07:06 Presenting theory "Category3.BinaryFunctor"


12:07:06 Presenting theory "Flyspeck-Tame.FaceDivisionProps"


12:07:07 Presenting theory "AWN.OAWN_SOS"


12:07:07 Presenting theory "Bicategory.Coherence"


12:07:07 Presenting theory "AWN.OAWN_SOS_Labels"


12:07:07 Presenting theory "MonoidalCategory.CartesianMonoidalCategory"


12:07:07 Presenting theory "AWN.OPnet"


12:07:07 Presenting ConcurrentIMP in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP" ...


12:07:07 Presenting document ConcurrentIMP/document


12:07:07 Presenting document ConcurrentIMP/outline


12:07:07 Presenting theory "ConcurrentIMP.CIMP_pred"


12:07:07 Presenting theory "ConcurrentIMP.Infinite_Sequences"


12:07:08 Presenting theory "Category3.FunctorCategory"


12:07:09 Presenting theory "ConcurrentIMP.LTL"


12:07:09 Presenting theory "Bicategory.CanonicalIsos"


12:07:10 Presenting theory "AWN.ONode_Lifting"


12:07:10 Presenting theory "ConcurrentIMP.CIMP_lang"


12:07:10 Presenting theory "AODV.Global_Invariants"


12:07:10 Presenting theory "Category3.Yoneda"


12:07:11 Presenting theory "AODV.Loop_Freedom"


12:07:11 Presenting theory "Flyspeck-Tame.Invariants"


12:07:11 Presenting theory "Bicategory.Subbicategory"


12:07:12 Presenting theory "ConcurrentIMP.CIMP_vcg"


12:07:12 Presenting theory "ConcurrentIMP.CIMP_vcg_rules"


12:07:13 Presenting theory "Flyspeck-Tame.PlaneProps"


12:07:13 Presenting theory "AODV.Aodv_Loop_Freedom"


12:07:13 Presenting theory "Flyspeck-Tame.ListSum"


12:07:13 Presenting theory "AODV.A_Norreqid"


12:07:13 Presenting theory "ConcurrentIMP.CIMP"


12:07:13 Presenting file "$AFP/ConcurrentIMP/cimp.ML"


12:07:13 Presenting theory "AWN.OPnet_Lifting"


12:07:13 Presenting theory "ConcurrentIMP.CIMP_locales"


12:07:13 Presenting theory "Flyspeck-Tame.Tame"


12:07:13 Presenting theory "Flyspeck-Tame.Plane1Props"


12:07:13 Presenting theory "ConcurrentIMP.CIMP_one_place_buffer"


12:07:13 Presenting theory "Flyspeck-Tame.Generator"


12:07:13 Presenting theory "ConcurrentIMP.CIMP_unbounded_buffer"


12:07:13 Presenting ConcurrentGC in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC" ...


12:07:13 Presenting document ConcurrentGC/document


12:07:13 Presenting document ConcurrentGC/outline


12:07:13 Presenting theory "Flyspeck-Tame.TameProps"


12:07:13 Presenting theory "Flyspeck-Tame.TameEnum"


12:07:13 Presenting theory "AWN.OClosed_Lifting"


12:07:13 Presenting theory "Bicategory.InternalEquivalence"


12:07:14 Presenting theory "ConcurrentGC.Model"


12:07:14 Presenting theory "Flyspeck-Tame.ScoreProps"


12:07:14 Presenting theory "Flyspeck-Tame.LowerBound"


12:07:15 Presenting theory "AWN.AWN_Invariants"


12:07:15 Presenting theory "AODV.A_Aodv_Data"


12:07:15 Presenting theory "ConcurrentGC.Proofs_Basis"


12:07:15 Presenting theory "AODV.A_Aodv_Message"


12:07:15 Presenting theory "Flyspeck-Tame.GeneratorProps"


12:07:15 Presenting theory "Flyspeck-Tame.TameEnumProps"


12:07:16 Presenting theory "ConcurrentGC.Global_Invariants"


12:07:17 Presenting theory "HOL-Library.BNF_Corec"


12:07:17 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML"


12:07:17 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML"


12:07:17 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML"


12:07:17 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML"


12:07:17 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML"


12:07:17 Presenting theory "AODV.A_Aodv"


12:07:17 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML"


12:07:17 Presenting theory "HOL-Library.AList"


12:07:17 Presenting theory "AODV.A_Aodv_Predicates"


12:07:17 Presenting theory "ConcurrentGC.Local_Invariants"


12:07:17 Presenting theory "HOL-Library.While_Combinator"


12:07:17 Presenting theory "Tools.Code_Generator"


12:07:17 Presenting file "~~/src/Tools/cache_io.ML"


12:07:17 Presenting file "~~/src/Tools/Code/code_preproc.ML"


12:07:17 Presenting file "~~/src/Tools/Code/code_symbol.ML"


12:07:17 Presenting file "~~/src/Tools/Code/code_thingol.ML"


12:07:17 Presenting file "~~/src/Tools/Code/code_simp.ML"


12:07:17 Presenting file "~~/src/Tools/Code/code_printer.ML"


12:07:17 Presenting file "~~/src/Tools/Code/code_target.ML"


12:07:17 Presenting file "~~/src/Tools/Code/code_namespace.ML"


12:07:17 Presenting file "~~/src/Tools/Code/code_ml.ML"


12:07:18 Presenting file "~~/src/Tools/Code/code_haskell.ML"


12:07:18 Presenting file "~~/src/Tools/Code/code_scala.ML"


12:07:18 Presenting file "~~/src/Tools/Code/code_runtime.ML"


12:07:18 Presenting theory "Trie.Trie"


12:07:18 Presenting theory "HOL-Library.Bourbaki_Witt_Fixpoint"


12:07:18 Presenting theory "AWN.OAWN_Invariants"


12:07:18 Presenting file "~~/src/Tools/nbe.ML"


12:07:18 Presenting theory "Bicategory.Pseudofunctor"


12:07:18 Presenting theory "HOL-Library.Centered_Division"


12:07:18 Presenting theory "Trie.Tries"


12:07:18 Presenting theory "HOL-Library.Char_ord"


12:07:18 Presenting theory "HOL-Library.Phantom_Type"


12:07:18 Presenting theory "HOL-Library.Cardinality"


12:07:18 Presenting theory "HOL-Library.Code_Cardinality"


12:07:18 Presenting theory "ConcurrentGC.Tactics"


12:07:18 Presenting theory "HOL-Library.While_Combinator"


12:07:18 Presenting theory "Category3.Adjunction"


12:07:18 Presenting theory "AWN.OAWN_Convert"


12:07:18 Presenting theory "AWN.Qmsg"


12:07:19 Presenting theory "Flyspeck-Tame.Worklist"


12:07:19 Presenting theory "AODV.A_Fresher"


12:07:19 Presenting theory "Flyspeck-Tame.Maps"


12:07:19 Presenting theory "HOL-Library.Code_Target_Int"


12:07:19 Presenting theory "HOL-Library.Code_Abstract_Nat"


12:07:20 Presenting theory "HOL-Library.Case_Converter"


12:07:20 Presenting file "~~/src/HOL/Library/case_converter.ML"


12:07:20 Presenting theory "HOL-Library.Code_Target_Nat"


12:07:20 Presenting theory "HOL-Library.Code_Target_Numeral"


12:07:20 Presenting theory "Flyspeck-Tame.Arch"


12:07:20 Presenting theory "Flyspeck-Tame.ArchCompAux"


12:07:20 Presenting theory "Flyspeck-Tame.ArchCompProps"


12:07:20 Presenting theory "Flyspeck-Tame.Relative_Completeness"


12:07:20 Presenting JinjaThreads in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads" ...


12:07:21 Presenting theory "AWN.Qmsg_Lifting"


12:07:21 Presenting theory "Category3.EquivalenceOfCategories"


12:07:21 Presenting theory "HOL-Library.Code_Lazy"


12:07:21 Presenting file "~~/src/HOL/Library/code_lazy.ML"


12:07:21 Presenting document JinjaThreads/document


12:07:21 Presenting document JinjaThreads/outline


12:07:21 Presenting theory "Category3.FreeCategory"


12:07:22 Presenting theory "Category3.DiscreteCategory"


12:07:22 Presenting theory "AODV.A_Seq_Invariants"


12:07:22 Presenting theory "ConcurrentGC.Global_Invariants_Lemmas"


12:07:22 Presenting theory "HOL-Library.Code_Test"


12:07:22 Presenting file "~~/src/HOL/Library/code_test.ML"


12:07:22 Presenting theory "HOL-Library.Combine_PER"


12:07:23 Presenting theory "ConcurrentGC.Local_Invariants_Lemmas"


12:07:23 Presenting theory "ConcurrentGC.Initial_Conditions"


12:07:24 Presenting theory "HOL-Library.Sublist"


12:07:24 Presenting theory "AODV.A_Quality_Increases"


12:07:24 Presenting theory "HOL-Library.Transitive_Closure_Table"


12:07:24 Presenting theory "AODV.A_OAodv"


12:07:24 Presenting theory "ConcurrentGC.Noninterference"


12:07:25 Presenting theory "HOL-Library.Predicate_Compile_Alternative_Defs"


12:07:25 Presenting theory "HOL-Library.Confluence"


12:07:26 Presenting theory "ConcurrentGC.Global_Noninterference"


12:07:26 Presenting theory "HOL-Library.Confluent_Quotient"


12:07:26 Presenting theory "HOL-Library.Dlist"


12:07:26 Presenting theory "JinjaThreads.Set_without_equal"


12:07:26 Presenting theory "ConcurrentGC.MarkObject"


12:07:27 Presenting theory "HOL-Library.Adhoc_Overloading"


12:07:27 Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"


12:07:27 Presenting theory "HOL-Library.Monad_Syntax"


12:07:27 Presenting theory "JinjaThreads.Set_Monad"


12:07:28 Presenting theory "ConcurrentGC.Phases"


12:07:28 Presenting theory "HOL-Library.Infinite_Set"


12:07:29 Presenting theory "HOL-Library.Complete_Partial_Order2"


12:07:29 Presenting theory "ConcurrentGC.StrongTricolour"


12:07:29 Presenting theory "ConcurrentGC.TSO"


12:07:30 Presenting theory "ConcurrentGC.Valid_Refs"


12:07:30 Presenting theory "HOL-Library.Conditional_Parametricity"


12:07:30 Presenting file "~~/src/HOL/Library/conditional_parametricity.ML"


12:07:30 Presenting theory "HOL-Library.Case_Converter"


12:07:30 Presenting file "~~/src/HOL/Library/case_converter.ML"


12:07:30 Presenting theory "HOL-Library.Confluence"


12:07:30 Presenting theory "ConcurrentGC.Worklists"


12:07:31 Presenting theory "ConcurrentGC.Proofs"


12:07:31 Presenting theory "ConcurrentGC.Concrete_heap"


12:07:31 Presenting theory "ConcurrentGC.Concrete"


12:07:31 Presenting theory "HOL-Library.Simps_Case_Conv"


12:07:31 Presenting file "~~/src/HOL/Library/simps_case_conv.ML"


12:07:31 Presenting Word_Lib in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib" ...


12:07:31 Presenting document Word_Lib/document


12:07:31 Presenting document Word_Lib/outline


12:07:31 Presenting theory "AWN.OClosed_Transfer"


12:07:31 Presenting theory "HOL-Library.Confluent_Quotient"


12:07:31 Presenting theory "Word_Lib.Enumeration"


12:07:31 Presenting theory "AWN.AWN_Main"


12:07:31 Presenting theory "Word_Lib.Even_More_List"


12:07:31 Presenting theory "HOL-Library.Phantom_Type"


12:07:32 Presenting theory "AODV.A_Global_Invariants"


12:07:32 Presenting theory "HOL-Library.Cardinality"


12:07:32 Presenting theory "AODV.A_Loop_Freedom"


12:07:33 Presenting theory "HOL-Library.Old_Datatype"


12:07:33 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"


12:07:33 Presenting theory "HOL-Library.Old_Datatype"


12:07:33 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"


12:07:33 Presenting theory "HOL-Library.Numeral_Type"


12:07:33 Presenting theory "HOL-Library.Type_Length"


12:07:33 Presenting theory "HOL-Library.Nat_Bijection"


12:07:33 Presenting theory "HOL-Library.Nat_Bijection"


12:07:34 Presenting theory "HOL-Library.Countable"


12:07:34 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"


12:07:34 Presenting theory "HOL-Library.Countable"


12:07:34 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"


12:07:34 Presenting theory "AWN.Toy"


12:07:35 Presenting theory "AODV.A_Aodv_Loop_Freedom"


12:07:35 Presenting theory "AODV.B_Fwdrreps"


12:07:35 Presenting theory "HOL-Library.Infinite_Set"


12:07:35 Presenting theory "AWN.AWN_Term_Graph"


12:07:35 Presenting theory "HOL-Library.Countable_Set"


12:07:35 Presenting IP_Addresses in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses" ...


12:07:35 Presenting document IP_Addresses/document


12:07:35 Presenting document IP_Addresses/outline


12:07:35 Presenting theory "HOL-Library.Cancellation"


12:07:35 Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"


12:07:35 Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"


12:07:35 Presenting theory "Bicategory.Strictness"


12:07:35 Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"


12:07:36 Presenting theory "HOL-Library.Countable_Complete_Lattices"


12:07:36 Presenting theory "HOL-Library.Countable_Set"


12:07:36 Presenting theory "HOL-Library.Countable_Complete_Lattices"


12:07:36 Presenting theory "HOL-Library.Order_Continuity"


12:07:37 Presenting theory "HOL-Library.Extended_Nat"


12:07:37 Presenting theory "HOL-Library.Countable_Set_Type"


12:07:37 Presenting theory "HOL-Library.Debug"


12:07:37 Presenting theory "HOL-Library.Diagonal_Subsequence"


12:07:38 Presenting theory "HOL-Library.Discrete"


12:07:38 Presenting theory "AODV.B_Aodv_Data"


12:07:38 Presenting theory "AODV.B_Aodv_Message"


12:07:40 Presenting theory "HOL-Library.FuncSet"


12:07:40 Presenting theory "HOL-Library.Word"


12:07:40 Presenting theory "AODV.B_Aodv"


12:07:40 Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"


12:07:40 Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"


12:07:40 Presenting theory "AODV.B_Aodv_Predicates"


12:07:40 Presenting theory "HOL-Library.Disjoint_Sets"


12:07:40 Presenting theory "Category3.Limit"


12:07:40 Presenting theory "Word_Lib.Legacy_Aliases"


12:07:41 Presenting theory "Word_Lib.More_Arithmetic"


12:07:41 Presenting theory "Word_Lib.More_Divides"


12:07:41 Presenting theory "Word_Lib.More_Misc"


12:07:41 Presenting theory "HOL-Library.Complete_Partial_Order2"


12:07:42 Presenting theory "HOL-Library.Multiset"


12:07:42 Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"


12:07:42 Presenting theory "HOL-ex.Quicksort"


12:07:43 Presenting theory "Category3.CategoryWithPullbacks"


12:07:43 Presenting theory "Coinductive.Coinductive_Nat"


12:07:43 Presenting theory "AODV.B_Fresher"


12:07:43 Presenting theory "HOL-Library.FSet"


12:07:43 Presenting theory "HOL-Library.Option_ord"


12:07:43 Presenting theory "HOL-Library.Sublist"


12:07:43 Presenting theory "Bicategory.InternalAdjunction"


12:07:43 Presenting theory "Word_Lib.More_Sublist"


12:07:44 Presenting theory "Word_Lib.More_Bit_Ring"


12:07:44 Presenting theory "HOL-Library.Infinite_Set"


12:07:47 Presenting theory "AODV.B_Seq_Invariants"


12:07:47 Presenting theory "Word_Lib.More_Word"


12:07:47 Presenting theory "HOL-Library.Finite_Map"


12:07:47 Presenting theory "Word_Lib.Strict_part_mono"


12:07:48 Presenting theory "HOL-Library.Disjoint_FSets"


12:07:48 Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"


12:07:48 Presenting theory "Word_Lib.Most_significant_bit"


12:07:48 Presenting theory "Category3.CartesianCategory"


12:07:48 Presenting theory "Word_Lib.Least_significant_bit"


12:07:48 Presenting theory "HOL-Library.Dlist"


12:07:48 Presenting theory "Word_Lib.Generic_set_bit"


12:07:48 Presenting theory "Word_Lib.Bit_Comprehension"


12:07:48 Presenting theory "HOL-Library.Dual_Ordered_Lattice"


12:07:48 Presenting theory "HOL.HOL"


12:07:49 Presenting file "~~/src/Tools/misc_legacy.ML"


12:07:49 Presenting file "~~/src/Tools/try.ML"


12:07:49 Presenting file "~~/src/Tools/quickcheck.ML"


12:07:49 Presenting file "~~/src/Tools/solve_direct.ML"


12:07:49 Presenting file "~~/src/Tools/IsaPlanner/zipper.ML"


12:07:49 Presenting file "~~/src/Tools/IsaPlanner/isand.ML"


12:07:49 Presenting file "~~/src/Tools/IsaPlanner/rw_inst.ML"


12:07:49 Presenting file "~~/src/Provers/hypsubst.ML"


12:07:49 Presenting file "~~/src/Provers/splitter.ML"


12:07:49 Presenting theory "AODV.B_Quality_Increases"


12:07:49 Presenting file "~~/src/Provers/classical.ML"


12:07:49 Presenting file "~~/src/Provers/blast.ML"


12:07:49 Presenting file "~~/src/Provers/clasimp.ML"


12:07:49 Presenting file "~~/src/Tools/eqsubst.ML"


12:07:49 Presenting file "~~/src/Provers/quantifier1.ML"


12:07:49 Presenting theory "Category3.CategoryWithFiniteLimits"


12:07:49 Presenting file "~~/src/Tools/atomize_elim.ML"


12:07:49 Presenting file "~~/src/Tools/cong_tac.ML"


12:07:49 Presenting theory "AODV.B_OAodv"


12:07:49 Presenting file "~~/src/Tools/intuitionistic.ML"


12:07:49 Presenting file "~~/src/Tools/project_rule.ML"


12:07:49 Presenting file "~~/src/Tools/subtyping.ML"


12:07:49 Presenting file "~~/src/Tools/case_product.ML"


12:07:49 Presenting file "~~/src/HOL/Tools/hologic.ML"


12:07:49 Presenting file "~~/src/HOL/Tools/rewrite_hol_proof.ML"


12:07:49 Presenting file "~~/src/HOL/Tools/simpdata.ML"


12:07:49 Presenting file "~~/src/Tools/induct.ML"


12:07:49 Presenting file "~~/src/Tools/induction.ML"


12:07:49 Presenting file "~~/src/Tools/induct_tacs.ML"


12:07:49 Presenting file "~~/src/Tools/coherent.ML"


12:07:49 Presenting file "~~/src/HOL/Tools/cnf.ML"


12:07:49 Presenting theory "HOL-Library.Equipollence"


12:07:50 Presenting theory "Category3.CartesianClosedCategory"


12:07:50 Presenting theory "HOL-Library.Simps_Case_Conv"


12:07:50 Presenting file "~~/src/HOL/Library/simps_case_conv.ML"


12:07:50 Presenting theory "Word_Lib.Bits_Int"


12:07:50 Presenting theory "HOL-Library.Extended"


12:07:52 Presenting theory "HOL-Library.Order_Continuity"


12:07:52 Presenting theory "HereditarilyFinite.HF"


12:07:52 Presenting theory "Automatic_Refinement.Misc"


12:07:52 Presenting theory "Word_Lib.Aligned"


12:07:52 Presenting theory "HOL-Library.Extended_Nat"


12:07:52 Presenting theory "IP_Addresses.NumberWang_IPv4"


12:07:52 Presenting theory "Word_Lib.Next_and_Prev"


12:07:53 Presenting theory "HOL-Library.Signed_Division"


12:07:53 Presenting theory "IP_Addresses.NumberWang_IPv6"


12:07:53 Presenting theory "Word_Lib.Signed_Division_Word"


12:07:54 Presenting theory "HOL-Library.Liminf_Limsup"


12:07:54 Presenting theory "Word_Lib.Many_More"


12:07:54 Presenting theory "IP_Addresses.WordInterval"


12:07:54 Presenting theory "Coinductive.Coinductive_List"


12:07:54 Presenting theory "Word_Lib.Singleton_Bit_Shifts"


12:07:54 Presenting theory "IP_Addresses.Hs_Compat"


12:07:54 Presenting theory "Word_Lib.Typedef_Morphisms"


12:07:54 Presenting theory "IP_Addresses.IP_Address"


12:07:54 Presenting theory "IP_Addresses.IPv4"


12:07:55 Presenting theory "AODV.B_Global_Invariants"


12:07:55 Presenting theory "AODV.B_Loop_Freedom"


12:07:56 Presenting theory "HOL.Orderings"


12:07:56 Presenting file "~~/src/Provers/order_procedure.ML"


12:07:56 Presenting file "~~/src/Provers/order_tac.ML"


12:07:57 Presenting theory "Word_Lib.Reversed_Bit_Lists"


12:07:57 Presenting theory "Coinductive.TLList"


12:07:58 Presenting theory "HOL.Groups"


12:07:58 Presenting file "~~/src/HOL/Tools/group_cancel.ML"


12:07:58 Presenting theory "AODV.B_Aodv_Loop_Freedom"


12:07:58 Presenting theory "IP_Addresses.IPv6"


12:07:58 Presenting theory "AODV.C_Gtobcast"


12:07:58 Presenting theory "Coinductive.Lazy_LList"


12:07:58 Presenting theory "Word_Lib.Bitwise"


12:07:58 Presenting theory "HOL-Library.Extended_Real"


12:07:58 Presenting theory "HOL.Lattices"


12:07:59 Presenting theory "Word_Lib.Bit_Comprehension_Int"


12:07:59 Presenting theory "Coinductive.Lazy_TLList"


12:07:59 Presenting theory "Word_Lib.Signed_Words"


12:07:59 Presenting theory "Word_Lib.Bitwise_Signed"


12:07:59 Presenting theory "IP_Addresses.Prefix_Match"


12:07:59 Presenting theory "HOL-Library.Cancellation"


12:07:59 Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"


12:07:59 Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"


12:07:59 Presenting theory "Word_Lib.Enumeration_Word"


12:07:59 Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"


12:07:59 Presenting theory "Word_Lib.Hex_Words"


12:07:59 Presenting theory "Word_Lib.Norm_Words"


12:07:59 Presenting theory "IP_Addresses.CIDR_Split"


12:07:59 Presenting theory "HOL.Boolean_Algebras"


12:07:59 Presenting file "~~/src/HOL/Tools/boolean_algebra_cancel.ML"


12:07:59 Presenting theory "Word_Lib.Rsplit"


12:07:59 Presenting theory "Word_Lib.Syntax_Bundles"


12:07:59 Presenting theory "HOL-Library.Product_Lexorder"


12:07:59 Presenting theory "IP_Addresses.WordInterval_Sorted"


12:07:59 Presenting theory "Word_Lib.Sgn_Abs"


12:07:59 Presenting theory "HOL-Library.Indicator_Function"


12:07:59 Presenting theory "Word_Lib.Type_Syntax"


12:07:59 Presenting theory "HOL-Library.Code_Abstract_Nat"


12:07:59 Presenting theory "HOL-Library.Code_Target_Nat"


12:08:00 Presenting theory "AODV.C_Aodv_Data"


12:08:00 Presenting theory "AODV.C_Aodv_Message"


12:08:01 Presenting theory "Category3.HF_SetCat"


12:08:01 Presenting theory "Category3.HF_SetCat_Interp"


12:08:01 Presenting theory "HOL-Cardinals.Fun_More"


12:08:02 Presenting theory "HOL.Set"


12:08:02 Presenting theory "AODV.C_Aodv"


12:08:02 Presenting theory "HOL-Library.Extended_Nonnegative_Real"


12:08:02 Presenting theory "AODV.C_Aodv_Predicates"


12:08:02 Presenting theory "HOL-Cardinals.Order_Relation_More"


12:08:03 Presenting theory "HOL-Cardinals.Wellfounded_More"


12:08:03 Presenting theory "HOL-Library.Log_Nat"


12:08:03 Presenting theory "HOL-Cardinals.Wellorder_Relation"


12:08:03 Presenting theory "HOL-Cardinals.Wellorder_Embedding"


12:08:04 Presenting theory "HOL-Library.Lattice_Algebras"


12:08:04 Presenting theory "HOL.Typedef"


12:08:04 Presenting file "~~/src/HOL/Tools/typedef.ML"


12:08:04 Presenting theory "HOL-Cardinals.Order_Union"


12:08:05 Presenting theory "HOL-Eisbach.Eisbach"


12:08:05 Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"


12:08:05 Presenting file "~~/src/HOL/Eisbach/method_closure.ML"


12:08:05 Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"


12:08:05 Presenting file "~~/src/HOL/Eisbach/match_method.ML"


12:08:05 Presenting theory "HOL-Eisbach.Eisbach_Tools"


12:08:05 Presenting theory "Word_Lib.Word_EqI"


12:08:05 Presenting theory "Word_Lib.Boolean_Inequalities"


12:08:06 Presenting theory "AODV.C_Fresher"


12:08:06 Presenting theory "HOL-Cardinals.Wellorder_Constructions"


12:08:06 Presenting theory "HOL-Library.Multiset"


12:08:06 Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"


12:08:07 Presenting theory "HOL-ex.Quicksort"


12:08:07 Presenting theory "HOL.Fun"


12:08:07 Presenting file "~~/src/HOL/Tools/functor.ML"


12:08:07 Presenting theory "HOL-Library.Float"


12:08:07 Presenting theory "HOL-Library.Option_ord"


12:08:07 Presenting theory "Word_Lib.Word_Lemmas"


12:08:07 Presenting theory "AODV.C_Seq_Invariants"


12:08:07 Presenting theory "IP_Addresses.IP_Address_Parser"


12:08:07 Presenting theory "HOL-Library.Function_Algebras"


12:08:07 Presenting theory "IP_Addresses.Lib_Numbers_toString"


12:08:08 Presenting theory "HOL-Library.Function_Division"


12:08:08 Presenting theory "HOL-Library.Fun_Lexorder"


12:08:08 Presenting theory "IP_Addresses.Lib_Word_toString"


12:08:08 Presenting theory "HOL-Library.Going_To_Filter"


12:08:08 Presenting theory "IP_Addresses.Lib_List_toString"


12:08:08 Presenting theory "Word_Lib.Word_8"


12:08:08 Presenting theory "Word_Lib.Word_16"


12:08:08 Presenting theory "Word_Lib.Word_Syntax"


12:08:08 Presenting theory "Word_Lib.Word_Names"


12:08:08 Presenting theory "IP_Addresses.IP_Address_toString"


12:08:08 Presenting theory "IP_Addresses.Prefix_Match_toString"


12:08:08 Presenting Simple_Firewall in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall" ...


12:08:08 Presenting document Simple_Firewall/document


12:08:08 Presenting document Simple_Firewall/outline


12:08:08 Presenting theory "Simple_Firewall.Lib_Enum_toString"


12:08:09 Presenting theory "Simple_Firewall.L4_Protocol"


12:08:09 Presenting theory "HOL-Library.Groups_Big_Fun"


12:08:09 Presenting theory "Simple_Firewall.Simple_Packet"


12:08:09 Presenting theory "Simple_Firewall.Firewall_Common_Decision_State"


12:08:09 Presenting theory "HOL-Library.Infinite_Typeclass"


12:08:09 Presenting theory "HOL-Library.Char_ord"


12:08:09 Presenting theory "HOL.Complete_Lattices"


12:08:09 Presenting theory "HOL-Library.Set_Algebras"


12:08:09 Presenting theory "HOL-Cardinals.Ordinal_Arithmetic"


12:08:09 Presenting theory "Word_Lib.More_Word_Operations"


12:08:09 Presenting theory "AODV.C_Quality_Increases"


12:08:09 Presenting theory "Word_Lib.Word_32"


12:08:09 Presenting theory "Simple_Firewall.Iface"


12:08:09 Presenting theory "Word_Lib.Word_Lib_Sumo"


12:08:09 Presenting theory "AODV.C_OAodv"


12:08:09 Presenting theory "Word_Lib.Machine_Word_32_Basics"


12:08:09 Presenting theory "Word_Lib.Machine_Word_32"


12:08:09 Presenting theory "Simple_Firewall.SimpleFw_Syntax"


12:08:09 Presenting theory "Word_Lib.Word_64"


12:08:09 Presenting theory "Word_Lib.Machine_Word_64_Basics"


12:08:09 Presenting theory "HOL-Library.Interval"


12:08:09 Presenting theory "Word_Lib.Machine_Word_64"


12:08:09 Presenting theory "Word_Lib.Guide"


12:08:10 Presenting theory "Bicategory.PseudonaturalTransformation"


12:08:10 Presenting theory "HOL-Library.Interval_Float"


12:08:10 Presenting theory "Simple_Firewall.SimpleFw_Semantics"


12:08:10 Presenting theory "HOL-Library.IArray"


12:08:10 Presenting theory "Simple_Firewall.List_Product_More"


12:08:10 Presenting theory "Word_Lib.Examples"


12:08:10 Presenting theory "Simple_Firewall.Option_Helpers"


12:08:10 Presenting Routing in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing" ...


12:08:10 Presenting document Routing/document


12:08:10 Presenting document Routing/outline


12:08:10 Presenting theory "Routing.Linorder_Helper"


12:08:10 Presenting theory "HOL-Eisbach.Eisbach"


12:08:10 Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"


12:08:10 Presenting file "~~/src/HOL/Eisbach/method_closure.ML"


12:08:10 Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"


12:08:10 Presenting file "~~/src/HOL/Eisbach/match_method.ML"


12:08:10 Presenting theory "HOL-Cardinals.Cardinal_Order_Relation"


12:08:11 Presenting theory "Simple_Firewall.Generic_SimpleFw"


12:08:11 Presenting theory "Pure-ex.Guess"


12:08:11 Presenting theory "Simple_Firewall.Shadowed"


12:08:11 Presenting theory "HOL-Cardinals.Cardinal_Arithmetic"


12:08:11 Presenting theory "Routing.Routing_Table"


12:08:11 Presenting theory "Simple_Firewall.IP_Partition_Preliminaries"


12:08:12 Presenting theory "HOL-Cardinals.Wellorder_Extension"


12:08:12 Presenting theory "HOL-Cardinals.Cardinals"


12:08:12 Presenting theory "Simple_Firewall.GroupF"


12:08:12 Presenting theory "ZFC_in_HOL.ZFC_Library"


12:08:12 Presenting theory "Simple_Firewall.IP_Addr_WordInterval_toString"


12:08:12 Presenting theory "HOL-Library.Adhoc_Overloading"


12:08:12 Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"


12:08:12 Presenting theory "HOL-Library.Monad_Syntax"


12:08:12 Presenting theory "Simple_Firewall.Primitives_toString"


12:08:12 Presenting theory "Routing.Linux_Router"


12:08:13 Presenting theory "Routing.IpRoute_Parser"


12:08:13 Presenting file "$AFP/Routing/IpRoute_Parser.ML"


12:08:13 Presenting Iptables_Semantics in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics" ...


12:08:13 Presenting theory "AODV.C_Global_Invariants"


12:08:13 Presenting document Iptables_Semantics/document


12:08:13 Presenting document Iptables_Semantics/outline


12:08:13 Presenting theory "Iptables_Semantics.List_Misc"


12:08:13 Presenting theory "ZFC_in_HOL.ZFC_in_HOL"


12:08:13 Presenting theory "Iptables_Semantics.Negation_Type"


12:08:13 Presenting theory "Iptables_Semantics.WordInterval_Lists"


12:08:13 Presenting theory "AODV.C_Loop_Freedom"


12:08:13 Presenting theory "Iptables_Semantics.Repeat_Stabilize"


12:08:13 Presenting theory "HOL-Library.Landau_Symbols"


12:08:13 Presenting theory "Iptables_Semantics.Firewall_Common"


12:08:13 Presenting theory "HOL-Library.LaTeXsugar"


12:08:14 Presenting theory "HOL-Library.Lattice_Constructions"


12:08:14 Presenting theory "Simple_Firewall.Service_Matrix"


12:08:14 Presenting theory "Simple_Firewall.SimpleFw_toString"


12:08:14 Presenting Iptables_Semantics_Examples in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples" ...


12:08:14 Presenting document Iptables_Semantics_Examples/document


12:08:14 Presenting document Iptables_Semantics_Examples/outline


12:08:15 Presenting theory "HOL.Ctr_Sugar"


12:08:15 Presenting file "~~/src/HOL/Tools/Ctr_Sugar/case_translation.ML"


12:08:15 Presenting theory "Automatic_Refinement.Misc"


12:08:15 Presenting theory "AODV.C_Aodv_Loop_Freedom"


12:08:15 Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML"


12:08:15 Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML"


12:08:15 Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML"


12:08:15 Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML"


12:08:15 Presenting theory "AODV.D_Fwdrreqs"


12:08:15 Presenting theory "HOL-Library.Stream"


12:08:15 Presenting file "~~/src/HOL/Tools/coinduction.ML"


12:08:15 Presenting theory "Iptables_Semantics.Semantics"


12:08:15 Presenting theory "Automatic_Refinement.Foldi"


12:08:16 Presenting theory "Iptables_Semantics.Matching"


12:08:17 Presenting theory "Iptables_Semantics.Ruleset_Update"


12:08:17 Presenting theory "ZFC_in_HOL.ZFC_Cardinals"


12:08:17 Presenting theory "HOL-Library.Sublist"


12:08:18 Presenting theory "Collections.SetIterator"


12:08:19 Presenting theory "Iptables_Semantics.Call_Return_Unfolding"


12:08:19 Presenting theory "AODV.D_Aodv_Data"


12:08:19 Presenting theory "Iptables_Semantics.Ternary"


12:08:19 Presenting theory "AODV.D_Aodv_Message"


12:08:19 Presenting theory "Iptables_Semantics_Examples.Parser_Test"


12:08:20 Presenting theory "Iptables_Semantics_Examples.Parser6_Test"


12:08:20 Presenting theory "Iptables_Semantics_Examples.Small_Examples"


12:08:20 Presenting theory "Iptables_Semantics_Examples.Ports_Fail"


12:08:20 Presenting theory "HOL-Library.Linear_Temporal_Logic_on_Streams"


12:08:20 Presenting theory "Iptables_Semantics_Examples.Contrived_Example"


12:08:20 Presenting theory "HOL-Library.ListVector"


12:08:20 Presenting theory "Collections.SetIteratorOperations"


12:08:20 Presenting theory "Iptables_Semantics_Examples.iptables_Ln_tuned_parsed"


12:08:20 Presenting theory "Automatic_Refinement.Refine_Util_Bootstrap1"


12:08:21 Presenting theory "Iptables_Semantics.Matching_Ternary"


12:08:21 Presenting theory "HOL-Library.Lub_Glb"


12:08:21 Presenting theory "Category3.ZFC_SetCat"


12:08:21 Presenting theory "AODV.D_Aodv"


12:08:21 Presenting theory "Automatic_Refinement.Mpat_Antiquot"


12:08:21 Presenting theory "AODV.D_Aodv_Predicates"


12:08:21 Presenting theory "Category3.ZFC_SetCat_Interp"


12:08:21 Presenting Iptables_Semantics_Examples_Big in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big" ...


12:08:21 Presenting document Iptables_Semantics_Examples_Big/document


12:08:21 Presenting document Iptables_Semantics_Examples_Big/outline


12:08:21 Presenting theory "Automatic_Refinement.Mk_Term_Antiquot"


12:08:21 Presenting theory "Iptables_Semantics_Examples.Analyze_Synology_Diskstation"


12:08:22 Presenting theory "Iptables_Semantics_Examples_Big.Analyze_topos_generated"


12:08:22 Presenting theory "Iptables_Semantics.Semantics_Ternary"


12:08:22 Presenting theory "Iptables_Semantics.Datatype_Selectors"


12:08:22 Presenting theory "Iptables_Semantics.IpAddresses"


12:08:23 Presenting theory "Iptables_Semantics.L4_Protocol_Flags"


12:08:23 Presenting theory "Iptables_Semantics.Ports"


12:08:23 Presenting theory "HOL-Library.Mapping"


12:08:23 Presenting theory "Iptables_Semantics.Conntrack_State"


12:08:23 Presenting theory "Iptables_Semantics.Tagged_Packet"


12:08:23 Presenting theory "HOL-Library.Monad_Syntax"


12:08:23 Presenting theory "Iptables_Semantics.Common_Primitive_Syntax"


12:08:23 Presenting theory "Iptables_Semantics.Unknown_Match_Tacs"


12:08:23 Presenting theory "Iptables_Semantics_Examples.Analyze_Ringofsaturn_com"


12:08:23 Presenting theory "Automatic_Refinement.Refine_Util"


12:08:23 Presenting theory "Automatic_Refinement.Attr_Comb"


12:08:23 Presenting theory "HOL-Library.More_List"


12:08:24 Presenting theory "Automatic_Refinement.Named_Sorted_Thms"


12:08:24 Presenting theory "Iptables_Semantics.Common_Primitive_Matcher_Generic"


12:08:24 Presenting theory "Automatic_Refinement.Prio_List"


12:08:24 Presenting theory "HOL-Library.Cancellation"


12:08:24 Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"


12:08:24 Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"


12:08:24 Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"


12:08:24 Presenting theory "Automatic_Refinement.Tagged_Solver"


12:08:25 Presenting theory "Iptables_Semantics.Common_Primitive_Matcher"


12:08:25 Presenting theory "AODV.D_Fresher"


12:08:25 Presenting theory "Iptables_Semantics.Example_Semantics"


12:08:25 Presenting theory "Automatic_Refinement.Anti_Unification"


12:08:25 Presenting theory "Automatic_Refinement.Indep_Vars"


12:08:25 Presenting theory "Automatic_Refinement.Select_Solve"


12:08:25 Presenting theory "Automatic_Refinement.Mk_Record_Simp"


12:08:26 Presenting theory "Automatic_Refinement.Refine_Lib"


12:08:26 Presenting file "$AFP/Automatic_Refinement/Lib/Cond_Rewr_Conv.ML"


12:08:26 Presenting file "$AFP/Automatic_Refinement/Lib/Revert_Abbrev.ML"


12:08:26 Presenting theory "Collections.Proper_Iterator"


12:08:27 Presenting theory "Iptables_Semantics.Alternative_Semantics"


12:08:27 Presenting theory "Collections.It_to_It"


12:08:27 Presenting theory "Iptables_Semantics.Semantics_Stateful"


12:08:28 Presenting theory "Collections.SetIteratorGA"


12:08:28 Presenting theory "AODV.D_Seq_Invariants"


12:08:28 Presenting theory "Refine_Monadic.Refine_Chapter"


12:08:29 Presenting theory "Automatic_Refinement.Autoref_Phases"


12:08:29 Presenting theory "Automatic_Refinement.Autoref_Data"


12:08:29 Presenting theory "Automatic_Refinement.Autoref_Tagging"


12:08:29 Presenting theory "Iptables_Semantics.Semantics_Goto"


12:08:30 Presenting theory "Iptables_Semantics.Negation_Type_DNF"


12:08:30 Presenting theory "AODV.D_Quality_Increases"


12:08:30 Presenting theory "Iptables_Semantics.Matching_Embeddings"


12:08:30 Presenting theory "AODV.D_OAodv"


12:08:30 Presenting theory "Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small"


12:08:31 Presenting theory "HOL-Library.Multiset"


12:08:31 Presenting theory "Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall"


12:08:31 Presenting theory "Iptables_Semantics_Examples.Analyze_SQRL_Shorewall"


12:08:31 Presenting theory "Automatic_Refinement.Relators"


12:08:31 Presenting theory "Iptables_Semantics_Examples.SQRL_2015_nospoof"


12:08:31 Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"


12:08:31 Presenting theory "Iptables_Semantics.Fixed_Action"


12:08:31 Presenting theory "Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing"


12:08:31 Presenting theory "Automatic_Refinement.Param_Tool"


12:08:31 Presenting theory "Iptables_Semantics_Examples_Big.Analyze_Containern"


12:08:31 Presenting theory "Iptables_Semantics.Normalized_Matches"


12:08:32 Presenting theory "HOL.Inductive"


12:08:32 Presenting file "~~/src/HOL/Tools/inductive.ML"


12:08:32 Presenting theory "Iptables_Semantics.Negation_Type_Matching"


12:08:32 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML"


12:08:32 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML"


12:08:32 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_data.ML"


12:08:32 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML"


12:08:32 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML"


12:08:32 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML"


12:08:32 Presenting theory "Iptables_Semantics_Examples.Analyze_medium_sized_company"


12:08:32 Presenting file "~~/src/HOL/Tools/Old_Datatype/old_primrec.ML"


12:08:32 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML"


12:08:32 Presenting theory "HOL-Library.Multiset_Order"


12:08:32 Presenting theory "Automatic_Refinement.Param_HOL"


12:08:32 Presenting theory "Automatic_Refinement.Parametricity"


12:08:32 Presenting theory "HOL-Library.NList"


12:08:32 Presenting theory "HOL-Library.Nonpos_Ints"


12:08:33 Presenting theory "HOL-Library.Numeral_Type"


12:08:33 Presenting theory "Automatic_Refinement.Autoref_Id_Ops"


12:08:33 Presenting theory "Iptables_Semantics.Primitive_Normalization"


12:08:33 Presenting theory "Iptables_Semantics.MatchExpr_Fold"


12:08:34 Presenting theory "Iptables_Semantics.Common_Primitive_Lemmas"


12:08:34 Presenting theory "HOL-Library.Omega_Words_Fun"


12:08:34 Presenting theory "Iptables_Semantics_Examples_Big.TUM_Spoofing_new3"


12:08:34 Presenting theory "AODV.D_Global_Invariants"


12:08:34 Presenting theory "Automatic_Refinement.Autoref_Fix_Rel"


12:08:34 Presenting theory "HOL-Library.Open_State_Syntax"


12:08:34 Presenting theory "Automatic_Refinement.Autoref_Translate"


12:08:34 Presenting theory "Automatic_Refinement.Autoref_Gen_Algo"


12:08:34 Presenting theory "Bicategory.EquivalenceOfBicategories"


12:08:34 Presenting theory "Automatic_Refinement.Autoref_Relator_Interface"


12:08:34 Presenting theory "AODV.D_Loop_Freedom"


12:08:34 Presenting theory "HOL-Library.Option_ord"


12:08:34 Presenting theory "Automatic_Refinement.Autoref_Tool"


12:08:34 Presenting theory "HOL-Library.Parallel"


12:08:35 Presenting theory "HOL-Library.Pattern_Aliases"


12:08:35 Presenting theory "HOL-Library.Periodic_Fun"


12:08:35 Presenting theory "Automatic_Refinement.Autoref_Bindings_HOL"


12:08:35 Presenting theory "Iptables_Semantics.Ports_Normalize"


12:08:35 Presenting theory "Iptables_Semantics_Examples_Big.TUM_Simple_FW"


12:08:35 Presenting theory "Automatic_Refinement.Automatic_Refinement"


12:08:35 Presenting theory "HOL.Product_Type"


12:08:35 Presenting theory "Refine_Monadic.Refine_Mono_Prover"


12:08:35 Presenting file "$AFP/Refine_Monadic/refine_mono_prover.ML"


12:08:35 Presenting file "~~/src/HOL/Tools/split_rule.ML"


12:08:35 Presenting theory "Iptables_Semantics.IpAddresses_Normalize"


12:08:35 Presenting file "~~/src/HOL/Tools/set_comprehension_pointfree.ML"


12:08:35 Presenting file "~~/src/HOL/Tools/inductive_set.ML"


12:08:35 Presenting theory "AODV.D_Aodv_Loop_Freedom"


12:08:35 Presenting theory "Refine_Monadic.Refine_Misc"


12:08:35 Presenting theory "AODV.E_All_ABCD"


12:08:35 Presenting theory "Iptables_Semantics.Interfaces_Normalize"


12:08:35 Presenting theory "HOL.Sum_Type"


12:08:35 Presenting theory "Iptables_Semantics.Word_Upto"


12:08:36 Presenting theory "Refine_Monadic.RefineG_Transfer"


12:08:36 Presenting theory "HOL-Library.Poly_Mapping"


12:08:36 Presenting theory "Refine_Monadic.RefineG_Domain"


12:08:36 Presenting theory "HOL-Library.Power_By_Squaring"


12:08:36 Presenting theory "Iptables_Semantics.Protocols_Normalize"


12:08:36 Presenting theory "Iptables_Semantics.Remdups_Rev"


12:08:36 Presenting theory "HOL-Library.Preorder"


12:08:36 Presenting file "~~/src/Provers/preorder.ML"


12:08:36 Presenting theory "Refine_Monadic.RefineG_Recursion"


12:08:36 Presenting theory "HOL-Library.Product_Plus"


12:08:36 Presenting theory "Refine_Monadic.RefineG_Assert"


12:08:36 Presenting theory "HOL-Library.Quadratic_Discriminant"


12:08:36 Presenting theory "HOL-Library.Quotient_Syntax"


12:08:37 Presenting theory "HOL-Library.Quotient_Set"


12:08:37 Presenting theory "AODV.E_Aodv_Data"


12:08:37 Presenting theory "Iptables_Semantics.Ipassmt"


12:08:37 Presenting theory "HOL-Library.Quotient_Product"


12:08:37 Presenting theory "AODV.E_Aodv_Message"


12:08:37 Presenting theory "HOL-Library.Quotient_Option"


12:08:37 Presenting theory "HOL.Rings"


12:08:37 Presenting file "~~/src/HOL/Tools/arith_data.ML"


12:08:37 Presenting file "~~/src/Provers/Arith/cancel_div_mod.ML"


12:08:37 Presenting theory "HOL-Library.Quotient_List"


12:08:37 Presenting theory "Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large"


12:08:37 Presenting theory "HOL-Library.Quotient_Sum"


12:08:37 Presenting theory "HOL-Library.Quotient_Type"


12:08:37 Presenting theory "AODV.E_Aodv"


12:08:37 Presenting theory "AODV.E_Aodv_Predicates"


12:08:37 Presenting theory "Iptables_Semantics.No_Spoof"


12:08:38 Presenting theory "Refine_Monadic.Refine_Basic"


12:08:38 Presenting theory "Iptables_Semantics.Common_Primitive_toString"


12:08:38 Presenting theory "Iptables_Semantics.Routing_IpAssmt"


12:08:38 Presenting theory "Iptables_Semantics.Output_Interface_Replace"


12:08:38 Presenting theory "HOL-Library.Ramsey"


12:08:38 Presenting theory "HOL.Nat"


12:08:38 Presenting theory "Refine_Monadic.Refine_Leof"


12:08:38 Presenting file "~~/src/HOL/Tools/nat_arith.ML"


12:08:38 Presenting theory "Refine_Monadic.Refine_Heuristics"


12:08:38 Presenting theory "Refine_Monadic.Refine_More_Comb"


12:08:38 Presenting theory "HOL-Library.Reflection"


12:08:38 Presenting file "~~/src/HOL/Tools/reflection.ML"


12:08:38 Presenting theory "Iptables_Semantics.Interface_Replace"


12:08:38 Presenting theory "AODV.E_Fresher"


12:08:39 Presenting theory "Iptables_Semantics.Optimizing"


12:08:39 Presenting theory "Bicategory.SpanBicategory"


12:08:39 Presenting theory "HOL-Library.While_Combinator"


12:08:39 Presenting theory "Refine_Monadic.RefineG_While"


12:08:39 Presenting theory "HOL-Library.Rewrite"


12:08:39 Presenting file "~~/src/HOL/Library/cconv.ML"


12:08:39 Presenting file "~~/src/HOL/Library/rewrite.ML"


12:08:39 Presenting theory "HOL-Library.Type_Length"


12:08:39 Presenting theory "HOL-Library.Saturated"


12:08:39 Presenting theory "AODV.E_Seq_Invariants"


12:08:40 Presenting theory "HOL-Library.Set_Idioms"


12:08:40 Presenting theory "HOL-Library.Signed_Division"


12:08:40 Presenting theory "Refine_Monadic.Refine_While"


12:08:40 Presenting theory "HOL-Library.State_Monad"


12:08:40 Presenting theory "HOL.Fields"


12:08:40 Presenting theory "HOL-Library.Comparator"


12:08:40 Presenting theory "Iptables_Semantics.Transform"


12:08:40 Presenting file "~~/src/Provers/Arith/fast_lin_arith.ML"


12:08:40 Presenting theory "AODV.E_Quality_Increases"


12:08:40 Presenting file "~~/src/HOL/Tools/lin_arith.ML"


12:08:40 Presenting theory "AODV.E_OAodv"


12:08:40 Presenting theory "Refine_Monadic.Refine_Det"


12:08:40 Presenting theory "HOL-Library.Sorting_Algorithms"


12:08:40 Presenting theory "Iptables_Semantics.Conntrack_State_Transform"


12:08:40 Presenting theory "Refine_Monadic.Refine_Pfun"


12:08:41 Presenting theory "Refine_Monadic.Refine_Transfer"


12:08:41 Presenting theory "Iptables_Semantics.Primitive_Abstract"


12:08:41 Presenting theory "HOL.Relation"


12:08:42 Presenting theory "Iptables_Semantics.SimpleFw_Compliance"


12:08:42 Presenting theory "HOL-Library.Sum_of_Squares"


12:08:42 Presenting file "~~/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML"


12:08:42 Presenting file "~~/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML"


12:08:42 Presenting file "~~/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML"


12:08:42 Presenting file "~~/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML"


12:08:42 Presenting theory "Iptables_Semantics.Semantics_Embeddings"


12:08:42 Presenting theory "AODV.E_Global_Invariants"


12:08:42 Presenting theory "Iptables_Semantics.Iptables_Semantics"


12:08:42 Presenting theory "Refine_Monadic.Refine_Foreach"


12:08:42 Presenting theory "HOL-Library.Transitive_Closure_Table"


12:08:42 Presenting theory "HOL-Library.Code_Target_Int"


12:08:42 Presenting theory "Native_Word.Code_Int_Integer_Conversion"


12:08:42 Presenting theory "Native_Word.Code_Target_Integer_Bit"


12:08:42 Presenting theory "HOL-Library.Tree"


12:08:42 Presenting theory "Native_Word.Code_Target_Int_Bit"


12:08:42 Presenting theory "AODV.E_Loop_Freedom"


12:08:42 Presenting theory "HOL-Library.Tree_Multiset"


12:08:42 Presenting theory "HOL.Finite_Set"


12:08:42 Presenting theory "Iptables_Semantics.Code_Interface"


12:08:42 Presenting theory "HOL-Library.Tree_Real"


12:08:43 Presenting theory "Refine_Monadic.Refine_Automation"


12:08:43 Presenting theory "Bicategory.Tabulation"


12:08:43 Presenting theory "Refine_Monadic.Autoref_Monadic"


12:08:43 Presenting theory "HOL-Library.Uprod"


12:08:43 Presenting theory "Refine_Monadic.Refine_Monadic"


12:08:43 Presenting theory "AODV.E_Aodv_Loop_Freedom"


12:08:43 Presenting theory "Collections.Gen_Iterator"


12:08:43 Presenting theory "AODV.All"


12:08:43 Presenting theory "Collections.Idx_Iterator"


12:08:43 Presenting theory "Collections.Iterator"


12:08:43 Presenting theory "Iptables_Semantics.Parser6"


12:08:43 Presenting theory "Collections.ICF_Tools"


12:08:43 Presenting theory "Iptables_Semantics.No_Spoof_Embeddings"


12:08:44 Presenting theory "Collections.Ord_Code_Preproc"


12:08:44 Presenting theory "HOL.Transitive_Closure"


12:08:44 Presenting theory "Collections.Record_Intf"


12:08:44 Presenting file "~~/src/Provers/trancl.ML"


12:08:44 Presenting theory "Collections.Locale_Code"


12:08:44 Presenting theory "Collections.ICF_Spec_Base"


12:08:44 Presenting theory "HOL.Wellfounded"


12:08:44 Presenting theory "Iptables_Semantics.Parser"


12:08:44 Presenting theory "Iptables_Semantics.Code_haskell"


12:08:45 Presenting theory "Iptables_Semantics.Access_Matrix_Embeddings"


12:08:45 Presenting theory "HOL.Wfrec"


12:08:45 Presenting theory "Collections.SetSpec"


12:08:45 Presenting theory "Iptables_Semantics.Documentation"


12:08:45 Presenting theory "HOL.Order_Relation"


12:08:45 Presenting theory "HOL-Library.Word"


12:08:45 Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"


12:08:45 Presenting theory "Collections.MapSpec"


12:08:45 Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"


12:08:45 Presenting theory "HOL.Hilbert_Choice"


12:08:45 Presenting theory "Collections.ListSpec"


12:08:45 Presenting file "~~/src/HOL/Tools/choice_specification.ML"


12:08:45 Presenting theory "HOL-Library.Z2"


12:08:45 Presenting theory "HOL-Library.Library"


12:08:45 Presenting theory "HOL-Library.Product_Order"


12:08:45 Presenting theory "Collections.AnnotatedListSpec"


12:08:46 Presenting theory "Collections.PrioSpec"


12:08:46 Presenting theory "HOL-Library.Finite_Lattice"


12:08:46 Presenting theory "Collections.PrioUniqueSpec"


12:08:46 Presenting theory "HOL-Library.List_Lexorder"


12:08:46 Presenting theory "HOL-Library.List_Lenlexorder"


12:08:46 Presenting theory "HOL-Library.Prefix_Order"


12:08:46 Presenting theory "Collections.Algos"


12:08:46 Presenting theory "HOL.Zorn"


12:08:46 Presenting theory "HOL-Library.Product_Lexorder"


12:08:46 Presenting theory "HOL-Library.Subseq_Order"


12:08:46 Presenting theory "Collections.SetIndex"


12:08:46 Presenting theory "HOL-Library.Datatype_Records"


12:08:46 Presenting file "~~/src/HOL/Library/datatype_records.ML"


12:08:46 Presenting theory "Collections.SetIteratorCollectionsGA"


12:08:46 Presenting theory "HOL.BNF_Wellorder_Relation"


12:08:46 Presenting theory "HOL-Library.AList_Mapping"


12:08:46 Presenting theory "HOL-Library.Code_Abstract_Char"


12:08:46 Presenting theory "HOL-Library.Code_Abstract_Nat"


12:08:46 Presenting theory "HOL-Library.Code_Binary_Nat"


12:08:46 Presenting theory "Collections.SetGA"


12:08:46 Presenting theory "Collections.Dlist_add"


12:08:46 Presenting theory "Collections.ListSetImpl"


12:08:46 Presenting theory "Collections.ListSetImpl_Invar"


12:08:46 Presenting theory "HOL.BNF_Wellorder_Embedding"


12:08:47 Presenting theory "Collections.ListSetImpl_NotDist"


12:08:47 Presenting theory "Collections.Sorted_List_Operations"


12:08:47 Presenting theory "HOL-Library.Code_Prolog"


12:08:47 Presenting file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"


12:08:47 Presenting theory "Collections.ListSetImpl_Sorted"


12:08:47 Presenting theory "HOL-Library.Code_Target_Int"


12:08:47 Presenting theory "HOL-Library.Code_Real_Approx_By_Float"


12:08:47 Presenting theory "HOL-Library.Code_Target_Nat"


12:08:47 Presenting theory "HOL-Library.Code_Target_Numeral"


12:08:47 Presenting theory "HOL-Library.Code_Target_Numeral_Float"


12:08:47 Presenting theory "HOL-Library.Complex_Order"


12:08:47 Presenting theory "HOL-Library.DAList"


12:08:47 Presenting theory "HOL-Library.DAList_Multiset"


12:08:47 Presenting theory "HOL.BNF_Wellorder_Constructions"


12:08:48 Presenting theory "HOL.BNF_Cardinal_Order_Relation"


12:08:49 Presenting theory "HOL-Library.RBT_Impl"


12:08:49 Presenting theory "HOL.BNF_Cardinal_Arithmetic"


12:08:49 Presenting theory "Bicategory.BicategoryOfSpans"


12:08:49 Presenting theory "HOL-Library.RBT_Impl"


12:08:49 Presenting theory "HOL.Fun_Def_Base"


12:08:49 Presenting file "~~/src/HOL/Tools/Function/function_lib.ML"


12:08:49 Presenting file "~~/src/HOL/Tools/Function/function_common.ML"


12:08:49 Presenting file "~~/src/HOL/Tools/Function/function_context_tree.ML"


12:08:49 Presenting file "~~/src/HOL/Tools/Function/sum_tree.ML"


12:08:49 Presenting theory "Collections.RBT_add"


12:08:49 Presenting theory "HOL-Library.RBT"


12:08:50 Presenting theory "HOL-Library.RBT"


12:08:50 Presenting theory "Collections.MapGA"


12:08:50 Presenting theory "HOL-Library.RBT_Mapping"


12:08:50 Presenting theory "Collections.RBTMapImpl"


12:08:50 Presenting theory "Collections.SetByMap"


12:08:50 Presenting theory "Collections.RBTSetImpl"


12:08:50 Presenting theory "HOL-Library.RBT_Set"


12:08:50 Presenting theory "HOL-Library.LaTeXsugar"


12:08:50 Presenting theory "HOL-Library.OptionalSugar"


12:08:50 Presenting theory "HOL-Library.Predicate_Compile_Alternative_Defs"


12:08:50 Presenting theory "HOL-Library.AList"


12:08:50 Presenting theory "HOL-Library.Predicate_Compile_Quickcheck"


12:08:50 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"


12:08:51 Presenting theory "Collections.Assoc_List"


12:08:51 Presenting theory "Collections.ListMapImpl"


12:08:51 Presenting theory "HOL-Library.Phantom_Type"


12:08:51 Presenting theory "HOL-Library.Cardinality"


12:08:51 Presenting theory "HOL-Library.Numeral_Type"


12:08:51 Presenting theory "HOL-Library.Type_Length"


12:08:51 Presenting theory "HOL.BNF_Def"


12:08:51 Presenting file "~~/src/HOL/Tools/BNF/bnf_util.ML"


12:08:51 Presenting file "~~/src/HOL/Tools/BNF/bnf_tactics.ML"


12:08:51 Presenting file "~~/src/HOL/Tools/BNF/bnf_def_tactics.ML"


12:08:51 Presenting file "~~/src/HOL/Tools/BNF/bnf_def.ML"


12:08:52 Presenting theory "HOL-Library.Old_Recdef"


12:08:52 Presenting file "~~/src/HOL/Library/old_recdef.ML"


12:08:52 Presenting theory "Bicategory.Modification"


12:08:53 Presenting theory "HOL-Library.Realizers"


12:08:53 Presenting file "~~/src/HOL/Tools/datatype_realizer.ML"


12:08:53 Presenting file "~~/src/HOL/Tools/inductive_realizer.ML"


12:08:53 Presenting theory "HOL.BNF_Composition"


12:08:53 Presenting file "~~/src/HOL/Tools/BNF/bnf_comp_tactics.ML"


12:08:53 Presenting file "~~/src/HOL/Tools/BNF/bnf_comp.ML"


12:08:53 Presenting theory "HOL-Library.Word"


12:08:53 Presenting theory "HOL.Basic_BNFs"


12:08:53 Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"


12:08:53 Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"


12:08:53 Presenting theory "Word_Lib.More_Arithmetic"


12:08:53 Presenting theory "Word_Lib.More_Divides"


12:08:53 Presenting theory "Word_Lib.More_Bit_Ring"


12:08:54 Presenting theory "Bicategory.ConcreteBicategory"


12:08:54 Presenting theory "HOL-Library.Refute"


12:08:54 Presenting file "~~/src/HOL/Library/refute.ML"


12:08:54 Presenting theory "Word_Lib.More_Word"


12:08:54 Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"


12:08:54 Presenting theory "Word_Lib.Most_significant_bit"


12:08:54 Presenting theory "Word_Lib.Least_significant_bit"


12:08:55 Presenting theory "Word_Lib.Generic_set_bit"


12:08:55 Presenting theory "Word_Lib.Bit_Comprehension"


12:08:55 Presenting theory "HOL-Library.Signed_Division"


12:08:55 Presenting theory "Word_Lib.Signed_Division_Word"


12:08:55 Presenting theory "Native_Word.Code_Target_Word_Base"


12:08:55 Presenting theory "Native_Word.Word_Type_Copies"


12:08:55 Presenting theory "Native_Word.Code_Int_Integer_Conversion"


12:08:55 Presenting theory "Native_Word.Code_Target_Integer_Bit"


12:08:55 Presenting theory "Native_Word.Uint32"


12:08:55 Presenting theory "Collections.HashCode"


12:08:56 Presenting theory "HOL-Library.Code_Target_Int"


12:08:56 Presenting theory "HOL-Library.Code_Abstract_Nat"


12:08:56 Presenting theory "HOL-Library.Code_Target_Nat"


12:08:56 Presenting theory "HOL-Library.Code_Target_Numeral"


12:08:56 Presenting theory "Bicategory.CatBicat"


12:08:56 Presenting theory "Native_Word.Code_Target_Int_Bit"


12:08:56 Presenting theory "Collections.Code_Target_ICF"


12:08:56 Presenting theory "Collections.HashMap_Impl"


12:08:56 Presenting theory "Collections.HashMap"


12:08:56 Presenting theory "Collections.HashSet"


12:08:56 Presenting theory "Trie.Trie"


12:08:56 Presenting theory "Collections.Trie_Impl"


12:08:56 Presenting theory "Collections.Trie2"


12:08:56 Presenting theory "Collections.TrieMapImpl"


12:08:56 Presenting theory "Collections.TrieSetImpl"


12:08:56 Presenting theory "Collections.Diff_Array"


12:08:56 Presenting theory "HOL.BNF_Fixpoint_Base"


12:08:56 Presenting theory "Collections.ListGA"


12:08:56 Presenting theory "Collections.Array_Iterator"


12:08:56 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_util_tactics.ML"


12:08:56 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_util.ML"


12:08:56 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML"


12:08:56 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML"


12:08:56 Presenting theory "Collections.ArrayHashMap_Impl"


12:08:57 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML"


12:08:57 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m.ML"


12:08:57 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML"


12:08:57 Presenting theory "Collections.ArrayHashMap"


12:08:57 Presenting theory "Collections.ArrayHashSet"


12:08:57 Presenting theory "Collections.ArrayMapImpl"


12:08:57 Presenting theory "Collections.ArraySetImpl"


12:08:57 Presenting theory "Collections.SetStdImpl"


12:08:57 Presenting theory "Collections.ListMapImpl_Invar"


12:08:57 Presenting theory "Collections.MapStdImpl"


12:08:57 Presenting theory "Collections.Fifo"


12:08:57 Presenting theory "Binomial-Heaps.BinomialHeap"


12:08:57 Presenting theory "Collections.BinoPrioImpl"


12:08:58 Presenting theory "HOL.BNF_Least_Fixpoint"


12:08:58 Presenting theory "Binomial-Heaps.SkewBinomialHeap"


12:08:58 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_util.ML"


12:08:58 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_tactics.ML"


12:08:58 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp.ML"


12:08:58 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_compat.ML"


12:08:58 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML"


12:08:58 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_size.ML"


12:08:58 Presenting file "~~/src/HOL/Tools/datatype_simprocs.ML"


12:08:58 Presenting theory "Collections.SkewPrioImpl"


12:08:58 Presenting theory "HOL.Equiv_Relations"


12:08:58 Presenting theory "HOL.Basic_BNF_LFPs"


12:08:58 Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML"


12:08:59 Presenting theory "HOL.Meson"


12:08:59 Presenting file "~~/src/HOL/Tools/Meson/meson.ML"


12:08:59 Presenting file "~~/src/HOL/Tools/Meson/meson_clausify.ML"


12:08:59 Presenting file "~~/src/HOL/Tools/Meson/meson_tactic.ML"


12:08:59 Presenting theory "Finger-Trees.FingerTree"


12:08:59 Presenting theory "Collections.FTAnnotatedListImpl"


12:08:59 Presenting theory "Collections.PrioByAnnotatedList"


12:08:59 Presenting theory "Collections.FTPrioImpl"


12:09:00 Presenting theory "Collections.PrioUniqueByAnnotatedList"


12:09:00 Presenting theory "Collections.FTPrioUniqueImpl"


12:09:00 Presenting theory "Collections.ICF_Impl"


12:09:00 Presenting theory "Collections.ICF_Refine_Monadic"


12:09:00 Presenting theory "Collections.Intf_Set"


12:09:00 Presenting theory "Collections.Intf_Map"


12:09:00 Presenting theory "Collections.ICF_Autoref"


12:09:01 Presenting theory "Collections.DatRef"


12:09:01 Presenting theory "Collections.Collections"


12:09:01 Presenting theory "Collections.CollectionsV1"


12:09:01 Presenting theory "JinjaThreads.JT_ICF"


12:09:01 Presenting theory "HOL.ATP"


12:09:01 Presenting theory "FinFun.FinFun"


12:09:01 Presenting file "~~/src/HOL/Tools/ATP/atp_util.ML"


12:09:01 Presenting file "~~/src/HOL/Tools/ATP/atp_problem.ML"


12:09:01 Presenting file "~~/src/HOL/Tools/ATP/atp_proof.ML"


12:09:01 Presenting file "~~/src/HOL/Tools/ATP/atp_proof_redirect.ML"


12:09:01 Presenting file "~~/src/HOL/Tools/lambda_lifting.ML"


12:09:01 Presenting file "~~/src/HOL/Tools/monomorph.ML"


12:09:01 Presenting file "~~/src/HOL/Tools/ATP/atp_problem_generate.ML"


12:09:01 Presenting file "~~/src/HOL/Tools/ATP/atp_proof_reconstruct.ML"


12:09:01 Presenting theory "JinjaThreads.Auxiliary"


12:09:01 Presenting theory "JinjaThreads.Basic_Main"


12:09:02 Presenting theory "JinjaThreads.FWState"


12:09:02 Presenting theory "JinjaThreads.FWLock"


12:09:02 Presenting theory "JinjaThreads.FWLocking"


12:09:02 Presenting theory "JinjaThreads.FWThread"


12:09:02 Presenting theory "JinjaThreads.FWWait"


12:09:02 Presenting theory "JinjaThreads.FWCondAction"


12:09:02 Presenting theory "JinjaThreads.FWWellform"


12:09:02 Presenting theory "JinjaThreads.FWLockingThread"


12:09:02 Presenting theory "JinjaThreads.FWInterrupt"


12:09:03 Presenting theory "JinjaThreads.FWSemantics"


12:09:03 Presenting theory "JinjaThreads.FWProgressAux"


12:09:04 Presenting theory "JinjaThreads.FWDeadlock"


12:09:04 Presenting theory "JinjaThreads.FWProgress"


12:09:04 Presenting theory "HOL.Metis"


12:09:04 Presenting file "~~/src/Tools/Metis/metis.ML"


12:09:04 Presenting theory "JinjaThreads.FWLifting"


12:09:05 Presenting file "~~/src/HOL/Tools/Metis/metis_generate.ML"


12:09:05 Presenting file "~~/src/HOL/Tools/Metis/metis_reconstruct.ML"


12:09:05 Presenting theory "JinjaThreads.LTS"


12:09:05 Presenting file "~~/src/HOL/Tools/Metis/metis_tactic.ML"


12:09:05 Presenting theory "HOL.Transfer"


12:09:05 Presenting file "~~/src/HOL/Tools/Transfer/transfer.ML"


12:09:05 Presenting file "~~/src/HOL/Tools/Transfer/transfer_bnf.ML"


12:09:05 Presenting theory "JinjaThreads.FWLTS"


12:09:05 Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML"


12:09:06 Presenting theory "JinjaThreads.Bisimulation"


12:09:06 Presenting theory "HOL.Lifting"


12:09:06 Presenting file "~~/src/HOL/Tools/Lifting/lifting_util.ML"


12:09:06 Presenting file "~~/src/HOL/Tools/Lifting/lifting_info.ML"


12:09:06 Presenting file "~~/src/HOL/Tools/Lifting/lifting_bnf.ML"


12:09:06 Presenting file "~~/src/HOL/Tools/Lifting/lifting_term.ML"


12:09:06 Presenting file "~~/src/HOL/Tools/Lifting/lifting_def.ML"


12:09:06 Presenting file "~~/src/HOL/Tools/Lifting/lifting_setup.ML"


12:09:06 Presenting file "~~/src/HOL/Tools/Lifting/lifting_def_code_dt.ML"


12:09:07 Presenting theory "JinjaThreads.FWBisimulation"


12:09:07 Presenting theory "HOL.Quotient"


12:09:07 Presenting file "~~/src/HOL/Tools/Quotient/quotient_info.ML"


12:09:07 Presenting file "~~/src/HOL/Tools/Quotient/quotient_term.ML"


12:09:07 Presenting file "~~/src/HOL/Tools/Quotient/quotient_type.ML"


12:09:07 Presenting file "~~/src/HOL/Tools/Quotient/quotient_def.ML"


12:09:08 Presenting file "~~/src/HOL/Tools/Quotient/quotient_tacs.ML"


12:09:08 Presenting file "~~/src/HOL/Tools/BNF/bnf_lift.ML"


12:09:08 Presenting theory "JinjaThreads.FWBisimDeadlock"


12:09:08 Presenting theory "HOL.Num"


12:09:08 Presenting file "~~/src/HOL/Tools/numeral.ML"


12:09:08 Presenting theory "JinjaThreads.FWLiftingSem"


12:09:08 Presenting theory "HOL.Power"


12:09:08 Presenting theory "JinjaThreads.FWInitFinLift"


12:09:08 Presenting theory "JinjaThreads.FWBisimLift"


12:09:09 Presenting theory "JinjaThreads.Semilat"


12:09:09 Presenting theory "HOL.Groups_Big"


12:09:09 Presenting theory "JinjaThreads.Err"


12:09:09 Presenting theory "JinjaThreads.Opt"


12:09:09 Presenting theory "JinjaThreads.Product"


12:09:09 Presenting theory "HOL.Complete_Partial_Order"


12:09:09 Presenting theory "JinjaThreads.Listn"


12:09:09 Presenting theory "JinjaThreads.Semilattices"


12:09:09 Presenting theory "JinjaThreads.Typing_Framework"


12:09:09 Presenting theory "HOL.Option"


12:09:09 Presenting theory "JinjaThreads.SemilatAlg"


12:09:09 Presenting theory "JinjaThreads.Typing_Framework_err"


12:09:09 Presenting theory "HOL.Partial_Function"


12:09:09 Presenting theory "JinjaThreads.Kildall"


12:09:09 Presenting file "~~/src/HOL/Tools/Function/partial_function.ML"


12:09:09 Presenting theory "JinjaThreads.LBVSpec"


12:09:09 Presenting theory "JinjaThreads.LBVCorrect"


12:09:10 Presenting theory "JinjaThreads.LBVComplete"


12:09:10 Presenting theory "JinjaThreads.Abstract_BV"


12:09:10 Presenting theory "JinjaThreads.Type"


12:09:10 Presenting theory "JinjaThreads.Decl"


12:09:10 Presenting theory "JinjaThreads.TypeRel"


12:09:10 Presenting theory "JinjaThreads.Value"


12:09:10 Presenting theory "JinjaThreads.Exceptions"


12:09:10 Presenting theory "JinjaThreads.SystemClasses"


12:09:10 Presenting theory "JinjaThreads.Heap"


12:09:10 Presenting theory "JinjaThreads.Observable_Events"


12:09:10 Presenting theory "JinjaThreads.StartConfig"


12:09:10 Presenting theory "JinjaThreads.Conform"


12:09:10 Presenting theory "HOL.Argo"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_expr.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_term.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_lit.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_proof.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_rewr.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_cls.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_common.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_cc.ML"


12:09:10 Presenting theory "JinjaThreads.ExternalCall"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_simplex.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_thy.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_heap.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_cdcl.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_core.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_clausify.ML"


12:09:10 Presenting file "~~/src/Tools/Argo/argo_solver.ML"


12:09:10 Presenting file "~~/src/HOL/Tools/Argo/argo_tactic.ML"


12:09:11 Presenting theory "JinjaThreads.WellForm"


12:09:11 Presenting theory "HOL.SAT"


12:09:11 Presenting file "~~/src/HOL/Tools/prop_logic.ML"


12:09:11 Presenting file "~~/src/HOL/Tools/sat_solver.ML"


12:09:11 Presenting file "~~/src/HOL/Tools/sat.ML"


12:09:11 Presenting file "~~/src/HOL/Tools/Argo/argo_sat_solver.ML"


12:09:11 Presenting theory "JinjaThreads.ExternalCallWF"


12:09:11 Presenting theory "JinjaThreads.ConformThreaded"


12:09:11 Presenting theory "JinjaThreads.BinOp"


12:09:11 Presenting theory "JinjaThreads.SemiType"


12:09:12 Presenting theory "JinjaThreads.Common_Main"


12:09:12 Presenting theory "JinjaThreads.State"


12:09:12 Presenting theory "HOL.Fun_Def"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/function_core.ML"


12:09:12 Presenting theory "JinjaThreads.Expr"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/mutual.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/pattern_split.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/relation.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/function_elims.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/function.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/pat_completeness.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/fun.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/induction_schema.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/measure_functions.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/lexicographic_order.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/termination.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/scnp_solve.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/scnp_reconstruct.ML"


12:09:12 Presenting file "~~/src/HOL/Tools/Function/fun_cases.ML"


12:09:12 Presenting theory "JinjaThreads.JHeap"


12:09:12 Presenting theory "HOL.Int"


12:09:12 Presenting theory "JinjaThreads.SmallStep"


12:09:12 Presenting file "~~/src/HOL/Tools/int_arith.ML"


12:09:12 Presenting theory "JinjaThreads.WWellForm"


12:09:12 Presenting theory "JinjaThreads.WellType"


12:09:13 Presenting theory "HOL.Lattices_Big"


12:09:13 Presenting theory "JinjaThreads.DefAss"


12:09:13 Presenting theory "JinjaThreads.JWellForm"


12:09:13 Presenting theory "JinjaThreads.Threaded"


12:09:13 Presenting theory "HOL.Euclidean_Rings"


12:09:13 Presenting theory "JinjaThreads.WellTypeRT"


12:09:13 Presenting theory "JinjaThreads.Progress"


12:09:14 Presenting theory "JinjaThreads.DefAssPreservation"


12:09:14 Presenting theory "HOL.Parity"


12:09:14 Presenting theory "HOL.Numeral_Simprocs"


12:09:14 Presenting theory "JinjaThreads.TypeSafe"


12:09:14 Presenting file "~~/src/Provers/Arith/assoc_fold.ML"


12:09:14 Presenting file "~~/src/Provers/Arith/cancel_numerals.ML"


12:09:14 Presenting file "~~/src/Provers/Arith/combine_numerals.ML"


12:09:14 Presenting file "~~/src/Provers/Arith/cancel_numeral_factor.ML"


12:09:14 Presenting file "~~/src/Provers/Arith/extract_common_term.ML"


12:09:14 Presenting file "~~/src/HOL/Tools/numeral_simprocs.ML"


12:09:14 Presenting file "~~/src/HOL/Tools/nat_numeral_simprocs.ML"


12:09:14 Presenting theory "HOL.Semiring_Normalization"


12:09:14 Presenting file "~~/src/HOL/Tools/semiring_normalizer.ML"


12:09:15 Presenting theory "JinjaThreads.ProgressThreaded"


12:09:15 Presenting theory "HOL.Groebner_Basis"


12:09:15 Presenting file "~~/src/HOL/Tools/groebner.ML"


12:09:15 Presenting theory "JinjaThreads.Deadlocked"


12:09:15 Presenting theory "JinjaThreads.Annotate"


12:09:15 Presenting theory "JinjaThreads.J_Main"


12:09:15 Presenting theory "JinjaThreads.JVMState"


12:09:15 Presenting theory "JinjaThreads.JVMInstructions"


12:09:15 Presenting theory "JinjaThreads.JVMHeap"


12:09:15 Presenting theory "HOL.Set_Interval"


12:09:15 Presenting theory "JinjaThreads.JVMExecInstr"


12:09:15 Presenting theory "JinjaThreads.JVMExceptions"


12:09:15 Presenting theory "JinjaThreads.JVMExec"


12:09:16 Presenting theory "JinjaThreads.JVMDefensive"


12:09:16 Presenting theory "JinjaThreads.JVMThreaded"


12:09:16 Presenting theory "JinjaThreads.JVM_Main"


12:09:16 Presenting theory "JinjaThreads.JVM_SemiType"


12:09:16 Presenting theory "JinjaThreads.Effect"


12:09:16 Presenting theory "JinjaThreads.BVSpec"


12:09:16 Presenting theory "JinjaThreads.BVConform"


12:09:17 Presenting theory "HOL.Presburger"


12:09:17 Presenting file "~~/src/HOL/Tools/Qelim/qelim.ML"


12:09:17 Presenting file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"


12:09:17 Presenting file "~~/src/HOL/Tools/Qelim/cooper.ML"


12:09:17 Presenting file "~~/src/HOL/Tools/try0.ML"


12:09:17 Presenting theory "JinjaThreads.BVSpecTypeSafe"


12:09:17 Presenting theory "JinjaThreads.BVNoTypeError"


12:09:18 Presenting theory "JinjaThreads.BVProgressThreaded"


12:09:18 Presenting theory "JinjaThreads.JVMDeadlocked"


12:09:19 Presenting theory "JinjaThreads.EffectMono"


12:09:19 Presenting theory "JinjaThreads.TF_JVM"


12:09:19 Presenting theory "JinjaThreads.LBVJVM"


12:09:19 Presenting theory "JinjaThreads.BVExec"


12:09:19 Presenting theory "JinjaThreads.BCVExec"


12:09:19 Presenting theory "JinjaThreads.BV_Main"


12:09:19 Presenting theory "JinjaThreads.CallExpr"


12:09:19 Presenting theory "HOL.SMT"


12:09:19 Presenting file "~~/src/HOL/Tools/SMT/smt_util.ML"


12:09:19 Presenting file "~~/src/HOL/Tools/SMT/smt_failure.ML"


12:09:19 Presenting file "~~/src/HOL/Tools/SMT/smt_config.ML"


12:09:19 Presenting file "~~/src/HOL/Tools/SMT/smt_builtin.ML"


12:09:19 Presenting file "~~/src/HOL/Tools/SMT/smt_datatypes.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/smt_normalize.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/smt_translate.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/smtlib.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/smtlib_interface.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/smtlib_proof.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/smtlib_isar.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/z3_proof.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/z3_isar.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/smt_solver.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/cvc_interface.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/lethe_proof.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/lethe_isar.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/lethe_proof_parse.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/cvc_proof_parse.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/conj_disj_perm.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/smt_replay_methods.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/smt_replay.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/smt_replay_arith.ML"


12:09:20 Presenting theory "JinjaThreads.J0"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/z3_interface.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/z3_replay_rules.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/z3_replay_methods.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/z3_replay.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/lethe_replay_methods.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/cvc5_replay_methods.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/verit_replay_methods.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/verit_strategies.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/verit_replay.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/cvc5_replay.ML"


12:09:20 Presenting file "~~/src/HOL/Tools/SMT/smt_systems.ML"


12:09:20 Presenting theory "JinjaThreads.J0Bisim"


12:09:21 Presenting theory "JinjaThreads.J1State"


12:09:21 Presenting theory "JinjaThreads.J1Heap"


12:09:21 Presenting theory "JinjaThreads.J1"


12:09:22 Presenting theory "JinjaThreads.J1Deadlock"


12:09:22 Presenting theory "HOL.Sledgehammer"


12:09:22 Presenting file "~~/src/HOL/Tools/ATP/system_on_tptp.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML"


12:09:22 Presenting theory "JinjaThreads.PCompiler"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML"


12:09:22 Presenting theory "JinjaThreads.Compiler2"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML"


12:09:22 Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML"


12:09:22 Presenting theory "JinjaThreads.Exception_Tables"


12:09:22 Presenting theory "HOL.Lifting_Set"


12:09:22 Presenting theory "JinjaThreads.J1WellType"


12:09:22 Presenting theory "JinjaThreads.J1WellForm"


12:09:22 Presenting theory "HOL-Library.Prefix_Order"


12:09:23 Presenting theory "JinjaThreads.TypeComp"


12:09:23 Presenting theory "JinjaThreads.JVMTau"


12:09:24 Presenting theory "HOL.List"


12:09:25 Presenting theory "HOL.Groups_List"


12:09:25 Presenting theory "JinjaThreads.Execs"


12:09:25 Presenting theory "HOL.Bit_Operations"


12:09:26 Presenting theory "HOL.Code_Numeral"


12:09:26 Presenting theory "HOL.Random"


12:09:27 Presenting theory "HOL.Map"


12:09:27 Presenting theory "HOL.Enum"


12:09:27 Presenting theory "HOL.String"


12:09:27 Presenting file "~~/src/HOL/Tools/string_syntax.ML"


12:09:27 Presenting file "~~/src/HOL/Tools/literal.ML"


12:09:27 Presenting theory "HOL.Typerep"


12:09:28 Presenting theory "HOL.Predicate"


12:09:28 Presenting theory "HOL.Lazy_Sequence"


12:09:28 Presenting theory "HOL.Limited_Sequence"


12:09:28 Presenting theory "HOL.Code_Evaluation"


12:09:28 Presenting file "~~/src/HOL/Tools/code_evaluation.ML"


12:09:28 Presenting file "~~/src/HOL/Tools/value_command.ML"


12:09:28 Presenting file "~~/src/HOL/Tools/reification.ML"


12:09:28 Presenting theory "JinjaThreads.J1JVMBisim"


12:09:29 Presenting theory "HOL.Quickcheck_Random"


12:09:29 Presenting file "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML"


12:09:29 Presenting file "~~/src/HOL/Tools/Quickcheck/random_generators.ML"


12:09:29 Presenting theory "HOL.Random_Pred"


12:09:29 Presenting theory "HOL.Random_Sequence"


12:09:29 Presenting theory "HOL.Quickcheck_Exhaustive"


12:09:29 Presenting file "~~/src/HOL/Tools/Quickcheck/exhaustive_generators.ML"


12:09:29 Presenting file "~~/src/HOL/Tools/Quickcheck/abstract_generators.ML"


12:09:31 Presenting theory "HOL.Predicate_Compile"


12:09:31 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML"


12:09:31 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML"


12:09:31 Presenting file "~~/src/HOL/Tools/Predicate_Compile/core_data.ML"


12:09:31 Presenting file "~~/src/HOL/Tools/Predicate_Compile/mode_inference.ML"


12:09:31 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML"


12:09:31 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML"


12:09:31 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML"


12:09:31 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML"


12:09:31 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML"


12:09:31 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML"


12:09:31 Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile.ML"


12:09:32 Presenting theory "HOL.Quickcheck_Narrowing"


12:09:32 Presenting file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"


12:09:32 Presenting file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"


12:09:32 Presenting file "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"


12:09:32 Presenting file "~~/src/HOL/Tools/Quickcheck/find_unused_assms.ML"


12:09:32 Presenting theory "HOL.Mirabelle"


12:09:32 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_util.ML"


12:09:32 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle.ML"


12:09:32 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_arith.ML"


12:09:32 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_metis.ML"


12:09:32 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML"


12:09:32 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML"


12:09:32 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML"


12:09:32 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"


12:09:32 Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_try0.ML"


12:09:32 Presenting theory "HOL.Extraction"


12:09:33 Presenting theory "HOL.Record"


12:09:33 Presenting file "~~/src/HOL/Tools/record.ML"


12:09:33 Presenting theory "JinjaThreads.J1JVM"


12:09:33 Presenting theory "HOL.GCD"


12:09:36 Presenting theory "JinjaThreads.JVMJ1"


12:09:37 Presenting theory "HOL.Nitpick"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/kodkod.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/kodkod_sat.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_util.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_hol.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_mono.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_preproc.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_scope.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_peephole.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_rep.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_nut.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_kodkod.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_model.ML"


12:09:37 Presenting theory "JinjaThreads.Correctness2"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_commands.ML"


12:09:37 Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_tests.ML"


12:09:37 Presenting theory "JinjaThreads.ListIndex"


12:09:38 Presenting theory "JinjaThreads.Compiler1"


12:09:38 Presenting theory "JinjaThreads.J0J1Bisim"


12:09:38 Presenting theory "HOL.Nunchaku"


12:09:38 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_util.ML"


12:09:38 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_collect.ML"


12:09:38 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_problem.ML"


12:09:38 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_translate.ML"


12:09:38 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_model.ML"


12:09:38 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML"


12:09:38 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_display.ML"


12:09:38 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_tool.ML"


12:09:38 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku.ML"


12:09:38 Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_commands.ML"


12:09:39 Presenting theory "JinjaThreads.Correctness1Threaded"


12:09:40 Presenting theory "HOL.BNF_Greatest_Fixpoint"


12:09:41 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_util.ML"


12:09:41 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_tactics.ML"


12:09:41 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp.ML"


12:09:41 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"


12:09:41 Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML"


12:09:41 Presenting theory "JinjaThreads.Correctness1"


12:09:41 Presenting theory "HOL.Filter"


12:09:41 Presenting theory "JinjaThreads.JJ1WellForm"


12:09:42 Presenting theory "JinjaThreads.Compiler"


12:09:42 Presenting theory "HOL.Conditionally_Complete_Lattices"


12:09:42 Presenting theory "HOL.Factorial"


12:09:42 Presenting theory "JinjaThreads.Correctness"


12:09:42 Presenting theory "JinjaThreads.Preprocessor"


12:09:42 Presenting theory "JinjaThreads.Compiler_Main"


12:09:42 Presenting theory "JinjaThreads.MM"


12:09:42 Presenting theory "JinjaThreads.SC"


12:09:42 Presenting theory "JinjaThreads.SC_Interp"


12:09:42 Presenting theory "HOL.Binomial"


12:09:42 Presenting theory "JinjaThreads.SC_Collections"


12:09:42 Presenting theory "HOL.Divides"


12:09:43 Presenting theory "Main"


12:09:43 Presenting theory "HOL.Archimedean_Field"


12:09:43 Presenting theory "JinjaThreads.Orders"


12:09:43 Presenting theory "HOL.Rat"


12:09:43 Presenting theory "JinjaThreads.JMM_Spec"


12:09:43 Presenting theory "HOL.Real"


12:09:44 Presenting file "~~/src/HOL/Tools/SMT/smt_real.ML"


12:09:44 Presenting file "~~/src/HOL/Tools/SMT/z3_real.ML"


12:09:44 Presenting file "~~/src/HOL/Tools/Argo/argo_real.ML"


12:09:44 Presenting theory "JinjaThreads.JMM_DRF"


12:09:44 Presenting theory "JinjaThreads.SC_Legal"


12:09:44 Presenting theory "JinjaThreads.Non_Speculative"


12:09:44 Presenting theory "HOL.Topological_Spaces"


12:09:45 Presenting theory "HOL.Hull"


12:09:45 Presenting theory "HOL.Modules"


12:09:45 Presenting theory "JinjaThreads.SC_Completion"


12:09:46 Presenting theory "HOL.Vector_Spaces"


12:09:46 Presenting theory "JinjaThreads.HB_Completion"


12:09:46 Presenting theory "JinjaThreads.JMM_Heap"


12:09:46 Presenting theory "HOL.Real_Vector_Spaces"


12:09:47 Presenting theory "HOL.Limits"


12:09:48 Presenting theory "HOL.Inequalities"


12:09:48 Presenting theory "HOL.Series"


12:09:49 Presenting theory "JinjaThreads.JMM_Framework"


12:09:49 Presenting theory "HOL.Deriv"


12:09:49 Presenting theory "HOL.NthRoot"


12:09:49 Presenting theory "JinjaThreads.JMM_Typesafe"


12:09:50 Presenting theory "JinjaThreads.JMM_Common"


12:09:50 Presenting theory "JinjaThreads.JMM_J"


12:09:51 Presenting theory "HOL.Transcendental"


12:09:51 Presenting theory "JinjaThreads.DRF_J"


12:09:51 Presenting theory "JinjaThreads.JMM_JVM"


12:09:52 Presenting theory "JinjaThreads.DRF_JVM"


12:09:52 Presenting theory "JinjaThreads.JMM_Type"


12:09:52 Presenting theory "HOL.Complex"


12:09:52 Presenting theory "JinjaThreads.JMM_Compiler"


12:09:52 Presenting theory "JinjaThreads.JMM_Type2"


12:09:52 Presenting theory "JinjaThreads.JMM_Interp"


12:09:52 Presenting theory "HOL.MacLaurin"


12:09:52 Presenting theory "Complex_Main"


12:09:52 Presenting theory "JinjaThreads.JMM_Typesafe2"


12:09:53 Presenting theory "JinjaThreads.JMM_J_Typesafe"


12:09:53 Presenting theory "JinjaThreads.JMM_JVM_Typesafe"


12:09:53 Presenting theory "JinjaThreads.JMM_Compiler_Type2"


12:09:53 Presenting theory "JinjaThreads.JMM"


12:09:53 Presenting theory "JinjaThreads.MM_Main"


12:09:53 Presenting theory "JinjaThreads.State_Refinement"


12:09:53 Presenting theory "JinjaThreads.Scheduler"


12:09:54 Presenting theory "JinjaThreads.Random_Scheduler"


12:09:54 Presenting theory "JinjaThreads.Round_Robin"


12:09:54 Presenting theory "JinjaThreads.SC_Schedulers"


12:09:54 Presenting theory "HOL-Library.Mapping"


12:09:54 Presenting theory "HOL-Library.AList_Mapping"


12:09:55 Presenting theory "JinjaThreads.TypeRelRefine"


12:09:55 Presenting theory "JinjaThreads.PCompilerRefine"


12:09:55 Presenting theory "JinjaThreads.J_Execute"


12:09:55 Presenting theory "JinjaThreads.ExternalCall_Execute"


12:09:55 Presenting theory "JinjaThreads.JVMExec_Execute2"


12:09:56 Presenting theory "JinjaThreads.JVM_Execute2"


12:09:56 Presenting theory "HOL-Library.Code_Cardinality"


12:09:56 Presenting theory "JinjaThreads.Code_Generation"


12:09:56 Presenting theory "JinjaThreads.JVMExec_Execute"


12:09:56 Presenting theory "JinjaThreads.JVM_Execute"


12:09:56 Presenting theory "JinjaThreads.ToString"


12:09:56 Presenting theory "JinjaThreads.Java2Jinja"


12:09:56 Presenting theory "JinjaThreads.Execute_Main"


12:09:56 Presenting theory "JinjaThreads.ApprenticeChallenge"


12:09:56 Presenting theory "JinjaThreads.BufferExample"


12:09:56 Presenting theory "JinjaThreads.Examples_Main"


12:09:56 Presenting theory "JinjaThreads.JinjaThreads"


12:09:56 

12:09:56 === TIMING ===


12:09:56 

12:09:56 Group slow: 9:41:38 elapsed time, 32:23:54 cpu time, factor 3.34


12:09:56 Group AFP: 10:07:39 elapsed time, 34:17:14 cpu time, factor 3.39


12:09:56 Group main: 0:09:28 elapsed time, 0:41:17 cpu time, factor 4.36


12:09:56 Group timing: 0:03:20 elapsed time, 0:18:35 cpu time, factor 5.56


12:09:56 Group very_slow: 6:04:43 elapsed time, 14:00:39 cpu time, factor 2.30


12:09:56 Overall: 10:35:30 elapsed time, 34:58:57 cpu time, factor 3.30


12:09:57 Archiving artifacts


12:10:11 Started calculate disk usage of build


12:10:11 Finished Calculation of disk usage of build in 0 seconds


12:11:15 Started calculate disk usage of workspace


12:11:16 Finished Calculation of disk usage of workspace in 0 seconds


12:11:18 No emails were triggered.


12:11:18 Finished: SUCCESS