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