Started by an SCM change
Running as SYSTEM
[EnvInject] - Loading node environment variables.
Building remotely on workerlrz5 (lrz-cloud) in workspace /media/data/jenkins/workspace/isabelle-nightly-slow
[isabelle-nightly-slow] $ hg showconfig paths.default
[isabelle-nightly-slow] $ hg pull --rev default
pulling from https://isabelle.in.tum.de/repos/isabelle/
no changes found
[isabelle-nightly-slow] $ hg update --clean --rev default
27 files updated, 0 files merged, 4 files removed, 0 files unresolved
[isabelle-nightly-slow] $ hg --config extensions.purge= clean --all
[isabelle-nightly-slow] $ hg log --rev . --template {node}
[isabelle-nightly-slow] $ hg log --rev . --template {rev}
[isabelle-nightly-slow] $ hg log --rev e94a36467f4ee4be5da1eeabc206c7543903ca48 --template exists\n
exists
[isabelle-nightly-slow] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(e94a36467f4ee4be5da1eeabc206c7543903ca48)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
[afp] $ hg pull --rev default
pulling from https://foss.heptapod.net/isa-afp/afp-devel/
no changes found
[afp] $ hg update --clean --rev default
8 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp] $ hg --config extensions.purge= clean --all
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg log --rev 73b120ffbbc35d769000c00909a5bda4b40adf22 --template exists\n
exists
[afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(73b120ffbbc35d769000c00909a5bda4b40adf22)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins1993665381882694483.sh
+ Admin/jenkins/run_build slow
+ set -e
+ PROFILE=slow
+ shift
+ bin/isabelle components -a
### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/bash_process-20240326"
Getting "https://isabelle.sketis.net/components/bash_process-20240326.tar.gz"
Unpacking "/media/data/jenkins/.isabelle/contrib/bash_process-20240326.tar.gz"
+ bin/isabelle jedit -bf
### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle.jar) ...
### Building Demo (/media/data/jenkins/workspace/isabelle-nightly-slow/src/Tools/Demo/lib/demo.jar) ...
### Building graph browser (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle_graphbrowser.jar) ...
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle_admin.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-nightly-slow/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
+ bin/isabelle ocaml_setup
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
       opam update

[NOTE] Package zarith is already installed (current version is 1.12).
+ bin/isabelle ghc_setup
Stack will use a sandboxed GHC it installed. To use this GHC and packages outside of a project,
consider using: stack ghc, stack ghci, stack runghc, or stack exec.
The Glorious Glasgow Haskell Compilation System, version 9.6.4
+ bin/isabelle ci_build slow

=== CONFIGURATION ===

ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.9.1/x86_64-linux"
ML_SYSTEM="polyml-5.9.1"
ML_OPTIONS="-H 4000 --maxheap 32G"
jobs = 1, threads = 8, numa = false

=== BUILD ===

Build started at Wed, 27 Mar 2024 00:34:39 GMT
Isabelle id ac4412562c7b
Build for AFP id ba52e1ff7569

=== LOG ===

Session Pure/Pure
Session FOL/FOL
Session Pure/Pure-Examples
Session Pure/Pure-ex
Session Misc/Tools
Session HOL/HOL (main)
Session AFP/AWN (AFP)
Session AFP/AODV (AFP slow)
Session HOL/HOL-Cardinals (timing)
Session HOL/HOL-Library (main timing)
Session AFP/Binomial-Heaps (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/ConcurrentGC (AFP slow)
Session AFP/FinFun (AFP)
Session AFP/Finger-Trees (AFP)
Session HOL/HOL-Combinatorics (main timing)
Session HOL/HOL-Computational_Algebra (main timing)
Session HOL/HOL-Algebra (main timing)
Session HOL/HOL-Decision_Procs (timing)
Session HOL/HOL-Number_Theory (main timing)
Session HOL/HOL-ex (timing)
Session HOL/HOL-Imperative_HOL (timing)
Session AFP/HereditarilyFinite (AFP)
Session AFP/Trie (AFP)
Session AFP/Flyspeck-Tame (AFP)
Session AFP/Flyspeck-Tame-Computation (AFP slow very_slow)
Session HOL/HOL-Real_Asymp
Session HOL/HOL-Analysis (main timing)
Session AFP/Coinductive (AFP)
Session HOL/HOL-Eisbach
Session AFP/Automatic_Refinement (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Word_Lib (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Routing (AFP)
Session AFP/Native_Word (AFP)
Session AFP/Collections (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/Iptables_Semantics_Examples_Big (AFP slow very_slow)
Session AFP/JinjaThreads (AFP slow)
Session AFP/ZFC_in_HOL (AFP)
Session AFP/Category3 (AFP)
Session AFP/MonoidalCategory (AFP)
Session AFP/Bicategory (AFP slow)
Building Pure ...
Pure: theory Pure
Pure: theory ML_Bootstrap
Pure: theory Pure.Sessions
Timing Pure (1 threads, 0.868s elapsed time, 0.915s cpu time, 0.000s GC time, factor 1.05)
Finished Pure (0:00:24 elapsed time, 0:00:24 cpu time, factor 0.99)
Building HOL ...
HOL: theory Tools.Code_Generator
HOL: theory HOL.HOL
HOL: theory HOL.Argo
HOL: theory HOL.Ctr_Sugar
HOL: theory HOL.Orderings
HOL: theory HOL.Groups
HOL: theory HOL.SAT
HOL: theory HOL.Lattices
HOL: theory HOL.Boolean_Algebras
HOL: theory HOL.Set
HOL: theory HOL.Typedef
HOL: theory HOL.Fun
HOL: theory HOL.Complete_Lattices
HOL: theory HOL.Rings
HOL: theory HOL.Inductive
HOL: theory HOL.Product_Type
HOL: theory HOL.Sum_Type
HOL: theory HOL.Complete_Partial_Order
HOL: theory HOL.Nat
HOL: theory HOL.Fields
HOL: theory HOL.Meson
HOL: theory HOL.Relation
HOL: theory HOL.Finite_Set
HOL: theory HOL.Transitive_Closure
HOL: theory HOL.Wellfounded
HOL: theory HOL.Fun_Def_Base
HOL: theory HOL.Hilbert_Choice
HOL: theory HOL.Wfrec
HOL: theory HOL.Order_Relation
HOL: theory HOL.BNF_Wellorder_Relation
HOL: theory HOL.BNF_Wellorder_Embedding
HOL: theory HOL.Zorn
HOL: theory HOL.ATP
HOL: theory HOL.BNF_Wellorder_Constructions
HOL: theory HOL.BNF_Cardinal_Order_Relation
HOL: theory HOL.BNF_Cardinal_Arithmetic
HOL: theory HOL.BNF_Def
HOL: theory HOL.Metis
HOL: theory HOL.BNF_Composition
HOL: theory HOL.Basic_BNFs
HOL: theory HOL.BNF_Fixpoint_Base
HOL: theory HOL.BNF_Least_Fixpoint
HOL: theory HOL.Basic_BNF_LFPs
HOL: theory HOL.Equiv_Relations
HOL: theory HOL.Transfer
HOL: theory HOL.Lifting
HOL: theory HOL.Num
HOL: theory HOL.Option
HOL: theory HOL.Quotient
HOL: theory HOL.Extraction
HOL: theory HOL.Partial_Function
HOL: theory HOL.Power
HOL: theory HOL.Fun_Def
HOL: theory HOL.Groups_Big
HOL: theory HOL.Lifting_Set
HOL: theory HOL.Lattices_Big
HOL: theory HOL.Int
HOL: theory HOL.Euclidean_Rings
HOL: theory HOL.Parity
HOL: theory HOL.Divides
HOL: theory HOL.Numeral_Simprocs
HOL: theory HOL.Set_Interval
HOL: theory HOL.SMT
HOL: theory HOL.Semiring_Normalization
HOL: theory HOL.Groebner_Basis
HOL: theory HOL.Conditionally_Complete_Lattices
HOL: theory HOL.Presburger
HOL: theory HOL.Filter
HOL: theory HOL.Sledgehammer
HOL: theory HOL.List
HOL: theory HOL.Groups_List
HOL: theory HOL.Map
HOL: theory HOL.Bit_Operations
HOL: theory HOL.Factorial
HOL: theory HOL.Enum
HOL: theory HOL.Binomial
HOL: theory HOL.Code_Numeral
HOL: theory HOL.GCD
HOL: theory HOL.String
HOL: theory HOL.Random
HOL: theory HOL.BNF_Greatest_Fixpoint
HOL: theory HOL.Predicate
HOL: theory HOL.Typerep
HOL: theory HOL.Lazy_Sequence
HOL: theory HOL.Limited_Sequence
HOL: theory HOL.Code_Evaluation
HOL: theory HOL.Quickcheck_Random
HOL: theory HOL.Quickcheck_Exhaustive
HOL: theory HOL.Quickcheck_Narrowing
HOL: theory HOL.Random_Pred
HOL: theory HOL.Random_Sequence
HOL: theory HOL.Record
HOL: theory HOL.Predicate_Compile
HOL: theory HOL.Nitpick
HOL: theory HOL.Mirabelle
HOL: theory HOL.Nunchaku
HOL: theory Main
HOL: theory HOL.Archimedean_Field
HOL: theory HOL.Hull
HOL: theory HOL.Topological_Spaces
HOL: theory HOL.Modules
HOL: theory HOL.Vector_Spaces
HOL: theory HOL.Rat
HOL: theory HOL.Real
HOL: theory HOL.Real_Vector_Spaces
HOL: theory HOL.Limits
HOL: theory HOL.Inequalities
HOL: theory HOL.Deriv
HOL: theory HOL.Series
HOL: theory HOL.NthRoot
HOL: theory HOL.Transcendental
HOL: theory HOL.Complex
HOL: theory HOL.MacLaurin
HOL: theory Complex_Main
Preparing HOL/document ...
Finished HOL/document (0:01:52 elapsed time)
Preparing HOL/outline ...
Finished HOL/outline (0:01:03 elapsed time)
Timing HOL (8 threads, 295.009s elapsed time, 1038.773s cpu time, 64.478s GC time, factor 3.52)
Finished HOL (0:05:24 elapsed time, 0:18:20 cpu time, factor 3.39)
Running JinjaThreads ...
JinjaThreads: theory Automatic_Refinement.Foldi
JinjaThreads: theory Automatic_Refinement.Prio_List
JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1
JinjaThreads: theory Collections.ICF_Tools
JinjaThreads: theory Finger-Trees.FingerTree
JinjaThreads: theory HOL-Library.AList
JinjaThreads: theory HOL-Library.Adhoc_Overloading
JinjaThreads: theory HOL-Eisbach.Eisbach
JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot
JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot
JinjaThreads: theory HOL-Library.Monad_Syntax
JinjaThreads: theory HOL-Library.Cancellation
JinjaThreads: theory Collections.Ord_Code_Preproc
JinjaThreads: theory HOL-Library.Case_Converter
JinjaThreads: theory HOL-Library.Code_Abstract_Nat
JinjaThreads: theory Automatic_Refinement.Refine_Util
JinjaThreads: theory Collections.Locale_Code
JinjaThreads: theory Collections.Record_Intf
JinjaThreads: theory HOL-Library.Code_Target_Nat
JinjaThreads: theory HOL-Library.Code_Target_Int
JinjaThreads: theory HOL-Library.Simps_Case_Conv
JinjaThreads: theory HOL-Library.Complete_Partial_Order2
JinjaThreads: theory HOL-Library.Confluence
JinjaThreads: theory HOL-Library.Code_Target_Numeral
JinjaThreads: theory HOL-Library.Confluent_Quotient
JinjaThreads: theory Automatic_Refinement.Anti_Unification
JinjaThreads: theory Automatic_Refinement.Attr_Comb
JinjaThreads: theory Automatic_Refinement.Autoref_Data
JinjaThreads: theory Automatic_Refinement.Indep_Vars
JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp
JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms
JinjaThreads: theory Automatic_Refinement.Tagged_Solver
JinjaThreads: theory Automatic_Refinement.Select_Solve
JinjaThreads: theory HOL-Library.Multiset
JinjaThreads: theory HOL-Library.Dlist
JinjaThreads: theory HOL-Library.Infinite_Set
JinjaThreads: theory HOL-Library.Nat_Bijection
JinjaThreads: theory HOL-Library.Old_Datatype
JinjaThreads: theory HOL-Library.Option_ord
JinjaThreads: theory Trie.Trie
JinjaThreads: theory HOL-Library.Phantom_Type
JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs
JinjaThreads: theory HOL-Library.RBT_Impl
JinjaThreads: theory HOL-Library.Signed_Division
JinjaThreads: theory HOL-Library.Sublist
JinjaThreads: theory HOL-Library.Cardinality
JinjaThreads: theory HOL-Library.Transitive_Closure_Table
JinjaThreads: theory HOL-Library.While_Combinator
JinjaThreads: theory HOL-Library.Countable
JinjaThreads: theory FinFun.FinFun
JinjaThreads: theory HOL-Library.Numeral_Type
JinjaThreads: theory Collections.DatRef
JinjaThreads: theory JinjaThreads.Set_Monad
JinjaThreads: theory JinjaThreads.Set_without_equal
JinjaThreads: theory Native_Word.Code_Int_Integer_Conversion
JinjaThreads: theory Refine_Monadic.Refine_Chapter
JinjaThreads: theory HOL-Library.Type_Length
JinjaThreads: theory Word_Lib.More_Bit_Ring
JinjaThreads: theory HOL-Library.Countable_Set
JinjaThreads: theory JinjaThreads.Auxiliary
JinjaThreads: theory HOL-Library.Countable_Complete_Lattices
JinjaThreads: theory HOL-Library.Word
JinjaThreads: theory Word_Lib.More_Arithmetic
JinjaThreads: theory Binomial-Heaps.BinomialHeap
JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap
JinjaThreads: theory HOL-ex.Quicksort
JinjaThreads: theory Automatic_Refinement.Misc
JinjaThreads: theory HOL-Library.Order_Continuity
JinjaThreads: theory HOL-Library.Extended_Nat
JinjaThreads: theory Coinductive.Coinductive_Nat
JinjaThreads: theory Coinductive.Coinductive_List
JinjaThreads: theory Automatic_Refinement.Refine_Lib
JinjaThreads: theory Collections.SetIterator
JinjaThreads: theory Collections.Sorted_List_Operations
JinjaThreads: theory Word_Lib.Bit_Comprehension
JinjaThreads: theory Word_Lib.More_Divides
JinjaThreads: theory Automatic_Refinement.Autoref_Phases
JinjaThreads: theory Automatic_Refinement.Autoref_Tagging
JinjaThreads: theory Automatic_Refinement.Relators
JinjaThreads: theory Word_Lib.Signed_Division_Word
JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover
JinjaThreads: theory Word_Lib.More_Word
JinjaThreads: theory Collections.SetIteratorOperations
JinjaThreads: theory Automatic_Refinement.Param_Tool
JinjaThreads: theory Automatic_Refinement.Param_HOL
JinjaThreads: theory Native_Word.Code_Target_Word_Base
JinjaThreads: theory Word_Lib.Bit_Shifts_Infix_Syntax
JinjaThreads: theory Word_Lib.Least_significant_bit
JinjaThreads: theory Collections.Assoc_List
JinjaThreads: theory Collections.Dlist_add
JinjaThreads: theory Automatic_Refinement.Parametricity
JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops
JinjaThreads: theory Collections.Proper_Iterator
JinjaThreads: theory Collections.SetIteratorGA
JinjaThreads: theory Collections.Diff_Array
JinjaThreads: theory Collections.Trie_Impl
JinjaThreads: theory Collections.It_to_It
JinjaThreads: theory Coinductive.Lazy_LList
JinjaThreads: theory Coinductive.TLList
JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel
JinjaThreads: theory Collections.Trie2
JinjaThreads: theory Word_Lib.Most_significant_bit
JinjaThreads: theory Word_Lib.Generic_set_bit
JinjaThreads: theory Automatic_Refinement.Autoref_Translate
JinjaThreads: theory Automatic_Refinement.Autoref_Relator_Interface
JinjaThreads: theory Automatic_Refinement.Autoref_Gen_Algo
JinjaThreads: theory Automatic_Refinement.Autoref_Tool
JinjaThreads: theory Native_Word.Code_Target_Integer_Bit
JinjaThreads: theory Native_Word.Word_Type_Copies
JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL
JinjaThreads: theory Coinductive.Lazy_TLList
JinjaThreads: theory Automatic_Refinement.Automatic_Refinement
JinjaThreads: theory Collections.Idx_Iterator
JinjaThreads: theory Refine_Monadic.Refine_Misc
JinjaThreads: theory Refine_Monadic.RefineG_Domain
JinjaThreads: theory Refine_Monadic.RefineG_Transfer
JinjaThreads: theory Refine_Monadic.RefineG_Assert
JinjaThreads: theory Refine_Monadic.RefineG_Recursion
JinjaThreads: theory Refine_Monadic.RefineG_While
JinjaThreads: theory Refine_Monadic.Refine_Basic
JinjaThreads: theory Refine_Monadic.Refine_Det
JinjaThreads: theory Refine_Monadic.Refine_Heuristics
JinjaThreads: theory Refine_Monadic.Refine_Leof
JinjaThreads: theory Refine_Monadic.Refine_Pfun
JinjaThreads: theory Refine_Monadic.Refine_More_Comb
JinjaThreads: theory Refine_Monadic.Refine_While
JinjaThreads: theory Native_Word.Code_Target_Int_Bit
JinjaThreads: theory Native_Word.Uint32
JinjaThreads: theory Collections.Code_Target_ICF
JinjaThreads: theory Refine_Monadic.Refine_Transfer
JinjaThreads: theory Refine_Monadic.Autoref_Monadic
JinjaThreads: theory Refine_Monadic.Refine_Automation
JinjaThreads: theory Refine_Monadic.Refine_Foreach
JinjaThreads: theory Collections.HashCode
JinjaThreads: theory Refine_Monadic.Refine_Monadic
JinjaThreads: theory Collections.Gen_Iterator
JinjaThreads: theory Collections.Intf_Map
JinjaThreads: theory Collections.Intf_Set
JinjaThreads: theory Collections.Iterator
JinjaThreads: theory Collections.Array_Iterator
JinjaThreads: theory Collections.ICF_Spec_Base
JinjaThreads: theory Collections.ListSpec
JinjaThreads: theory Collections.AnnotatedListSpec
JinjaThreads: theory Collections.MapSpec
JinjaThreads: theory Collections.PrioSpec
JinjaThreads: theory Collections.PrioUniqueSpec
JinjaThreads: theory Collections.SetSpec
JinjaThreads: theory Collections.BinoPrioImpl
JinjaThreads: theory Collections.ListGA
JinjaThreads: theory Collections.SkewPrioImpl
JinjaThreads: theory Collections.FTAnnotatedListImpl
JinjaThreads: theory Collections.PrioByAnnotatedList
JinjaThreads: theory Collections.Fifo
JinjaThreads: theory Collections.PrioUniqueByAnnotatedList
JinjaThreads: theory Collections.Algos
JinjaThreads: theory Collections.SetIndex
JinjaThreads: theory Collections.SetIteratorCollectionsGA
JinjaThreads: theory Collections.MapGA
JinjaThreads: theory Collections.SetGA
JinjaThreads: theory Collections.FTPrioImpl
JinjaThreads: theory Collections.FTPrioUniqueImpl
JinjaThreads: theory Collections.ArrayMapImpl
JinjaThreads: theory Collections.ListMapImpl
JinjaThreads: theory Collections.ListMapImpl_Invar
JinjaThreads: theory Collections.TrieMapImpl
JinjaThreads: theory Collections.ListSetImpl
JinjaThreads: theory Collections.ListSetImpl_Invar
JinjaThreads: theory Collections.ListSetImpl_NotDist
JinjaThreads: theory Collections.ListSetImpl_Sorted
JinjaThreads: theory Collections.SetByMap
JinjaThreads: theory Collections.ArrayHashMap_Impl
JinjaThreads: theory Collections.ArraySetImpl
JinjaThreads: theory Collections.TrieSetImpl
JinjaThreads: theory Collections.ArrayHashMap
JinjaThreads: theory HOL-Library.RBT
JinjaThreads: theory Collections.RBT_add
JinjaThreads: theory Collections.RBTMapImpl
JinjaThreads: theory Collections.ArrayHashSet
JinjaThreads: theory Collections.RBTSetImpl
JinjaThreads: theory Collections.HashMap_Impl
JinjaThreads: theory Collections.HashMap
JinjaThreads: theory Collections.HashSet
JinjaThreads: theory Collections.MapStdImpl
JinjaThreads: theory Collections.SetStdImpl
JinjaThreads: theory Collections.ICF_Impl
JinjaThreads: theory Collections.ICF_Refine_Monadic
JinjaThreads: theory Collections.ICF_Autoref
JinjaThreads: theory Collections.Collections
JinjaThreads: theory Collections.CollectionsV1
JinjaThreads: theory JinjaThreads.JT_ICF
JinjaThreads: theory JinjaThreads.Basic_Main
JinjaThreads: theory HOL-Library.Mapping
JinjaThreads: theory HOL-Library.Code_Cardinality
JinjaThreads: theory HOL-Library.Prefix_Order
JinjaThreads: theory JinjaThreads.LTS
JinjaThreads: theory JinjaThreads.Type
JinjaThreads: theory JinjaThreads.FWState
JinjaThreads: theory JinjaThreads.ListIndex
JinjaThreads: theory JinjaThreads.Orders
JinjaThreads: theory JinjaThreads.Semilat
JinjaThreads: theory JinjaThreads.Err
JinjaThreads: theory JinjaThreads.Listn
JinjaThreads: theory JinjaThreads.Opt
JinjaThreads: theory HOL-Library.AList_Mapping
JinjaThreads: theory JinjaThreads.Product
JinjaThreads: theory JinjaThreads.Semilattices
JinjaThreads: theory JinjaThreads.Decl
JinjaThreads: theory JinjaThreads.Bisimulation
JinjaThreads: theory JinjaThreads.Typing_Framework
JinjaThreads: theory JinjaThreads.SemilatAlg
JinjaThreads: theory JinjaThreads.Kildall
JinjaThreads: theory JinjaThreads.LBVSpec
JinjaThreads: theory JinjaThreads.Typing_Framework_err
JinjaThreads: theory JinjaThreads.LBVComplete
JinjaThreads: theory JinjaThreads.LBVCorrect
JinjaThreads: theory JinjaThreads.TypeRel
JinjaThreads: theory JinjaThreads.Abstract_BV
JinjaThreads: theory JinjaThreads.TypeRelRefine
JinjaThreads: theory JinjaThreads.Value
JinjaThreads: theory JinjaThreads.Exceptions
JinjaThreads: theory JinjaThreads.Heap
JinjaThreads: theory JinjaThreads.SystemClasses
JinjaThreads: theory JinjaThreads.MM
JinjaThreads: theory JinjaThreads.State
JinjaThreads: theory JinjaThreads.FWCondAction
JinjaThreads: theory JinjaThreads.FWInterrupt
JinjaThreads: theory JinjaThreads.FWLock
JinjaThreads: theory JinjaThreads.FWThread
JinjaThreads: theory JinjaThreads.FWWait
JinjaThreads: theory JinjaThreads.Observable_Events
JinjaThreads: theory JinjaThreads.FWLocking
JinjaThreads: theory JinjaThreads.FWLockingThread
JinjaThreads: theory JinjaThreads.FWWellform
JinjaThreads: theory JinjaThreads.FWLifting
JinjaThreads: theory JinjaThreads.FWSemantics
JinjaThreads: theory JinjaThreads.JVMState
JinjaThreads: theory JinjaThreads.StartConfig
JinjaThreads: theory JinjaThreads.JMM_Spec
JinjaThreads: theory JinjaThreads.FWLiftingSem
JinjaThreads: theory JinjaThreads.FWProgressAux
JinjaThreads: theory JinjaThreads.Conform
JinjaThreads: theory JinjaThreads.State_Refinement
JinjaThreads: theory JinjaThreads.FWDeadlock
JinjaThreads: theory JinjaThreads.FWLTS
JinjaThreads: theory JinjaThreads.ConformThreaded
JinjaThreads: theory JinjaThreads.ExternalCall
JinjaThreads: theory JinjaThreads.SC
JinjaThreads: theory JinjaThreads.FWProgress
JinjaThreads: theory JinjaThreads.SC_Collections
JinjaThreads: theory JinjaThreads.JMM_DRF
JinjaThreads: theory JinjaThreads.SC_Legal
JinjaThreads: theory JinjaThreads.FWBisimulation
JinjaThreads: theory JinjaThreads.FWInitFinLift
JinjaThreads: theory JinjaThreads.Non_Speculative
JinjaThreads: theory JinjaThreads.Scheduler
JinjaThreads: theory JinjaThreads.HB_Completion
JinjaThreads: theory JinjaThreads.SC_Completion
JinjaThreads: theory JinjaThreads.WellForm
JinjaThreads: theory JinjaThreads.ExternalCall_Execute
JinjaThreads: theory JinjaThreads.ExternalCallWF
JinjaThreads: theory JinjaThreads.JMM_Heap
JinjaThreads: theory JinjaThreads.SemiType
JinjaThreads: theory JinjaThreads.BinOp
JinjaThreads: theory JinjaThreads.JVM_SemiType
JinjaThreads: theory JinjaThreads.JMM_Type
JinjaThreads: theory JinjaThreads.JMM_Type2
JinjaThreads: theory JinjaThreads.Random_Scheduler
JinjaThreads: theory JinjaThreads.Round_Robin
JinjaThreads: theory JinjaThreads.JMM_Framework
JinjaThreads: theory JinjaThreads.SC_Schedulers
JinjaThreads: theory JinjaThreads.Expr
JinjaThreads: theory JinjaThreads.JVMInstructions
JinjaThreads: theory JinjaThreads.PCompiler
JinjaThreads: theory JinjaThreads.PCompilerRefine
JinjaThreads: theory JinjaThreads.JVMExceptions
JinjaThreads: theory JinjaThreads.JVMHeap
JinjaThreads: theory JinjaThreads.Effect
JinjaThreads: theory JinjaThreads.JVMExecInstr
JinjaThreads: theory JinjaThreads.CallExpr
JinjaThreads: theory JinjaThreads.DefAss
JinjaThreads: theory JinjaThreads.JHeap
JinjaThreads: theory JinjaThreads.WWellForm
JinjaThreads: theory JinjaThreads.WellType
JinjaThreads: theory JinjaThreads.JVMExec
JinjaThreads: theory JinjaThreads.ToString
JinjaThreads: theory JinjaThreads.JVMDefensive
JinjaThreads: theory JinjaThreads.J1State
JinjaThreads: theory JinjaThreads.SmallStep
JinjaThreads: theory JinjaThreads.Annotate
JinjaThreads: theory JinjaThreads.J1Heap
JinjaThreads: theory JinjaThreads.J1WellType
JinjaThreads: theory JinjaThreads.JWellForm
JinjaThreads: theory JinjaThreads.J1WellForm
JinjaThreads: theory JinjaThreads.WellTypeRT
JinjaThreads: theory JinjaThreads.JVMThreaded
JinjaThreads: theory JinjaThreads.JVMExec_Execute
JinjaThreads: theory JinjaThreads.Compiler1
JinjaThreads: theory JinjaThreads.Compiler2
JinjaThreads: theory JinjaThreads.JMM_Typesafe
JinjaThreads: theory JinjaThreads.Preprocessor
JinjaThreads: theory JinjaThreads.JJ1WellForm
JinjaThreads: theory JinjaThreads.JMM_JVM
JinjaThreads: theory JinjaThreads.JVM_Main
JinjaThreads: theory JinjaThreads.Compiler
JinjaThreads: theory JinjaThreads.Exception_Tables
JinjaThreads: theory JinjaThreads.JMM_Common
JinjaThreads: theory JinjaThreads.BVSpec
JinjaThreads: theory JinjaThreads.EffectMono
JinjaThreads: theory JinjaThreads.TF_JVM
JinjaThreads: theory JinjaThreads.BVConform
JinjaThreads: theory JinjaThreads.BVExec
JinjaThreads: theory JinjaThreads.JMM_Typesafe2
JinjaThreads: theory JinjaThreads.LBVJVM
JinjaThreads: theory JinjaThreads.TypeComp
JinjaThreads: theory JinjaThreads.FWBisimDeadlock
JinjaThreads: theory JinjaThreads.FWBisimLift
JinjaThreads: theory JinjaThreads.J1
JinjaThreads: theory JinjaThreads.BVSpecTypeSafe
JinjaThreads: theory JinjaThreads.BVNoTypeError
JinjaThreads: theory JinjaThreads.JVMTau
JinjaThreads: theory JinjaThreads.BCVExec
JinjaThreads: theory JinjaThreads.JVMExec_Execute2
JinjaThreads: theory JinjaThreads.BVProgressThreaded
JinjaThreads: theory JinjaThreads.Common_Main
JinjaThreads: theory JinjaThreads.J1Deadlock
JinjaThreads: theory JinjaThreads.Execs
JinjaThreads: theory JinjaThreads.DefAssPreservation
JinjaThreads: theory JinjaThreads.Threaded
JinjaThreads: theory JinjaThreads.Progress
JinjaThreads: theory JinjaThreads.TypeSafe
JinjaThreads: theory JinjaThreads.J0
JinjaThreads: theory JinjaThreads.JMM_J
JinjaThreads: theory JinjaThreads.ProgressThreaded
JinjaThreads: theory JinjaThreads.J_Execute
JinjaThreads: theory JinjaThreads.J1JVMBisim
JinjaThreads: theory JinjaThreads.Deadlocked
JinjaThreads: theory JinjaThreads.DRF_J
JinjaThreads: theory JinjaThreads.JVMDeadlocked
JinjaThreads: theory JinjaThreads.DRF_JVM
JinjaThreads: theory JinjaThreads.JVM_Execute
JinjaThreads: theory JinjaThreads.JVM_Execute2
JinjaThreads: theory JinjaThreads.J_Main
JinjaThreads: theory JinjaThreads.J0Bisim
JinjaThreads: theory JinjaThreads.BV_Main
JinjaThreads: theory JinjaThreads.J0J1Bisim
JinjaThreads: theory JinjaThreads.Correctness1
JinjaThreads: theory JinjaThreads.Correctness1Threaded
JinjaThreads: theory JinjaThreads.Code_Generation
JinjaThreads: theory JinjaThreads.ApprenticeChallenge
JinjaThreads: theory JinjaThreads.BufferExample
JinjaThreads: theory JinjaThreads.Java2Jinja
JinjaThreads: theory JinjaThreads.Examples_Main
JinjaThreads: theory JinjaThreads.JMM_JVM_Typesafe
JinjaThreads: theory JinjaThreads.JMM_J_Typesafe
JinjaThreads: theory JinjaThreads.J1JVM
JinjaThreads: theory JinjaThreads.JVMJ1
JinjaThreads: theory JinjaThreads.Execute_Main
JinjaThreads: theory JinjaThreads.Correctness2
JinjaThreads: theory JinjaThreads.Correctness
JinjaThreads: theory JinjaThreads.JMM_Compiler
JinjaThreads: theory JinjaThreads.SC_Interp
JinjaThreads: theory JinjaThreads.Compiler_Main
JinjaThreads: theory JinjaThreads.JMM_Interp
JinjaThreads: theory JinjaThreads.JMM_Compiler_Type2
JinjaThreads: theory JinjaThreads.JMM
JinjaThreads: theory JinjaThreads.MM_Main
JinjaThreads: theory JinjaThreads.JinjaThreads
Preparing JinjaThreads/document ...
Finished JinjaThreads/document (0:01:44 elapsed time)
Preparing JinjaThreads/outline ...
Finished JinjaThreads/outline (0:00:42 elapsed time)
Timing JinjaThreads (8 threads, 3421.885s elapsed time, 15437.100s cpu time, 3541.407s GC time, factor 4.51)
Finished JinjaThreads (0:57:11 elapsed time, 4:17:59 cpu time, factor 4.51)
Building Flyspeck-Tame ...
Flyspeck-Tame: theory HOL-Library.AList
Flyspeck-Tame: theory HOL-Library.Code_Target_Int
Flyspeck-Tame: theory HOL-Library.While_Combinator
Flyspeck-Tame: theory Flyspeck-Tame.ListAux
Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat
Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order
Flyspeck-Tame: theory HOL-Library.IArray
Flyspeck-Tame: theory Flyspeck-Tame.RTranCl
Flyspeck-Tame: theory HOL-Library.Code_Target_Nat
Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso
Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral
Flyspeck-Tame: theory Flyspeck-Tame.Worklist
Flyspeck-Tame: theory Flyspeck-Tame.Arch
Flyspeck-Tame: theory Flyspeck-Tame.IArray_Syntax
Flyspeck-Tame: theory Flyspeck-Tame.ListSum
Flyspeck-Tame: theory Flyspeck-Tame.Rotation
Flyspeck-Tame: theory Flyspeck-Tame.Graph
Flyspeck-Tame: theory Flyspeck-Tame.Maps
Flyspeck-Tame: theory Trie.Trie
Flyspeck-Tame: theory Flyspeck-Tame.FaceDivision
Flyspeck-Tame: theory Flyspeck-Tame.GraphProps
Flyspeck-Tame: theory Flyspeck-Tame.Tame
Flyspeck-Tame: theory Trie.Tries
Flyspeck-Tame: theory Flyspeck-Tame.Enumerator
Flyspeck-Tame: theory Flyspeck-Tame.TameProps
Flyspeck-Tame: theory Flyspeck-Tame.EnumeratorProps
Flyspeck-Tame: theory Flyspeck-Tame.Plane
Flyspeck-Tame: theory Flyspeck-Tame.FaceDivisionProps
Flyspeck-Tame: theory Flyspeck-Tame.Plane1
Flyspeck-Tame: theory Flyspeck-Tame.Generator
Flyspeck-Tame: theory Flyspeck-Tame.TameEnum
Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux
Flyspeck-Tame: theory Flyspeck-Tame.Invariants
Flyspeck-Tame: theory Flyspeck-Tame.PlaneProps
Flyspeck-Tame: theory Flyspeck-Tame.ScoreProps
Flyspeck-Tame: theory Flyspeck-Tame.Plane1Props
Flyspeck-Tame: theory Flyspeck-Tame.LowerBound
Flyspeck-Tame: theory Flyspeck-Tame.GeneratorProps
Flyspeck-Tame: theory Flyspeck-Tame.TameEnumProps
Flyspeck-Tame: theory Flyspeck-Tame.ArchCompProps
Flyspeck-Tame: theory Flyspeck-Tame.Relative_Completeness
Preparing Flyspeck-Tame/document ...
Finished Flyspeck-Tame/document (0:00:17 elapsed time)
Preparing Flyspeck-Tame/outline ...
Finished Flyspeck-Tame/outline (0:00:08 elapsed time)
Timing Flyspeck-Tame (8 threads, 72.852s elapsed time, 387.384s cpu time, 23.952s GC time, factor 5.32)
Finished Flyspeck-Tame (0:01:40 elapsed time, 0:07:29 cpu time, factor 4.46)
Running Flyspeck-Tame-Computation ...
Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.ArchComp
Flyspeck-Tame-Computation: theory Flyspeck-Tame-Computation.Completeness
Timing Flyspeck-Tame-Computation (8 threads, 17494.965s elapsed time, 26360.567s cpu time, 1003.980s GC time, factor 1.51)
Finished Flyspeck-Tame-Computation (4:51:36 elapsed time, 7:19:22 cpu time, factor 1.51)
Building AWN ...
AWN: theory AWN.Lib
AWN: theory AWN.TransitionSystems
AWN: theory AWN.AWN
AWN: theory AWN.Invariants
AWN: theory AWN.OInvariants
AWN: theory AWN.AWN_Cterms
AWN: theory AWN.AWN_SOS
AWN: theory AWN.OAWN_SOS
AWN: theory AWN.AWN_Labels
AWN: theory AWN.Inv_Cterms
AWN: theory AWN.AWN_Invariants
AWN: theory AWN.Pnet
AWN: theory AWN.Closed
AWN: theory AWN.AWN_SOS_Labels
AWN: theory AWN.Qmsg
AWN: theory AWN.OAWN_Invariants
AWN: theory AWN.OAWN_SOS_Labels
AWN: theory AWN.ONode_Lifting
AWN: theory AWN.OPnet
AWN: theory AWN.OPnet_Lifting
AWN: theory AWN.OClosed_Lifting
AWN: theory AWN.OAWN_Convert
AWN: theory AWN.OClosed_Transfer
AWN: theory AWN.Qmsg_Lifting
AWN: theory AWN.AWN_Main
AWN: theory AWN.Toy
AWN: theory AWN.AWN_Term_Graph
Preparing AWN/document ...
Finished AWN/document (0:00:12 elapsed time)
Preparing AWN/outline ...
Finished AWN/outline (0:00:07 elapsed time)
Timing AWN (8 threads, 43.040s elapsed time, 209.423s cpu time, 6.908s GC time, factor 4.87)
Finished AWN (0:01:03 elapsed time, 0:04:09 cpu time, factor 3.95)
Running AODV ...
AODV: theory AODV.Aodv_Basic
AODV: theory AODV.A_Norreqid
AODV: theory AODV.Aodv_Data
AODV: theory AODV.Aodv_Message
AODV: theory AODV.C_Gtobcast
AODV: theory AODV.B_Fwdrreps
AODV: theory AODV.D_Fwdrreqs
AODV: theory AODV.E_All_ABCD
AODV: theory AODV.A_Aodv_Data
AODV: theory AODV.A_Aodv_Message
AODV: theory AODV.C_Aodv_Data
AODV: theory AODV.C_Aodv_Message
AODV: theory AODV.B_Aodv_Data
AODV: theory AODV.B_Aodv_Message
AODV: theory AODV.C_Fresher
AODV: theory AODV.Fresher
AODV: theory AODV.A_Fresher
AODV: theory AODV.B_Fresher
AODV: theory AODV.D_Aodv_Data
AODV: theory AODV.D_Aodv_Message
AODV: theory AODV.E_Aodv_Data
AODV: theory AODV.E_Aodv_Message
AODV: theory AODV.A_Aodv
AODV: theory AODV.Aodv
AODV: theory AODV.B_Aodv
AODV: theory AODV.C_Aodv
AODV: theory AODV.E_Fresher
AODV: theory AODV.D_Fresher
AODV: theory AODV.D_Aodv
AODV: theory AODV.E_Aodv
AODV: theory AODV.A_Aodv_Predicates
AODV: theory AODV.A_OAodv
AODV: theory AODV.A_Loop_Freedom
AODV: theory AODV.A_Quality_Increases
AODV: theory AODV.A_Seq_Invariants
AODV: theory AODV.A_Global_Invariants
AODV: theory AODV.A_Aodv_Loop_Freedom
AODV: theory AODV.C_Aodv_Predicates
AODV: theory AODV.C_OAodv
AODV: theory AODV.C_Loop_Freedom
AODV: theory AODV.C_Quality_Increases
AODV: theory AODV.C_Seq_Invariants
AODV: theory AODV.C_Global_Invariants
AODV: theory AODV.C_Aodv_Loop_Freedom
AODV: theory AODV.Aodv_Predicates
AODV: theory AODV.OAodv
AODV: theory AODV.Loop_Freedom
AODV: theory AODV.Quality_Increases
AODV: theory AODV.Seq_Invariants
AODV: theory AODV.Global_Invariants
AODV: theory AODV.Aodv_Loop_Freedom
AODV: theory AODV.B_Aodv_Predicates
AODV: theory AODV.B_OAodv
AODV: theory AODV.B_Loop_Freedom
AODV: theory AODV.B_Quality_Increases
AODV: theory AODV.B_Seq_Invariants
AODV: theory AODV.B_Global_Invariants
AODV: theory AODV.E_Aodv_Predicates
AODV: theory AODV.E_OAodv
AODV: theory AODV.E_Loop_Freedom
AODV: theory AODV.E_Quality_Increases
AODV: theory AODV.E_Seq_Invariants
AODV: theory AODV.B_Aodv_Loop_Freedom
AODV: theory AODV.E_Global_Invariants
AODV: theory AODV.E_Aodv_Loop_Freedom
AODV: theory AODV.D_Aodv_Predicates
AODV: theory AODV.D_Loop_Freedom
AODV: theory AODV.D_Quality_Increases
AODV: theory AODV.D_Seq_Invariants
AODV: theory AODV.D_OAodv
AODV: theory AODV.D_Global_Invariants
AODV: theory AODV.D_Aodv_Loop_Freedom
AODV: theory AODV.All
Preparing AODV/document ...
Finished AODV/document (0:00:24 elapsed time)
Preparing AODV/outline ...
Finished AODV/outline (0:00:14 elapsed time)
Timing AODV (8 threads, 5523.939s elapsed time, 33295.488s cpu time, 1499.958s GC time, factor 6.03)
Finished AODV (1:32:05 elapsed time, 9:15:00 cpu time, factor 6.03)
Building Word_Lib ...
Word_Lib: theory Word_Lib.Enumeration
Word_Lib: theory Word_Lib.Even_More_List
Word_Lib: theory HOL-Library.Phantom_Type
Word_Lib: theory HOL-Library.Sublist
Word_Lib: theory Word_Lib.More_Bit_Ring
Word_Lib: theory Word_Lib.More_Misc
Word_Lib: theory HOL-Library.Cardinality
Word_Lib: theory HOL-Library.Numeral_Type
Word_Lib: theory Word_Lib.More_Sublist
Word_Lib: theory HOL-Library.Type_Length
Word_Lib: theory HOL-Library.Word
Word_Lib: theory Word_Lib.More_Arithmetic
Word_Lib: theory Word_Lib.Legacy_Aliases
Word_Lib: theory Word_Lib.More_Divides
Word_Lib: theory Word_Lib.More_Word
Word_Lib: theory Word_Lib.Strict_part_mono
Word_Lib: theory Word_Lib.Bit_Comprehension
Word_Lib: theory Word_Lib.Bit_Shifts_Infix_Syntax
Word_Lib: theory HOL-Library.Signed_Division
Word_Lib: theory Word_Lib.Least_significant_bit
Word_Lib: theory Word_Lib.Signed_Division_Word
Word_Lib: theory Word_Lib.Aligned
Word_Lib: theory Word_Lib.Most_significant_bit
Word_Lib: theory Word_Lib.Generic_set_bit
Word_Lib: theory Word_Lib.Next_and_Prev
Word_Lib: theory Word_Lib.Bits_Int
Word_Lib: theory Word_Lib.Singleton_Bit_Shifts
Word_Lib: theory Word_Lib.Many_More
Word_Lib: theory Word_Lib.Typedef_Morphisms
Word_Lib: theory HOL-Eisbach.Eisbach
Word_Lib: theory Word_Lib.Bit_Comprehension_Int
Word_Lib: theory Word_Lib.Signed_Words
Word_Lib: theory Word_Lib.Hex_Words
Word_Lib: theory Word_Lib.Word_Syntax
Word_Lib: theory Word_Lib.Enumeration_Word
Word_Lib: theory Word_Lib.Type_Syntax
Word_Lib: theory Word_Lib.Syntax_Bundles
Word_Lib: theory Word_Lib.Sgn_Abs
Word_Lib: theory Word_Lib.Rsplit
Word_Lib: theory Word_Lib.Reversed_Bit_Lists
Word_Lib: theory Word_Lib.Norm_Words
Word_Lib: theory Word_Lib.Word_Names
Word_Lib: theory Word_Lib.Word_16
Word_Lib: theory HOL-Eisbach.Eisbach_Tools
Word_Lib: theory Word_Lib.Word_EqI
Word_Lib: theory Word_Lib.Bitwise
Word_Lib: theory Word_Lib.Boolean_Inequalities
Word_Lib: theory Word_Lib.Bitwise_Signed
Word_Lib: theory Word_Lib.Word_Lemmas
Word_Lib: theory Word_Lib.Word_8
Word_Lib: theory Word_Lib.More_Word_Operations
Word_Lib: theory Word_Lib.Word_32
Word_Lib: theory Word_Lib.Word_64
Word_Lib: theory Word_Lib.Machine_Word_64_Basics
Word_Lib: theory Word_Lib.Machine_Word_64
Word_Lib: theory Word_Lib.Machine_Word_32_Basics
Word_Lib: theory Word_Lib.Word_Lib_Sumo
Word_Lib: theory Word_Lib.Machine_Word_32
Word_Lib: theory Word_Lib.Guide
Word_Lib: theory Word_Lib.Examples
Preparing Word_Lib/document ...
Finished Word_Lib/document (0:00:10 elapsed time)
Preparing Word_Lib/outline ...
Finished Word_Lib/outline (0:00:07 elapsed time)
Timing Word_Lib (8 threads, 51.970s elapsed time, 260.694s cpu time, 12.146s GC time, factor 5.02)
Finished Word_Lib (0:01:05 elapsed time, 0:04:48 cpu time, factor 4.40)
Building IP_Addresses ...
IP_Addresses: theory IP_Addresses.NumberWang_IPv4
IP_Addresses: theory IP_Addresses.NumberWang_IPv6
IP_Addresses: theory HOL-Library.Cancellation
IP_Addresses: theory HOL-Library.Infinite_Set
IP_Addresses: theory HOL-Library.Option_ord
IP_Addresses: theory HOL-Library.Multiset
IP_Addresses: theory HOL-ex.Quicksort
IP_Addresses: theory Automatic_Refinement.Misc
IP_Addresses: theory IP_Addresses.Hs_Compat
IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
IP_Addresses: theory HOL-Library.Code_Abstract_Nat
IP_Addresses: theory IP_Addresses.WordInterval
IP_Addresses: theory HOL-Library.Product_Lexorder
IP_Addresses: theory HOL-Library.Code_Target_Nat
IP_Addresses: theory IP_Addresses.Lib_List_toString
IP_Addresses: theory IP_Addresses.Lib_Word_toString
IP_Addresses: theory IP_Addresses.WordInterval_Sorted
IP_Addresses: theory IP_Addresses.IP_Address
IP_Addresses: theory IP_Addresses.IPv4
IP_Addresses: theory IP_Addresses.Prefix_Match
IP_Addresses: theory IP_Addresses.IPv6
IP_Addresses: theory IP_Addresses.CIDR_Split
IP_Addresses: theory IP_Addresses.IP_Address_Parser
IP_Addresses: theory IP_Addresses.IP_Address_toString
IP_Addresses: theory IP_Addresses.Prefix_Match_toString
Preparing IP_Addresses/document ...
Finished IP_Addresses/document (0:00:04 elapsed time)
Preparing IP_Addresses/outline ...
Finished IP_Addresses/outline (0:00:03 elapsed time)
Timing IP_Addresses (8 threads, 226.197s elapsed time, 748.275s cpu time, 36.791s GC time, factor 3.31)
Finished IP_Addresses (0:04:03 elapsed time, 0:13:04 cpu time, factor 3.22)
Building Simple_Firewall ...
Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
Simple_Firewall: theory HOL-Library.Char_ord
Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
Simple_Firewall: theory Simple_Firewall.GroupF
Simple_Firewall: theory Simple_Firewall.List_Product_More
Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
Simple_Firewall: theory Simple_Firewall.Option_Helpers
Simple_Firewall: theory Simple_Firewall.Iface
Simple_Firewall: theory Simple_Firewall.L4_Protocol
Simple_Firewall: theory Simple_Firewall.Simple_Packet
Simple_Firewall: theory Simple_Firewall.Primitives_toString
Simple_Firewall: theory Simple_Firewall.SimpleFw_Syntax
Simple_Firewall: theory Simple_Firewall.SimpleFw_Semantics
Simple_Firewall: theory Simple_Firewall.SimpleFw_toString
Simple_Firewall: theory Simple_Firewall.Service_Matrix
Simple_Firewall: theory Simple_Firewall.Generic_SimpleFw
Simple_Firewall: theory Simple_Firewall.Shadowed
Preparing Simple_Firewall/document ...
Finished Simple_Firewall/document (0:00:08 elapsed time)
Preparing Simple_Firewall/outline ...
Finished Simple_Firewall/outline (0:00:06 elapsed time)
Timing Simple_Firewall (8 threads, 19.781s elapsed time, 82.416s cpu time, 2.804s GC time, factor 4.17)
Finished Simple_Firewall (0:00:33 elapsed time, 0:01:50 cpu time, factor 3.27)
Building Routing ...
Routing: theory Routing.Linorder_Helper
Routing: theory HOL-Library.Adhoc_Overloading
Routing: theory Pure-ex.Guess
Routing: theory HOL-Library.Monad_Syntax
Routing: theory Routing.Routing_Table
Routing: theory Routing.IpRoute_Parser
Routing: theory Routing.Linux_Router
Preparing Routing/document ...
Finished Routing/document (0:00:02 elapsed time)
Preparing Routing/outline ...
Finished Routing/outline (0:00:02 elapsed time)
Timing Routing (8 threads, 9.360s elapsed time, 31.906s cpu time, 0.836s GC time, factor 3.41)
Finished Routing (0:00:21 elapsed time, 0:00:54 cpu time, factor 2.54)
Building Iptables_Semantics ...
Iptables_Semantics: theory Iptables_Semantics.List_Misc
Iptables_Semantics: theory Iptables_Semantics.Negation_Type
Iptables_Semantics: theory Iptables_Semantics.WordInterval_Lists
Iptables_Semantics: theory HOL-Library.LaTeXsugar
Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
Iptables_Semantics: theory Iptables_Semantics.Ternary
Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
Iptables_Semantics: theory Native_Word.Code_Int_Integer_Conversion
Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
Iptables_Semantics: theory HOL-Library.Code_Target_Int
Iptables_Semantics: theory Iptables_Semantics.Conntrack_State
Iptables_Semantics: theory Iptables_Semantics.L4_Protocol_Flags
Iptables_Semantics: theory Native_Word.Code_Target_Integer_Bit
Iptables_Semantics: theory Iptables_Semantics.Word_Upto
Iptables_Semantics: theory Iptables_Semantics.Firewall_Common
Iptables_Semantics: theory Iptables_Semantics.IpAddresses
Iptables_Semantics: theory Iptables_Semantics.Ports
Iptables_Semantics: theory Iptables_Semantics.Tagged_Packet
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Syntax
Iptables_Semantics: theory Native_Word.Code_Target_Int_Bit
Iptables_Semantics: theory Iptables_Semantics.Matching_Ternary
Iptables_Semantics: theory Iptables_Semantics.Semantics
Iptables_Semantics: theory Iptables_Semantics.Semantics_Goto
Iptables_Semantics: theory Iptables_Semantics.Alternative_Semantics
Iptables_Semantics: theory Iptables_Semantics.Matching
Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
Iptables_Semantics: theory Iptables_Semantics.Semantics_Stateful
Iptables_Semantics: theory Iptables_Semantics.Call_Return_Unfolding
Iptables_Semantics: theory Iptables_Semantics.Semantics_Ternary
Iptables_Semantics: theory Iptables_Semantics.Unknown_Match_Tacs
Iptables_Semantics: theory Iptables_Semantics.Matching_Embeddings
Iptables_Semantics: theory Iptables_Semantics.Fixed_Action
Iptables_Semantics: theory Iptables_Semantics.Optimizing
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher_Generic
Iptables_Semantics: theory Iptables_Semantics.Normalized_Matches
Iptables_Semantics: theory Iptables_Semantics.Negation_Type_Matching
Iptables_Semantics: theory Iptables_Semantics.Primitive_Normalization
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Matcher
Iptables_Semantics: theory Iptables_Semantics.MatchExpr_Fold
Iptables_Semantics: theory Iptables_Semantics.Ipassmt
Iptables_Semantics: theory Iptables_Semantics.Routing_IpAssmt
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_Lemmas
Iptables_Semantics: theory Iptables_Semantics.Conntrack_State_Transform
Iptables_Semantics: theory Iptables_Semantics.Example_Semantics
Iptables_Semantics: theory Iptables_Semantics.Common_Primitive_toString
Iptables_Semantics: theory Iptables_Semantics.Interfaces_Normalize
Iptables_Semantics: theory Iptables_Semantics.IpAddresses_Normalize
Iptables_Semantics: theory Iptables_Semantics.Ports_Normalize
Iptables_Semantics: theory Iptables_Semantics.Protocols_Normalize
Iptables_Semantics: theory Iptables_Semantics.No_Spoof
Iptables_Semantics: theory Iptables_Semantics.Output_Interface_Replace
Iptables_Semantics: theory Iptables_Semantics.Interface_Replace
Iptables_Semantics: theory Iptables_Semantics.Transform
Iptables_Semantics: theory Iptables_Semantics.Primitive_Abstract
Iptables_Semantics: theory Iptables_Semantics.SimpleFw_Compliance
Iptables_Semantics: theory Iptables_Semantics.Code_Interface
Iptables_Semantics: theory Iptables_Semantics.Semantics_Embeddings
Iptables_Semantics: theory Iptables_Semantics.Access_Matrix_Embeddings
Iptables_Semantics: theory Iptables_Semantics.Iptables_Semantics
Iptables_Semantics: theory Iptables_Semantics.No_Spoof_Embeddings
Iptables_Semantics: theory Iptables_Semantics.Parser
Iptables_Semantics: theory Iptables_Semantics.Parser6
Iptables_Semantics: theory Iptables_Semantics.Documentation
Iptables_Semantics: theory Iptables_Semantics.Code_haskell
Preparing Iptables_Semantics/document ...
Finished Iptables_Semantics/document (0:00:24 elapsed time)
Preparing Iptables_Semantics/outline ...
Finished Iptables_Semantics/outline (0:00:12 elapsed time)
Timing Iptables_Semantics (8 threads, 113.723s elapsed time, 555.067s cpu time, 51.939s GC time, factor 4.88)
Finished Iptables_Semantics (0:02:24 elapsed time, 0:10:21 cpu time, factor 4.29)
Building Iptables_Semantics_Examples ...
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Contrived_Example
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Ports_Fail
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Small_Examples
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation
Preparing Iptables_Semantics_Examples/document ...
Finished Iptables_Semantics_Examples/document (0:00:05 elapsed time)
Preparing Iptables_Semantics_Examples/outline ...
Finished Iptables_Semantics_Examples/outline (0:00:05 elapsed time)
Timing Iptables_Semantics_Examples (8 threads, 220.416s elapsed time, 1280.995s cpu time, 106.109s GC time, factor 5.81)
Finished Iptables_Semantics_Examples (0:03:55 elapsed time, 0:21:50 cpu time, factor 5.56)
Running Iptables_Semantics_Examples_Big ...
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Simple_FW
Preparing Iptables_Semantics_Examples_Big/document ...
Finished Iptables_Semantics_Examples_Big/document (0:00:04 elapsed time)
Preparing Iptables_Semantics_Examples_Big/outline ...
Finished Iptables_Semantics_Examples_Big/outline (0:00:04 elapsed time)
Run out of store - interrupting threads
Run out of store - interrupting threads
Timing Iptables_Semantics_Examples_Big (8 threads, 4006.847s elapsed time, 23503.603s cpu time, 4752.355s GC time, factor 5.87)
Finished Iptables_Semantics_Examples_Big (1:06:52 elapsed time, 6:31:54 cpu time, factor 5.86)
Building HOL-Library ...
HOL-Library: theory HOL-Library.README
HOL-Library: theory HOL-Library.AList
HOL-Library: theory HOL-Library.Adhoc_Overloading
HOL-Library: theory HOL-Library.BNF_Axiomatization
HOL-Library: theory HOL-Library.Centered_Division
HOL-Library: theory HOL-Library.BNF_Corec
HOL-Library: theory HOL-Library.Cancellation
HOL-Library: theory HOL-Library.Case_Converter
HOL-Library: theory HOL-Library.Char_ord
HOL-Library: theory HOL-Library.Code_Abstract_Char
HOL-Library: theory HOL-Library.Monad_Syntax
HOL-Library: theory HOL-Library.Code_Abstract_Nat
HOL-Library: theory HOL-Library.Code_Prolog
HOL-Library: theory HOL-Library.State_Monad
HOL-Library: theory HOL-Library.Code_Binary_Nat
HOL-Library: theory HOL-Library.Code_Lazy
HOL-Library: theory HOL-Library.Simps_Case_Conv
HOL-Library: theory HOL-Library.Extended
HOL-Library: theory HOL-Library.Multiset
HOL-Library: theory HOL-Library.Code_Target_Nat
HOL-Library: theory HOL-Library.Code_Target_Int
HOL-Library: theory HOL-Library.Code_Test
HOL-Library: theory HOL-Library.Code_Target_Numeral
HOL-Library: theory HOL-Library.Combine_PER
HOL-Library: theory HOL-Library.Comparator
HOL-Library: theory HOL-Library.DAList
HOL-Library: theory HOL-Library.Complete_Partial_Order2
HOL-Library: theory HOL-Library.Conditional_Parametricity
HOL-Library: theory HOL-Library.Confluence
HOL-Library: theory HOL-Library.Datatype_Records
HOL-Library: theory HOL-Library.Confluent_Quotient
HOL-Library: theory HOL-Library.Dlist
HOL-Library: theory HOL-Library.Debug
HOL-Library: theory HOL-Library.Dual_Ordered_Lattice
HOL-Library: theory HOL-Library.Fun_Lexorder
HOL-Library: theory HOL-Library.FuncSet
HOL-Library: theory HOL-Library.Function_Algebras
HOL-Library: theory HOL-Library.Function_Division
HOL-Library: theory HOL-Library.Groups_Big_Fun
HOL-Library: theory HOL-Library.IArray
HOL-Library: theory HOL-Library.Infinite_Set
HOL-Library: theory HOL-Library.LaTeXsugar
HOL-Library: theory HOL-Library.Disjoint_Sets
HOL-Library: theory HOL-Library.Lattice_Constructions
HOL-Library: theory HOL-Library.Omega_Words_Fun
HOL-Library: theory HOL-Library.ListVector
HOL-Library: theory HOL-Library.List_Lenlexorder
HOL-Library: theory HOL-Library.List_Lexorder
HOL-Library: theory HOL-Library.Mapping
HOL-Library: theory HOL-Library.More_List
HOL-Library: theory HOL-Library.NList
HOL-Library: theory HOL-Library.Nat_Bijection
HOL-Library: theory HOL-Library.Poly_Mapping
HOL-Library: theory HOL-Library.Stream
HOL-Library: theory HOL-Library.Old_Datatype
HOL-Library: theory HOL-Library.AList_Mapping
HOL-Library: theory HOL-Library.Old_Recdef
HOL-Library: theory HOL-Library.Open_State_Syntax
HOL-Library: theory HOL-Library.Option_ord
HOL-Library: theory HOL-Library.Parallel
HOL-Library: theory HOL-Library.Pattern_Aliases
HOL-Library: theory HOL-Library.Phantom_Type
HOL-Library: theory HOL-Library.Power_By_Squaring
HOL-Library: theory HOL-Library.Predicate_Compile_Alternative_Defs
HOL-Library: theory HOL-Library.Preorder
HOL-Library: theory HOL-Library.DAList_Multiset
HOL-Library: theory HOL-Library.Multiset_Order
HOL-Library: theory HOL-Library.Product_Lexorder
HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
HOL-Library: theory HOL-Library.Cardinality
HOL-Library: theory HOL-Library.Product_Plus
HOL-Library: theory HOL-Library.Product_Order
HOL-Library: theory HOL-Library.Quotient_Syntax
HOL-Library: theory HOL-Library.Quotient_Option
HOL-Library: theory HOL-Library.Quotient_Product
HOL-Library: theory HOL-Library.Quotient_Set
HOL-Library: theory HOL-Library.Quotient_Sum
HOL-Library: theory HOL-Library.Quotient_Type
HOL-Library: theory HOL-Library.Quotient_List
HOL-Library: theory HOL-Library.Finite_Lattice
HOL-Library: theory HOL-Library.RBT_Impl
HOL-Library: theory HOL-Library.Realizers
HOL-Library: theory HOL-Library.Reflection
HOL-Library: theory HOL-Library.Refute
HOL-Library: theory HOL-Library.Rewrite
HOL-Library: theory HOL-Library.Set_Algebras
HOL-Library: theory HOL-Library.Code_Cardinality
HOL-Library: theory HOL-Library.Numeral_Type
HOL-Library: theory HOL-Library.Signed_Division
HOL-Library: theory HOL-Library.Sorting_Algorithms
HOL-Library: theory HOL-Library.Sublist
HOL-Library: theory HOL-Library.Transitive_Closure_Table
HOL-Library: theory HOL-Library.Type_Length
HOL-Library: theory HOL-Library.Tree
HOL-Library: theory HOL-Library.Uprod
HOL-Library: theory HOL-Library.While_Combinator
HOL-Library: theory HOL-Library.Z2
HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
HOL-Library: theory HOL-Library.Saturated
HOL-Library: theory HOL-Library.Word
HOL-Library: theory HOL-Library.Countable
HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
HOL-Library: theory HOL-Library.Prefix_Order
HOL-Library: theory HOL-Library.Subseq_Order
HOL-Library: theory HOL-Library.Complex_Order
HOL-Library: theory HOL-Library.Diagonal_Subsequence
HOL-Library: theory HOL-Library.Discrete
HOL-Library: theory HOL-Library.Going_To_Filter
HOL-Library: theory HOL-Library.Indicator_Function
HOL-Library: theory HOL-Library.Infinite_Typeclass
HOL-Library: theory HOL-Library.Landau_Symbols
HOL-Library: theory HOL-Library.Lattice_Algebras
HOL-Library: theory HOL-Library.Countable_Set
HOL-Library: theory HOL-Library.FSet
HOL-Library: theory HOL-Library.Countable_Complete_Lattices
HOL-Library: theory HOL-Library.Tree_Multiset
HOL-Library: theory HOL-Library.Countable_Set_Type
HOL-Library: theory HOL-Library.Equipollence
HOL-Library: theory HOL-Library.Set_Idioms
HOL-Library: theory HOL-Library.Liminf_Limsup
HOL-Library: theory HOL-Library.Log_Nat
HOL-Library: theory HOL-Library.Ramsey
HOL-Library: theory HOL-Library.Lub_Glb
HOL-Library: theory HOL-Library.Nonpos_Ints
HOL-Library: theory HOL-Library.Finite_Map
HOL-Library: theory HOL-Library.OptionalSugar
HOL-Library: theory HOL-Library.Order_Continuity
HOL-Library: theory HOL-Library.Periodic_Fun
HOL-Library: theory HOL-Library.Quadratic_Discriminant
HOL-Library: theory HOL-Library.Real_Mod
HOL-Library: theory HOL-Library.Sum_of_Squares
HOL-Library: theory HOL-Library.Extended_Nat
HOL-Library: theory HOL-Library.Tree_Real
HOL-Library: theory HOL-Library.Interval
HOL-Library: theory HOL-Library.Float
HOL-Library: theory HOL-Library.Extended_Real
HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
HOL-Library: theory HOL-Library.Code_Target_Numeral_Float
HOL-Library: theory HOL-Library.Interval_Float
HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
HOL-Library: theory HOL-Library.Disjoint_FSets
HOL-Library: theory HOL-Library.Library
HOL-Library: theory HOL-Library.RBT
HOL-Library: theory HOL-Library.RBT_Mapping
HOL-Library: theory HOL-Library.RBT_Set
Preparing HOL-Library/document ...
Finished HOL-Library/document (0:01:02 elapsed time)
Preparing HOL-Library/outline ...
Finished HOL-Library/outline (0:00:38 elapsed time)
Timing HOL-Library (8 threads, 304.362s elapsed time, 1222.480s cpu time, 47.339s GC time, factor 4.02)
Finished HOL-Library (0:05:37 elapsed time, 0:21:35 cpu time, factor 3.84)
Building Category3 ...
Category3: theory HOL-Cardinals.Fun_More
Category3: theory HOL-Cardinals.Order_Relation_More
Category3: theory HereditarilyFinite.HF
Category3: theory Category3.Category
Category3: theory HOL-Cardinals.Order_Union
Category3: theory HOL-Cardinals.Wellorder_Extension
Category3: theory HOL-Cardinals.Wellfounded_More
Category3: theory HOL-Cardinals.Wellorder_Relation
Category3: theory Category3.ConcreteCategory
Category3: theory Category3.DiscreteCategory
Category3: theory Category3.EpiMonoIso
Category3: theory HOL-Cardinals.Wellorder_Embedding
Category3: theory HOL-Cardinals.Wellorder_Constructions
Category3: theory Category3.DualCategory
Category3: theory Category3.InitialTerminal
Category3: theory Category3.ProductCategory
Category3: theory HOL-Cardinals.Cardinal_Order_Relation
Category3: theory HOL-Cardinals.Ordinal_Arithmetic
Category3: theory Category3.FreeCategory
Category3: theory Category3.Functor
Category3: theory HOL-Cardinals.Cardinal_Arithmetic
Category3: theory HOL-Cardinals.Cardinals
Category3: theory ZFC_in_HOL.ZFC_Library
Category3: theory ZFC_in_HOL.ZFC_in_HOL
Category3: theory ZFC_in_HOL.ZFC_Cardinals
Category3: theory Category3.NaturalTransformation
Category3: theory Category3.Subcategory
Category3: theory Category3.SetCategory
Category3: theory Category3.BinaryFunctor
Category3: theory Category3.SetCat
Category3: theory Category3.FunctorCategory
Category3: theory Category3.Yoneda
Category3: theory Category3.Adjunction
Category3: theory Category3.EquivalenceOfCategories
Category3: theory Category3.Limit
Category3: theory Category3.CategoryWithPullbacks
Category3: theory Category3.ZFC_SetCat
Category3: theory Category3.ZFC_SetCat_Interp
Category3: theory Category3.CartesianCategory
Category3: theory Category3.CartesianClosedCategory
Category3: theory Category3.CategoryWithFiniteLimits
Category3: theory Category3.HF_SetCat
Category3: theory Category3.HF_SetCat_Interp
Preparing Category3/document ...
Finished Category3/document (0:00:29 elapsed time)
Preparing Category3/outline ...
Finished Category3/outline (0:00:11 elapsed time)
Timing Category3 (8 threads, 344.988s elapsed time, 1758.216s cpu time, 121.800s GC time, factor 5.10)
Finished Category3 (0:06:17 elapsed time, 0:30:27 cpu time, factor 4.84)
Building MonoidalCategory ...
MonoidalCategory: theory MonoidalCategory.MonoidalCategory
MonoidalCategory: theory MonoidalCategory.MonoidalFunctor
MonoidalCategory: theory MonoidalCategory.CartesianMonoidalCategory
MonoidalCategory: theory MonoidalCategory.FreeMonoidalCategory
Preparing MonoidalCategory/document ...
Finished MonoidalCategory/document (0:00:13 elapsed time)
Preparing MonoidalCategory/outline ...
Finished MonoidalCategory/outline (0:00:06 elapsed time)
Timing MonoidalCategory (8 threads, 218.710s elapsed time, 813.742s cpu time, 72.638s GC time, factor 3.72)
Finished MonoidalCategory (0:04:00 elapsed time, 0:14:17 cpu time, factor 3.57)
Running Bicategory ...
Bicategory: theory Bicategory.IsomorphismClass
Bicategory: theory Bicategory.Prebicategory
Bicategory: theory Bicategory.Bicategory
Bicategory: theory Bicategory.Coherence
Bicategory: theory Bicategory.ConcreteBicategory
Bicategory: theory Bicategory.InternalEquivalence
Bicategory: theory Bicategory.Subbicategory
Bicategory: theory Bicategory.CanonicalIsos
Bicategory: theory Bicategory.Pseudofunctor
Bicategory: theory Bicategory.Strictness
Bicategory: theory Bicategory.CatBicat
Bicategory: theory Bicategory.InternalAdjunction
Bicategory: theory Bicategory.PseudonaturalTransformation
Bicategory: theory Bicategory.Tabulation
Bicategory: theory Bicategory.SpanBicategory
Bicategory: theory Bicategory.EquivalenceOfBicategories
Bicategory: theory Bicategory.Modification
Bicategory: theory Bicategory.BicategoryOfSpans
Preparing Bicategory/document ...
Finished Bicategory/document (0:01:42 elapsed time)
Preparing Bicategory/outline ...
Finished Bicategory/outline (0:00:21 elapsed time)
Timing Bicategory (8 threads, 2848.279s elapsed time, 10326.874s cpu time, 1549.228s GC time, factor 3.63)
Finished Bicategory (0:47:34 elapsed time, 2:52:30 cpu time, factor 3.63)
Building ConcurrentIMP ...
ConcurrentIMP: theory ConcurrentIMP.CIMP_pred
ConcurrentIMP: theory ConcurrentIMP.Infinite_Sequences
ConcurrentIMP: theory ConcurrentIMP.LTL
ConcurrentIMP: theory ConcurrentIMP.CIMP_lang
ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg
ConcurrentIMP: theory ConcurrentIMP.CIMP_vcg_rules
ConcurrentIMP: theory ConcurrentIMP.CIMP
ConcurrentIMP: theory ConcurrentIMP.CIMP_locales
ConcurrentIMP: theory ConcurrentIMP.CIMP_one_place_buffer
ConcurrentIMP: theory ConcurrentIMP.CIMP_unbounded_buffer
Preparing ConcurrentIMP/document ...
Finished ConcurrentIMP/document (0:00:05 elapsed time)
Preparing ConcurrentIMP/outline ...
Finished ConcurrentIMP/outline (0:00:05 elapsed time)
Timing ConcurrentIMP (8 threads, 21.966s elapsed time, 75.929s cpu time, 2.919s GC time, factor 3.46)
Finished ConcurrentIMP (0:00:38 elapsed time, 0:01:49 cpu time, factor 2.84)
Running ConcurrentGC ...
ConcurrentGC: theory ConcurrentGC.Model
ConcurrentGC: theory ConcurrentGC.Proofs_Basis
ConcurrentGC: theory ConcurrentGC.Global_Invariants
ConcurrentGC: theory ConcurrentGC.Local_Invariants
ConcurrentGC: theory ConcurrentGC.Tactics
ConcurrentGC: theory ConcurrentGC.Concrete_heap
ConcurrentGC: theory ConcurrentGC.Global_Invariants_Lemmas
ConcurrentGC: theory ConcurrentGC.Concrete
ConcurrentGC: theory ConcurrentGC.Global_Noninterference
ConcurrentGC: theory ConcurrentGC.Local_Invariants_Lemmas
ConcurrentGC: theory ConcurrentGC.Initial_Conditions
ConcurrentGC: theory ConcurrentGC.MarkObject
ConcurrentGC: theory ConcurrentGC.Noninterference
ConcurrentGC: theory ConcurrentGC.Phases
ConcurrentGC: theory ConcurrentGC.StrongTricolour
ConcurrentGC: theory ConcurrentGC.TSO
ConcurrentGC: theory ConcurrentGC.Valid_Refs
ConcurrentGC: theory ConcurrentGC.Worklists
ConcurrentGC: theory ConcurrentGC.Proofs
Preparing ConcurrentGC/document ...
Finished ConcurrentGC/document (0:00:11 elapsed time)
Preparing ConcurrentGC/outline ...
Finished ConcurrentGC/outline (0:00:07 elapsed time)
Timing ConcurrentGC (8 threads, 1088.408s elapsed time, 6466.827s cpu time, 359.834s GC time, factor 5.94)
Finished ConcurrentGC (0:18:11 elapsed time, 1:47:53 cpu time, factor 5.93)
Presentation in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info"
Presenting Pure in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/Pure/Pure" ...
Presenting HOL in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL" ...
Presenting Category3 in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Category3" ...
Presenting AODV in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV" ...
Presenting AWN in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN" ...
Presenting Flyspeck-Tame in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame" ...
Presenting HOL-Library in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library" ...
Presenting Flyspeck-Tame-Computation in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame-Computation" ...
Presenting document AWN/document
Presenting document Category3/document
Presenting document AWN/outline
Presenting document Category3/outline
Presenting theory "Flyspeck-Tame-Computation.ArchComp"
Presenting document Flyspeck-Tame/document
Presenting theory "AWN.Lib"
Presenting document Flyspeck-Tame/outline
Presenting document AODV/document
Presenting document AODV/outline
Presenting theory "AODV.Aodv_Basic"
Presenting theory "Flyspeck-Tame-Computation.Completeness"
Presenting theory "AWN.TransitionSystems"
Presenting MonoidalCategory in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/MonoidalCategory" ...
Presenting document MonoidalCategory/document
Presenting document MonoidalCategory/outline
Presenting theory "Category3.Category"
Presenting document HOL/document
Presenting document HOL/outline
Presenting theory "AWN.Invariants"
Presenting document HOL-Library/document
Presenting document HOL-Library/outline
Presenting theory "HOL-Library.README"
Presenting theory "Category3.EpiMonoIso"
Presenting theory "Category3.DualCategory"
Presenting theory "Flyspeck-Tame.ListAux"
Presenting theory "Flyspeck-Tame.Quasi_Order"
Presenting theory "Category3.ConcreteCategory"
Presenting theory "Category3.InitialTerminal"
Presenting theory "HOL-Library.AList"
Presenting theory "AWN.OInvariants"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "Category3.Functor"
Presenting theory "HOL-Library.BNF_Axiomatization"
Presenting file "~~/src/HOL/Tools/BNF/bnf_axiomatization.ML"
Presenting theory "Pure"
Presenting file "~~/src/Pure/ROOT0.ML"
Presenting file "~~/src/Pure/ROOT.ML"
Presenting theory "Flyspeck-Tame.PlaneGraphIso"
Presenting theory "Category3.Subcategory"
Presenting theory "ML_Bootstrap"
Presenting theory "AODV.Aodv_Data"
Presenting theory "Pure.Sessions"
Presenting Bicategory in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Bicategory" ...
Presenting document Bicategory/document
Presenting document Bicategory/outline
Presenting theory "Flyspeck-Tame.Rotation"
Presenting theory "Bicategory.IsomorphismClass"
Presenting theory "AODV.Aodv_Message"
Presenting theory "Flyspeck-Tame.Graph"
Presenting theory "HOL-Library.IArray"
Presenting theory "Flyspeck-Tame.IArray_Syntax"
Presenting theory "Flyspeck-Tame.Enumerator"
Presenting theory "AWN.AWN"
Presenting theory "Flyspeck-Tame.FaceDivision"
Presenting theory "Flyspeck-Tame.RTranCl"
Presenting theory "Flyspeck-Tame.Plane"
Presenting theory "Flyspeck-Tame.Plane1"
Presenting theory "AODV.Aodv"
Presenting theory "Flyspeck-Tame.GraphProps"
Presenting theory "AODV.Aodv_Predicates"
Presenting theory "AWN.AWN_SOS"
Presenting theory "Flyspeck-Tame.EnumeratorProps"
Presenting theory "Bicategory.Prebicategory"
Presenting theory "Category3.SetCategory"
Presenting theory "MonoidalCategory.MonoidalCategory"
Presenting theory "AODV.Fresher"
Presenting theory "MonoidalCategory.MonoidalFunctor"
Presenting theory "AWN.AWN_Cterms"
Presenting theory "AWN.AWN_Labels"
Presenting theory "AWN.Inv_Cterms"
Presenting theory "Bicategory.Bicategory"
Presenting theory "AWN.AWN_SOS_Labels"
Presenting theory "AODV.Seq_Invariants"
Presenting theory "Category3.SetCat"
Presenting theory "Category3.ProductCategory"
Presenting theory "AWN.Pnet"
Presenting theory "AWN.Closed"
Presenting theory "AODV.Quality_Increases"
Presenting theory "AODV.OAodv"
Presenting theory "Category3.NaturalTransformation"
Presenting theory "MonoidalCategory.FreeMonoidalCategory"
Presenting theory "Category3.BinaryFunctor"
Presenting theory "Flyspeck-Tame.FaceDivisionProps"
Presenting theory "AWN.OAWN_SOS"
Presenting theory "AWN.OAWN_SOS_Labels"
Presenting theory "MonoidalCategory.CartesianMonoidalCategory"
Presenting ConcurrentIMP in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentIMP" ...
Presenting document ConcurrentIMP/document
Presenting document ConcurrentIMP/outline
Presenting theory "ConcurrentIMP.CIMP_pred"
Presenting theory "AWN.OPnet"
Presenting theory "ConcurrentIMP.Infinite_Sequences"
Presenting theory "Category3.FunctorCategory"
Presenting theory "ConcurrentIMP.LTL"
Presenting theory "AWN.ONode_Lifting"
Presenting theory "ConcurrentIMP.CIMP_lang"
Presenting theory "AODV.Global_Invariants"
Presenting theory "Category3.Yoneda"
Presenting theory "AODV.Loop_Freedom"
Presenting theory "Bicategory.Coherence"
Presenting theory "Flyspeck-Tame.Invariants"
Presenting theory "ConcurrentIMP.CIMP_vcg"
Presenting theory "ConcurrentIMP.CIMP_vcg_rules"
Presenting theory "Flyspeck-Tame.PlaneProps"
Presenting theory "AODV.Aodv_Loop_Freedom"
Presenting theory "Flyspeck-Tame.ListSum"
Presenting theory "AODV.A_Norreqid"
Presenting theory "Flyspeck-Tame.Tame"
Presenting theory "ConcurrentIMP.CIMP"
Presenting file "$AFP/ConcurrentIMP/cimp.ML"
Presenting theory "Bicategory.CanonicalIsos"
Presenting theory "Flyspeck-Tame.Plane1Props"
Presenting theory "ConcurrentIMP.CIMP_locales"
Presenting theory "ConcurrentIMP.CIMP_one_place_buffer"
Presenting theory "Flyspeck-Tame.Generator"
Presenting theory "Flyspeck-Tame.TameProps"
Presenting theory "Flyspeck-Tame.TameEnum"
Presenting theory "ConcurrentIMP.CIMP_unbounded_buffer"
Presenting ConcurrentGC in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/ConcurrentGC" ...
Presenting document ConcurrentGC/document
Presenting document ConcurrentGC/outline
Presenting theory "AWN.OPnet_Lifting"
Presenting theory "AWN.OClosed_Lifting"
Presenting theory "ConcurrentGC.Model"
Presenting theory "Flyspeck-Tame.ScoreProps"
Presenting theory "Flyspeck-Tame.LowerBound"
Presenting theory "Bicategory.Subbicategory"
Presenting theory "AODV.A_Aodv_Data"
Presenting theory "ConcurrentGC.Proofs_Basis"
Presenting theory "AODV.A_Aodv_Message"
Presenting theory "Flyspeck-Tame.GeneratorProps"
Presenting theory "AWN.AWN_Invariants"
Presenting theory "Flyspeck-Tame.TameEnumProps"
Presenting theory "ConcurrentGC.Global_Invariants"
Presenting theory "HOL-Library.BNF_Corec"
Presenting theory "Bicategory.InternalEquivalence"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML"
Presenting theory "AODV.A_Aodv"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
Presenting theory "AODV.A_Aodv_Predicates"
Presenting theory "HOL-Library.AList"
Presenting theory "ConcurrentGC.Local_Invariants"
Presenting theory "HOL-Library.While_Combinator"
Presenting theory "Trie.Trie"
Presenting theory "Tools.Code_Generator"
Presenting theory "HOL-Library.Bourbaki_Witt_Fixpoint"
Presenting theory "Trie.Tries"
Presenting file "~~/src/Tools/cache_io.ML"
Presenting file "~~/src/Tools/Code/code_preproc.ML"
Presenting file "~~/src/Tools/Code/code_symbol.ML"
Presenting file "~~/src/Tools/Code/code_thingol.ML"
Presenting file "~~/src/Tools/Code/code_simp.ML"
Presenting file "~~/src/Tools/Code/code_printer.ML"
Presenting file "~~/src/Tools/Code/code_target.ML"
Presenting theory "HOL-Library.Centered_Division"
Presenting file "~~/src/Tools/Code/code_namespace.ML"
Presenting file "~~/src/Tools/Code/code_ml.ML"
Presenting file "~~/src/Tools/Code/code_haskell.ML"
Presenting theory "HOL-Library.Char_ord"
Presenting file "~~/src/Tools/Code/code_scala.ML"
Presenting file "~~/src/Tools/Code/code_runtime.ML"
Presenting file "~~/src/Tools/nbe.ML"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "AWN.OAWN_Invariants"
Presenting theory "HOL-Library.While_Combinator"
Presenting theory "ConcurrentGC.Tactics"
Presenting theory "HOL-Library.Code_Cardinality"
Presenting theory "Category3.Adjunction"
Presenting theory "Flyspeck-Tame.Worklist"
Presenting theory "Flyspeck-Tame.Maps"
Presenting theory "AODV.A_Fresher"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "AWN.OAWN_Convert"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "AWN.Qmsg"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "HOL-Library.Code_Target_Numeral"
Presenting theory "Flyspeck-Tame.Arch"
Presenting theory "HOL-Library.Case_Converter"
Presenting file "~~/src/HOL/Library/case_converter.ML"
Presenting theory "Flyspeck-Tame.ArchCompAux"
Presenting theory "Flyspeck-Tame.ArchCompProps"
Presenting theory "Flyspeck-Tame.Relative_Completeness"
Presenting JinjaThreads in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/JinjaThreads" ...
Presenting theory "Category3.EquivalenceOfCategories"
Presenting theory "Category3.FreeCategory"
Presenting theory "HOL-Library.Code_Lazy"
Presenting file "~~/src/HOL/Library/code_lazy.ML"
Presenting theory "Bicategory.Pseudofunctor"
Presenting document JinjaThreads/document
Presenting theory "Category3.DiscreteCategory"
Presenting document JinjaThreads/outline
Presenting theory "AWN.Qmsg_Lifting"
Presenting theory "ConcurrentGC.Global_Invariants_Lemmas"
Presenting theory "AODV.A_Seq_Invariants"
Presenting theory "HOL-Library.Code_Test"
Presenting file "~~/src/HOL/Library/code_test.ML"
Presenting theory "HOL-Library.Combine_PER"
Presenting theory "ConcurrentGC.Local_Invariants_Lemmas"
Presenting theory "ConcurrentGC.Initial_Conditions"
Presenting theory "HOL-Library.Sublist"
Presenting theory "ConcurrentGC.Noninterference"
Presenting theory "HOL-Library.Transitive_Closure_Table"
Presenting theory "AODV.A_Quality_Increases"
Presenting theory "AODV.A_OAodv"
Presenting theory "HOL-Library.Predicate_Compile_Alternative_Defs"
Presenting theory "HOL-Library.Confluence"
Presenting theory "ConcurrentGC.Global_Noninterference"
Presenting theory "HOL-Library.Confluent_Quotient"
Presenting theory "ConcurrentGC.MarkObject"
Presenting theory "HOL-Library.Dlist"
Presenting theory "JinjaThreads.Set_without_equal"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "JinjaThreads.Set_Monad"
Presenting theory "ConcurrentGC.Phases"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "ConcurrentGC.StrongTricolour"
Presenting theory "HOL-Library.Complete_Partial_Order2"
Presenting theory "ConcurrentGC.TSO"
Presenting theory "ConcurrentGC.Valid_Refs"
Presenting theory "ConcurrentGC.Worklists"
Presenting theory "ConcurrentGC.Proofs"
Presenting theory "ConcurrentGC.Concrete_heap"
Presenting theory "HOL-Library.Case_Converter"
Presenting file "~~/src/HOL/Library/case_converter.ML"
Presenting theory "ConcurrentGC.Concrete"
Presenting Word_Lib in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib" ...
Presenting theory "HOL-Library.Conditional_Parametricity"
Presenting file "~~/src/HOL/Library/conditional_parametricity.ML"
Presenting document Word_Lib/document
Presenting document Word_Lib/outline
Presenting theory "HOL-Library.Confluence"
Presenting theory "HOL-Library.Simps_Case_Conv"
Presenting file "~~/src/HOL/Library/simps_case_conv.ML"
Presenting theory "Word_Lib.Enumeration"
Presenting theory "Word_Lib.Even_More_List"
Presenting theory "HOL-Library.Confluent_Quotient"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "AODV.A_Global_Invariants"
Presenting theory "AWN.OClosed_Transfer"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "HOL-Library.Numeral_Type"
Presenting theory "AWN.AWN_Main"
Presenting theory "HOL-Library.Type_Length"
Presenting theory "AODV.A_Loop_Freedom"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "AODV.A_Aodv_Loop_Freedom"
Presenting theory "AODV.B_Fwdrreps"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "HOL-Library.Countable_Complete_Lattices"
Presenting theory "AWN.Toy"
Presenting theory "HOL-Library.Order_Continuity"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "AWN.AWN_Term_Graph"
Presenting IP_Addresses in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/IP_Addresses" ...
Presenting document IP_Addresses/document
Presenting document IP_Addresses/outline
Presenting theory "HOL-Library.Cancellation"
Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
Presenting theory "HOL-Library.Countable_Complete_Lattices"
Presenting theory "HOL-Library.Extended_Nat"
Presenting theory "HOL-Library.Countable_Set_Type"
Presenting theory "HOL-Library.Debug"
Presenting theory "HOL-Library.Diagonal_Subsequence"
Presenting theory "HOL-Library.Discrete"
Presenting theory "AODV.B_Aodv_Data"
Presenting theory "AODV.B_Aodv_Message"
Presenting theory "HOL-Library.Word"
Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
Presenting theory "HOL-Library.FuncSet"
Presenting theory "Word_Lib.Legacy_Aliases"
Presenting theory "Word_Lib.More_Arithmetic"
Presenting theory "Bicategory.Strictness"
Presenting theory "Word_Lib.More_Divides"
Presenting theory "Word_Lib.More_Misc"
Presenting theory "HOL-Library.Disjoint_Sets"
Presenting theory "AODV.B_Aodv"
Presenting theory "Category3.Limit"
Presenting theory "AODV.B_Aodv_Predicates"
Presenting theory "HOL-Library.Complete_Partial_Order2"
Presenting theory "HOL-Library.Sublist"
Presenting theory "HOL-Library.Multiset"
Presenting theory "Word_Lib.More_Sublist"
Presenting theory "Coinductive.Coinductive_Nat"
Presenting theory "Word_Lib.More_Bit_Ring"
Presenting theory "HOL-Library.FSet"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "Category3.CategoryWithPullbacks"
Presenting theory "HOL-ex.Quicksort"
Presenting theory "AODV.B_Fresher"
Presenting theory "HOL-Library.Option_ord"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "Word_Lib.More_Word"
Presenting theory "Word_Lib.Strict_part_mono"
Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"
Presenting theory "Word_Lib.Most_significant_bit"
Presenting theory "Word_Lib.Least_significant_bit"
Presenting theory "Word_Lib.Generic_set_bit"
Presenting theory "Word_Lib.Bit_Comprehension"
Presenting theory "HOL-Library.Finite_Map"
Presenting theory "Bicategory.InternalAdjunction"
Presenting theory "HOL-Library.Disjoint_FSets"
Presenting theory "AODV.B_Seq_Invariants"
Presenting theory "HOL-Library.Dlist"
Presenting theory "HOL.HOL"
Presenting theory "HOL-Library.Dual_Ordered_Lattice"
Presenting theory "Category3.CartesianCategory"
Presenting file "~~/src/Tools/misc_legacy.ML"
Presenting file "~~/src/Tools/try.ML"
Presenting file "~~/src/Tools/quickcheck.ML"
Presenting file "~~/src/Tools/solve_direct.ML"
Presenting file "~~/src/Tools/IsaPlanner/zipper.ML"
Presenting file "~~/src/Tools/IsaPlanner/isand.ML"
Presenting file "~~/src/Tools/IsaPlanner/rw_inst.ML"
Presenting file "~~/src/Provers/hypsubst.ML"
Presenting file "~~/src/Provers/splitter.ML"
Presenting file "~~/src/Provers/classical.ML"
Presenting file "~~/src/Provers/blast.ML"
Presenting file "~~/src/Provers/clasimp.ML"
Presenting file "~~/src/Tools/eqsubst.ML"
Presenting file "~~/src/Provers/quantifier1.ML"
Presenting file "~~/src/Tools/atomize_elim.ML"
Presenting file "~~/src/Tools/cong_tac.ML"
Presenting file "~~/src/Tools/intuitionistic.ML"
Presenting file "~~/src/Tools/project_rule.ML"
Presenting file "~~/src/Tools/subtyping.ML"
Presenting file "~~/src/Tools/case_product.ML"
Presenting file "~~/src/HOL/Tools/hologic.ML"
Presenting file "~~/src/HOL/Tools/rewrite_hol_proof.ML"
Presenting file "~~/src/HOL/Tools/simpdata.ML"
Presenting file "~~/src/Tools/induct.ML"
Presenting file "~~/src/Tools/induction.ML"
Presenting file "~~/src/Tools/induct_tacs.ML"
Presenting file "~~/src/Tools/coherent.ML"
Presenting file "~~/src/HOL/Tools/cnf.ML"
Presenting theory "Word_Lib.Bits_Int"
Presenting theory "Category3.CategoryWithFiniteLimits"
Presenting theory "HOL-Library.Equipollence"
Presenting theory "AODV.B_Quality_Increases"
Presenting theory "AODV.B_OAodv"
Presenting theory "HOL-Library.Simps_Case_Conv"
Presenting file "~~/src/HOL/Library/simps_case_conv.ML"
Presenting theory "Category3.CartesianClosedCategory"
Presenting theory "HOL-Library.Extended"
Presenting theory "Word_Lib.Aligned"
Presenting theory "Word_Lib.Next_and_Prev"
Presenting theory "HOL-Library.Order_Continuity"
Presenting theory "HOL-Library.Signed_Division"
Presenting theory "Word_Lib.Signed_Division_Word"
Presenting theory "HereditarilyFinite.HF"
Presenting theory "HOL-Library.Extended_Nat"
Presenting theory "Automatic_Refinement.Misc"
Presenting theory "Word_Lib.Many_More"
Presenting theory "Word_Lib.Singleton_Bit_Shifts"
Presenting theory "IP_Addresses.NumberWang_IPv4"
Presenting theory "IP_Addresses.NumberWang_IPv6"
Presenting theory "Word_Lib.Typedef_Morphisms"
Presenting theory "HOL-Library.Liminf_Limsup"
Presenting theory "Coinductive.Coinductive_List"
Presenting theory "IP_Addresses.WordInterval"
Presenting theory "IP_Addresses.Hs_Compat"
Presenting theory "IP_Addresses.IP_Address"
Presenting theory "IP_Addresses.IPv4"
Presenting theory "HOL.Orderings"
Presenting file "~~/src/Provers/order_procedure.ML"
Presenting file "~~/src/Provers/order_tac.ML"
Presenting theory "Word_Lib.Reversed_Bit_Lists"
Presenting theory "AODV.B_Global_Invariants"
Presenting theory "Coinductive.TLList"
Presenting theory "HOL.Groups"
Presenting theory "AODV.B_Loop_Freedom"
Presenting file "~~/src/HOL/Tools/group_cancel.ML"
Presenting theory "Word_Lib.Bitwise"
Presenting theory "Coinductive.Lazy_LList"
Presenting theory "Word_Lib.Bit_Comprehension_Int"
Presenting theory "Word_Lib.Signed_Words"
Presenting theory "Word_Lib.Bitwise_Signed"
Presenting theory "HOL.Lattices"
Presenting theory "Coinductive.Lazy_TLList"
Presenting theory "Word_Lib.Enumeration_Word"
Presenting theory "Word_Lib.Hex_Words"
Presenting theory "Word_Lib.Norm_Words"
Presenting theory "HOL-Library.Extended_Real"
Presenting theory "Word_Lib.Rsplit"
Presenting theory "HOL-Library.Cancellation"
Presenting theory "IP_Addresses.IPv6"
Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
Presenting theory "Word_Lib.Syntax_Bundles"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
Presenting theory "Word_Lib.Sgn_Abs"
Presenting theory "Word_Lib.Type_Syntax"
Presenting theory "HOL.Boolean_Algebras"
Presenting file "~~/src/HOL/Tools/boolean_algebra_cancel.ML"
Presenting theory "AODV.B_Aodv_Loop_Freedom"
Presenting theory "IP_Addresses.Prefix_Match"
Presenting theory "AODV.C_Gtobcast"
Presenting theory "HOL-Library.Indicator_Function"
Presenting theory "IP_Addresses.CIDR_Split"
Presenting theory "HOL-Library.Product_Lexorder"
Presenting theory "IP_Addresses.WordInterval_Sorted"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "HOL.Set"
Presenting theory "HOL-Library.Extended_Nonnegative_Real"
Presenting theory "AODV.C_Aodv_Data"
Presenting theory "AODV.C_Aodv_Message"
Presenting theory "Category3.HF_SetCat"
Presenting theory "Category3.HF_SetCat_Interp"
Presenting theory "HOL-Library.Log_Nat"
Presenting theory "HOL.Typedef"
Presenting theory "HOL-Cardinals.Fun_More"
Presenting file "~~/src/HOL/Tools/typedef.ML"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting theory "HOL-Library.Lattice_Algebras"
Presenting theory "HOL-Eisbach.Eisbach_Tools"
Presenting theory "Word_Lib.Word_EqI"
Presenting theory "AODV.C_Aodv"
Presenting theory "Word_Lib.Boolean_Inequalities"
Presenting theory "HOL-Cardinals.Order_Relation_More"
Presenting theory "HOL-Cardinals.Wellfounded_More"
Presenting theory "AODV.C_Aodv_Predicates"
Presenting theory "HOL-Cardinals.Wellorder_Relation"
Presenting theory "HOL-Cardinals.Wellorder_Embedding"
Presenting theory "HOL-Cardinals.Order_Union"
Presenting theory "HOL-Library.Multiset"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "HOL-ex.Quicksort"
Presenting theory "HOL.Fun"
Presenting file "~~/src/HOL/Tools/functor.ML"
Presenting theory "Word_Lib.Word_Lemmas"
Presenting theory "HOL-Library.Float"
Presenting theory "HOL-Library.Option_ord"
Presenting theory "Word_Lib.Word_8"
Presenting theory "HOL-Cardinals.Wellorder_Constructions"
Presenting theory "Word_Lib.Word_16"
Presenting theory "Word_Lib.Word_Syntax"
Presenting theory "Word_Lib.Word_Names"
Presenting theory "HOL-Library.Function_Algebras"
Presenting theory "AODV.C_Fresher"
Presenting theory "HOL-Library.Function_Division"
Presenting theory "HOL-Library.Fun_Lexorder"
Presenting theory "HOL-Library.Going_To_Filter"
Presenting theory "HOL.Complete_Lattices"
Presenting theory "IP_Addresses.IP_Address_Parser"
Presenting theory "HOL-Library.Groups_Big_Fun"
Presenting theory "IP_Addresses.Lib_Numbers_toString"
Presenting theory "Word_Lib.More_Word_Operations"
Presenting theory "HOL-Library.Infinite_Typeclass"
Presenting theory "IP_Addresses.Lib_Word_toString"
Presenting theory "IP_Addresses.Lib_List_toString"
Presenting theory "HOL-Library.Set_Algebras"
Presenting theory "Word_Lib.Word_32"
Presenting theory "IP_Addresses.IP_Address_toString"
Presenting theory "IP_Addresses.Prefix_Match_toString"
Presenting theory "Word_Lib.Word_Lib_Sumo"
Presenting theory "Word_Lib.Machine_Word_32_Basics"
Presenting Simple_Firewall in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Simple_Firewall" ...
Presenting document Simple_Firewall/document
Presenting document Simple_Firewall/outline
Presenting theory "Word_Lib.Machine_Word_32"
Presenting theory "Simple_Firewall.Lib_Enum_toString"
Presenting theory "Word_Lib.Word_64"
Presenting theory "Word_Lib.Machine_Word_64_Basics"
Presenting theory "Simple_Firewall.L4_Protocol"
Presenting theory "Simple_Firewall.Simple_Packet"
Presenting theory "Simple_Firewall.Firewall_Common_Decision_State"
Presenting theory "Word_Lib.Machine_Word_64"
Presenting theory "HOL-Library.Char_ord"
Presenting theory "Word_Lib.Guide"
Presenting theory "AODV.C_Seq_Invariants"
Presenting theory "HOL-Library.Interval"
Presenting theory "Word_Lib.Examples"
Presenting theory "Simple_Firewall.Iface"
Presenting theory "HOL-Library.Interval_Float"
Presenting Routing in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing" ...
Presenting theory "Simple_Firewall.SimpleFw_Syntax"
Presenting document Routing/document
Presenting document Routing/outline
Presenting theory "Routing.Linorder_Helper"
Presenting theory "HOL-Library.IArray"
Presenting theory "Pure-ex.Guess"
Presenting theory "HOL-Cardinals.Ordinal_Arithmetic"
Presenting theory "Simple_Firewall.SimpleFw_Semantics"
Presenting theory "Simple_Firewall.List_Product_More"
Presenting theory "Simple_Firewall.Option_Helpers"
Presenting theory "AODV.C_Quality_Increases"
Presenting theory "AODV.C_OAodv"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
Presenting theory "Simple_Firewall.Generic_SimpleFw"
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting theory "Routing.Routing_Table"
Presenting theory "Simple_Firewall.Shadowed"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "Routing.Linux_Router"
Presenting theory "Simple_Firewall.IP_Partition_Preliminaries"
Presenting theory "Simple_Firewall.GroupF"
Presenting theory "Simple_Firewall.IP_Addr_WordInterval_toString"
Presenting theory "Simple_Firewall.Primitives_toString"
Presenting theory "HOL-Cardinals.Cardinal_Order_Relation"
Presenting theory "Routing.IpRoute_Parser"
Presenting file "$AFP/Routing/IpRoute_Parser.ML"
Presenting Iptables_Semantics in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics" ...
Presenting document Iptables_Semantics/document
Presenting document Iptables_Semantics/outline
Presenting theory "Iptables_Semantics.List_Misc"
Presenting theory "Bicategory.PseudonaturalTransformation"
Presenting theory "Iptables_Semantics.Negation_Type"
Presenting theory "Iptables_Semantics.WordInterval_Lists"
Presenting theory "Iptables_Semantics.Repeat_Stabilize"
Presenting theory "HOL-Cardinals.Cardinal_Arithmetic"
Presenting theory "Iptables_Semantics.Firewall_Common"
Presenting theory "HOL-Library.LaTeXsugar"
Presenting theory "HOL-Library.Landau_Symbols"
Presenting theory "HOL-Cardinals.Wellorder_Extension"
Presenting theory "HOL-Cardinals.Cardinals"
Presenting theory "ZFC_in_HOL.ZFC_Library"
Presenting theory "HOL-Library.Lattice_Constructions"
Presenting theory "Simple_Firewall.Service_Matrix"
Presenting theory "AODV.C_Global_Invariants"
Presenting theory "Simple_Firewall.SimpleFw_toString"
Presenting Iptables_Semantics_Examples in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples" ...
Presenting document Iptables_Semantics_Examples/document
Presenting theory "HOL.Ctr_Sugar"
Presenting document Iptables_Semantics_Examples/outline
Presenting file "~~/src/HOL/Tools/Ctr_Sugar/case_translation.ML"
Presenting theory "Iptables_Semantics.Semantics"
Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML"
Presenting theory "ZFC_in_HOL.ZFC_in_HOL"
Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML"
Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML"
Presenting theory "HOL-Library.Stream"
Presenting file "~~/src/HOL/Tools/coinduction.ML"
Presenting theory "AODV.C_Loop_Freedom"
Presenting theory "Automatic_Refinement.Misc"
Presenting theory "Iptables_Semantics.Matching"
Presenting theory "Automatic_Refinement.Foldi"
Presenting theory "Iptables_Semantics.Ruleset_Update"
Presenting theory "AODV.C_Aodv_Loop_Freedom"
Presenting theory "AODV.D_Fwdrreqs"
Presenting theory "HOL-Library.Sublist"
Presenting theory "Iptables_Semantics.Call_Return_Unfolding"
Presenting theory "Collections.SetIterator"
Presenting theory "Iptables_Semantics.Ternary"
Presenting theory "ZFC_in_HOL.ZFC_Cardinals"
Presenting theory "Iptables_Semantics_Examples.Parser_Test"
Presenting theory "HOL-Library.Linear_Temporal_Logic_on_Streams"
Presenting theory "Iptables_Semantics_Examples.Parser6_Test"
Presenting theory "Iptables_Semantics_Examples.Small_Examples"
Presenting theory "Iptables_Semantics.Matching_Ternary"
Presenting theory "HOL-Library.ListVector"
Presenting theory "Iptables_Semantics_Examples.Ports_Fail"
Presenting theory "Iptables_Semantics_Examples.Contrived_Example"
Presenting theory "HOL-Library.Lub_Glb"
Presenting theory "Iptables_Semantics_Examples.iptables_Ln_tuned_parsed"
Presenting theory "Collections.SetIteratorOperations"
Presenting theory "Automatic_Refinement.Refine_Util_Bootstrap1"
Presenting theory "AODV.D_Aodv_Data"
Presenting theory "Iptables_Semantics.Semantics_Ternary"
Presenting theory "Automatic_Refinement.Mpat_Antiquot"
Presenting theory "Iptables_Semantics.Datatype_Selectors"
Presenting theory "AODV.D_Aodv_Message"
Presenting theory "Iptables_Semantics_Examples.Analyze_Synology_Diskstation"
Presenting theory "Iptables_Semantics.IpAddresses"
Presenting theory "Automatic_Refinement.Mk_Term_Antiquot"
Presenting theory "Iptables_Semantics.L4_Protocol_Flags"
Presenting theory "Iptables_Semantics.Ports"
Presenting theory "Iptables_Semantics.Conntrack_State"
Presenting theory "Iptables_Semantics.Tagged_Packet"
Presenting theory "Iptables_Semantics.Common_Primitive_Syntax"
Presenting theory "HOL-Library.Mapping"
Presenting theory "Iptables_Semantics.Unknown_Match_Tacs"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "Iptables_Semantics.Common_Primitive_Matcher_Generic"
Presenting theory "HOL-Library.More_List"
Presenting theory "Iptables_Semantics_Examples.Analyze_Ringofsaturn_com"
Presenting theory "AODV.D_Aodv"
Presenting theory "Category3.ZFC_SetCat"
Presenting theory "HOL-Library.Cancellation"
Presenting theory "Automatic_Refinement.Refine_Util"
Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
Presenting theory "Iptables_Semantics.Common_Primitive_Matcher"
Presenting theory "AODV.D_Aodv_Predicates"
Presenting theory "Automatic_Refinement.Attr_Comb"
Presenting theory "Iptables_Semantics.Example_Semantics"
Presenting theory "Automatic_Refinement.Named_Sorted_Thms"
Presenting theory "Category3.ZFC_SetCat_Interp"
Presenting Iptables_Semantics_Examples_Big in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics_Examples_Big" ...
Presenting document Iptables_Semantics_Examples_Big/document
Presenting document Iptables_Semantics_Examples_Big/outline
Presenting theory "Automatic_Refinement.Prio_List"
Presenting theory "Iptables_Semantics_Examples_Big.Analyze_topos_generated"
Presenting theory "Automatic_Refinement.Tagged_Solver"
Presenting theory "Automatic_Refinement.Anti_Unification"
Presenting theory "Automatic_Refinement.Indep_Vars"
Presenting theory "Iptables_Semantics.Alternative_Semantics"
Presenting theory "Automatic_Refinement.Select_Solve"
Presenting theory "Automatic_Refinement.Mk_Record_Simp"
Presenting theory "Automatic_Refinement.Refine_Lib"
Presenting file "$AFP/Automatic_Refinement/Lib/Cond_Rewr_Conv.ML"
Presenting file "$AFP/Automatic_Refinement/Lib/Revert_Abbrev.ML"
Presenting theory "Iptables_Semantics.Semantics_Stateful"
Presenting theory "Collections.Proper_Iterator"
Presenting theory "Collections.It_to_It"
Presenting theory "AODV.D_Fresher"
Presenting theory "Collections.SetIteratorGA"
Presenting theory "Refine_Monadic.Refine_Chapter"
Presenting theory "Iptables_Semantics.Semantics_Goto"
Presenting theory "Automatic_Refinement.Autoref_Phases"
Presenting theory "Automatic_Refinement.Autoref_Data"
Presenting theory "Automatic_Refinement.Autoref_Tagging"
Presenting theory "Iptables_Semantics.Negation_Type_DNF"
Presenting theory "Iptables_Semantics.Matching_Embeddings"
Presenting theory "AODV.D_Seq_Invariants"
Presenting theory "Iptables_Semantics.Fixed_Action"
Presenting theory "HOL-Library.Multiset"
Presenting theory "Iptables_Semantics_Examples.Analyze_SQRL_Shorewall"
Presenting theory "Automatic_Refinement.Relators"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "Iptables_Semantics_Examples.SQRL_2015_nospoof"
Presenting theory "Iptables_Semantics.Normalized_Matches"
Presenting theory "Iptables_Semantics.Negation_Type_Matching"
Presenting theory "Automatic_Refinement.Param_Tool"
Presenting theory "Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing"
Presenting theory "HOL.Inductive"
Presenting theory "AODV.D_Quality_Increases"
Presenting file "~~/src/HOL/Tools/inductive.ML"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_data.ML"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML"
Presenting theory "HOL-Library.Multiset_Order"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML"
Presenting theory "AODV.D_OAodv"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_primrec.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML"
Presenting theory "Iptables_Semantics_Examples.Analyze_medium_sized_company"
Presenting theory "Automatic_Refinement.Param_HOL"
Presenting theory "Automatic_Refinement.Parametricity"
Presenting theory "HOL-Library.NList"
Presenting theory "HOL-Library.Nonpos_Ints"
Presenting theory "Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small"
Presenting theory "Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall"
Presenting theory "Automatic_Refinement.Autoref_Id_Ops"
Presenting theory "HOL-Library.Numeral_Type"
Presenting theory "Iptables_Semantics.Primitive_Normalization"
Presenting theory "Iptables_Semantics.MatchExpr_Fold"
Presenting theory "Iptables_Semantics.Common_Primitive_Lemmas"
Presenting theory "Iptables_Semantics_Examples_Big.Analyze_Containern"
Presenting theory "HOL-Library.Omega_Words_Fun"
Presenting theory "HOL-Library.Open_State_Syntax"
Presenting theory "Automatic_Refinement.Autoref_Fix_Rel"
Presenting theory "Automatic_Refinement.Autoref_Translate"
Presenting theory "Automatic_Refinement.Autoref_Gen_Algo"
Presenting theory "HOL-Library.Option_ord"
Presenting theory "Automatic_Refinement.Autoref_Relator_Interface"
Presenting theory "HOL-Library.Parallel"
Presenting theory "Automatic_Refinement.Autoref_Tool"
Presenting theory "HOL-Library.Pattern_Aliases"
Presenting theory "HOL-Library.Periodic_Fun"
Presenting theory "Iptables_Semantics.Ports_Normalize"
Presenting theory "Automatic_Refinement.Autoref_Bindings_HOL"
Presenting theory "Automatic_Refinement.Automatic_Refinement"
Presenting theory "Refine_Monadic.Refine_Mono_Prover"
Presenting file "$AFP/Refine_Monadic/refine_mono_prover.ML"
Presenting theory "Iptables_Semantics.IpAddresses_Normalize"
Presenting theory "Iptables_Semantics.Interfaces_Normalize"
Presenting theory "HOL.Product_Type"
Presenting theory "Refine_Monadic.Refine_Misc"
Presenting theory "AODV.D_Global_Invariants"
Presenting theory "Iptables_Semantics.Word_Upto"
Presenting file "~~/src/HOL/Tools/split_rule.ML"
Presenting file "~~/src/HOL/Tools/set_comprehension_pointfree.ML"
Presenting file "~~/src/HOL/Tools/inductive_set.ML"
Presenting theory "Iptables_Semantics_Examples_Big.TUM_Spoofing_new3"
Presenting theory "Bicategory.EquivalenceOfBicategories"
Presenting theory "Refine_Monadic.RefineG_Transfer"
Presenting theory "HOL.Sum_Type"
Presenting theory "HOL-Library.Poly_Mapping"
Presenting theory "AODV.D_Loop_Freedom"
Presenting theory "Iptables_Semantics.Protocols_Normalize"
Presenting theory "Refine_Monadic.RefineG_Domain"
Presenting theory "Iptables_Semantics.Remdups_Rev"
Presenting theory "HOL-Library.Power_By_Squaring"
Presenting theory "Refine_Monadic.RefineG_Recursion"
Presenting theory "Refine_Monadic.RefineG_Assert"
Presenting theory "Iptables_Semantics.Ipassmt"
Presenting theory "Iptables_Semantics_Examples_Big.TUM_Simple_FW"
Presenting theory "HOL-Library.Preorder"
Presenting file "~~/src/Provers/preorder.ML"
Presenting theory "HOL-Library.Product_Plus"
Presenting theory "HOL-Library.Quadratic_Discriminant"
Presenting theory "HOL-Library.Quotient_Syntax"
Presenting theory "AODV.D_Aodv_Loop_Freedom"
Presenting theory "HOL-Library.Quotient_Set"
Presenting theory "AODV.E_All_ABCD"
Presenting theory "HOL.Rings"
Presenting theory "HOL-Library.Quotient_Product"
Presenting theory "HOL-Library.Quotient_Option"
Presenting file "~~/src/HOL/Tools/arith_data.ML"
Presenting file "~~/src/Provers/Arith/cancel_div_mod.ML"
Presenting theory "HOL-Library.Quotient_List"
Presenting theory "Iptables_Semantics.No_Spoof"
Presenting theory "HOL-Library.Quotient_Sum"
Presenting theory "HOL-Library.Quotient_Type"
Presenting theory "Iptables_Semantics.Common_Primitive_toString"
Presenting theory "Iptables_Semantics.Routing_IpAssmt"
Presenting theory "Refine_Monadic.Refine_Basic"
Presenting theory "Iptables_Semantics.Output_Interface_Replace"
Presenting theory "AODV.E_Aodv_Data"
Presenting theory "AODV.E_Aodv_Message"
Presenting theory "Refine_Monadic.Refine_Leof"
Presenting theory "HOL-Library.Ramsey"
Presenting theory "Refine_Monadic.Refine_Heuristics"
Presenting theory "Iptables_Semantics.Interface_Replace"
Presenting theory "Refine_Monadic.Refine_More_Comb"
Presenting theory "Iptables_Semantics.Optimizing"
Presenting theory "HOL.Nat"
Presenting theory "HOL-Library.Real_Mod"
Presenting theory "AODV.E_Aodv"
Presenting file "~~/src/HOL/Tools/nat_arith.ML"
Presenting theory "HOL-Library.Reflection"
Presenting file "~~/src/HOL/Tools/reflection.ML"
Presenting theory "Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large"
Presenting theory "HOL-Library.While_Combinator"
Presenting theory "AODV.E_Aodv_Predicates"
Presenting theory "Refine_Monadic.RefineG_While"
Presenting theory "HOL-Library.Rewrite"
Presenting file "~~/src/HOL/Library/cconv.ML"
Presenting file "~~/src/HOL/Library/rewrite.ML"
Presenting theory "HOL-Library.Type_Length"
Presenting theory "HOL-Library.Saturated"
Presenting theory "AODV.E_Fresher"
Presenting theory "HOL-Library.Set_Idioms"
Presenting theory "Iptables_Semantics.Transform"
Presenting theory "Refine_Monadic.Refine_While"
Presenting theory "Bicategory.SpanBicategory"
Presenting theory "HOL-Library.Signed_Division"
Presenting theory "HOL-Library.State_Monad"
Presenting theory "HOL.Fields"
Presenting theory "Iptables_Semantics.Conntrack_State_Transform"
Presenting theory "HOL-Library.Comparator"
Presenting theory "Refine_Monadic.Refine_Det"
Presenting theory "AODV.E_Seq_Invariants"
Presenting file "~~/src/Provers/Arith/fast_lin_arith.ML"
Presenting file "~~/src/HOL/Tools/lin_arith.ML"
Presenting theory "Refine_Monadic.Refine_Pfun"
Presenting theory "Iptables_Semantics.Primitive_Abstract"
Presenting theory "HOL-Library.Sorting_Algorithms"
Presenting theory "Refine_Monadic.Refine_Transfer"
Presenting theory "AODV.E_Quality_Increases"
Presenting theory "AODV.E_OAodv"
Presenting theory "HOL.Relation"
Presenting theory "Iptables_Semantics.SimpleFw_Compliance"
Presenting theory "Iptables_Semantics.Semantics_Embeddings"
Presenting theory "Iptables_Semantics.Iptables_Semantics"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "Native_Word.Code_Int_Integer_Conversion"
Presenting theory "Refine_Monadic.Refine_Foreach"
Presenting theory "Native_Word.Code_Target_Integer_Bit"
Presenting theory "Native_Word.Code_Target_Int_Bit"
Presenting theory "HOL-Library.Sum_of_Squares"
Presenting file "~~/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML"
Presenting theory "Iptables_Semantics.Code_Interface"
Presenting file "~~/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML"
Presenting file "~~/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML"
Presenting file "~~/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML"
Presenting theory "HOL-Library.Transitive_Closure_Table"
Presenting theory "Refine_Monadic.Refine_Automation"
Presenting theory "Refine_Monadic.Autoref_Monadic"
Presenting theory "Refine_Monadic.Refine_Monadic"
Presenting theory "HOL-Library.Tree"
Presenting theory "HOL-Library.Tree_Multiset"
Presenting theory "HOL-Library.Tree_Real"
Presenting theory "HOL-Library.Uprod"
Presenting theory "AODV.E_Global_Invariants"
Presenting theory "HOL.Finite_Set"
Presenting theory "Collections.Gen_Iterator"
Presenting theory "Collections.Idx_Iterator"
Presenting theory "Collections.Iterator"
Presenting theory "Iptables_Semantics.Parser6"
Presenting theory "AODV.E_Loop_Freedom"
Presenting theory "Collections.ICF_Tools"
Presenting theory "Iptables_Semantics.No_Spoof_Embeddings"
Presenting theory "Collections.Ord_Code_Preproc"
Presenting theory "Collections.Record_Intf"
Presenting theory "Collections.Locale_Code"
Presenting theory "Collections.ICF_Spec_Base"
Presenting theory "AODV.E_Aodv_Loop_Freedom"
Presenting theory "AODV.All"
Presenting theory "HOL.Transitive_Closure"
Presenting theory "Bicategory.Tabulation"
Presenting theory "Iptables_Semantics.Parser"
Presenting file "~~/src/Provers/trancl.ML"
Presenting theory "Collections.SetSpec"
Presenting theory "Iptables_Semantics.Code_haskell"
Presenting theory "Iptables_Semantics.Access_Matrix_Embeddings"
Presenting theory "Iptables_Semantics.Documentation"
Presenting theory "HOL.Wellfounded"
Presenting theory "HOL-Library.Word"
Presenting theory "Collections.MapSpec"
Presenting theory "HOL.Wfrec"
Presenting theory "Collections.ListSpec"
Presenting theory "Collections.AnnotatedListSpec"
Presenting theory "HOL.Order_Relation"
Presenting theory "Collections.PrioSpec"
Presenting theory "Collections.PrioUniqueSpec"
Presenting theory "Collections.Algos"
Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
Presenting theory "Collections.SetIndex"
Presenting theory "Collections.SetIteratorCollectionsGA"
Presenting theory "HOL-Library.Z2"
Presenting theory "HOL-Library.Library"
Presenting theory "HOL-Library.Product_Order"
Presenting theory "HOL-Library.Finite_Lattice"
Presenting theory "HOL.Hilbert_Choice"
Presenting theory "HOL-Library.List_Lexorder"
Presenting theory "HOL-Library.List_Lenlexorder"
Presenting file "~~/src/HOL/Tools/choice_specification.ML"
Presenting theory "HOL-Library.Prefix_Order"
Presenting theory "Collections.SetGA"
Presenting theory "HOL-Library.Product_Lexorder"
Presenting theory "HOL-Library.Subseq_Order"
Presenting theory "Collections.Dlist_add"
Presenting theory "Collections.ListSetImpl"
Presenting theory "Collections.ListSetImpl_Invar"
Presenting theory "HOL-Library.Datatype_Records"
Presenting file "~~/src/HOL/Library/datatype_records.ML"
Presenting theory "Collections.ListSetImpl_NotDist"
Presenting theory "HOL-Library.AList_Mapping"
Presenting theory "Collections.Sorted_List_Operations"
Presenting theory "HOL-Library.Code_Abstract_Char"
Presenting theory "HOL.Zorn"
Presenting theory "Collections.ListSetImpl_Sorted"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "HOL-Library.Code_Binary_Nat"
Presenting theory "HOL.BNF_Wellorder_Relation"
Presenting theory "HOL-Library.Code_Prolog"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
Presenting theory "HOL.BNF_Wellorder_Embedding"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "HOL-Library.Code_Real_Approx_By_Float"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "HOL-Library.Code_Target_Numeral"
Presenting theory "HOL-Library.Code_Target_Numeral_Float"
Presenting theory "HOL-Library.Complex_Order"
Presenting theory "HOL-Library.DAList"
Presenting theory "HOL-Library.DAList_Multiset"
Presenting theory "HOL.BNF_Wellorder_Constructions"
Presenting theory "HOL-Library.RBT_Impl"
Presenting theory "Collections.RBT_add"
Presenting theory "HOL-Library.RBT"
Presenting theory "HOL.BNF_Cardinal_Order_Relation"
Presenting theory "Collections.MapGA"
Presenting theory "Collections.RBTMapImpl"
Presenting theory "HOL.BNF_Cardinal_Arithmetic"
Presenting theory "Collections.SetByMap"
Presenting theory "Collections.RBTSetImpl"
Presenting theory "HOL-Library.RBT_Impl"
Presenting theory "HOL-Library.AList"
Presenting theory "HOL.Fun_Def_Base"
Presenting file "~~/src/HOL/Tools/Function/function_lib.ML"
Presenting file "~~/src/HOL/Tools/Function/function_common.ML"
Presenting file "~~/src/HOL/Tools/Function/function_context_tree.ML"
Presenting file "~~/src/HOL/Tools/Function/sum_tree.ML"
Presenting theory "Collections.Assoc_List"
Presenting theory "Collections.ListMapImpl"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "HOL-Library.RBT"
Presenting theory "HOL-Library.RBT_Mapping"
Presenting theory "Bicategory.BicategoryOfSpans"
Presenting theory "HOL-Library.Numeral_Type"
Presenting theory "HOL-Library.Type_Length"
Presenting theory "HOL-Library.RBT_Set"
Presenting theory "HOL-Library.LaTeXsugar"
Presenting theory "HOL-Library.OptionalSugar"
Presenting theory "HOL-Library.Predicate_Compile_Alternative_Defs"
Presenting theory "HOL-Library.Predicate_Compile_Quickcheck"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
Presenting theory "HOL-Library.Word"
Presenting theory "HOL.BNF_Def"
Presenting file "~~/src/HOL/Tools/BNF/bnf_util.ML"
Presenting theory "HOL-Library.Old_Recdef"
Presenting file "~~/src/HOL/Tools/BNF/bnf_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_def_tactics.ML"
Presenting file "~~/src/HOL/Library/old_recdef.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_def.ML"
Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
Presenting theory "Word_Lib.More_Arithmetic"
Presenting theory "Word_Lib.More_Divides"
Presenting theory "Word_Lib.More_Bit_Ring"
Presenting theory "HOL-Library.Realizers"
Presenting file "~~/src/HOL/Tools/datatype_realizer.ML"
Presenting file "~~/src/HOL/Tools/inductive_realizer.ML"
Presenting theory "Bicategory.Modification"
Presenting theory "Word_Lib.More_Word"
Presenting theory "HOL.BNF_Composition"
Presenting file "~~/src/HOL/Tools/BNF/bnf_comp_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_comp.ML"
Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"
Presenting theory "HOL.Basic_BNFs"
Presenting theory "Word_Lib.Most_significant_bit"
Presenting theory "Word_Lib.Least_significant_bit"
Presenting theory "HOL-Library.Refute"
Presenting file "~~/src/HOL/Library/refute.ML"
Presenting theory "Word_Lib.Generic_set_bit"
Presenting theory "Word_Lib.Bit_Comprehension"
Presenting theory "HOL-Library.Signed_Division"
Presenting theory "Word_Lib.Signed_Division_Word"
Presenting theory "Native_Word.Code_Target_Word_Base"
Presenting theory "Native_Word.Word_Type_Copies"
Presenting theory "Native_Word.Code_Int_Integer_Conversion"
Presenting theory "Bicategory.ConcreteBicategory"
Presenting theory "Native_Word.Code_Target_Integer_Bit"
Presenting theory "Native_Word.Uint32"
Presenting theory "Collections.HashCode"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "HOL-Library.Code_Target_Numeral"
Presenting theory "Native_Word.Code_Target_Int_Bit"
Presenting theory "Collections.Code_Target_ICF"
Presenting theory "Collections.HashMap_Impl"
Presenting theory "Collections.HashMap"
Presenting theory "Collections.HashSet"
Presenting theory "Trie.Trie"
Presenting theory "Collections.Trie_Impl"
Presenting theory "Collections.Trie2"
Presenting theory "Collections.TrieMapImpl"
Presenting theory "Collections.TrieSetImpl"
Presenting theory "Collections.Diff_Array"
Presenting theory "Collections.ListGA"
Presenting theory "Collections.Array_Iterator"
Presenting theory "Bicategory.CatBicat"
Presenting theory "Collections.ArrayHashMap_Impl"
Presenting theory "Collections.ArrayHashMap"
Presenting theory "Collections.ArrayHashSet"
Presenting theory "Collections.ArrayMapImpl"
Presenting theory "Collections.ArraySetImpl"
Presenting theory "Collections.SetStdImpl"
Presenting theory "Collections.ListMapImpl_Invar"
Presenting theory "Collections.MapStdImpl"
Presenting theory "Collections.Fifo"
Presenting theory "HOL.BNF_Fixpoint_Base"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_util_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_util.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML"
Presenting theory "Binomial-Heaps.BinomialHeap"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML"
Presenting theory "Collections.BinoPrioImpl"
Presenting theory "Binomial-Heaps.SkewBinomialHeap"
Presenting theory "Collections.SkewPrioImpl"
Presenting theory "HOL.BNF_Least_Fixpoint"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_util.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_compat.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_size.ML"
Presenting file "~~/src/HOL/Tools/datatype_simprocs.ML"
Presenting theory "Finger-Trees.FingerTree"
Presenting theory "HOL.Equiv_Relations"
Presenting theory "HOL.Basic_BNF_LFPs"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML"
Presenting theory "Collections.FTAnnotatedListImpl"
Presenting theory "HOL.Meson"
Presenting file "~~/src/HOL/Tools/Meson/meson.ML"
Presenting theory "Collections.PrioByAnnotatedList"
Presenting file "~~/src/HOL/Tools/Meson/meson_clausify.ML"
Presenting file "~~/src/HOL/Tools/Meson/meson_tactic.ML"
Presenting theory "Collections.FTPrioImpl"
Presenting theory "Collections.PrioUniqueByAnnotatedList"
Presenting theory "Collections.FTPrioUniqueImpl"
Presenting theory "Collections.ICF_Impl"
Presenting theory "Collections.ICF_Refine_Monadic"
Presenting theory "Collections.Intf_Set"
Presenting theory "Collections.Intf_Map"
Presenting theory "Collections.ICF_Autoref"
Presenting theory "Collections.DatRef"
Presenting theory "Collections.Collections"
Presenting theory "Collections.CollectionsV1"
Presenting theory "JinjaThreads.JT_ICF"
Presenting theory "FinFun.FinFun"
Presenting theory "JinjaThreads.Auxiliary"
Presenting theory "HOL.ATP"
Presenting theory "JinjaThreads.Basic_Main"
Presenting file "~~/src/HOL/Tools/ATP/atp_util.ML"
Presenting file "~~/src/HOL/Tools/ATP/atp_problem.ML"
Presenting theory "JinjaThreads.FWState"
Presenting file "~~/src/HOL/Tools/ATP/atp_proof.ML"
Presenting file "~~/src/HOL/Tools/ATP/atp_proof_redirect.ML"
Presenting file "~~/src/HOL/Tools/lambda_lifting.ML"
Presenting file "~~/src/HOL/Tools/monomorph.ML"
Presenting file "~~/src/HOL/Tools/ATP/atp_problem_generate.ML"
Presenting theory "JinjaThreads.FWLock"
Presenting file "~~/src/HOL/Tools/ATP/atp_proof_reconstruct.ML"
Presenting theory "JinjaThreads.FWLocking"
Presenting theory "JinjaThreads.FWThread"
Presenting theory "JinjaThreads.FWWait"
Presenting theory "JinjaThreads.FWCondAction"
Presenting theory "JinjaThreads.FWWellform"
Presenting theory "JinjaThreads.FWLockingThread"
Presenting theory "JinjaThreads.FWInterrupt"
Presenting theory "JinjaThreads.FWSemantics"
Presenting theory "JinjaThreads.FWProgressAux"
Presenting theory "JinjaThreads.FWDeadlock"
Presenting theory "JinjaThreads.FWProgress"
Presenting theory "JinjaThreads.FWLifting"
Presenting theory "JinjaThreads.LTS"
Presenting theory "HOL.Metis"
Presenting file "~~/src/Tools/Metis/metis.ML"
Presenting theory "JinjaThreads.FWLTS"
Presenting file "~~/src/HOL/Tools/Metis/metis_generate.ML"
Presenting file "~~/src/HOL/Tools/Metis/metis_reconstruct.ML"
Presenting file "~~/src/HOL/Tools/Metis/metis_tactic.ML"
Presenting theory "JinjaThreads.Bisimulation"
Presenting theory "HOL.Transfer"
Presenting file "~~/src/HOL/Tools/Transfer/transfer.ML"
Presenting file "~~/src/HOL/Tools/Transfer/transfer_bnf.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML"
Presenting theory "HOL.Lifting"
Presenting theory "JinjaThreads.FWBisimulation"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_util.ML"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_info.ML"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_bnf.ML"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_term.ML"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_def.ML"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_setup.ML"
Presenting file "~~/src/HOL/Tools/Lifting/lifting_def_code_dt.ML"
Presenting theory "JinjaThreads.FWBisimDeadlock"
Presenting theory "JinjaThreads.FWLiftingSem"
Presenting theory "JinjaThreads.FWInitFinLift"
Presenting theory "HOL.Quotient"
Presenting theory "JinjaThreads.FWBisimLift"
Presenting file "~~/src/HOL/Tools/Quotient/quotient_info.ML"
Presenting file "~~/src/HOL/Tools/Quotient/quotient_term.ML"
Presenting file "~~/src/HOL/Tools/Quotient/quotient_type.ML"
Presenting file "~~/src/HOL/Tools/Quotient/quotient_def.ML"
Presenting file "~~/src/HOL/Tools/Quotient/quotient_tacs.ML"
Presenting theory "JinjaThreads.Semilat"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lift.ML"
Presenting theory "JinjaThreads.Err"
Presenting theory "JinjaThreads.Opt"
Presenting theory "JinjaThreads.Product"
Presenting theory "JinjaThreads.Listn"
Presenting theory "HOL.Num"
Presenting theory "JinjaThreads.Semilattices"
Presenting theory "JinjaThreads.Typing_Framework"
Presenting theory "JinjaThreads.SemilatAlg"
Presenting file "~~/src/HOL/Tools/numeral.ML"
Presenting theory "JinjaThreads.Typing_Framework_err"
Presenting theory "JinjaThreads.Kildall"
Presenting theory "HOL.Power"
Presenting theory "JinjaThreads.LBVSpec"
Presenting theory "JinjaThreads.LBVCorrect"
Presenting theory "JinjaThreads.LBVComplete"
Presenting theory "JinjaThreads.Abstract_BV"
Presenting theory "JinjaThreads.Type"
Presenting theory "JinjaThreads.Decl"
Presenting theory "HOL.Groups_Big"
Presenting theory "JinjaThreads.TypeRel"
Presenting theory "JinjaThreads.Value"
Presenting theory "JinjaThreads.Exceptions"
Presenting theory "JinjaThreads.SystemClasses"
Presenting theory "HOL.Complete_Partial_Order"
Presenting theory "JinjaThreads.Heap"
Presenting theory "JinjaThreads.Observable_Events"
Presenting theory "HOL.Option"
Presenting theory "JinjaThreads.StartConfig"
Presenting theory "JinjaThreads.Conform"
Presenting theory "HOL.Partial_Function"
Presenting file "~~/src/HOL/Tools/Function/partial_function.ML"
Presenting theory "JinjaThreads.ExternalCall"
Presenting theory "JinjaThreads.WellForm"
Presenting theory "JinjaThreads.ExternalCallWF"
Presenting theory "JinjaThreads.ConformThreaded"
Presenting theory "JinjaThreads.BinOp"
Presenting theory "JinjaThreads.SemiType"
Presenting theory "HOL.Argo"
Presenting theory "JinjaThreads.Common_Main"
Presenting theory "JinjaThreads.State"
Presenting file "~~/src/Tools/Argo/argo_expr.ML"
Presenting file "~~/src/Tools/Argo/argo_term.ML"
Presenting file "~~/src/Tools/Argo/argo_lit.ML"
Presenting file "~~/src/Tools/Argo/argo_proof.ML"
Presenting file "~~/src/Tools/Argo/argo_rewr.ML"
Presenting file "~~/src/Tools/Argo/argo_cls.ML"
Presenting file "~~/src/Tools/Argo/argo_common.ML"
Presenting file "~~/src/Tools/Argo/argo_cc.ML"
Presenting file "~~/src/Tools/Argo/argo_simplex.ML"
Presenting file "~~/src/Tools/Argo/argo_thy.ML"
Presenting file "~~/src/Tools/Argo/argo_heap.ML"
Presenting file "~~/src/Tools/Argo/argo_cdcl.ML"
Presenting file "~~/src/Tools/Argo/argo_core.ML"
Presenting file "~~/src/Tools/Argo/argo_clausify.ML"
Presenting file "~~/src/Tools/Argo/argo_solver.ML"
Presenting file "~~/src/HOL/Tools/Argo/argo_tactic.ML"
Presenting theory "JinjaThreads.Expr"
Presenting theory "JinjaThreads.JHeap"
Presenting theory "HOL.SAT"
Presenting file "~~/src/HOL/Tools/prop_logic.ML"
Presenting file "~~/src/HOL/Tools/sat_solver.ML"
Presenting file "~~/src/HOL/Tools/sat.ML"
Presenting file "~~/src/HOL/Tools/Argo/argo_sat_solver.ML"
Presenting theory "JinjaThreads.SmallStep"
Presenting theory "JinjaThreads.WWellForm"
Presenting theory "JinjaThreads.WellType"
Presenting theory "JinjaThreads.DefAss"
Presenting theory "JinjaThreads.JWellForm"
Presenting theory "HOL.Fun_Def"
Presenting file "~~/src/HOL/Tools/Function/function_core.ML"
Presenting file "~~/src/HOL/Tools/Function/mutual.ML"
Presenting file "~~/src/HOL/Tools/Function/pattern_split.ML"
Presenting file "~~/src/HOL/Tools/Function/relation.ML"
Presenting file "~~/src/HOL/Tools/Function/function_elims.ML"
Presenting file "~~/src/HOL/Tools/Function/function.ML"
Presenting file "~~/src/HOL/Tools/Function/pat_completeness.ML"
Presenting file "~~/src/HOL/Tools/Function/fun.ML"
Presenting file "~~/src/HOL/Tools/Function/induction_schema.ML"
Presenting file "~~/src/HOL/Tools/Function/measure_functions.ML"
Presenting file "~~/src/HOL/Tools/Function/lexicographic_order.ML"
Presenting theory "JinjaThreads.Threaded"
Presenting file "~~/src/HOL/Tools/Function/termination.ML"
Presenting file "~~/src/HOL/Tools/Function/scnp_solve.ML"
Presenting file "~~/src/HOL/Tools/Function/scnp_reconstruct.ML"
Presenting file "~~/src/HOL/Tools/Function/fun_cases.ML"
Presenting theory "JinjaThreads.WellTypeRT"
Presenting theory "HOL.Int"
Presenting theory "JinjaThreads.Progress"
Presenting file "~~/src/HOL/Tools/int_arith.ML"
Presenting theory "JinjaThreads.DefAssPreservation"
Presenting theory "HOL.Lattices_Big"
Presenting theory "JinjaThreads.TypeSafe"
Presenting theory "HOL.Euclidean_Rings"
Presenting theory "JinjaThreads.ProgressThreaded"
Presenting theory "JinjaThreads.Deadlocked"
Presenting theory "HOL.Parity"
Presenting theory "JinjaThreads.Annotate"
Presenting theory "JinjaThreads.J_Main"
Presenting theory "JinjaThreads.JVMState"
Presenting theory "JinjaThreads.JVMInstructions"
Presenting theory "JinjaThreads.JVMHeap"
Presenting theory "JinjaThreads.JVMExecInstr"
Presenting theory "HOL.Numeral_Simprocs"
Presenting theory "JinjaThreads.JVMExceptions"
Presenting file "~~/src/Provers/Arith/assoc_fold.ML"
Presenting file "~~/src/Provers/Arith/cancel_numerals.ML"
Presenting file "~~/src/Provers/Arith/combine_numerals.ML"
Presenting file "~~/src/Provers/Arith/cancel_numeral_factor.ML"
Presenting file "~~/src/Provers/Arith/extract_common_term.ML"
Presenting file "~~/src/HOL/Tools/numeral_simprocs.ML"
Presenting theory "JinjaThreads.JVMExec"
Presenting file "~~/src/HOL/Tools/nat_numeral_simprocs.ML"
Presenting theory "JinjaThreads.JVMDefensive"
Presenting theory "HOL.Semiring_Normalization"
Presenting theory "JinjaThreads.JVMThreaded"
Presenting file "~~/src/HOL/Tools/semiring_normalizer.ML"
Presenting theory "JinjaThreads.JVM_Main"
Presenting theory "JinjaThreads.JVM_SemiType"
Presenting theory "JinjaThreads.Effect"
Presenting theory "HOL.Groebner_Basis"
Presenting file "~~/src/HOL/Tools/groebner.ML"
Presenting theory "JinjaThreads.BVSpec"
Presenting theory "JinjaThreads.BVConform"
Presenting theory "HOL.Set_Interval"
Presenting theory "JinjaThreads.BVSpecTypeSafe"
Presenting theory "JinjaThreads.BVNoTypeError"
Presenting theory "JinjaThreads.BVProgressThreaded"
Presenting theory "HOL.Presburger"
Presenting file "~~/src/HOL/Tools/Qelim/qelim.ML"
Presenting file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"
Presenting theory "JinjaThreads.JVMDeadlocked"
Presenting file "~~/src/HOL/Tools/Qelim/cooper.ML"
Presenting file "~~/src/HOL/Tools/try0.ML"
Presenting theory "JinjaThreads.EffectMono"
Presenting theory "JinjaThreads.TF_JVM"
Presenting theory "JinjaThreads.LBVJVM"
Presenting theory "JinjaThreads.BVExec"
Presenting theory "JinjaThreads.BCVExec"
Presenting theory "JinjaThreads.BV_Main"
Presenting theory "JinjaThreads.CallExpr"
Presenting theory "JinjaThreads.J0"
Presenting theory "JinjaThreads.J0Bisim"
Presenting theory "JinjaThreads.J1State"
Presenting theory "JinjaThreads.J1Heap"
Presenting theory "HOL.SMT"
Presenting file "~~/src/HOL/Tools/SMT/smt_util.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_failure.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_config.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_builtin.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_datatypes.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_normalize.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_translate.ML"
Presenting file "~~/src/HOL/Tools/SMT/smtlib.ML"
Presenting file "~~/src/HOL/Tools/SMT/smtlib_interface.ML"
Presenting file "~~/src/HOL/Tools/SMT/smtlib_proof.ML"
Presenting file "~~/src/HOL/Tools/SMT/smtlib_isar.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_proof.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_isar.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_solver.ML"
Presenting theory "JinjaThreads.J1"
Presenting file "~~/src/HOL/Tools/SMT/cvc_interface.ML"
Presenting file "~~/src/HOL/Tools/SMT/lethe_proof.ML"
Presenting file "~~/src/HOL/Tools/SMT/lethe_isar.ML"
Presenting file "~~/src/HOL/Tools/SMT/lethe_proof_parse.ML"
Presenting file "~~/src/HOL/Tools/SMT/cvc_proof_parse.ML"
Presenting file "~~/src/HOL/Tools/SMT/conj_disj_perm.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_replay_methods.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_replay.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_replay_arith.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_interface.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_replay_rules.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_replay_methods.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_replay.ML"
Presenting file "~~/src/HOL/Tools/SMT/lethe_replay_methods.ML"
Presenting file "~~/src/HOL/Tools/SMT/cvc5_replay_methods.ML"
Presenting file "~~/src/HOL/Tools/SMT/verit_replay_methods.ML"
Presenting file "~~/src/HOL/Tools/SMT/verit_strategies.ML"
Presenting file "~~/src/HOL/Tools/SMT/verit_replay.ML"
Presenting file "~~/src/HOL/Tools/SMT/cvc5_replay.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_systems.ML"
Presenting theory "JinjaThreads.J1Deadlock"
Presenting theory "JinjaThreads.PCompiler"
Presenting theory "JinjaThreads.Compiler2"
Presenting theory "JinjaThreads.Exception_Tables"
Presenting theory "JinjaThreads.J1WellType"
Presenting theory "JinjaThreads.J1WellForm"
Presenting theory "HOL-Library.Prefix_Order"
Presenting theory "JinjaThreads.TypeComp"
Presenting theory "HOL.Sledgehammer"
Presenting file "~~/src/HOL/Tools/ATP/system_on_tptp.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML"
Presenting theory "JinjaThreads.JVMTau"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML"
Presenting file "~~/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML"
Presenting theory "HOL.Lifting_Set"
Presenting theory "JinjaThreads.Execs"
Presenting theory "HOL.List"
Presenting theory "HOL.Groups_List"
Presenting theory "HOL.Bit_Operations"
Presenting theory "HOL.Code_Numeral"
Presenting theory "HOL.Random"
Presenting theory "HOL.Map"
Presenting theory "JinjaThreads.J1JVMBisim"
Presenting theory "HOL.Enum"
Presenting theory "HOL.String"
Presenting file "~~/src/HOL/Tools/string_syntax.ML"
Presenting file "~~/src/HOL/Tools/literal.ML"
Presenting theory "HOL.Typerep"
Presenting theory "HOL.Predicate"
Presenting theory "HOL.Lazy_Sequence"
Presenting theory "HOL.Limited_Sequence"
Presenting theory "HOL.Code_Evaluation"
Presenting file "~~/src/HOL/Tools/code_evaluation.ML"
Presenting file "~~/src/HOL/Tools/value_command.ML"
Presenting file "~~/src/HOL/Tools/reification.ML"
Presenting theory "HOL.Quickcheck_Random"
Presenting file "~~/src/HOL/Tools/Quickcheck/quickcheck_common.ML"
Presenting file "~~/src/HOL/Tools/Quickcheck/random_generators.ML"
Presenting theory "HOL.Random_Pred"
Presenting theory "HOL.Random_Sequence"
Presenting theory "HOL.Quickcheck_Exhaustive"
Presenting file "~~/src/HOL/Tools/Quickcheck/exhaustive_generators.ML"
Presenting file "~~/src/HOL/Tools/Quickcheck/abstract_generators.ML"
Presenting theory "HOL.Predicate_Compile"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/core_data.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/mode_inference.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile.ML"
Presenting theory "HOL.Quickcheck_Narrowing"
Presenting file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"
Presenting file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"
Presenting file "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
Presenting file "~~/src/HOL/Tools/Quickcheck/find_unused_assms.ML"
Presenting theory "HOL.Mirabelle"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_util.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle.ML"
Presenting theory "JinjaThreads.J1JVM"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_arith.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_order.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_metis.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_presburger.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_try0.ML"
Presenting theory "HOL.Extraction"
Presenting theory "HOL.Record"
Presenting file "~~/src/HOL/Tools/record.ML"
Presenting theory "HOL.GCD"
Presenting theory "JinjaThreads.JVMJ1"
Presenting theory "JinjaThreads.Correctness2"
Presenting theory "HOL.Nitpick"
Presenting theory "JinjaThreads.ListIndex"
Presenting theory "JinjaThreads.Compiler1"
Presenting file "~~/src/HOL/Tools/Nitpick/kodkod.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/kodkod_sat.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_util.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_hol.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_mono.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_preproc.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_scope.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_peephole.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_rep.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_nut.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_kodkod.ML"
Presenting theory "JinjaThreads.J0J1Bisim"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_model.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_commands.ML"
Presenting file "~~/src/HOL/Tools/Nitpick/nitpick_tests.ML"
Presenting theory "JinjaThreads.Correctness1Threaded"
Presenting theory "HOL.Nunchaku"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_util.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_collect.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_problem.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_translate.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_model.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_display.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_tool.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku.ML"
Presenting file "~~/src/HOL/Tools/Nunchaku/nunchaku_commands.ML"
Presenting theory "JinjaThreads.Correctness1"
Presenting theory "HOL.BNF_Greatest_Fixpoint"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_util.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML"
Presenting theory "JinjaThreads.JJ1WellForm"
Presenting theory "JinjaThreads.Compiler"
Presenting theory "HOL.Filter"
Presenting theory "JinjaThreads.Correctness"
Presenting theory "JinjaThreads.Preprocessor"
Presenting theory "JinjaThreads.Compiler_Main"
Presenting theory "JinjaThreads.MM"
Presenting theory "JinjaThreads.SC"
Presenting theory "HOL.Conditionally_Complete_Lattices"
Presenting theory "JinjaThreads.SC_Interp"
Presenting theory "JinjaThreads.SC_Collections"
Presenting theory "HOL.Factorial"
Presenting theory "JinjaThreads.Orders"
Presenting theory "HOL.Binomial"
Presenting theory "HOL.Divides"
Presenting theory "Main"
Presenting theory "JinjaThreads.JMM_Spec"
Presenting theory "HOL.Archimedean_Field"
Presenting theory "HOL.Rat"
Presenting theory "JinjaThreads.JMM_DRF"
Presenting theory "JinjaThreads.SC_Legal"
Presenting theory "JinjaThreads.Non_Speculative"
Presenting theory "HOL.Real"
Presenting file "~~/src/HOL/Tools/SMT/smt_real.ML"
Presenting file "~~/src/HOL/Tools/SMT/z3_real.ML"
Presenting file "~~/src/HOL/Tools/Argo/argo_real.ML"
Presenting theory "JinjaThreads.SC_Completion"
Presenting theory "HOL.Topological_Spaces"
Presenting theory "JinjaThreads.HB_Completion"
Presenting theory "HOL.Hull"
Presenting theory "JinjaThreads.JMM_Heap"
Presenting theory "HOL.Modules"
Presenting theory "HOL.Vector_Spaces"
Presenting theory "HOL.Real_Vector_Spaces"
Presenting theory "HOL.Limits"
Presenting theory "JinjaThreads.JMM_Framework"
Presenting theory "HOL.Inequalities"
Presenting theory "HOL.Series"
Presenting theory "JinjaThreads.JMM_Typesafe"
Presenting theory "HOL.Deriv"
Presenting theory "JinjaThreads.JMM_Common"
Presenting theory "HOL.NthRoot"
Presenting theory "JinjaThreads.JMM_J"
Presenting theory "JinjaThreads.DRF_J"
Presenting theory "JinjaThreads.JMM_JVM"
Presenting theory "JinjaThreads.DRF_JVM"
Presenting theory "HOL.Transcendental"
Presenting theory "JinjaThreads.JMM_Type"
Presenting theory "JinjaThreads.JMM_Compiler"
Presenting theory "JinjaThreads.JMM_Type2"
Presenting theory "JinjaThreads.JMM_Interp"
Presenting theory "JinjaThreads.JMM_Typesafe2"
Presenting theory "JinjaThreads.JMM_J_Typesafe"
Presenting theory "JinjaThreads.JMM_JVM_Typesafe"
Presenting theory "JinjaThreads.JMM_Compiler_Type2"
Presenting theory "HOL.Complex"
Presenting theory "JinjaThreads.JMM"
Presenting theory "JinjaThreads.MM_Main"
Presenting theory "JinjaThreads.State_Refinement"
Presenting theory "HOL.MacLaurin"
Presenting theory "Complex_Main"
Presenting theory "JinjaThreads.Scheduler"
Presenting theory "JinjaThreads.Random_Scheduler"
Presenting theory "JinjaThreads.Round_Robin"
Presenting theory "JinjaThreads.SC_Schedulers"
Presenting theory "HOL-Library.Mapping"
Presenting theory "HOL-Library.AList_Mapping"
Presenting theory "JinjaThreads.TypeRelRefine"
Presenting theory "JinjaThreads.PCompilerRefine"
Presenting theory "JinjaThreads.J_Execute"
Presenting theory "JinjaThreads.ExternalCall_Execute"
Presenting theory "JinjaThreads.JVMExec_Execute2"
Presenting theory "JinjaThreads.JVM_Execute2"
Presenting theory "HOL-Library.Code_Cardinality"
Presenting theory "JinjaThreads.Code_Generation"
Presenting theory "JinjaThreads.JVMExec_Execute"
Presenting theory "JinjaThreads.JVM_Execute"
Presenting theory "JinjaThreads.ToString"
Presenting theory "JinjaThreads.Java2Jinja"
Presenting theory "JinjaThreads.Execute_Main"
Presenting theory "JinjaThreads.ApprenticeChallenge"
Presenting theory "JinjaThreads.BufferExample"
Presenting theory "JinjaThreads.Examples_Main"
Presenting theory "JinjaThreads.JinjaThreads"

=== TIMING ===

Group slow: 9:33:33 elapsed time, 32:04:40 cpu time, factor 3.36
Group AFP: 9:59:38 elapsed time, 33:55:42 cpu time, factor 3.39
Group main: 0:11:01 elapsed time, 0:39:56 cpu time, factor 3.62
Group timing: 0:05:37 elapsed time, 0:21:35 cpu time, factor 3.84
Group very_slow: 5:58:29 elapsed time, 13:51:16 cpu time, factor 2.32
Overall: 10:30:05 elapsed time, 34:36:03 cpu time, factor 3.29
Archiving artifacts
Started calculate disk usage of build
Finished Calculation of disk usage of build in 0 seconds
Started calculate disk usage of workspace
Finished Calculation of disk usage of workspace in 0 seconds
No emails were triggered.
Finished: SUCCESS