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 http://isabelle.in.tum.de/repos/isabelle/
real URL is https://isabelle.in.tum.de/repos/isabelle/
no changes found
[isabelle-nightly-slow] $ hg update --clean --rev default
15 files updated, 0 files merged, 0 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 e59d7d6fe1bde1f42dc7f590cae85f9f83bd805a --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(e59d7d6fe1bde1f42dc7f590cae85f9f83bd805a)" --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
1 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 88472837e52457aa0540336bbb4de22cdf14bf5a --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(88472837e52457aa0540336bbb4de22cdf14bf5a)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-nightly-slow] $ /bin/sh -xe /tmp/jenkins11686488048377597636.sh
+ Admin/jenkins/run_build slow
+ set -e
+ PROFILE=slow
+ shift
+ bin/isabelle components -a
+ bin/isabelle jedit -bf
### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-nightly-slow/lib/classes/isabelle.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
For more information on paths, see 'stack path' and 'stack exec env'
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 8.10.7
+ 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-test-15c840d48c9a/x86_64-linux"
ML_SYSTEM="polyml-5.9"
ML_OPTIONS="-H 4000 --maxheap 20G"
jobs = 1, threads = 8, numa = false

=== BUILD ===

Build started at Sat, 10 Sep 2022 23:34:16 GMT
Isabelle id 6308eaaa88f1
Build for AFP id 34a31d29f666

=== 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-Analysis (main timing)
Session AFP/Coinductive (AFP)
Session HOL/HOL-Eisbach
Session HOL/HOL-Number_Theory (main timing)
Session HOL/HOL-ex (timing)
Session AFP/Automatic_Refinement (AFP)
Session AFP/Refine_Monadic (AFP)
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 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, 1.379s elapsed time, 1.366s cpu time, 0.041s GC time, factor 0.99)
Finished Pure (0:00:24 elapsed time, 0:00:23 cpu time, factor 0.97)
Building HOL ...
HOL: theory Tools.Code_Generator
HOL: theory HOL.HOL
HOL: theory HOL.Argo
HOL: theory HOL.Orderings
HOL: theory HOL.Ctr_Sugar
HOL: theory HOL.Groups
HOL: theory HOL.SAT
HOL: theory HOL.Lattices
HOL: theory HOL.Boolean_Algebras
HOL: theory HOL.Set
HOL: theory HOL.Fun
HOL: theory HOL.Typedef
HOL: theory HOL.Rings
HOL: theory HOL.Complete_Lattices
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.Finite_Set
HOL: theory HOL.Relation
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.Int
HOL: theory HOL.Lattices_Big
HOL: theory HOL.Lifting_Set
HOL: theory HOL.Euclidean_Division
HOL: theory HOL.Parity
HOL: theory HOL.Divides
HOL: theory HOL.Set_Interval
HOL: theory HOL.Numeral_Simprocs
HOL: theory HOL.Semiring_Normalization
HOL: theory HOL.SMT
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.Random
HOL: theory HOL.String
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.Inequalities
HOL: theory HOL.Limits
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:26 elapsed time)
Preparing HOL/outline ...
Finished HOL/outline (0:00:48 elapsed time)
Timing HOL (8 threads, 255.793s elapsed time, 917.532s cpu time, 61.171s GC time, factor 3.59)
Finished HOL (0:05:14 elapsed time, 0:17:16 cpu time, factor 3.29)
Running JinjaThreads ...
JinjaThreads: theory HOL-Eisbach.Eisbach
JinjaThreads: theory Automatic_Refinement.Prio_List
JinjaThreads: theory Collections.ICF_Tools
JinjaThreads: theory Finger-Trees.FingerTree
JinjaThreads: theory Automatic_Refinement.Refine_Util_Bootstrap1
JinjaThreads: theory Automatic_Refinement.Foldi
JinjaThreads: theory HOL-Library.Adhoc_Overloading
JinjaThreads: theory HOL-Library.AList
JinjaThreads: theory Automatic_Refinement.Mk_Term_Antiquot
JinjaThreads: theory Automatic_Refinement.Mpat_Antiquot
JinjaThreads: theory Collections.Ord_Code_Preproc
JinjaThreads: theory HOL-Library.Monad_Syntax
JinjaThreads: theory HOL-Library.Cancellation
JinjaThreads: theory HOL-Library.Case_Converter
JinjaThreads: theory HOL-Library.Code_Abstract_Nat
JinjaThreads: theory Collections.Locale_Code
JinjaThreads: theory Automatic_Refinement.Refine_Util
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 HOL-Library.Infinite_Set
JinjaThreads: theory HOL-Library.Multiset
JinjaThreads: theory HOL-Library.Nat_Bijection
JinjaThreads: theory Automatic_Refinement.Anti_Unification
JinjaThreads: theory Automatic_Refinement.Attr_Comb
JinjaThreads: theory Automatic_Refinement.Autoref_Data
JinjaThreads: theory Automatic_Refinement.Named_Sorted_Thms
JinjaThreads: theory Automatic_Refinement.Indep_Vars
JinjaThreads: theory Automatic_Refinement.Mk_Record_Simp
JinjaThreads: theory Automatic_Refinement.Tagged_Solver
JinjaThreads: theory Automatic_Refinement.Select_Solve
JinjaThreads: theory HOL-Library.Dlist
JinjaThreads: theory HOL-Library.Old_Datatype
JinjaThreads: theory HOL-Library.Option_ord
JinjaThreads: theory HOL-Library.Phantom_Type
JinjaThreads: theory Trie.Trie
JinjaThreads: theory HOL-Library.Predicate_Compile_Alternative_Defs
JinjaThreads: theory HOL-Library.RBT_Impl
JinjaThreads: theory HOL-Library.Signed_Division
JinjaThreads: theory HOL-Library.Cardinality
JinjaThreads: theory HOL-Library.Sublist
JinjaThreads: theory HOL-Library.Transitive_Closure_Table
JinjaThreads: theory FinFun.FinFun
JinjaThreads: theory HOL-Library.Numeral_Type
JinjaThreads: theory HOL-Library.While_Combinator
JinjaThreads: theory HOL-Library.Type_Length
JinjaThreads: theory Collections.DatRef
JinjaThreads: theory HOL-Library.Countable
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.Word
JinjaThreads: theory Word_Lib.More_Arithmetic
JinjaThreads: theory JinjaThreads.Auxiliary
JinjaThreads: theory HOL-Library.Countable_Set
JinjaThreads: theory Binomial-Heaps.BinomialHeap
JinjaThreads: theory Binomial-Heaps.SkewBinomialHeap
JinjaThreads: theory HOL-ex.Quicksort
JinjaThreads: theory HOL-Library.Countable_Complete_Lattices
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 Word_Lib.Signed_Division_Word
JinjaThreads: theory Collections.SetIteratorOperations
JinjaThreads: theory Automatic_Refinement.Autoref_Phases
JinjaThreads: theory Automatic_Refinement.Autoref_Tagging
JinjaThreads: theory Automatic_Refinement.Relators
JinjaThreads: theory Refine_Monadic.Refine_Mono_Prover
JinjaThreads: theory Word_Lib.More_Word
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 Collections.Assoc_List
JinjaThreads: theory Collections.Dlist_add
JinjaThreads: theory Collections.Proper_Iterator
JinjaThreads: theory Automatic_Refinement.Parametricity
JinjaThreads: theory Automatic_Refinement.Autoref_Id_Ops
JinjaThreads: theory Collections.Diff_Array
JinjaThreads: theory Collections.Trie_Impl
JinjaThreads: theory Collections.It_to_It
JinjaThreads: theory Collections.SetIteratorGA
JinjaThreads: theory Collections.Trie2
JinjaThreads: theory Word_Lib.Least_significant_bit
JinjaThreads: theory Word_Lib.Most_significant_bit
JinjaThreads: theory Automatic_Refinement.Autoref_Fix_Rel
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 Coinductive.Lazy_LList
JinjaThreads: theory Automatic_Refinement.Autoref_Bindings_HOL
JinjaThreads: theory Coinductive.TLList
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_While
JinjaThreads: theory Refine_Monadic.Refine_More_Comb
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 Native_Word.Code_Target_Int_Bit
JinjaThreads: theory Native_Word.Uint32
JinjaThreads: theory Collections.Code_Target_ICF
JinjaThreads: theory Refine_Monadic.Refine_Monadic
JinjaThreads: theory Collections.HashCode
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.AnnotatedListSpec
JinjaThreads: theory Collections.ListSpec
JinjaThreads: theory Collections.MapSpec
JinjaThreads: theory Collections.PrioSpec
JinjaThreads: theory Collections.PrioUniqueSpec
JinjaThreads: theory Collections.SetSpec
JinjaThreads: theory Collections.BinoPrioImpl
JinjaThreads: theory Collections.SkewPrioImpl
JinjaThreads: theory Collections.ListGA
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.Prefix_Order
JinjaThreads: theory HOL-Library.Mapping
JinjaThreads: theory HOL-Library.Code_Cardinality
JinjaThreads: theory JinjaThreads.FWState
JinjaThreads: theory JinjaThreads.LTS
JinjaThreads: theory JinjaThreads.Type
JinjaThreads: theory JinjaThreads.ListIndex
JinjaThreads: theory JinjaThreads.Orders
JinjaThreads: theory JinjaThreads.Semilat
JinjaThreads: theory JinjaThreads.Err
JinjaThreads: theory JinjaThreads.Listn
JinjaThreads: theory HOL-Library.AList_Mapping
JinjaThreads: theory JinjaThreads.Opt
JinjaThreads: theory JinjaThreads.Product
JinjaThreads: theory JinjaThreads.Semilattices
JinjaThreads: theory JinjaThreads.Decl
JinjaThreads: theory JinjaThreads.Typing_Framework
JinjaThreads: theory JinjaThreads.SemilatAlg
JinjaThreads: theory JinjaThreads.Kildall
JinjaThreads: theory JinjaThreads.LBVSpec
JinjaThreads: theory JinjaThreads.Bisimulation
JinjaThreads: theory JinjaThreads.LBVComplete
JinjaThreads: theory JinjaThreads.LBVCorrect
JinjaThreads: theory JinjaThreads.Typing_Framework_err
JinjaThreads: theory JinjaThreads.Abstract_BV
JinjaThreads: theory JinjaThreads.TypeRel
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.FWLock
JinjaThreads: theory JinjaThreads.FWInterrupt
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.FWProgressAux
JinjaThreads: theory JinjaThreads.FWLiftingSem
JinjaThreads: theory JinjaThreads.JVMState
JinjaThreads: theory JinjaThreads.StartConfig
JinjaThreads: theory JinjaThreads.JMM_Spec
JinjaThreads: theory JinjaThreads.FWDeadlock
JinjaThreads: theory JinjaThreads.FWLTS
JinjaThreads: theory JinjaThreads.Conform
JinjaThreads: theory JinjaThreads.State_Refinement
JinjaThreads: theory JinjaThreads.ConformThreaded
JinjaThreads: theory JinjaThreads.ExternalCall
JinjaThreads: theory JinjaThreads.FWProgress
JinjaThreads: theory JinjaThreads.SC
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.Effect
JinjaThreads: theory JinjaThreads.JVMHeap
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.J1State
JinjaThreads: theory JinjaThreads.SmallStep
JinjaThreads: theory JinjaThreads.JVMDefensive
JinjaThreads: theory JinjaThreads.Annotate
JinjaThreads: theory JinjaThreads.J1Heap
JinjaThreads: theory JinjaThreads.J1WellType
JinjaThreads: theory JinjaThreads.JWellForm
JinjaThreads: theory JinjaThreads.JMM_Typesafe
JinjaThreads: theory JinjaThreads.WellTypeRT
JinjaThreads: theory JinjaThreads.JVMThreaded
JinjaThreads: theory JinjaThreads.J1WellForm
JinjaThreads: theory JinjaThreads.JVMExec_Execute
JinjaThreads: theory JinjaThreads.Compiler1
JinjaThreads: theory JinjaThreads.Compiler2
JinjaThreads: theory JinjaThreads.Preprocessor
JinjaThreads: theory JinjaThreads.JJ1WellForm
JinjaThreads: theory JinjaThreads.JMM_Common
JinjaThreads: theory JinjaThreads.JMM_JVM
JinjaThreads: theory JinjaThreads.JVM_Main
JinjaThreads: theory JinjaThreads.Compiler
JinjaThreads: theory JinjaThreads.Exception_Tables
JinjaThreads: theory JinjaThreads.JMM_Typesafe2
JinjaThreads: theory JinjaThreads.BVSpec
JinjaThreads: theory JinjaThreads.EffectMono
JinjaThreads: theory JinjaThreads.TF_JVM
JinjaThreads: theory JinjaThreads.BVConform
JinjaThreads: theory JinjaThreads.FWBisimDeadlock
JinjaThreads: theory JinjaThreads.FWBisimLift
JinjaThreads: theory JinjaThreads.J1
JinjaThreads: theory JinjaThreads.BVExec
JinjaThreads: theory JinjaThreads.LBVJVM
JinjaThreads: theory JinjaThreads.TypeComp
JinjaThreads: theory JinjaThreads.BVSpecTypeSafe
JinjaThreads: theory JinjaThreads.BVNoTypeError
JinjaThreads: theory JinjaThreads.BCVExec
JinjaThreads: theory JinjaThreads.JVMExec_Execute2
JinjaThreads: theory JinjaThreads.BVProgressThreaded
JinjaThreads: theory JinjaThreads.Common_Main
JinjaThreads: theory JinjaThreads.JVMTau
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.J1JVMBisim
JinjaThreads: theory JinjaThreads.J0
JinjaThreads: theory JinjaThreads.JMM_J
JinjaThreads: theory JinjaThreads.ProgressThreaded
JinjaThreads: theory JinjaThreads.JVMDeadlocked
JinjaThreads: theory JinjaThreads.DRF_JVM
JinjaThreads: theory JinjaThreads.JVM_Execute
JinjaThreads: theory JinjaThreads.JVM_Execute2
JinjaThreads: theory JinjaThreads.J_Execute
JinjaThreads: theory JinjaThreads.BV_Main
JinjaThreads: theory JinjaThreads.Deadlocked
JinjaThreads: theory JinjaThreads.DRF_J
JinjaThreads: theory JinjaThreads.J_Main
JinjaThreads: theory JinjaThreads.J0Bisim
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:22 elapsed time)
Preparing JinjaThreads/outline ...
Finished JinjaThreads/outline (0:00:34 elapsed time)
Timing JinjaThreads (8 threads, 3504.017s elapsed time, 16153.069s cpu time, 6342.127s GC time, factor 4.61)
Finished JinjaThreads (0:58:26 elapsed time, 4:29:15 cpu time, factor 4.61)
Building Flyspeck-Tame ...
Flyspeck-Tame: theory Flyspeck-Tame.Quasi_Order
Flyspeck-Tame: theory Flyspeck-Tame.RTranCl
Flyspeck-Tame: theory HOL-Library.AList
Flyspeck-Tame: theory HOL-Library.Code_Abstract_Nat
Flyspeck-Tame: theory HOL-Library.Code_Target_Int
Flyspeck-Tame: theory Flyspeck-Tame.ListAux
Flyspeck-Tame: theory HOL-Library.IArray
Flyspeck-Tame: theory HOL-Library.While_Combinator
Flyspeck-Tame: theory Flyspeck-Tame.PlaneGraphIso
Flyspeck-Tame: theory HOL-Library.Code_Target_Nat
Flyspeck-Tame: theory HOL-Library.Code_Target_Numeral
Flyspeck-Tame: theory Flyspeck-Tame.Arch
Flyspeck-Tame: theory Flyspeck-Tame.Worklist
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.Invariants
Flyspeck-Tame: theory Flyspeck-Tame.ArchCompAux
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:13 elapsed time)
Preparing Flyspeck-Tame/outline ...
Finished Flyspeck-Tame/outline (0:00:06 elapsed time)
Timing Flyspeck-Tame (8 threads, 65.891s elapsed time, 352.532s cpu time, 28.526s GC time, factor 5.35)
Finished Flyspeck-Tame (0:01:43 elapsed time, 0:07:06 cpu time, factor 4.14)
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, 16113.507s elapsed time, 24142.619s cpu time, 864.117s GC time, factor 1.50)
Finished Flyspeck-Tame-Computation (4:28:35 elapsed time, 6:42:24 cpu time, factor 1.50)
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.AWN_SOS_Labels
AWN: theory AWN.Closed
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.OClosed_Transfer
AWN: theory AWN.OAWN_Convert
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:08 elapsed time)
Preparing AWN/outline ...
Finished AWN/outline (0:00:05 elapsed time)
Timing AWN (8 threads, 37.222s elapsed time, 181.682s cpu time, 8.572s GC time, factor 4.88)
Finished AWN (0:01:08 elapsed time, 0:04:00 cpu time, factor 3.53)
Running AODV ...
AODV: theory AODV.Aodv_Basic
AODV: theory AODV.Aodv_Data
AODV: theory AODV.A_Norreqid
AODV: theory AODV.Aodv_Message
AODV: theory AODV.B_Fwdrreps
AODV: theory AODV.C_Gtobcast
AODV: theory AODV.D_Fwdrreqs
AODV: theory AODV.E_All_ABCD
AODV: theory AODV.C_Aodv_Data
AODV: theory AODV.C_Aodv_Message
AODV: theory AODV.A_Aodv_Data
AODV: theory AODV.A_Aodv_Message
AODV: theory AODV.B_Aodv_Data
AODV: theory AODV.B_Aodv_Message
AODV: theory AODV.C_Fresher
AODV: theory AODV.D_Aodv_Data
AODV: theory AODV.D_Aodv_Message
AODV: theory AODV.E_Aodv_Data
AODV: theory AODV.B_Fresher
AODV: theory AODV.Fresher
AODV: theory AODV.A_Fresher
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_Loop_Freedom
AODV: theory AODV.C_Quality_Increases
AODV: theory AODV.C_Seq_Invariants
AODV: theory AODV.C_OAodv
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.E_Aodv_Predicates
AODV: theory AODV.E_OAodv
AODV: theory AODV.Global_Invariants
AODV: theory AODV.E_Loop_Freedom
AODV: theory AODV.E_Quality_Increases
AODV: theory AODV.E_Seq_Invariants
AODV: theory AODV.B_Aodv_Predicates
AODV: theory AODV.B_OAodv
AODV: theory AODV.Aodv_Loop_Freedom
AODV: theory AODV.E_Global_Invariants
AODV: theory AODV.B_Loop_Freedom
AODV: theory AODV.B_Quality_Increases
AODV: theory AODV.B_Seq_Invariants
AODV: theory AODV.E_Aodv_Loop_Freedom
AODV: theory AODV.B_Global_Invariants
AODV: theory AODV.B_Aodv_Loop_Freedom
AODV: theory AODV.D_Aodv_Predicates
AODV: theory AODV.D_OAodv
AODV: theory AODV.D_Loop_Freedom
AODV: theory AODV.D_Quality_Increases
AODV: theory AODV.D_Seq_Invariants
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:18 elapsed time)
Preparing AODV/outline ...
Finished AODV/outline (0:00:10 elapsed time)
Timing AODV (8 threads, 5036.952s elapsed time, 30657.252s cpu time, 1005.820s GC time, factor 6.09)
Finished AODV (1:23:59 elapsed time, 8:30:59 cpu time, factor 6.08)
Building Word_Lib ...
Word_Lib: theory HOL-Library.Signed_Division
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_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 Word_Lib.More_Arithmetic
Word_Lib: theory HOL-Library.Word
Word_Lib: theory Word_Lib.Bit_Comprehension
Word_Lib: theory Word_Lib.Legacy_Aliases
Word_Lib: theory Word_Lib.More_Divides
Word_Lib: theory Word_Lib.Signed_Division_Word
Word_Lib: theory Word_Lib.More_Word
Word_Lib: theory Word_Lib.Bit_Shifts_Infix_Syntax
Word_Lib: theory Word_Lib.Least_significant_bit
Word_Lib: theory Word_Lib.Many_More
Word_Lib: theory Word_Lib.Strict_part_mono
Word_Lib: theory Word_Lib.Aligned
Word_Lib: theory Word_Lib.Singleton_Bit_Shifts
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.Typedef_Morphisms
Word_Lib: theory Word_Lib.Reversed_Bit_Lists
Word_Lib: theory Word_Lib.Bitwise
Word_Lib: theory Word_Lib.Examples
Word_Lib: theory HOL-Eisbach.Eisbach
Word_Lib: theory Word_Lib.Bit_Comprehension_Int
Word_Lib: theory Word_Lib.Hex_Words
Word_Lib: theory Word_Lib.Syntax_Bundles
Word_Lib: theory Word_Lib.Word_Syntax
Word_Lib: theory Word_Lib.Type_Syntax
Word_Lib: theory Word_Lib.Enumeration
Word_Lib: theory Word_Lib.Signed_Words
Word_Lib: theory Word_Lib.Rsplit
Word_Lib: theory Word_Lib.Norm_Words
Word_Lib: theory Word_Lib.Word_Names
Word_Lib: theory Word_Lib.Word_16
Word_Lib: theory Word_Lib.Bitwise_Signed
Word_Lib: theory Word_Lib.Enumeration_Word
Word_Lib: theory HOL-Eisbach.Eisbach_Tools
Word_Lib: theory Word_Lib.Word_EqI
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_64
Word_Lib: theory Word_Lib.Word_32
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
Preparing Word_Lib/document ...
Finished Word_Lib/document (0:00:03 elapsed time)
Preparing Word_Lib/outline ...
Finished Word_Lib/outline (0:00:02 elapsed time)
Timing Word_Lib (8 threads, 40.659s elapsed time, 210.200s cpu time, 14.179s GC time, factor 5.17)
Finished Word_Lib (0:01:04 elapsed time, 0:04:16 cpu time, factor 3.96)
Building IP_Addresses ...
IP_Addresses: theory HOL-Library.Cancellation
IP_Addresses: theory IP_Addresses.NumberWang_IPv4
IP_Addresses: theory IP_Addresses.NumberWang_IPv6
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 HOL-Library.Code_Abstract_Nat
IP_Addresses: theory HOL-Library.Product_Lexorder
IP_Addresses: theory IP_Addresses.Lib_Numbers_toString
IP_Addresses: theory IP_Addresses.WordInterval
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.IPv6
IP_Addresses: theory IP_Addresses.Prefix_Match
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:03 elapsed time)
Preparing IP_Addresses/outline ...
Finished IP_Addresses/outline (0:00:02 elapsed time)
Timing IP_Addresses (8 threads, 205.764s elapsed time, 670.028s cpu time, 44.465s GC time, factor 3.26)
Finished IP_Addresses (0:04:12 elapsed time, 0:12:41 cpu time, factor 3.02)
Building Simple_Firewall ...
Simple_Firewall: theory Simple_Firewall.GroupF
Simple_Firewall: theory Simple_Firewall.Firewall_Common_Decision_State
Simple_Firewall: theory Simple_Firewall.IP_Partition_Preliminaries
Simple_Firewall: theory Simple_Firewall.List_Product_More
Simple_Firewall: theory Simple_Firewall.Option_Helpers
Simple_Firewall: theory Simple_Firewall.IP_Addr_WordInterval_toString
Simple_Firewall: theory Simple_Firewall.Lib_Enum_toString
Simple_Firewall: theory HOL-Library.Char_ord
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.Generic_SimpleFw
Simple_Firewall: theory Simple_Firewall.Shadowed
Simple_Firewall: theory Simple_Firewall.Service_Matrix
Preparing Simple_Firewall/document ...
Finished Simple_Firewall/document (0:00:06 elapsed time)
Preparing Simple_Firewall/outline ...
Finished Simple_Firewall/outline (0:00:05 elapsed time)
Timing Simple_Firewall (8 threads, 18.403s elapsed time, 77.442s cpu time, 6.221s GC time, factor 4.21)
Finished Simple_Firewall (0:00:43 elapsed time, 0:02:05 cpu time, factor 2.89)
Building Routing ...
Routing: theory HOL-Library.Adhoc_Overloading
Routing: theory Routing.Linorder_Helper
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:01 elapsed time)
Preparing Routing/outline ...
Finished Routing/outline (0:00:01 elapsed time)
Timing Routing (8 threads, 9.101s elapsed time, 28.126s cpu time, 1.228s GC time, factor 3.09)
Finished Routing (0:00:27 elapsed time, 0:01:02 cpu time, factor 2.27)
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.Code_Target_Int
Iptables_Semantics: theory Iptables_Semantics.Negation_Type_DNF
Iptables_Semantics: theory Iptables_Semantics.Datatype_Selectors
Iptables_Semantics: theory Iptables_Semantics.Remdups_Rev
Iptables_Semantics: theory Iptables_Semantics.Repeat_Stabilize
Iptables_Semantics: theory Iptables_Semantics.Ternary
Iptables_Semantics: theory Native_Word.Code_Int_Integer_Conversion
Iptables_Semantics: theory HOL-Library.LaTeXsugar
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.Firewall_Common
Iptables_Semantics: theory Iptables_Semantics.Word_Upto
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.Semantics_Stateful
Iptables_Semantics: theory Iptables_Semantics.Ruleset_Update
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.Ports_Normalize
Iptables_Semantics: theory Iptables_Semantics.IpAddresses_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:19 elapsed time)
Preparing Iptables_Semantics/outline ...
Finished Iptables_Semantics/outline (0:00:09 elapsed time)
Timing Iptables_Semantics (8 threads, 109.311s elapsed time, 508.863s cpu time, 49.907s GC time, factor 4.66)
Finished Iptables_Semantics (0:02:44 elapsed time, 0:10:18 cpu time, factor 3.75)
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.Contrived_Example
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser_Test
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.SQRL_2015_nospoof
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Parser6_Test
Iptables_Semantics_Examples: theory Iptables_Semantics_Examples.Analyze_medium_sized_company
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:04 elapsed time)
Preparing Iptables_Semantics_Examples/outline ...
Finished Iptables_Semantics_Examples/outline (0:00:03 elapsed time)
Timing Iptables_Semantics_Examples (8 threads, 240.999s elapsed time, 1280.330s cpu time, 121.052s GC time, factor 5.31)
Finished Iptables_Semantics_Examples (0:04:25 elapsed time, 0:22:07 cpu time, factor 5.00)
Running Iptables_Semantics_Examples_Big ...
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_Containern
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_topos_generated
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.TUM_Spoofing_new3
Iptables_Semantics_Examples_Big: theory Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall
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:03 elapsed time)
Preparing Iptables_Semantics_Examples_Big/outline ...
Finished Iptables_Semantics_Examples_Big/outline (0:00:03 elapsed time)
Timing Iptables_Semantics_Examples_Big (8 threads, 7392.784s elapsed time, 32735.954s cpu time, 12603.519s GC time, factor 4.43)
Finished Iptables_Semantics_Examples_Big (2:03:16 elapsed time, 9:05:39 cpu time, factor 4.43)
Building HOL-Library ...
HOL-Library: theory HOL-Library.README
HOL-Library: theory HOL-Library.Case_Converter
HOL-Library: theory HOL-Library.Char_ord
HOL-Library: theory HOL-Library.Code_Abstract_Nat
HOL-Library: theory HOL-Library.Cancellation
HOL-Library: theory HOL-Library.BNF_Corec
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.Code_Binary_Nat
HOL-Library: theory HOL-Library.Code_Abstract_Char
HOL-Library: theory HOL-Library.Monad_Syntax
HOL-Library: theory HOL-Library.Code_Target_Nat
HOL-Library: theory HOL-Library.State_Monad
HOL-Library: theory HOL-Library.Code_Prolog
HOL-Library: theory HOL-Library.Code_Target_Int
HOL-Library: theory HOL-Library.Code_Lazy
HOL-Library: theory HOL-Library.Multiset
HOL-Library: theory HOL-Library.Simps_Case_Conv
HOL-Library: theory HOL-Library.Extended
HOL-Library: theory HOL-Library.Code_Target_Numeral
HOL-Library: theory HOL-Library.Code_Test
HOL-Library: theory HOL-Library.Combine_PER
HOL-Library: theory HOL-Library.Comparator
HOL-Library: theory HOL-Library.Complete_Partial_Order2
HOL-Library: theory HOL-Library.DAList
HOL-Library: theory HOL-Library.Conditional_Parametricity
HOL-Library: theory HOL-Library.Confluence
HOL-Library: theory HOL-Library.Confluent_Quotient
HOL-Library: theory HOL-Library.Datatype_Records
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.Groups_Big_Fun
HOL-Library: theory HOL-Library.IArray
HOL-Library: theory HOL-Library.Function_Division
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.Equipollence
HOL-Library: theory HOL-Library.Omega_Words_Fun
HOL-Library: theory HOL-Library.Ramsey
HOL-Library: theory HOL-Library.Lattice_Constructions
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.Old_Datatype
HOL-Library: theory HOL-Library.Stream
HOL-Library: theory HOL-Library.Old_Recdef
HOL-Library: theory HOL-Library.AList_Mapping
HOL-Library: theory HOL-Library.Open_State_Syntax
HOL-Library: theory HOL-Library.DAList_Multiset
HOL-Library: theory HOL-Library.Multiset_Order
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.Product_Lexorder
HOL-Library: theory HOL-Library.Product_Plus
HOL-Library: theory HOL-Library.Quotient_Syntax
HOL-Library: theory HOL-Library.Quotient_Option
HOL-Library: theory HOL-Library.Predicate_Compile_Quickcheck
HOL-Library: theory HOL-Library.Product_Order
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.RBT_Impl
HOL-Library: theory HOL-Library.Finite_Lattice
HOL-Library: theory HOL-Library.Realizers
HOL-Library: theory HOL-Library.Cardinality
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.Signed_Division
HOL-Library: theory HOL-Library.Sorting_Algorithms
HOL-Library: theory HOL-Library.Sublist
HOL-Library: theory HOL-Library.Code_Cardinality
HOL-Library: theory HOL-Library.Numeral_Type
HOL-Library: theory HOL-Library.Transitive_Closure_Table
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.Type_Length
HOL-Library: theory HOL-Library.Bourbaki_Witt_Fixpoint
HOL-Library: theory HOL-Library.Countable
HOL-Library: theory HOL-Library.BigO
HOL-Library: theory HOL-Library.Prefix_Order
HOL-Library: theory HOL-Library.Subseq_Order
HOL-Library: theory HOL-Library.Saturated
HOL-Library: theory HOL-Library.Word
HOL-Library: theory HOL-Library.Code_Real_Approx_By_Float
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.Tree_Multiset
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.Liminf_Limsup
HOL-Library: theory HOL-Library.Countable_Complete_Lattices
HOL-Library: theory HOL-Library.Countable_Set_Type
HOL-Library: theory HOL-Library.Set_Idioms
HOL-Library: theory HOL-Library.Log_Nat
HOL-Library: theory HOL-Library.Lub_Glb
HOL-Library: theory HOL-Library.Nonpos_Ints
HOL-Library: theory HOL-Library.OptionalSugar
HOL-Library: theory HOL-Library.Periodic_Fun
HOL-Library: theory HOL-Library.Order_Continuity
HOL-Library: theory HOL-Library.Quadratic_Discriminant
HOL-Library: theory HOL-Library.Sum_of_Squares
HOL-Library: theory HOL-Library.Tree_Real
HOL-Library: theory HOL-Library.Extended_Nat
HOL-Library: theory HOL-Library.Finite_Map
HOL-Library: theory HOL-Library.Extended_Real
HOL-Library: theory HOL-Library.Linear_Temporal_Logic_on_Streams
HOL-Library: theory HOL-Library.Interval
HOL-Library: theory HOL-Library.Float
HOL-Library: theory HOL-Library.Extended_Nonnegative_Real
HOL-Library: theory HOL-Library.Code_Target_Numeral_Float
HOL-Library: theory HOL-Library.Interval_Float
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:00:50 elapsed time)
Preparing HOL-Library/outline ...
Finished HOL-Library/outline (0:00:28 elapsed time)
Timing HOL-Library (8 threads, 143.870s elapsed time, 876.733s cpu time, 50.025s GC time, factor 6.09)
Finished HOL-Library (0:03:30 elapsed time, 0:16:47 cpu time, factor 4.79)
Building Category3 ...
Category3: theory Category3.Category
Category3: theory HOL-Cardinals.Fun_More
Category3: theory HOL-Cardinals.Order_Relation_More
Category3: theory HOL-Cardinals.Order_Union
Category3: theory HereditarilyFinite.HF
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.DualCategory
Category3: theory Category3.EpiMonoIso
Category3: theory HOL-Cardinals.Wellorder_Embedding
Category3: theory HOL-Cardinals.Wellorder_Constructions
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.BinaryFunctor
Category3: theory Category3.SetCategory
Category3: theory Category3.FunctorCategory
Category3: theory Category3.SetCat
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.CartesianCategory
Category3: theory Category3.CartesianClosedCategory
Category3: theory Category3.CategoryWithFiniteLimits
Category3: theory Category3.HFSetCat
Preparing Category3/document ...
Finished Category3/document (0:00:23 elapsed time)
Preparing Category3/outline ...
Finished Category3/outline (0:00:08 elapsed time)
Timing Category3 (8 threads, 304.028s elapsed time, 1520.502s cpu time, 129.844s GC time, factor 5.00)
Finished Category3 (0:06:21 elapsed time, 0:27:55 cpu time, factor 4.39)
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:11 elapsed time)
Preparing MonoidalCategory/outline ...
Finished MonoidalCategory/outline (0:00:05 elapsed time)
Timing MonoidalCategory (8 threads, 314.939s elapsed time, 717.033s cpu time, 60.354s GC time, factor 2.28)
Finished MonoidalCategory (0:06:24 elapsed time, 0:14:13 cpu time, factor 2.22)
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:28 elapsed time)
Preparing Bicategory/outline ...
Finished Bicategory/outline (0:00:17 elapsed time)
Timing Bicategory (8 threads, 4373.102s elapsed time, 11299.086s cpu time, 2077.304s GC time, factor 2.58)
Finished Bicategory (1:12:59 elapsed time, 3:08:25 cpu time, factor 2.58)
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:04 elapsed time)
Preparing ConcurrentIMP/outline ...
Finished ConcurrentIMP/outline (0:00:03 elapsed time)
Timing ConcurrentIMP (8 threads, 20.257s elapsed time, 71.657s cpu time, 5.544s GC time, factor 3.54)
Finished ConcurrentIMP (0:00:45 elapsed time, 0:02:00 cpu time, factor 2.63)
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:08 elapsed time)
Preparing ConcurrentGC/outline ...
Finished ConcurrentGC/outline (0:00:06 elapsed time)
Timing ConcurrentGC (8 threads, 949.727s elapsed time, 5602.713s cpu time, 196.947s GC time, factor 5.90)
Finished ConcurrentGC (0:15:52 elapsed time, 1:33:25 cpu time, factor 5.88)
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 AWN in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AWN" ...
Presenting AODV in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/AODV" ...
Presenting Flyspeck-Tame in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame" ...
Presenting Flyspeck-Tame-Computation in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Flyspeck-Tame-Computation" ...
Presenting HOL-Library in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/HOL/HOL-Library" ...
Presenting Category3 in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Category3" ...
Presenting MonoidalCategory in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/MonoidalCategory" ...
Presenting document MonoidalCategory/document
Presenting document MonoidalCategory/outline
Presenting document Flyspeck-Tame/document
Presenting document AWN/document
Presenting document Flyspeck-Tame/outline
Presenting theory "Flyspeck-Tame-Computation.ArchComp"
Presenting document AWN/outline
Presenting document Category3/document
Presenting document Category3/outline
Presenting document AODV/document
Presenting document AODV/outline
Presenting theory "AODV.Aodv_Basic"
Presenting theory "AWN.Lib"
Presenting theory "Flyspeck-Tame-Computation.Completeness"
Presenting theory "AWN.TransitionSystems"
Presenting Bicategory in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Bicategory" ...
Presenting document HOL/document
Presenting document Bicategory/document
Presenting document Bicategory/outline
Presenting document HOL/outline
Presenting theory "Bicategory.IsomorphismClass"
Presenting theory "Category3.Category"
Presenting document HOL-Library/document
Presenting document HOL-Library/outline
Presenting theory "AWN.Invariants"
Presenting theory "HOL-Library.README"
Presenting theory "Category3.DualCategory"
Presenting theory "Category3.ConcreteCategory"
Presenting theory "Flyspeck-Tame.ListAux"
Presenting theory "HOL-Library.AList"
Presenting theory "Flyspeck-Tame.Quasi_Order"
Presenting theory "Category3.EpiMonoIso"
Presenting theory "Category3.InitialTerminal"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "AWN.OInvariants"
Presenting theory "HOL-Library.Function_Algebras"
Presenting theory "AODV.Aodv_Data"
Presenting theory "AODV.Aodv_Message"
Presenting theory "HOL-Library.Set_Algebras"
Presenting theory "Flyspeck-Tame.PlaneGraphIso"
Presenting theory "Category3.Functor"
Presenting theory "Flyspeck-Tame.Rotation"
Presenting theory "Pure"
Presenting file "~~/src/Pure/ROOT0.ML"
Presenting file "~~/src/Pure/ROOT.ML"
Presenting theory "Bicategory.Prebicategory"
Presenting theory "ML_Bootstrap"
Presenting theory "Flyspeck-Tame.Graph"
Presenting theory "HOL-Library.BigO"
Presenting theory "Category3.Subcategory"
Presenting theory "HOL-Library.IArray"
Presenting theory "Flyspeck-Tame.IArray_Syntax"
Presenting theory "AODV.Aodv"
Presenting theory "Flyspeck-Tame.Enumerator"
Presenting theory "Pure.Sessions"
Presenting theory "AWN.AWN"
Presenting theory "Flyspeck-Tame.FaceDivision"
Presenting theory "HOL-Library.BNF_Axiomatization"
Presenting file "~~/src/HOL/Tools/BNF/bnf_axiomatization.ML"
Presenting theory "AODV.Aodv_Predicates"
Presenting theory "Flyspeck-Tame.RTranCl"
Presenting theory "Flyspeck-Tame.Plane"
Presenting theory "Flyspeck-Tame.Plane1"
Presenting theory "Flyspeck-Tame.GraphProps"
Presenting theory "AWN.AWN_SOS"
Presenting theory "MonoidalCategory.MonoidalCategory"
Presenting theory "Flyspeck-Tame.EnumeratorProps"
Presenting theory "Category3.SetCategory"
Presenting theory "AODV.Fresher"
Presenting theory "Bicategory.Bicategory"
Presenting theory "MonoidalCategory.MonoidalFunctor"
Presenting theory "AWN.AWN_Cterms"
Presenting theory "AODV.Seq_Invariants"
Presenting theory "AWN.AWN_Labels"
Presenting theory "AWN.Inv_Cterms"
Presenting theory "AWN.AWN_SOS_Labels"
Presenting theory "Category3.SetCat"
Presenting theory "Category3.ProductCategory"
Presenting theory "AODV.Quality_Increases"
Presenting theory "AODV.OAodv"
Presenting theory "AWN.Pnet"
Presenting theory "Category3.NaturalTransformation"
Presenting theory "AWN.Closed"
Presenting theory "Category3.BinaryFunctor"
Presenting theory "MonoidalCategory.FreeMonoidalCategory"
Presenting theory "AWN.OAWN_SOS"
Presenting theory "Bicategory.Coherence"
Presenting theory "AWN.OAWN_SOS_Labels"
Presenting theory "AWN.OPnet"
Presenting theory "Category3.FunctorCategory"
Presenting theory "MonoidalCategory.CartesianMonoidalCategory"
Presenting theory "Flyspeck-Tame.FaceDivisionProps"
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 "ConcurrentIMP.Infinite_Sequences"
Presenting theory "AODV.Global_Invariants"
Presenting theory "AWN.ONode_Lifting"
Presenting theory "Bicategory.CanonicalIsos"
Presenting theory "Category3.Yoneda"
Presenting theory "ConcurrentIMP.LTL"
Presenting theory "AODV.Loop_Freedom"
Presenting theory "ConcurrentIMP.CIMP_lang"
Presenting theory "AODV.Aodv_Loop_Freedom"
Presenting theory "AODV.A_Norreqid"
Presenting theory "Bicategory.Subbicategory"
Presenting theory "AWN.OPnet_Lifting"
Presenting theory "ConcurrentIMP.CIMP_vcg"
Presenting theory "AWN.OClosed_Lifting"
Presenting theory "ConcurrentIMP.CIMP_vcg_rules"
Presenting theory "ConcurrentIMP.CIMP"
Presenting file "$AFP/ConcurrentIMP/cimp.ML"
Presenting theory "ConcurrentIMP.CIMP_locales"
Presenting theory "Flyspeck-Tame.Invariants"
Presenting theory "ConcurrentIMP.CIMP_one_place_buffer"
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 "Bicategory.InternalEquivalence"
Presenting theory "HOL-Library.BNF_Corec"
Presenting theory "Tools.Code_Generator"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML"
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 theory "AODV.A_Aodv_Data"
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 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/Tools/Code/code_namespace.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML"
Presenting file "~~/src/Tools/Code/code_ml.ML"
Presenting theory "AWN.AWN_Invariants"
Presenting file "~~/src/Tools/Code/code_haskell.ML"
Presenting file "~~/src/Tools/Code/code_scala.ML"
Presenting theory "AODV.A_Aodv_Message"
Presenting file "~~/src/Tools/Code/code_runtime.ML"
Presenting theory "Flyspeck-Tame.PlaneProps"
Presenting theory "ConcurrentGC.Model"
Presenting file "~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML"
Presenting file "~~/src/Tools/nbe.ML"
Presenting theory "Flyspeck-Tame.ListSum"
Presenting theory "Flyspeck-Tame.Tame"
Presenting theory "Flyspeck-Tame.Plane1Props"
Presenting theory "Flyspeck-Tame.Generator"
Presenting theory "HOL-Library.While_Combinator"
Presenting theory "Flyspeck-Tame.TameProps"
Presenting theory "Flyspeck-Tame.TameEnum"
Presenting theory "HOL-Library.Bourbaki_Witt_Fixpoint"
Presenting theory "AODV.A_Aodv"
Presenting theory "HOL-Library.Char_ord"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "ConcurrentGC.Proofs_Basis"
Presenting theory "AODV.A_Aodv_Predicates"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "ConcurrentGC.Global_Invariants"
Presenting theory "HOL-Library.Code_Cardinality"
Presenting theory "Flyspeck-Tame.ScoreProps"
Presenting theory "Flyspeck-Tame.LowerBound"
Presenting theory "Category3.Adjunction"
Presenting theory "AWN.OAWN_Invariants"
Presenting theory "ConcurrentGC.Local_Invariants"
Presenting theory "HOL-Library.Case_Converter"
Presenting file "~~/src/HOL/Library/case_converter.ML"
Presenting theory "Flyspeck-Tame.GeneratorProps"
Presenting theory "Flyspeck-Tame.TameEnumProps"
Presenting theory "AWN.OAWN_Convert"
Presenting theory "AWN.Qmsg"
Presenting theory "AODV.A_Fresher"
Presenting theory "HOL-Library.Code_Lazy"
Presenting file "~~/src/HOL/Library/code_lazy.ML"
Presenting theory "Bicategory.Pseudofunctor"
Presenting theory "ConcurrentGC.Tactics"
Presenting theory "Category3.EquivalenceOfCategories"
Presenting theory "HOL-Library.AList"
Presenting theory "HOL-Library.Code_Test"
Presenting file "~~/src/HOL/Library/code_test.ML"
Presenting theory "HOL-Library.Combine_PER"
Presenting theory "AWN.Qmsg_Lifting"
Presenting theory "Category3.FreeCategory"
Presenting theory "Trie.Trie"
Presenting theory "Category3.DiscreteCategory"
Presenting theory "Trie.Tries"
Presenting theory "AODV.A_Seq_Invariants"
Presenting theory "HOL-Library.While_Combinator"
Presenting theory "Flyspeck-Tame.Worklist"
Presenting theory "Flyspeck-Tame.Maps"
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 "Flyspeck-Tame.Arch"
Presenting theory "Flyspeck-Tame.ArchCompAux"
Presenting theory "AODV.A_Quality_Increases"
Presenting theory "ConcurrentGC.Global_Invariants_Lemmas"
Presenting theory "AODV.A_OAodv"
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 "ConcurrentGC.Local_Invariants_Lemmas"
Presenting theory "HOL-Library.Complete_Partial_Order2"
Presenting theory "ConcurrentGC.Initial_Conditions"
Presenting document JinjaThreads/document
Presenting document JinjaThreads/outline
Presenting theory "ConcurrentGC.Noninterference"
Presenting theory "HOL-Library.Conditional_Parametricity"
Presenting file "~~/src/HOL/Library/conditional_parametricity.ML"
Presenting theory "HOL-Library.Confluence"
Presenting theory "HOL-Library.Confluent_Quotient"
Presenting theory "ConcurrentGC.Global_Noninterference"
Presenting theory "ConcurrentGC.MarkObject"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "AWN.OClosed_Transfer"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "HOL-Library.Sublist"
Presenting theory "ConcurrentGC.Phases"
Presenting theory "AWN.AWN_Main"
Presenting theory "HOL-Library.Transitive_Closure_Table"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Library.Predicate_Compile_Alternative_Defs"
Presenting theory "ConcurrentGC.StrongTricolour"
Presenting theory "HOL-Library.Confluence"
Presenting theory "ConcurrentGC.TSO"
Presenting theory "ConcurrentGC.Valid_Refs"
Presenting theory "AODV.A_Global_Invariants"
Presenting theory "HOL-Library.Confluent_Quotient"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "HOL-Library.Dlist"
Presenting theory "ConcurrentGC.Worklists"
Presenting theory "JinjaThreads.Set_without_equal"
Presenting theory "AODV.A_Loop_Freedom"
Presenting theory "ConcurrentGC.Proofs"
Presenting theory "ConcurrentGC.Concrete_heap"
Presenting theory "ConcurrentGC.Concrete"
Presenting Word_Lib in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Word_Lib" ...
Presenting document Word_Lib/document
Presenting document Word_Lib/outline
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "AWN.Toy"
Presenting theory "JinjaThreads.Set_Monad"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "HOL-Library.Cardinality"
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.Countable_Complete_Lattices"
Presenting theory "HOL-Library.Infinite_Set"
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.Numeral_Type"
Presenting theory "HOL-Library.Type_Length"
Presenting theory "Word_Lib.More_Arithmetic"
Presenting theory "AODV.A_Aodv_Loop_Freedom"
Presenting theory "HOL-Library.Countable_Set_Type"
Presenting theory "Word_Lib.Even_More_List"
Presenting theory "AODV.B_Fwdrreps"
Presenting theory "HOL-Library.Debug"
Presenting theory "HOL-Library.Diagonal_Subsequence"
Presenting theory "HOL-Library.Case_Converter"
Presenting file "~~/src/HOL/Library/case_converter.ML"
Presenting theory "HOL-Library.Discrete"
Presenting theory "HOL-Library.Simps_Case_Conv"
Presenting file "~~/src/HOL/Library/simps_case_conv.ML"
Presenting theory "Bicategory.Strictness"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "HOL-Library.FuncSet"
Presenting theory "HOL-Library.Sublist"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "Word_Lib.More_Sublist"
Presenting theory "Word_Lib.More_Misc"
Presenting theory "HOL-Library.Disjoint_Sets"
Presenting theory "HOL-Library.Countable"
Presenting theory "AODV.B_Aodv_Data"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "AODV.B_Aodv_Message"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "Category3.Limit"
Presenting theory "HOL-Library.Countable_Complete_Lattices"
Presenting theory "AODV.B_Aodv"
Presenting theory "HOL-Library.FSet"
Presenting theory "AODV.B_Aodv_Predicates"
Presenting theory "HOL-Library.Multiset"
Presenting theory "HOL-Library.Order_Continuity"
Presenting theory "HOL.HOL"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
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 theory "HOL-ex.Quicksort"
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 theory "HOL-Library.Extended_Nat"
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 "Category3.CategoryWithPullbacks"
Presenting theory "HOL-Library.Option_ord"
Presenting theory "HOL-Library.Finite_Map"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "HOL-Library.Disjoint_FSets"
Presenting theory "AODV.B_Fresher"
Presenting theory "HOL-Library.Dlist"
Presenting theory "HOL-Library.Word"
Presenting theory "HOL-Library.Dual_Ordered_Lattice"
Presenting theory "Bicategory.InternalAdjunction"
Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
Presenting theory "HOL-Library.Equipollence"
Presenting theory "Word_Lib.More_Divides"
Presenting theory "HOL-Library.Simps_Case_Conv"
Presenting file "~~/src/HOL/Library/simps_case_conv.ML"
Presenting theory "HOL-Library.Extended"
Presenting theory "Category3.CartesianCategory"
Presenting theory "HOL-Library.Complete_Partial_Order2"
Presenting theory "HOL-Library.Order_Continuity"
Presenting theory "Category3.CategoryWithFiniteLimits"
Presenting theory "AODV.B_Seq_Invariants"
Presenting theory "HOL-Library.Extended_Nat"
Presenting theory "Word_Lib.More_Word"
Presenting theory "Category3.CartesianClosedCategory"
Presenting theory "Coinductive.Coinductive_Nat"
Presenting theory "HOL.Orderings"
Presenting file "~~/src/Provers/order_procedure.ML"
Presenting file "~~/src/Provers/order_tac.ML"
Presenting theory "Word_Lib.Strict_part_mono"
Presenting theory "HOL-Library.Liminf_Limsup"
Presenting theory "Word_Lib.Many_More"
Presenting theory "HereditarilyFinite.HF"
Presenting theory "AODV.B_Quality_Increases"
Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"
Presenting theory "AODV.B_OAodv"
Presenting theory "Automatic_Refinement.Misc"
Presenting theory "HOL.Groups"
Presenting file "~~/src/HOL/Tools/group_cancel.ML"
Presenting theory "IP_Addresses.NumberWang_IPv4"
Presenting theory "IP_Addresses.NumberWang_IPv6"
Presenting theory "Word_Lib.Aligned"
Presenting theory "HOL.Lattices"
Presenting theory "Word_Lib.Next_and_Prev"
Presenting theory "HOL-Library.Signed_Division"
Presenting theory "HOL.Boolean_Algebras"
Presenting theory "Word_Lib.Signed_Division_Word"
Presenting file "~~/src/HOL/Tools/boolean_algebra_cancel.ML"
Presenting theory "IP_Addresses.WordInterval"
Presenting theory "Word_Lib.Bit_Comprehension"
Presenting theory "IP_Addresses.Hs_Compat"
Presenting theory "Word_Lib.Most_significant_bit"
Presenting theory "Word_Lib.Least_significant_bit"
Presenting theory "Word_Lib.Generic_set_bit"
Presenting theory "IP_Addresses.IP_Address"
Presenting theory "IP_Addresses.IPv4"
Presenting theory "HOL.Set"
Presenting theory "HOL-Library.Extended_Real"
Presenting theory "Word_Lib.Bits_Int"
Presenting theory "Word_Lib.Typedef_Morphisms"
Presenting theory "HOL.Typedef"
Presenting file "~~/src/HOL/Tools/typedef.ML"
Presenting theory "HOL-Library.Indicator_Function"
Presenting theory "Word_Lib.Singleton_Bit_Shifts"
Presenting theory "Word_Lib.Legacy_Aliases"
Presenting theory "AODV.B_Global_Invariants"
Presenting theory "IP_Addresses.IPv6"
Presenting theory "AODV.B_Loop_Freedom"
Presenting theory "IP_Addresses.Prefix_Match"
Presenting theory "IP_Addresses.CIDR_Split"
Presenting theory "Coinductive.Coinductive_List"
Presenting theory "HOL-Library.Product_Lexorder"
Presenting theory "IP_Addresses.WordInterval_Sorted"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "HOL.Fun"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "Word_Lib.Reversed_Bit_Lists"
Presenting file "~~/src/HOL/Tools/functor.ML"
Presenting theory "HOL-Library.Extended_Nonnegative_Real"
Presenting theory "AODV.B_Aodv_Loop_Freedom"
Presenting theory "Category3.HFSetCat"
Presenting theory "AODV.C_Gtobcast"
Presenting theory "HOL-Library.Log_Nat"
Presenting theory "Word_Lib.Bitwise"
Presenting theory "HOL-Cardinals.Fun_More"
Presenting theory "HOL.Complete_Lattices"
Presenting theory "HOL-Library.Lattice_Algebras"
Presenting theory "Word_Lib.Examples"
Presenting theory "HOL-Cardinals.Order_Relation_More"
Presenting theory "Word_Lib.Bit_Comprehension_Int"
Presenting theory "Coinductive.TLList"
Presenting theory "HOL-Cardinals.Wellfounded_More"
Presenting theory "Word_Lib.Signed_Words"
Presenting theory "Word_Lib.Bitwise_Signed"
Presenting theory "Word_Lib.Enumeration"
Presenting theory "Coinductive.Lazy_LList"
Presenting theory "HOL-Cardinals.Wellorder_Relation"
Presenting theory "Word_Lib.Enumeration_Word"
Presenting theory "AODV.C_Aodv_Data"
Presenting theory "Word_Lib.Hex_Words"
Presenting theory "Word_Lib.Norm_Words"
Presenting theory "Coinductive.Lazy_TLList"
Presenting theory "AODV.C_Aodv_Message"
Presenting theory "Word_Lib.Rsplit"
Presenting theory "Word_Lib.Syntax_Bundles"
Presenting theory "HOL-Cardinals.Wellorder_Embedding"
Presenting theory "Word_Lib.Type_Syntax"
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-Cardinals.Order_Union"
Presenting theory "HOL-Library.Float"
Presenting theory "AODV.C_Aodv"
Presenting theory "HOL-Library.Function_Division"
Presenting theory "AODV.C_Aodv_Predicates"
Presenting theory "HOL-Library.Fun_Lexorder"
Presenting theory "HOL-Library.Going_To_Filter"
Presenting theory "IP_Addresses.IP_Address_Parser"
Presenting theory "HOL-Library.Groups_Big_Fun"
Presenting theory "IP_Addresses.Lib_Numbers_toString"
Presenting theory "IP_Addresses.Lib_Word_toString"
Presenting theory "HOL-Cardinals.Wellorder_Constructions"
Presenting theory "IP_Addresses.Lib_List_toString"
Presenting theory "IP_Addresses.IP_Address_toString"
Presenting theory "IP_Addresses.Prefix_Match_toString"
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 "Simple_Firewall.Lib_Enum_toString"
Presenting theory "Simple_Firewall.L4_Protocol"
Presenting theory "Simple_Firewall.Simple_Packet"
Presenting theory "Simple_Firewall.Firewall_Common_Decision_State"
Presenting theory "HOL-Library.Char_ord"
Presenting theory "HOL-Library.Interval"
Presenting theory "HOL-Library.Interval_Float"
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 "Simple_Firewall.Iface"
Presenting theory "HOL-Library.IArray"
Presenting theory "AODV.C_Fresher"
Presenting theory "HOL-Eisbach.Eisbach_Tools"
Presenting theory "Simple_Firewall.SimpleFw_Syntax"
Presenting theory "Word_Lib.Word_EqI"
Presenting theory "HOL.Ctr_Sugar"
Presenting file "~~/src/HOL/Tools/Ctr_Sugar/case_translation.ML"
Presenting file "~~/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML"
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 file "~~/src/HOL/Tools/coinduction.ML"
Presenting theory "Simple_Firewall.SimpleFw_Semantics"
Presenting theory "Simple_Firewall.List_Product_More"
Presenting theory "Simple_Firewall.Option_Helpers"
Presenting theory "HOL-Library.Multiset"
Presenting theory "Bicategory.PseudonaturalTransformation"
Presenting theory "Simple_Firewall.Generic_SimpleFw"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "Simple_Firewall.Shadowed"
Presenting theory "HOL-Cardinals.Ordinal_Arithmetic"
Presenting theory "HOL-ex.Quicksort"
Presenting theory "AODV.C_Seq_Invariants"
Presenting theory "Word_Lib.Word_Lemmas"
Presenting theory "Simple_Firewall.IP_Partition_Preliminaries"
Presenting theory "HOL-Library.Option_ord"
Presenting theory "Word_Lib.Word_8"
Presenting theory "Word_Lib.Word_16"
Presenting theory "Word_Lib.Word_Syntax"
Presenting theory "Word_Lib.Word_Names"
Presenting theory "Simple_Firewall.GroupF"
Presenting theory "Simple_Firewall.IP_Addr_WordInterval_toString"
Presenting theory "Simple_Firewall.Primitives_toString"
Presenting theory "AODV.C_Quality_Increases"
Presenting theory "AODV.C_OAodv"
Presenting theory "Word_Lib.More_Word_Operations"
Presenting theory "HOL-Library.Landau_Symbols"
Presenting theory "Word_Lib.Word_32"
Presenting theory "Word_Lib.Word_Lib_Sumo"
Presenting theory "Word_Lib.Machine_Word_32_Basics"
Presenting theory "Word_Lib.Machine_Word_32"
Presenting theory "Word_Lib.Word_64"
Presenting theory "Word_Lib.Machine_Word_64_Basics"
Presenting theory "Word_Lib.Machine_Word_64"
Presenting theory "HOL-Cardinals.Cardinal_Order_Relation"
Presenting theory "HOL-Library.Lattice_Constructions"
Presenting theory "Word_Lib.Guide"
Presenting Routing in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Routing" ...
Presenting document Routing/document
Presenting document Routing/outline
Presenting theory "Routing.Linorder_Helper"
Presenting theory "Pure-ex.Guess"
Presenting theory "Simple_Firewall.Service_Matrix"
Presenting theory "HOL-Cardinals.Cardinal_Arithmetic"
Presenting theory "Simple_Firewall.SimpleFw_toString"
Presenting Iptables_Semantics in "/media/data/jenkins/workspace/isabelle-nightly-slow/browser_info/AFP/Iptables_Semantics" ...
Presenting theory "HOL-Library.Stream"
Presenting document Iptables_Semantics/document
Presenting document Iptables_Semantics/outline
Presenting theory "Iptables_Semantics.List_Misc"
Presenting theory "HOL-Cardinals.Wellorder_Extension"
Presenting theory "HOL-Cardinals.Cardinals"
Presenting theory "Routing.Routing_Table"
Presenting theory "Iptables_Semantics.Negation_Type"
Presenting theory "ZFC_in_HOL.ZFC_Library"
Presenting theory "Iptables_Semantics.WordInterval_Lists"
Presenting theory "Iptables_Semantics.Repeat_Stabilize"
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 "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "Iptables_Semantics.Firewall_Common"
Presenting theory "Routing.Linux_Router"
Presenting theory "HOL-Library.LaTeXsugar"
Presenting theory "Routing.IpRoute_Parser"
Presenting file "$AFP/Routing/IpRoute_Parser.ml"
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 document Iptables_Semantics_Examples/outline
Presenting theory "ZFC_in_HOL.ZFC_in_HOL"
Presenting theory "AODV.C_Global_Invariants"
Presenting theory "Iptables_Semantics.Semantics"
Presenting theory "HOL-Library.Sublist"
Presenting theory "AODV.C_Loop_Freedom"
Presenting theory "Iptables_Semantics.Matching"
Presenting theory "Iptables_Semantics.Ruleset_Update"
Presenting theory "HOL-Library.Linear_Temporal_Logic_on_Streams"
Presenting theory "HOL-Library.ListVector"
Presenting theory "AODV.C_Aodv_Loop_Freedom"
Presenting theory "AODV.D_Fwdrreqs"
Presenting theory "HOL-Library.Lub_Glb"
Presenting theory "Iptables_Semantics_Examples.Parser_Test"
Presenting theory "Iptables_Semantics_Examples.Parser6_Test"
Presenting theory "Iptables_Semantics.Call_Return_Unfolding"
Presenting theory "Iptables_Semantics_Examples.Small_Examples"
Presenting theory "ZFC_in_HOL.ZFC_Cardinals"
Presenting theory "Iptables_Semantics_Examples.Ports_Fail"
Presenting theory "Iptables_Semantics_Examples.Contrived_Example"
Presenting theory "Iptables_Semantics.Ternary"
Presenting theory "Iptables_Semantics_Examples.iptables_Ln_tuned_parsed"
Presenting theory "Automatic_Refinement.Misc"
Presenting theory "HOL-Library.Mapping"
Presenting theory "HOL.Inductive"
Presenting theory "Iptables_Semantics.Matching_Ternary"
Presenting theory "Iptables_Semantics_Examples.Analyze_Synology_Diskstation"
Presenting file "~~/src/HOL/Tools/inductive.ML"
Presenting theory "Automatic_Refinement.Foldi"
Presenting theory "HOL-Library.Monad_Syntax"
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 file "~~/src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_primrec.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML"
Presenting theory "HOL-Library.More_List"
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 "AODV.D_Aodv_Data"
Presenting theory "Iptables_Semantics.Semantics_Ternary"
Presenting theory "Iptables_Semantics.Datatype_Selectors"
Presenting theory "Iptables_Semantics_Examples.Analyze_Ringofsaturn_com"
Presenting theory "AODV.D_Aodv_Message"
Presenting theory "Iptables_Semantics.IpAddresses"
Presenting theory "Iptables_Semantics.L4_Protocol_Flags"
Presenting theory "Iptables_Semantics.Ports"
Presenting theory "Iptables_Semantics.Conntrack_State"
Presenting theory "Collections.SetIterator"
Presenting theory "Iptables_Semantics.Tagged_Packet"
Presenting theory "Category3.ZFC_SetCat"
Presenting theory "Iptables_Semantics.Common_Primitive_Syntax"
Presenting theory "Iptables_Semantics.Unknown_Match_Tacs"
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 "Iptables_Semantics_Examples_Big.Analyze_topos_generated"
Presenting theory "Iptables_Semantics.Common_Primitive_Matcher_Generic"
Presenting theory "AODV.D_Aodv"
Presenting theory "Iptables_Semantics.Common_Primitive_Matcher"
Presenting theory "Iptables_Semantics.Example_Semantics"
Presenting theory "AODV.D_Aodv_Predicates"
Presenting theory "Collections.SetIteratorOperations"
Presenting theory "Automatic_Refinement.Refine_Util_Bootstrap1"
Presenting theory "Automatic_Refinement.Mpat_Antiquot"
Presenting theory "Automatic_Refinement.Mk_Term_Antiquot"
Presenting theory "Iptables_Semantics.Alternative_Semantics"
Presenting theory "HOL.Product_Type"
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.Semantics_Stateful"
Presenting theory "HOL.Sum_Type"
Presenting theory "Automatic_Refinement.Refine_Util"
Presenting theory "Automatic_Refinement.Attr_Comb"
Presenting theory "AODV.D_Fresher"
Presenting theory "Automatic_Refinement.Named_Sorted_Thms"
Presenting theory "Automatic_Refinement.Prio_List"
Presenting theory "HOL-Library.Multiset"
Presenting theory "Automatic_Refinement.Tagged_Solver"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "Automatic_Refinement.Anti_Unification"
Presenting theory "Automatic_Refinement.Indep_Vars"
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 "HOL-Library.Multiset_Order"
Presenting theory "Iptables_Semantics_Examples.Analyze_SQRL_Shorewall"
Presenting theory "HOL-Library.NList"
Presenting theory "Iptables_Semantics.Semantics_Goto"
Presenting theory "Collections.Proper_Iterator"
Presenting theory "Iptables_Semantics_Examples.SQRL_2015_nospoof"
Presenting theory "HOL-Library.Nonpos_Ints"
Presenting theory "Iptables_Semantics.Negation_Type_DNF"
Presenting theory "HOL.Rings"
Presenting theory "Collections.It_to_It"
Presenting theory "Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing"
Presenting theory "AODV.D_Seq_Invariants"
Presenting theory "Iptables_Semantics.Matching_Embeddings"
Presenting file "~~/src/HOL/Tools/arith_data.ML"
Presenting file "~~/src/Provers/Arith/cancel_div_mod.ML"
Presenting theory "HOL-Library.Numeral_Type"
Presenting theory "Collections.SetIteratorGA"
Presenting theory "Refine_Monadic.Refine_Chapter"
Presenting theory "Iptables_Semantics.Fixed_Action"
Presenting theory "Iptables_Semantics_Examples.Analyze_medium_sized_company"
Presenting theory "Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Small"
Presenting theory "Automatic_Refinement.Autoref_Phases"
Presenting theory "Automatic_Refinement.Autoref_Data"
Presenting theory "Iptables_Semantics_Examples_Big.Analyze_TUM_Net_Firewall"
Presenting theory "Automatic_Refinement.Autoref_Tagging"
Presenting theory "Iptables_Semantics.Normalized_Matches"
Presenting theory "HOL-Library.Omega_Words_Fun"
Presenting theory "Iptables_Semantics.Negation_Type_Matching"
Presenting theory "HOL-Library.Open_State_Syntax"
Presenting theory "AODV.D_Quality_Increases"
Presenting theory "Iptables_Semantics_Examples_Big.Analyze_Containern"
Presenting theory "AODV.D_OAodv"
Presenting theory "HOL.Nat"
Presenting theory "Bicategory.EquivalenceOfBicategories"
Presenting theory "HOL-Library.Option_ord"
Presenting theory "Automatic_Refinement.Relators"
Presenting file "~~/src/HOL/Tools/nat_arith.ML"
Presenting theory "HOL-Library.Parallel"
Presenting theory "HOL-Library.Pattern_Aliases"
Presenting theory "HOL-Library.Periodic_Fun"
Presenting theory "Iptables_Semantics.Primitive_Normalization"
Presenting theory "Automatic_Refinement.Param_Tool"
Presenting theory "Iptables_Semantics.MatchExpr_Fold"
Presenting theory "Iptables_Semantics.Common_Primitive_Lemmas"
Presenting theory "Iptables_Semantics_Examples_Big.TUM_Spoofing_new3"
Presenting theory "Automatic_Refinement.Param_HOL"
Presenting theory "Automatic_Refinement.Parametricity"
Presenting theory "HOL-Library.Poly_Mapping"
Presenting theory "HOL-Library.Power_By_Squaring"
Presenting theory "Iptables_Semantics.Ports_Normalize"
Presenting theory "Automatic_Refinement.Autoref_Id_Ops"
Presenting theory "Iptables_Semantics_Examples_Big.TUM_Simple_FW"
Presenting theory "HOL-Library.Preorder"
Presenting file "~~/src/Provers/preorder.ML"
Presenting theory "Iptables_Semantics.IpAddresses_Normalize"
Presenting theory "HOL-Library.Product_Plus"
Presenting theory "HOL-Library.Quadratic_Discriminant"
Presenting theory "HOL-Library.Quotient_Syntax"
Presenting theory "Iptables_Semantics.Interfaces_Normalize"
Presenting theory "HOL-Library.Quotient_Set"
Presenting theory "Iptables_Semantics.Word_Upto"
Presenting theory "HOL-Library.Quotient_Product"
Presenting theory "HOL-Library.Quotient_Option"
Presenting theory "HOL-Library.Quotient_List"
Presenting theory "Automatic_Refinement.Autoref_Fix_Rel"
Presenting theory "AODV.D_Global_Invariants"
Presenting theory "Iptables_Semantics.Protocols_Normalize"
Presenting theory "HOL-Library.Quotient_Sum"
Presenting theory "HOL-Library.Quotient_Type"
Presenting theory "Iptables_Semantics.Remdups_Rev"
Presenting theory "HOL.Fields"
Presenting theory "Automatic_Refinement.Autoref_Translate"
Presenting theory "Automatic_Refinement.Autoref_Gen_Algo"
Presenting file "~~/src/Provers/Arith/fast_lin_arith.ML"
Presenting file "~~/src/HOL/Tools/lin_arith.ML"
Presenting theory "Automatic_Refinement.Autoref_Relator_Interface"
Presenting theory "AODV.D_Loop_Freedom"
Presenting theory "Automatic_Refinement.Autoref_Tool"
Presenting theory "Iptables_Semantics.Ipassmt"
Presenting theory "HOL-Library.Ramsey"
Presenting theory "Automatic_Refinement.Autoref_Bindings_HOL"
Presenting theory "Automatic_Refinement.Automatic_Refinement"
Presenting theory "HOL-Library.Reflection"
Presenting file "~~/src/HOL/Tools/reflection.ML"
Presenting theory "Refine_Monadic.Refine_Mono_Prover"
Presenting file "$AFP/Refine_Monadic/refine_mono_prover.ML"
Presenting theory "Iptables_Semantics_Examples_Big.IP_Address_Space_Examples_All_Large"
Presenting theory "Iptables_Semantics.No_Spoof"
Presenting theory "Iptables_Semantics.Common_Primitive_toString"
Presenting theory "AODV.D_Aodv_Loop_Freedom"
Presenting theory "Bicategory.SpanBicategory"
Presenting theory "Iptables_Semantics.Routing_IpAssmt"
Presenting theory "Refine_Monadic.Refine_Misc"
Presenting theory "AODV.E_All_ABCD"
Presenting theory "Iptables_Semantics.Output_Interface_Replace"
Presenting theory "Refine_Monadic.RefineG_Transfer"
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 "Refine_Monadic.RefineG_Domain"
Presenting theory "HOL-Library.Saturated"
Presenting theory "HOL.Finite_Set"
Presenting theory "Iptables_Semantics.Interface_Replace"
Presenting theory "Iptables_Semantics.Optimizing"
Presenting theory "Refine_Monadic.RefineG_Recursion"
Presenting theory "HOL-Library.Set_Idioms"
Presenting theory "Refine_Monadic.RefineG_Assert"
Presenting theory "HOL-Library.Signed_Division"
Presenting theory "HOL-Library.State_Monad"
Presenting theory "AODV.E_Aodv_Data"
Presenting theory "AODV.E_Aodv_Message"
Presenting theory "HOL.Relation"
Presenting theory "HOL-Library.Comparator"
Presenting theory "HOL-Library.Sorting_Algorithms"
Presenting theory "AODV.E_Aodv"
Presenting theory "AODV.E_Aodv_Predicates"
Presenting theory "Refine_Monadic.Refine_Basic"
Presenting theory "HOL.Transitive_Closure"
Presenting file "~~/src/Provers/trancl.ML"
Presenting theory "Iptables_Semantics.Transform"
Presenting theory "Refine_Monadic.Refine_Leof"
Presenting theory "Refine_Monadic.Refine_Heuristics"
Presenting theory "Refine_Monadic.Refine_More_Comb"
Presenting theory "Iptables_Semantics.Conntrack_State_Transform"
Presenting theory "HOL.Wellfounded"
Presenting theory "HOL-Library.While_Combinator"
Presenting theory "HOL.Wfrec"
Presenting theory "Refine_Monadic.RefineG_While"
Presenting theory "Iptables_Semantics.Primitive_Abstract"
Presenting theory "AODV.E_Fresher"
Presenting theory "HOL.Order_Relation"
Presenting theory "HOL-Library.Sum_of_Squares"
Presenting file "~~/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML"
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 "HOL-Library.Tree"
Presenting theory "HOL-Library.Tree_Multiset"
Presenting theory "HOL-Library.Tree_Real"
Presenting theory "Iptables_Semantics.SimpleFw_Compliance"
Presenting theory "HOL-Library.Uprod"
Presenting theory "Refine_Monadic.Refine_While"
Presenting theory "AODV.E_Seq_Invariants"
Presenting theory "HOL.Hilbert_Choice"
Presenting theory "Refine_Monadic.Refine_Det"
Presenting file "~~/src/HOL/Tools/choice_specification.ML"
Presenting theory "Iptables_Semantics.Semantics_Embeddings"
Presenting theory "Iptables_Semantics.Iptables_Semantics"
Presenting theory "Refine_Monadic.Refine_Pfun"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "Native_Word.Code_Int_Integer_Conversion"
Presenting theory "Refine_Monadic.Refine_Transfer"
Presenting theory "Bicategory.Tabulation"
Presenting theory "Native_Word.Code_Target_Integer_Bit"
Presenting theory "Native_Word.Code_Target_Int_Bit"
Presenting theory "AODV.E_Quality_Increases"
Presenting theory "Iptables_Semantics.Code_Interface"
Presenting theory "HOL.Zorn"
Presenting theory "AODV.E_OAodv"
Presenting theory "HOL.BNF_Wellorder_Relation"
Presenting theory "Iptables_Semantics.Parser6"
Presenting theory "Iptables_Semantics.No_Spoof_Embeddings"
Presenting theory "Refine_Monadic.Refine_Foreach"
Presenting theory "HOL.BNF_Wellorder_Embedding"
Presenting theory "Refine_Monadic.Refine_Automation"
Presenting theory "Refine_Monadic.Autoref_Monadic"
Presenting theory "Refine_Monadic.Refine_Monadic"
Presenting theory "HOL-Library.Word"
Presenting theory "Collections.Gen_Iterator"
Presenting file "~~/src/HOL/Library/Tools/word_lib.ML"
Presenting file "~~/src/HOL/Library/Tools/smt_word.ML"
Presenting theory "Collections.Idx_Iterator"
Presenting theory "Iptables_Semantics.Parser"
Presenting theory "Collections.Iterator"
Presenting theory "Iptables_Semantics.Code_haskell"
Presenting theory "Collections.ICF_Tools"
Presenting theory "HOL-Library.Z2"
Presenting theory "AODV.E_Global_Invariants"
Presenting theory "HOL-Library.Library"
Presenting theory "Collections.Ord_Code_Preproc"
Presenting theory "Iptables_Semantics.Access_Matrix_Embeddings"
Presenting theory "Iptables_Semantics.Documentation"
Presenting theory "Collections.Record_Intf"
Presenting theory "HOL-Library.Product_Order"
Presenting theory "HOL.BNF_Wellorder_Constructions"
Presenting theory "AODV.E_Loop_Freedom"
Presenting theory "Collections.Locale_Code"
Presenting theory "Collections.ICF_Spec_Base"
Presenting theory "HOL-Library.Finite_Lattice"
Presenting theory "HOL-Library.List_Lexorder"
Presenting theory "HOL-Library.List_Lenlexorder"
Presenting theory "HOL-Library.Prefix_Order"
Presenting theory "HOL-Library.Product_Lexorder"
Presenting theory "HOL-Library.Subseq_Order"
Presenting theory "HOL-Library.Datatype_Records"
Presenting file "~~/src/HOL/Library/datatype_records.ML"
Presenting theory "HOL-Library.AList_Mapping"
Presenting theory "HOL-Library.Code_Abstract_Char"
Presenting theory "AODV.E_Aodv_Loop_Freedom"
Presenting theory "Collections.SetSpec"
Presenting theory "AODV.All"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "HOL-Library.Code_Binary_Nat"
Presenting theory "HOL.BNF_Cardinal_Order_Relation"
Presenting theory "HOL-Library.Code_Prolog"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/code_prolog.ML"
Presenting theory "Collections.MapSpec"
Presenting theory "HOL.BNF_Cardinal_Arithmetic"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "HOL-Library.Code_Real_Approx_By_Float"
Presenting theory "Collections.ListSpec"
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 "Collections.AnnotatedListSpec"
Presenting theory "Collections.PrioSpec"
Presenting theory "Collections.PrioUniqueSpec"
Presenting theory "Collections.Algos"
Presenting theory "HOL-Library.DAList_Multiset"
Presenting theory "Collections.SetIndex"
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.SetIteratorCollectionsGA"
Presenting theory "Collections.SetGA"
Presenting theory "Collections.Dlist_add"
Presenting theory "Collections.ListSetImpl"
Presenting theory "Collections.ListSetImpl_Invar"
Presenting theory "Collections.ListSetImpl_NotDist"
Presenting theory "Collections.Sorted_List_Operations"
Presenting theory "Collections.ListSetImpl_Sorted"
Presenting theory "HOL.BNF_Def"
Presenting file "~~/src/HOL/Tools/BNF/bnf_util.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_def_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_def.ML"
Presenting theory "HOL-Library.RBT_Impl"
Presenting theory "Bicategory.BicategoryOfSpans"
Presenting theory "HOL-Library.RBT_Impl"
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 "HOL-Library.RBT"
Presenting theory "HOL-Library.RBT_Mapping"
Presenting theory "HOL.Basic_BNFs"
Presenting theory "Collections.RBT_add"
Presenting theory "HOL-Library.RBT"
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 "Collections.MapGA"
Presenting theory "Collections.RBTMapImpl"
Presenting theory "HOL-Library.Predicate_Compile_Quickcheck"
Presenting file "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
Presenting theory "Collections.SetByMap"
Presenting theory "Collections.RBTSetImpl"
Presenting theory "HOL-Library.AList"
Presenting theory "Collections.Assoc_List"
Presenting theory "Collections.ListMapImpl"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "HOL-Library.Numeral_Type"
Presenting theory "HOL-Library.Type_Length"
Presenting theory "HOL-Library.Old_Recdef"
Presenting file "~~/src/HOL/Library/old_recdef.ML"
Presenting theory "Bicategory.Modification"
Presenting theory "HOL-Library.Realizers"
Presenting file "~~/src/HOL/Tools/datatype_realizer.ML"
Presenting file "~~/src/HOL/Tools/inductive_realizer.ML"
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 "Bicategory.ConcreteBicategory"
Presenting theory "HOL-Library.Refute"
Presenting file "~~/src/HOL/Library/refute.ML"
Presenting theory "Word_Lib.More_Arithmetic"
Presenting theory "Word_Lib.More_Divides"
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 file "~~/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m.ML"
Presenting theory "Word_Lib.More_Word"
Presenting file "~~/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML"
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 "Bicategory.CatBicat"
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 "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 "HOL.BNF_Least_Fixpoint"
Presenting theory "Collections.HashMap"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_util.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_tactics.ML"
Presenting theory "Collections.HashSet"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp.ML"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_compat.ML"
Presenting theory "Trie.Trie"
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 "Collections.Trie_Impl"
Presenting theory "Collections.Trie2"
Presenting theory "HOL.Equiv_Relations"
Presenting theory "Collections.TrieMapImpl"
Presenting theory "Collections.TrieSetImpl"
Presenting theory "HOL.Basic_BNF_LFPs"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML"
Presenting theory "Collections.Diff_Array"
Presenting theory "Collections.ListGA"
Presenting theory "Collections.Array_Iterator"
Presenting theory "HOL.Meson"
Presenting file "~~/src/HOL/Tools/Meson/meson.ML"
Presenting file "~~/src/HOL/Tools/Meson/meson_clausify.ML"
Presenting file "~~/src/HOL/Tools/Meson/meson_tactic.ML"
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 "Binomial-Heaps.BinomialHeap"
Presenting theory "Collections.BinoPrioImpl"
Presenting theory "Binomial-Heaps.SkewBinomialHeap"
Presenting theory "Collections.SkewPrioImpl"
Presenting theory "HOL.ATP"
Presenting file "~~/src/HOL/Tools/ATP/atp_util.ML"
Presenting file "~~/src/HOL/Tools/ATP/atp_problem.ML"
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 file "~~/src/HOL/Tools/ATP/atp_proof_reconstruct.ML"
Presenting theory "Finger-Trees.FingerTree"
Presenting theory "Collections.FTAnnotatedListImpl"
Presenting theory "Collections.PrioByAnnotatedList"
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 "HOL.Metis"
Presenting theory "JinjaThreads.Auxiliary"
Presenting theory "JinjaThreads.Basic_Main"
Presenting file "~~/src/Tools/Metis/metis.ML"
Presenting theory "JinjaThreads.FWState"
Presenting theory "JinjaThreads.FWLock"
Presenting theory "JinjaThreads.FWLocking"
Presenting theory "JinjaThreads.FWThread"
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.FWWait"
Presenting theory "JinjaThreads.FWCondAction"
Presenting theory "JinjaThreads.FWWellform"
Presenting theory "JinjaThreads.FWLockingThread"
Presenting theory "JinjaThreads.FWInterrupt"
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 "JinjaThreads.FWSemantics"
Presenting theory "JinjaThreads.FWProgressAux"
Presenting theory "HOL.Lifting"
Presenting theory "JinjaThreads.FWDeadlock"
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.FWProgress"
Presenting theory "JinjaThreads.FWLifting"
Presenting theory "JinjaThreads.LTS"
Presenting theory "HOL.Quotient"
Presenting theory "JinjaThreads.FWLTS"
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 file "~~/src/HOL/Tools/BNF/bnf_lift.ML"
Presenting theory "HOL.Num"
Presenting theory "JinjaThreads.Bisimulation"
Presenting file "~~/src/HOL/Tools/numeral.ML"
Presenting theory "HOL.Power"
Presenting theory "HOL.Groups_Big"
Presenting theory "HOL.Complete_Partial_Order"
Presenting theory "HOL.Option"
Presenting theory "HOL.Partial_Function"
Presenting file "~~/src/HOL/Tools/Function/partial_function.ML"
Presenting theory "JinjaThreads.FWBisimulation"
Presenting theory "JinjaThreads.FWBisimDeadlock"
Presenting theory "JinjaThreads.FWLiftingSem"
Presenting theory "HOL.Argo"
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 theory "JinjaThreads.FWInitFinLift"
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.FWBisimLift"
Presenting theory "JinjaThreads.Semilat"
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 theory "JinjaThreads.Err"
Presenting file "~~/src/HOL/Tools/Argo/argo_sat_solver.ML"
Presenting theory "JinjaThreads.Opt"
Presenting theory "JinjaThreads.Product"
Presenting theory "JinjaThreads.Listn"
Presenting theory "JinjaThreads.Semilattices"
Presenting theory "JinjaThreads.Typing_Framework"
Presenting theory "JinjaThreads.SemilatAlg"
Presenting theory "JinjaThreads.Typing_Framework_err"
Presenting theory "JinjaThreads.Kildall"
Presenting theory "JinjaThreads.LBVSpec"
Presenting theory "JinjaThreads.LBVCorrect"
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 theory "JinjaThreads.LBVComplete"
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.Abstract_BV"
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 theory "JinjaThreads.Type"
Presenting file "~~/src/HOL/Tools/Function/fun_cases.ML"
Presenting theory "JinjaThreads.Decl"
Presenting theory "JinjaThreads.TypeRel"
Presenting theory "JinjaThreads.Value"
Presenting theory "JinjaThreads.Exceptions"
Presenting theory "JinjaThreads.SystemClasses"
Presenting theory "HOL.Int"
Presenting theory "JinjaThreads.Heap"
Presenting theory "JinjaThreads.Observable_Events"
Presenting file "~~/src/HOL/Tools/int_arith.ML"
Presenting theory "JinjaThreads.StartConfig"
Presenting theory "JinjaThreads.Conform"
Presenting theory "HOL.Lattices_Big"
Presenting theory "JinjaThreads.ExternalCall"
Presenting theory "JinjaThreads.WellForm"
Presenting theory "HOL.Euclidean_Division"
Presenting theory "JinjaThreads.ExternalCallWF"
Presenting theory "JinjaThreads.ConformThreaded"
Presenting theory "HOL.Parity"
Presenting theory "JinjaThreads.BinOp"
Presenting theory "HOL.Divides"
Presenting theory "JinjaThreads.SemiType"
Presenting theory "JinjaThreads.Common_Main"
Presenting theory "JinjaThreads.State"
Presenting theory "HOL.Numeral_Simprocs"
Presenting file "~~/src/Provers/Arith/assoc_fold.ML"
Presenting file "~~/src/Provers/Arith/cancel_numerals.ML"
Presenting theory "JinjaThreads.Expr"
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 file "~~/src/HOL/Tools/nat_numeral_simprocs.ML"
Presenting theory "JinjaThreads.JHeap"
Presenting theory "HOL.Semiring_Normalization"
Presenting file "~~/src/HOL/Tools/semiring_normalizer.ML"
Presenting theory "JinjaThreads.SmallStep"
Presenting theory "JinjaThreads.WWellForm"
Presenting theory "HOL.Groebner_Basis"
Presenting file "~~/src/HOL/Tools/groebner.ML"
Presenting theory "JinjaThreads.WellType"
Presenting theory "JinjaThreads.DefAss"
Presenting theory "JinjaThreads.JWellForm"
Presenting theory "HOL.Set_Interval"
Presenting theory "JinjaThreads.Threaded"
Presenting theory "JinjaThreads.WellTypeRT"
Presenting theory "JinjaThreads.Progress"
Presenting theory "JinjaThreads.DefAssPreservation"
Presenting theory "JinjaThreads.TypeSafe"
Presenting theory "HOL.Presburger"
Presenting file "~~/src/HOL/Tools/Qelim/qelim.ML"
Presenting file "~~/src/HOL/Tools/Qelim/cooper_procedure.ML"
Presenting theory "JinjaThreads.ProgressThreaded"
Presenting file "~~/src/HOL/Tools/Qelim/cooper.ML"
Presenting file "~~/src/HOL/Tools/try0.ML"
Presenting theory "JinjaThreads.Deadlocked"
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 "JinjaThreads.JVMExceptions"
Presenting theory "JinjaThreads.JVMExec"
Presenting theory "JinjaThreads.JVMDefensive"
Presenting theory "JinjaThreads.JVMThreaded"
Presenting theory "JinjaThreads.JVM_Main"
Presenting theory "JinjaThreads.JVM_SemiType"
Presenting theory "JinjaThreads.Effect"
Presenting theory "JinjaThreads.BVSpec"
Presenting theory "JinjaThreads.BVConform"
Presenting theory "HOL.SMT"
Presenting theory "JinjaThreads.BVSpecTypeSafe"
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 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/verit_replay_methods.ML"
Presenting theory "JinjaThreads.BVNoTypeError"
Presenting file "~~/src/HOL/Tools/SMT/verit_strategies.ML"
Presenting file "~~/src/HOL/Tools/SMT/verit_replay.ML"
Presenting file "~~/src/HOL/Tools/SMT/smt_systems.ML"
Presenting theory "JinjaThreads.BVProgressThreaded"
Presenting theory "JinjaThreads.JVMDeadlocked"
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 "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 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.J0"
Presenting theory "JinjaThreads.J0Bisim"
Presenting theory "JinjaThreads.J1State"
Presenting theory "JinjaThreads.J1Heap"
Presenting theory "HOL.List"
Presenting theory "JinjaThreads.J1"
Presenting theory "JinjaThreads.J1Deadlock"
Presenting theory "JinjaThreads.PCompiler"
Presenting theory "JinjaThreads.Compiler2"
Presenting theory "HOL.Groups_List"
Presenting theory "JinjaThreads.Exception_Tables"
Presenting theory "JinjaThreads.J1WellType"
Presenting theory "JinjaThreads.J1WellForm"
Presenting theory "HOL-Library.Prefix_Order"
Presenting theory "HOL.Bit_Operations"
Presenting theory "JinjaThreads.TypeComp"
Presenting theory "HOL.Code_Numeral"
Presenting theory "JinjaThreads.JVMTau"
Presenting theory "HOL.Random"
Presenting theory "HOL.Map"
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 "JinjaThreads.Execs"
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 "JinjaThreads.J1JVMBisim"
Presenting theory "HOL.Mirabelle"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_util.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle.ML"
Presenting file "~~/src/HOL/Tools/Mirabelle/mirabelle_arith.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.J1JVM"
Presenting theory "HOL.Nitpick"
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 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 "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.JVMJ1"
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.Correctness2"
Presenting theory "HOL.Filter"
Presenting theory "JinjaThreads.ListIndex"
Presenting theory "JinjaThreads.Compiler1"
Presenting theory "HOL.Conditionally_Complete_Lattices"
Presenting theory "JinjaThreads.J0J1Bisim"
Presenting theory "HOL.Factorial"
Presenting theory "HOL.Binomial"
Presenting theory "Main"
Presenting theory "HOL.Archimedean_Field"
Presenting theory "JinjaThreads.Correctness1Threaded"
Presenting theory "HOL.Rat"
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 "HOL.Topological_Spaces"
Presenting theory "JinjaThreads.Correctness1"
Presenting theory "HOL.Hull"
Presenting theory "HOL.Modules"
Presenting theory "JinjaThreads.JJ1WellForm"
Presenting theory "JinjaThreads.Compiler"
Presenting theory "HOL.Vector_Spaces"
Presenting theory "JinjaThreads.Correctness"
Presenting theory "JinjaThreads.Preprocessor"
Presenting theory "JinjaThreads.Compiler_Main"
Presenting theory "JinjaThreads.MM"
Presenting theory "JinjaThreads.SC"
Presenting theory "JinjaThreads.SC_Interp"
Presenting theory "HOL.Real_Vector_Spaces"
Presenting theory "JinjaThreads.SC_Collections"
Presenting theory "JinjaThreads.Orders"
Presenting theory "HOL.Limits"
Presenting theory "JinjaThreads.JMM_Spec"
Presenting theory "HOL.Inequalities"
Presenting theory "JinjaThreads.JMM_DRF"
Presenting theory "HOL.Series"
Presenting theory "JinjaThreads.SC_Legal"
Presenting theory "JinjaThreads.Non_Speculative"
Presenting theory "HOL.Deriv"
Presenting theory "HOL.NthRoot"
Presenting theory "JinjaThreads.SC_Completion"
Presenting theory "JinjaThreads.HB_Completion"
Presenting theory "JinjaThreads.JMM_Heap"
Presenting theory "HOL.Transcendental"
Presenting theory "HOL.Complex"
Presenting theory "HOL.MacLaurin"
Presenting theory "Complex_Main"
Presenting theory "JinjaThreads.JMM_Framework"
Presenting theory "JinjaThreads.JMM_Typesafe"
Presenting theory "JinjaThreads.JMM_Common"
Presenting theory "JinjaThreads.JMM_J"
Presenting theory "JinjaThreads.DRF_J"
Presenting theory "JinjaThreads.JMM_JVM"
Presenting theory "JinjaThreads.DRF_JVM"
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 "JinjaThreads.JMM"
Presenting theory "JinjaThreads.MM_Main"
Presenting theory "JinjaThreads.State_Refinement"
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: 10:23:10 elapsed time, 33:30:10 cpu time, factor 3.23
Group AFP: 10:53:11 elapsed time, 35:17:59 cpu time, factor 3.24
Group main: 0:08:45 elapsed time, 0:34:04 cpu time, factor 3.89
Group timing: 0:03:30 elapsed time, 0:16:47 cpu time, factor 4.79
Group very_slow: 6:31:52 elapsed time, 15:48:04 cpu time, factor 2.42
Overall: 11:17:40 elapsed time, 35:52:26 cpu time, factor 3.18
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