13:07:15 Started by upstream project "isabelle-repo" build number 499

13:07:15 originally caused by:

13:07:15 Started by an SCM change

13:07:15 [EnvInject] - Loading node environment variables.

13:07:15 Building remotely on workermta2 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-repo-afp

13:07:15 [isabelle-repo-afp] $ hg showconfig paths.default

13:07:15 [isabelle-repo-afp] $ hg pull --rev f3ac9153bc0d97fcd42df0da7888f66ed70710b9

13:07:16 pulling from http://isabelle.in.tum.de/repos/isabelle/

13:07:16 searching for changes

13:07:16 adding changesets

13:07:16 adding manifests

13:07:16 adding file changes

13:07:16 added 45 changesets with 69 changes to 21 files

13:07:16 (run 'hg update' to get a working copy)

13:07:16 [isabelle-repo-afp] $ hg update --clean --rev f3ac9153bc0d97fcd42df0da7888f66ed70710b9

13:07:16 21 files updated, 0 files merged, 0 files removed, 0 files unresolved

13:07:16 [isabelle-repo-afp] $ hg --config extensions.purge= clean --all

13:07:17 [isabelle-repo-afp] $ hg log --rev . --template {node}

13:07:17 [isabelle-repo-afp] $ hg log --rev . --template {rev}

13:07:17 [isabelle-repo-afp] $ hg id --branch

13:07:17 [afp] $ hg showconfig paths.default

13:07:17 [afp] $ hg pull --rev default

13:07:19 pulling from https://bitbucket.org/isa-afp/afp-devel/

13:07:19 searching for changes

13:07:19 adding changesets

13:07:19 adding manifests

13:07:19 adding file changes

13:07:19 added 4 changesets with 3 changes to 3 files

13:07:19 (run 'hg update' to get a working copy)

13:07:19 [afp] $ hg update --clean --rev default

13:07:19 314 files updated, 0 files merged, 0 files removed, 0 files unresolved

13:07:19 [afp] $ hg --config extensions.purge= clean --all

13:07:19 [afp] $ hg log --rev . --template {node}

13:07:19 [afp] $ hg log --rev . --template {rev}

13:07:19 No emails were triggered.

13:07:19 [isabelle-repo-afp] $ /bin/sh -xe /tmp/hudson1644655016639186417.sh

13:07:19 + Admin/jenkins/run_build afp

13:07:19 + set -e

13:07:19 + PROFILE=afp

13:07:19 + shift

13:07:19 + bin/isabelle components -a

13:07:19 + bin/isabelle jedit -bf

13:07:20 ### Building graph browser ...

13:07:20 warning: [options] bootstrap class path not set in conjunction with -source 1.4

13:07:20 warning: [options] source value 1.4 is obsolete and will be removed in a future release

13:07:20 warning: [options] target value 1.4 is obsolete and will be removed in a future release

13:07:20 warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.

13:07:21 Note: GraphBrowser/GraphBrowser.java uses or overrides a deprecated API.

13:07:21 Note: Recompile with -Xlint:deprecation for details.

13:07:21 4 warnings

13:07:21 ### Building Isabelle/Scala ...

13:07:50 ### Building Isabelle/jEdit ...

13:08:07 + bin/isabelle ci_build_afp

13:08:13

13:08:13 === CONFIGURATION ===

13:08:13

13:08:13 ML_PLATFORM="x86_64-linux"

13:08:13 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.6-1/x86_64-linux"

13:08:13 ML_SYSTEM="polyml-5.6"

13:08:13 ML_OPTIONS="-H 4000 --gcthreads 2 --maxheap 8G"

13:08:14

13:08:14 === BUILD ===

13:08:14

13:08:14 Build started at Thu, 6 Oct 2016 11:08:13 GMT

13:08:14 Isabelle id f3ac9153bc0d

13:08:14 AFP id 1e958cc1942e

13:08:14

13:08:14 === LOG ===

13:08:14

13:08:14 Session Pure/Pure

13:08:15 Session HOL/HOL (main)

13:08:15 Session AFP/AVL-Trees (AFP)

13:08:15 Session AFP/AWN (AFP)

13:08:15 Session AFP/Abortable_Linearizable_Modules (AFP)

13:08:15 Session AFP/Abstract-Hoare-Logics (AFP)

13:08:15 Session AFP/Abstract-Rewriting (AFP)

13:08:15 Session AFP/Decreasing-Diagrams (AFP)

13:08:15 Session AFP/Decreasing-Diagrams-II (AFP)

13:08:16 Session AFP/Matrix (AFP)

13:08:16 Session AFP/Matrix_Tensor (AFP)

13:08:16 Session AFP/Knot_Theory (AFP)

13:08:16 Session AFP/Polynomials (AFP)

13:08:16 Session AFP/Abstract_Completeness (AFP)

13:08:16 Session AFP/Automatic_Refinement (AFP)

13:08:16 Session AFP/Refine_Monadic (AFP)

13:08:16 Session AFP/Collections (AFP)

13:08:17 Session AFP/CAVA_Base (AFP)

13:08:17 Session AFP/CAVA_Automata (AFP)

13:08:17 Session AFP/DFS_Framework (AFP)

13:08:17 Session AFP/Gabow_SCC (AFP)

13:08:17 Session AFP/LTL_to_GBA (AFP)

13:08:17 Session AFP/CAVA_buildchain1 (AFP)

13:08:17 Session AFP/CAVA_buildchain3 (AFP)

13:08:17 Session AFP/CAVA_LTL_Modelchecker (AFP)

13:08:17 Session AFP/Promela (AFP)

13:08:17 Session AFP/Collections_Examples (AFP)

13:08:17 Session AFP/Dijkstra_Shortest_Path (AFP)

13:08:17 Session AFP/Formal_SSA (AFP)

13:08:17 Session AFP/Network_Security_Policy_Verification (AFP)

13:08:17 Session AFP/Sepref_Prereq (AFP)

13:08:17 Session AFP/Refine_Imperative_HOL (AFP)

13:08:17 Session AFP/Sepref_Basic (AFP)

13:08:17 Session AFP/Sepref_IICF (AFP)

13:08:17 Session AFP/Edka_Base (AFP)

13:08:17 Session AFP/EdmondsKarp_Maxflow (AFP)

13:08:17 Session AFP/Transitive-Closure (AFP)

13:08:17 Session AFP/Tree-Automata (AFP)

13:08:17 Session AFP/BinarySearchTree (AFP)

13:08:17 Session AFP/Binomial-Queues (AFP)

13:08:17 Session AFP/Bondy (AFP)

13:08:17 Session AFP/Bounded_Deducibility_Security (AFP)

13:08:17 Session AFP/BytecodeLogicJmlTypes (AFP)

13:08:17 Session AFP/CISC-Kernel (AFP)

13:08:17 Session AFP/CYK (AFP)

13:08:17 Session AFP/Card_Number_Partitions (AFP)

13:08:17 Session AFP/Case_Labeling (AFP)

13:08:17 Session AFP/Cauchy (AFP)

13:08:17 Session AFP/Sqrt_Babylonian (AFP)

13:08:17 Session AFP/Real_Impl (AFP)

13:08:17 Session AFP/Certification_Monads (AFP)

13:08:17 Session AFP/ClockSynchInst (AFP)

13:08:17 Session AFP/Coinductive_Languages (AFP)

13:08:17 Session AFP/Compiling-Exceptions-Correctly (AFP)

13:08:17 Session AFP/Completeness (AFP)

13:08:18 Session AFP/ComponentDependencies (AFP)

13:08:18 Session AFP/Consensus_Refined (AFP)

13:08:18 Session AFP/CryptoBasedCompositionalProperties (AFP)

13:08:18 Session AFP/DPT-SAT-Solver (AFP)

13:08:18 Session AFP/DataRefinementIBP (AFP)

13:08:18 Session AFP/Dependent_SIFUM_Type_Systems (AFP)

13:08:18 Session AFP/Dependent_SIFUM_Refinement (AFP)

13:08:18 Session AFP/Depth-First-Search (AFP)

13:08:18 Session AFP/Derangements (AFP)

13:08:18 Session AFP/Discrete_Summation (AFP)

13:08:18 Session AFP/Card_Partitions (AFP)

13:08:18 Session AFP/DiskPaxos (AFP)

13:08:18 Session AFP/Encodability_Process_Calculi (AFP)

13:08:18 Session AFP/Euler_Partition (AFP)

13:08:18 Session AFP/Example-Submission (AFP)

13:08:18 Session AFP/FFT (AFP)

13:08:18 Session AFP/FLP (AFP)

13:08:18 Session AFP/FeatherweightJava (AFP)

13:08:18 Session AFP/Featherweight_OCL (AFP)

13:08:18 Session AFP/FileRefinement (AFP)

13:08:18 Session AFP/FinFun (AFP)

13:08:18 Session AFP/Finite_Automata_HF (AFP)

13:08:18 Session AFP/FocusStreamsCaseStudies (AFP)

13:08:18 Session AFP/Free-Groups (AFP)

13:08:18 Session AFP/FunWithFunctions (AFP)

13:08:18 Session AFP/FunWithTilings (AFP)

13:08:18 Session AFP/GPU_Kernel_PL (AFP)

13:08:18 Session AFP/Gauss-Jordan-Elim-Fun (AFP)

13:08:18 Session AFP/GenClock (AFP)

13:08:18 Session AFP/General-Triangle (AFP)

13:08:18 Session AFP/GoedelGod (AFP)

13:08:18 Session AFP/GraphMarkingIBP (AFP)

13:08:18 Session AFP/Graph_Theory (AFP)

13:08:19 Session AFP/ShortestPath (AFP)

13:08:19 Session HOL/HOL-Algebra (main timing)

13:08:19 Session AFP/JNF-HOL-Lib (AFP)

13:08:19 Session AFP/JNF-AFP-Lib (AFP)

13:08:19 Session AFP/Jordan_Normal_Form (AFP)

13:08:19 Session AFP/Pre_Perron_Frobenius (AFP)

13:08:20 Session AFP/Perron_Frobenius (AFP)

13:08:20 Session AFP/Pre_Polynomial_Factorization (AFP)

13:08:20 Session AFP/Polynomial_Factorization (AFP)

13:08:20 Session AFP/Pre_Algebraic_Numbers (AFP)

13:08:20 Session AFP/Algebraic_Number_Lib (AFP)

13:08:20 Session AFP/Algebraic_Numbers (AFP)

13:08:20 Session AFP/Jordan_Hoelder (AFP)

13:08:20 Session AFP/Perfect-Number-Thm (AFP)

13:08:20 Session AFP/Secondary_Sylow (AFP)

13:08:20 Session AFP/VectorSpace (AFP)

13:08:20 Session HOL/HOL-Analysis (main timing)

13:08:20 Session AFP/Affine_Arithmetic (AFP)

13:08:20 Session AFP/Cartan_FP (AFP)

13:08:20 Session AFP/Cayley_Hamilton (AFP)

13:08:20 Session AFP/Echelon_Form (AFP)

13:08:20 Session AFP/Hermite (AFP)

13:08:20 Session AFP/Gauss_Jordan (AFP)

13:08:20 Session HOL/HOL-Probability (timing)

13:08:20 Session AFP/Applicative_Lifting (AFP)

13:08:20 Session AFP/Stern_Brocot (AFP)

13:08:20 Session AFP/Density_Compiler (AFP)

13:08:20 Session AFP/Ergodic_Theory (AFP)

13:08:20 Session AFP/Fisher_Yates (AFP)

13:08:20 Session AFP/Girth_Chromatic (AFP)

13:08:21 Session AFP/List_Update (AFP)

13:08:21 Session AFP/Lp (AFP)

13:08:21 Session AFP/MFMC_Countable (AFP)

13:08:21 Session AFP/Markov_Models (AFP)

13:08:21 Session AFP/Probabilistic_Noninterference (AFP)

13:08:21 Session AFP/Probabilistic_System_Zoo (AFP)

13:08:21 Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)

13:08:21 Session AFP/Random_Graph_Subgraph_Threshold (AFP)

13:08:21 Session AFP/Randomised_Social_Choice (AFP)

13:08:21 Session AFP/SDS_Impossibility (AFP)

13:08:21 Session AFP/UpDown_Scheme (AFP)

13:08:21 Session AFP/Landau_Analysis (AFP)

13:08:21 Session AFP/Akra_Bazzi (AFP)

13:08:21 Session AFP/Catalan_Numbers (AFP)

13:08:21 Session AFP/Stirling_Formula (AFP)

13:08:21 Session AFP/Lower_Semicontinuous (AFP)

13:08:21 Session AFP/Ordinary_Differential_Equations (AFP)

13:08:22 Session AFP/HOL-ODE (AFP)

13:08:22 Session AFP/HOL-ODE-Refinement (AFP)

13:08:22 Session AFP/HOL-ODE-Numerics (AFP)

13:08:22 Session AFP/HOL-ODE-Examples (AFP)

13:08:22 Session AFP/Prime_Harmonic_Series (AFP)

13:08:22 Session AFP/Probabilistic_System_Zoo-BNFs (AFP)

13:08:22 Session AFP/Ptolemys_Theorem (AFP)

13:08:22 Session AFP/QR_Decomposition (AFP)

13:08:22 Session AFP/Rank_Nullity_Theorem (AFP)

13:08:22 Session AFP/Tarskis_Geometry (AFP)

13:08:22 Session AFP/Triangle (AFP)

13:08:22 Session AFP/pGCL (AFP)

13:08:22 Session HOL/HOL-Cardinals (timing)

13:08:22 Session AFP/Ordinals_and_Cardinals (AFP)

13:08:22 Session AFP/Sort_Encodings (AFP)

13:08:22 Session HOL/HOL-Imperative_HOL

13:08:23 Session AFP/Imperative_Insertion_Sort (AFP)

13:08:23 Session HOL/HOL-Library (main timing)

13:08:23 Session AFP/Amortized_Complexity (AFP)

13:08:23 Session AFP/Dynamic_Tables (AFP)

13:08:23 Session AFP/ArrowImpossibilityGS (AFP)

13:08:23 Session AFP/Bell_Numbers_Spivey (AFP)

13:08:23 Session AFP/Card_Equiv_Relations (AFP)

13:08:23 Session AFP/Binomial-Heaps (AFP)

13:08:23 Session AFP/Boolean_Expression_Checkers (AFP)

13:08:23 Session AFP/Buildings (AFP)

13:08:23 Session AFP/Card_Multisets (AFP)

13:08:23 Session AFP/Category (AFP)

13:08:23 Session AFP/Category2 (AFP)

13:08:23 Session AFP/Category3 (AFP)

13:08:23 Session AFP/CofGroups (AFP)

13:08:23 Session AFP/Coinductive (AFP)

13:08:23 Session AFP/Lazy-Lists-II (AFP)

13:08:23 Session AFP/Topology (AFP)

13:08:23 Session AFP/Parity_Game (AFP)

13:08:23 Session AFP/Stream_Fusion_Code (AFP)

13:08:23 Session AFP/ConcurrentIMP (AFP)

13:08:23 Session AFP/CoreC++ (AFP)

13:08:23 Session AFP/Datatype_Order_Generator (AFP)

13:08:23 Session AFP/Old_Datatype_Show (AFP)

13:08:23 Session AFP/Deriving (AFP)

13:08:23 Session AFP/Containers (AFP)

13:08:23 Session AFP/Containers-Benchmarks (AFP)

13:08:24 Session AFP/Show (AFP)

13:08:24 Session AFP/Descartes_Sign_Rule (AFP)

13:08:24 Session AFP/Efficient-Mergesort (AFP)

13:08:24 Session AFP/FOL-Fitting (AFP)

13:08:24 Session AFP/Finger-Trees (AFP)

13:08:24 Session AFP/Formula_Derivatives (AFP)

13:08:24 Session AFP/Formula_Derivatives-Examples (AFP)

13:08:24 Session AFP/Free-Boolean-Algebra (AFP)

13:08:24 Session AFP/Functional-Automata (AFP)

13:08:24 Session AFP/Group-Ring-Module (AFP)

13:08:24 Session AFP/Valuation (AFP)

13:08:24 Session AFP/Isabelle_Meta_Model (AFP)

13:08:24 Session AFP/KBPs (AFP)

13:08:24 Session AFP/LTL (AFP)

13:08:24 Session AFP/LTL_to_DRA (AFP)

13:08:24 Session AFP/Stuttering_Equivalence (AFP)

13:08:24 Session AFP/Landau_Symbols (AFP)

13:08:24 Session AFP/LinearQuantifierElim (AFP)

13:08:24 Session AFP/List-Infinite (AFP)

13:08:24 Session AFP/Nat-Interval-Logic (AFP)

13:08:24 Session AFP/AutoFocus-Stream (AFP)

13:08:24 Session AFP/MSO_Regex_Equivalence (AFP)

13:08:24 Session AFP/MSO_Examples (AFP)

13:08:24 Session AFP/MuchAdoAboutTwo (AFP)

13:08:24 Session AFP/Myhill-Nerode (AFP)

13:08:24 Session AFP/POPLmark-deBruijn (AFP)

13:08:24 Session AFP/Pairing_Heap (AFP)

13:08:24 Session AFP/Presburger-Automata (AFP)

13:08:24 Session AFP/Program-Conflict-Analysis (AFP)

13:08:24 Session AFP/Regex_Equivalence (AFP)

13:08:24 Session AFP/Regex_Equivalence_Examples (AFP)

13:08:24 Session AFP/Regular-Sets (AFP)

13:08:24 Session AFP/Posix-Lexing (AFP)

13:08:24 Session AFP/Ribbon_Proofs (AFP)

13:08:24 Session AFP/SATSolverVerification (AFP)

13:08:24 Session AFP/Selection_Heap_Sort (AFP)

13:08:24 Session AFP/Separation_Logic_Imperative_HOL (AFP)

13:08:24 Session AFP/Sturm_Sequences (AFP)

13:08:24 Session AFP/Special_Function_Bounds (AFP)

13:08:24 Session AFP/SuperCalc (AFP)

13:08:24 Session AFP/Tail_Recursive_Functions (AFP)

13:08:24 Session AFP/Vickrey_Clarke_Groves (AFP)

13:08:24 Session AFP/Well_Quasi_Orders (AFP)

13:08:24 Session HOL/HOL-Nominal

13:08:24 Session AFP/CCS (AFP)

13:08:24 Session AFP/Lam-ml-Normalization (AFP)

13:08:24 Session AFP/Pi_Calculus (AFP)

13:08:25 Session AFP/Psi_Calculi (AFP)

13:08:25 Session AFP/SequentInvertibility (AFP)

13:08:25 Session HOL/HOL-Number_Theory (timing)

13:08:25 Session AFP/Lehmer (AFP)

13:08:25 Session AFP/Pratt_Certificate (AFP)

13:08:25 Session HOL/HOL-Old_Number_Theory

13:08:25 Session AFP/Fermat3_4 (AFP)

13:08:25 Session HOL/HOL-Word (main timing)

13:08:26 Session HOL/HOL-SPARK (main)

13:08:26 Session HOL/HOL-SPARK-Examples

13:08:26 Session AFP/RIPEMD-160-SPARK (AFP)

13:08:26 Session AFP/Kleene_Algebra (AFP)

13:08:26 Session AFP/KAT_and_DRA (AFP)

13:08:26 Session AFP/Algebraic_VCs (AFP)

13:08:26 Session AFP/Multirelations (AFP)

13:08:26 Session AFP/Regular_Algebras (AFP)

13:08:26 Session AFP/Relation_Algebra (AFP)

13:08:26 Session AFP/Residuated_Lattices (AFP)

13:08:26 Session AFP/Native_Word (AFP)

13:08:26 Session AFP/Separation_Algebra (AFP)

13:08:26 Session AFP/Word_Lib (AFP)

13:08:26 Session AFP/IP_Addresses (AFP)

13:08:26 Session AFP/Simple_Firewall (AFP)

13:08:26 Session AFP/Routing (AFP)

13:08:26 Session AFP/Iptables_Semantics (AFP)

13:08:26 Session HOL/HOLCF (main timing)

13:08:26 Session AFP/Circus (AFP)

13:08:26 Session AFP/HOLCF-HOL-Library (AFP)

13:08:26 Session AFP/HOLCF-Nominal2 (AFP)

13:08:26 Session AFP/Launchbury (AFP)

13:08:26 Session AFP/Call_Arity (AFP)

13:08:26 Session AFP/PCF (AFP)

13:08:26 Session AFP/Shivers-CFA (AFP)

13:08:26 Session AFP/Stream-Fusion (AFP)

13:08:26 Session AFP/Tycon (AFP)

13:08:26 Session AFP/WorkerWrapper (AFP)

13:08:26 Session AFP/Heard_Of (AFP)

13:08:26 Session AFP/HereditarilyFinite (AFP)

13:08:27 Session AFP/HotelKeyCards (AFP)

13:08:27 Session AFP/Huffman (AFP)

13:08:27 Session AFP/HyperCTL (AFP)

13:08:27 Session AFP/IEEE_Floating_Point (AFP)

13:08:27 Session AFP/Impossible_Geometry (AFP)

13:08:27 Session AFP/Incompleteness (AFP)

13:08:27 Session AFP/Surprise_Paradox (AFP)

13:08:27 Session AFP/Incredible_Proof_Machine (AFP)

13:08:27 Session AFP/Inductive_Confidentiality (AFP)

13:08:27 Session AFP/InfPathElimination (AFP)

13:08:27 Session AFP/Integration (AFP)

13:08:27 Session AFP/Jinja (AFP)

13:08:27 Session AFP/HRB-Slicing (AFP)

13:08:27 Session AFP/InformationFlowSlicing_Inter (AFP)

13:08:27 Session AFP/Slicing (AFP)

13:08:27 Session AFP/InformationFlowSlicing (AFP)

13:08:27 Session AFP/JiveDataStoreModel (AFP)

13:08:27 Session AFP/KAD (AFP)

13:08:27 Session AFP/Koenigsberg_Friendship_Base (AFP)

13:08:27 Session AFP/Koenigsberg_Friendship (AFP)

13:08:27 Session AFP/Lambda_Free_RPOs (AFP)

13:08:28 Session AFP/LatticeProperties (AFP)

13:08:28 Session AFP/MonoBoolTranAlgebra (AFP)

13:08:28 Session AFP/PseudoHoops (AFP)

13:08:28 Session AFP/Lifting_Definition_Option (AFP)

13:08:28 Session AFP/LightweightJava (AFP)

13:08:28 Session AFP/Liouville_Numbers (AFP)

13:08:28 Session AFP/List-Index (AFP)

13:08:28 Session AFP/List_Interleaving (AFP)

13:08:28 Session AFP/Locally-Nameless-Sigma (AFP)

13:08:28 Session AFP/Marriage (AFP)

13:08:28 Session AFP/Latin_Square (AFP)

13:08:28 Session AFP/Max-Card-Matching (AFP)

13:08:28 Session AFP/MiniML (AFP)

13:08:28 Session AFP/Multivariate_Polynomials (AFP)

13:08:28 Session AFP/Groebner_Bases (AFP)

13:08:28 Session AFP/No_FTL_observers (AFP)

13:08:28 Session AFP/Nominal2 (AFP)

13:08:28 Session AFP/Rewriting_Z (AFP)

13:08:28 Session AFP/Noninterference_CSP (AFP)

13:08:28 Session AFP/Noninterference_Ipurge_Unwinding (AFP)

13:08:28 Session AFP/Noninterference_Generic_Unwinding (AFP)

13:08:28 Session AFP/Noninterference_Inductive_Unwinding (AFP)

13:08:28 Session AFP/Noninterference_Sequential_Composition (AFP)

13:08:28 Session AFP/Noninterference_Concurrent_Composition (AFP)

13:08:28 Session AFP/NormByEval (AFP)

13:08:28 Session AFP/Open_Induction (AFP)

13:08:28 Session AFP/Ordinal (AFP)

13:08:28 Session AFP/Partial_Function_MR (AFP)

13:08:28 Session AFP/Polynomial_Interpolation (AFP)

13:08:28 Session AFP/Pop_Refinement (AFP)

13:08:28 Session AFP/Possibilistic_Noninterference (AFP)

13:08:28 Session AFP/Priority_Queue_Braun (AFP)

13:08:28 Session AFP/PropResPI (AFP)

13:08:28 Session AFP/ROBDD (AFP)

13:08:29 Session AFP/RSAPSS (AFP)

13:08:29 Session AFP/Ramsey-Infinite (AFP)

13:08:29 Session AFP/Recursion-Theory-I (AFP)

13:08:29 Session AFP/RefinementReactive (AFP)

13:08:29 Session AFP/Rep_Fin_Groups (AFP)

13:08:29 Session AFP/Resolution_FOL (AFP)

13:08:29 Session AFP/Robbins-Conjecture (AFP)

13:08:29 Session AFP/Roy_Floyd_Warshall (AFP)

13:08:29 Session AFP/SIFPL (AFP)

13:08:29 Session AFP/SIFUM_Type_Systems (AFP)

13:08:29 Session AFP/SenSocialChoice (AFP)

13:08:29 Session AFP/Simpl (AFP)

13:08:29 Session AFP/BDD (AFP)

13:08:29 Session AFP/Planarity_Certificates (AFP)

13:08:30 Session AFP/Skew_Heap (AFP)

13:08:30 Session AFP/Splay_Tree (AFP)

13:08:30 Session AFP/Statecharts (AFP)

13:08:30 Session AFP/Stone_Algebras (AFP)

13:08:30 Session AFP/Strong_Security (AFP)

13:08:30 Session AFP/Sturm_Tarski (AFP)

13:08:30 Session AFP/SumSquares (AFP)

13:08:30 Session AFP/TLA (AFP)

13:08:30 Session AFP/Timed_Automata (AFP)

13:08:30 Session AFP/TortoiseHare (AFP)

13:08:30 Session AFP/Transitive-Closure-II (AFP)

13:08:30 Session AFP/Tree_Decomposition (AFP)

13:08:30 Session AFP/Trie (AFP)

13:08:30 Session AFP/UPF (AFP)

13:08:30 Session AFP/Verified-Prover (AFP)

13:08:30 Session AFP/VolpanoSmith (AFP)

13:08:30 Session AFP/WHATandWHERE_Security (AFP)

13:08:30 Session AFP/XML (AFP)

13:08:31 Building Pure ...

13:08:43 Pure: theory Pure

13:08:43 Pure: theory ML_Bootstrap

13:08:45 Warning: missing document directory

13:08:45 Timing Pure (2 threads, 0.720s elapsed time, 0.752s cpu time, 0.000s GC time, factor 1.04)

13:08:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/Pure/Pure

13:08:45 Finished Pure (0:00:14 elapsed time, 0:00:15 cpu time, factor 1.07)

13:08:46 Building HOL ...

13:08:46 HOL: theory Code_Generator

13:08:49 HOL: theory HOL

13:08:52 HOL: theory Argo

13:08:52 HOL: theory Ctr_Sugar

13:08:53 HOL: theory Orderings

13:08:54 HOL: theory SAT

13:08:55 HOL: theory Groups

13:08:57 HOL: theory Lattices

13:08:59 HOL: theory Set

13:09:01 HOL: theory Fun

13:09:01 HOL: theory Typedef

13:09:01 HOL: theory Rings

13:09:02 HOL: theory Complete_Lattices

13:09:04 HOL: theory Inductive

13:09:06 HOL: theory Product_Type

13:09:08 HOL: theory Complete_Partial_Order

13:09:08 HOL: theory Sum_Type

13:09:11 HOL: theory Nat

13:09:13 HOL: theory Fields

13:09:13 HOL: theory Meson

13:09:14 HOL: theory ATP

13:09:16 HOL: theory Metis

13:09:18 HOL: theory Finite_Set

13:09:19 HOL: theory Relation

13:09:21 HOL: theory Transitive_Closure

13:09:22 HOL: theory Wellfounded

13:09:23 HOL: theory Fun_Def_Base

13:09:23 HOL: theory Hilbert_Choice

13:09:23 HOL: theory Wfrec

13:09:23 HOL: theory Order_Relation

13:09:23 HOL: theory BNF_Wellorder_Relation

13:09:23 HOL: theory Zorn

13:09:23 HOL: theory BNF_Wellorder_Embedding

13:09:24 HOL: theory BNF_Wellorder_Constructions

13:09:25 HOL: theory BNF_Cardinal_Order_Relation

13:09:25 HOL: theory BNF_Cardinal_Arithmetic

13:09:26 HOL: theory BNF_Def

13:09:28 HOL: theory BNF_Composition

13:09:28 HOL: theory Basic_BNFs

13:09:29 HOL: theory BNF_Fixpoint_Base

13:09:32 HOL: theory BNF_Least_Fixpoint

13:09:35 HOL: theory Basic_BNF_LFPs

13:09:35 HOL: theory Num

13:09:35 HOL: theory Transfer

13:09:38 HOL: theory Power

13:09:40 HOL: theory Groups_Big

13:09:42 HOL: theory Equiv_Relations

13:09:43 HOL: theory Lifting

13:09:44 HOL: theory Lifting_Set

13:09:44 HOL: theory Option

13:09:45 HOL: theory Quotient

13:09:45 HOL: theory Extraction

13:09:46 HOL: theory Lattices_Big

13:09:47 HOL: theory Partial_Function

13:09:48 HOL: theory Fun_Def

13:09:49 HOL: theory Int

13:09:52 HOL: theory Nat_Transfer

13:09:52 HOL: theory Parity

13:09:54 HOL: theory Divides

13:09:59 HOL: theory Code_Numeral

13:10:00 HOL: theory Numeral_Simprocs

13:10:01 HOL: theory SMT

13:10:03 HOL: theory Semiring_Normalization

13:10:05 HOL: theory Groebner_Basis

13:10:06 HOL: theory Set_Interval

13:10:09 HOL: theory Conditionally_Complete_Lattices

13:10:09 HOL: theory Filter

13:10:10 HOL: theory Presburger

13:10:12 HOL: theory Sledgehammer

13:10:14 HOL: theory List

13:10:22 HOL: theory Groups_List

13:10:22 HOL: theory Map

13:10:23 HOL: theory Enum

13:10:23 HOL: theory Random

13:10:26 HOL: theory String

13:10:27 HOL: theory BNF_Greatest_Fixpoint

13:10:27 HOL: theory Predicate

13:10:28 HOL: theory Lazy_Sequence

13:10:29 HOL: theory Limited_Sequence

13:10:30 HOL: theory Typerep

13:10:31 HOL: theory Code_Evaluation

13:10:32 HOL: theory Quickcheck_Random

13:10:35 HOL: theory Quickcheck_Exhaustive

13:10:35 HOL: theory Quickcheck_Narrowing

13:10:39 HOL: theory Random_Pred

13:10:39 HOL: theory Record

13:10:44 HOL: theory Random_Sequence

13:10:45 HOL: theory Predicate_Compile

13:10:45 HOL: theory Nitpick

13:10:51 HOL: theory Main

13:10:53 HOL: theory Archimedean_Field

13:10:53 HOL: theory Binomial

13:10:54 HOL: theory GCD

13:10:57 HOL: theory Topological_Spaces

13:10:59 HOL: theory Rat

13:11:01 HOL: theory Real

13:11:04 HOL: theory Real_Vector_Spaces

13:11:16 HOL: theory Inequalities

13:11:16 HOL: theory Limits

13:11:19 HOL: theory Deriv

13:11:19 HOL: theory Series

13:11:20 HOL: theory NthRoot

13:11:21 HOL: theory Transcendental

13:11:25 HOL: theory Complex

13:11:26 HOL: theory MacLaurin

13:11:27 HOL: theory Complex_Main

13:14:51 Timing HOL (2 threads, 267.723s elapsed time, 528.808s cpu time, 39.740s GC time, factor 1.98)

13:14:51 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL

13:14:51 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL/document.pdf

13:14:51 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL/outline.pdf

13:14:51 Finished HOL (0:06:04 elapsed time, 0:11:27 cpu time, factor 1.88)

13:14:53 Building HOL-Library ...

13:14:53 Building HOL-Analysis ...

13:14:54 Building HOLCF ...

13:14:54 Building HOL-Algebra ...

13:14:54 Building HOL-Nominal ...

13:14:54 Building HOL-Word ...

13:14:54 Building Abstract-Rewriting ...

13:14:54 Building Jinja ...

13:14:55 HOLCF: theory Nat_Bijection

13:14:55 HOLCF: theory Old_Datatype

13:14:55 Abstract-Rewriting: theory While_Combinator

13:14:55 Abstract-Rewriting: theory Regular_Set

13:14:55 HOL-Nominal: theory Infinite_Set

13:14:55 HOL-Nominal: theory Old_Datatype

13:14:55 Jinja: theory Code_Abstract_Nat

13:14:55 Jinja: theory Code_Target_Int

13:14:55 HOL-Word: theory Bit

13:14:55 HOL-Word: theory Bits

13:14:55 HOL-Algebra: theory Multiset

13:14:55 HOL-Algebra: theory FuncSet

13:14:55 Jinja: theory Code_Target_Nat

13:14:55 Jinja: theory Sublist

13:14:55 HOL-Word: theory Boolean_Algebra

13:14:55 HOL-Library: theory Adhoc_Overloading

13:14:55 HOL-Library: theory Lattice_Syntax

13:14:55 HOL-Library: theory AList

13:14:55 HOL-Library: theory BNF_Axiomatization

13:14:56 Jinja: theory Code_Target_Numeral

13:14:56 HOL-Library: theory BNF_Corec

13:14:56 Jinja: theory While_Combinator

13:14:56 HOL-Word: theory Bits_Bit

13:14:56 HOL-Word: theory Misc_Numeric

13:14:56 HOL-Word: theory Bit_Representation

13:14:56 HOL-Analysis: theory Disjoint_Sets

13:14:56 HOL-Analysis: theory FuncSet

13:14:56 HOL-Word: theory Misc_Typedef

13:14:57 HOL-Word: theory Phantom_Type

13:14:57 HOL-Analysis: theory Infinite_Set

13:14:57 HOLCF: theory Countable

13:14:57 HOL-Nominal: theory Nominal

13:14:57 HOL-Word: theory Bits_Int

13:14:57 HOL-Analysis: theory Multiset

13:14:57 HOL-Analysis: theory Nat_Bijection

13:14:58 HOL-Library: theory DAList

13:14:58 HOL-Word: theory Cardinality

13:14:58 HOL-Analysis: theory Old_Datatype

13:14:58 Abstract-Rewriting: theory Regular_Exp

13:14:59 HOL-Word: theory Numeral_Type

13:14:59 HOLCF: theory Porder

13:14:59 HOL-Word: theory Bool_List_Representation

13:14:59 HOL-Library: theory Stirling

13:15:00 HOLCF: theory Pcpo

13:15:00 HOL-Analysis: theory Countable

13:15:00 HOL-Word: theory Type_Length

13:15:00 HOL-Library: theory Bit

13:15:01 HOL-Library: theory Bits

13:15:01 HOL-Word: theory Word_Miscellaneous

13:15:01 HOL-Library: theory Bits_Bit

13:15:01 HOL-Algebra: theory Factorial_Ring

13:15:01 HOL-Word: theory Word

13:15:01 HOL-Algebra: theory Permutation

13:15:01 HOL-Library: theory Boolean_Algebra

13:15:01 HOLCF: theory Cont

13:15:01 HOL-Analysis: theory Countable_Set

13:15:02 HOL-Library: theory Cardinal_Notations

13:15:02 HOLCF: theory Adm

13:15:02 HOLCF: theory Discrete

13:15:02 HOL-Library: theory Char_ord

13:15:02 HOLCF: theory Cpodef

13:15:02 HOL-Library: theory Code_Abstract_Nat

13:15:02 HOL-Library: theory Code_Binary_Nat

13:15:02 HOL-Analysis: theory Countable_Complete_Lattices

13:15:02 HOLCF: theory Fun_Cpo

13:15:02 Abstract-Rewriting: theory NDerivative

13:15:02 HOLCF: theory Product_Cpo

13:15:02 Abstract-Rewriting: theory Relation_Interpretation

13:15:02 HOL-Library: theory Code_Target_Nat

13:15:02 HOLCF: theory Cfun

13:15:02 HOL-Library: theory Code_Char

13:15:03 HOL-Library: theory Code_Prolog

13:15:03 HOL-Analysis: theory Permutations

13:15:03 HOL-Library: theory Code_Test

13:15:03 HOLCF: theory Cprod

13:15:03 HOLCF: theory Fix

13:15:03 HOL-Library: theory Combine_PER

13:15:03 HOLCF: theory Sfun

13:15:03 HOLCF: theory Sprod

13:15:03 HOLCF: theory Up

13:15:03 HOL-Library: theory Complete_Partial_Order2

13:15:04 HOL-Library: theory Debug

13:15:04 HOL-Library: theory Discrete

13:15:04 HOLCF: theory Lift

13:15:04 HOL-Analysis: theory Phantom_Type

13:15:04 HOL-Library: theory Disjoint_Sets

13:15:04 Jinja: theory Auxiliary

13:15:04 Jinja: theory List_Index

13:15:05 HOL-Library: theory Dlist

13:15:05 Jinja: theory Type

13:15:05 Jinja: theory Hidden

13:15:05 Jinja: theory Transitive_Closure_Table

13:15:05 HOLCF: theory One

13:15:05 HOLCF: theory Tr

13:15:05 HOL-Analysis: theory Cardinality

13:15:05 Jinja: theory Decl

13:15:05 HOLCF: theory Ssum

13:15:05 HOL-Analysis: theory Product_Plus

13:15:05 Jinja: theory Semilat

13:15:05 Jinja: theory TypeRel

13:15:06 HOLCF: theory Plain_HOLCF

13:15:06 HOL-Analysis: theory Product_Order

13:15:06 Jinja: theory Err

13:15:06 HOL-Library: theory FSet

13:15:06 Abstract-Rewriting: theory Equivalence_Checking

13:15:06 HOL-Analysis: theory Set_Algebras

13:15:06 Abstract-Rewriting: theory Regexp_Method

13:15:06 HOLCF: theory Deflation

13:15:06 HOLCF: theory Completion

13:15:06 HOL-Analysis: theory Numeral_Type

13:15:06 HOL-Analysis: theory L2_Norm

13:15:07 HOLCF: theory Map_Functions

13:15:07 HOLCF: theory Fixrec

13:15:07 HOL-Analysis: theory Continuum_Not_Denumerable

13:15:07 Jinja: theory Listn

13:15:07 HOL-Library: theory Fraction_Field

13:15:07 HOLCF: theory Bifinite

13:15:07 Jinja: theory Value

13:15:07 HOL-Analysis: theory Indicator_Function

13:15:07 HOLCF: theory Domain_Aux

13:15:07 Jinja: theory Opt

13:15:07 HOL-Analysis: theory Inner_Product

13:15:08 Jinja: theory Product

13:15:08 HOL-Analysis: theory Liminf_Limsup

13:15:08 Jinja: theory Semilattices

13:15:08 Jinja: theory Objects

13:15:08 Jinja: theory Exceptions

13:15:08 Jinja: theory JVMState

13:15:08 HOLCF: theory Universal

13:15:08 Jinja: theory JVMInstructions

13:15:08 Jinja: theory Conform

13:15:08 HOL-Library: theory Fun_Lexorder

13:15:08 HOL-Library: theory FuncSet

13:15:08 HOL-Analysis: theory Nonpos_Ints

13:15:08 Jinja: theory Expr

13:15:09 HOL-Analysis: theory Product_Vector

13:15:09 HOL-Analysis: theory Operator_Norm

13:15:09 HOL-Library: theory Function_Algebras

13:15:09 HOL-Algebra: theory Euclidean_Algorithm

13:15:09 HOL-Library: theory Function_Division

13:15:09 HOL-Library: theory Finite_Map

13:15:09 HOL-Analysis: theory Order_Continuity

13:15:09 HOL-Library: theory Code_Target_Int

13:15:09 HOL-Analysis: theory Euclidean_Space

13:15:10 HOL-Library: theory Code_Target_Numeral

13:15:10 HOLCF: theory Algebraic

13:15:10 HOL-Library: theory Groups_Big_Fun

13:15:10 HOLCF: theory Compact_Basis

13:15:10 Abstract-Rewriting: theory Infinite_Set

13:15:10 HOLCF: theory LowerPD

13:15:10 HOLCF: theory UpperPD

13:15:10 HOL-Analysis: theory Extended_Nat

13:15:10 HOL-Library: theory IArray

13:15:10 Abstract-Rewriting: theory Seq

13:15:10 Jinja: theory State

13:15:11 HOLCF: theory Representable

13:15:11 Jinja: theory SystemClasses

13:15:11 HOLCF: theory ConvexPD

13:15:11 Jinja: theory JVMExceptions

13:15:11 Abstract-Rewriting: theory Abstract_Rewriting

13:15:11 Jinja: theory JVMExecInstr

13:15:11 HOL-Analysis: theory Extended_Real

13:15:11 HOL-Analysis: theory Finite_Cartesian_Product

13:15:11 HOL-Library: theory Infinite_Set

13:15:12 HOL-Library: theory LaTeXsugar

13:15:12 HOL-Library: theory Lattice_Constructions

13:15:12 HOL-Library: theory Omega_Words_Fun

13:15:12 Jinja: theory JVMExec

13:15:12 HOL-Library: theory ListVector

13:15:12 HOL-Analysis: theory Linear_Algebra

13:15:12 Abstract-Rewriting: theory Relative_Rewriting

13:15:13 HOL-Library: theory List_lexord

13:15:13 Abstract-Rewriting: theory SN_Orders

13:15:13 HOL-Library: theory Mapping

13:15:13 Jinja: theory JVMDefensive

13:15:13 HOLCF: theory Domain

13:15:14 HOL-Library: theory AList_Mapping

13:15:14 HOL-Library: theory Misc_Numeric

13:15:15 HOL-Library: theory Misc_Typedef

13:15:15 HOL-Library: theory Bit_Representation

13:15:15 HOL-Library: theory Monad_Syntax

13:15:15 HOL-Library: theory More_List

13:15:15 HOLCF: theory Powerdomains

13:15:15 Abstract-Rewriting: theory SN_Order_Carrier

13:15:15 HOL-Library: theory Bits_Int

13:15:15 HOL-Library: theory Multiset

13:15:15 Jinja: theory JVMListExample

13:15:16 HOL-Analysis: theory Extended_Nonnegative_Real

13:15:16 HOL-Analysis: theory Periodic_Fun

13:15:16 Jinja: theory Examples

13:15:16 Jinja: theory BigStep

13:15:16 HOL-Analysis: theory Poly_Roots

13:15:16 HOLCF: theory HOLCF

13:15:16 HOL-Analysis: theory Sum_of_Squares

13:15:17 HOL-Library: theory Nat_Bijection

13:15:17 HOL-Library: theory Stream

13:15:18 Jinja: theory SmallStep

13:15:18 HOL-Algebra: theory Primes

13:15:18 HOL-Analysis: theory Sigma_Algebra

13:15:19 HOL-Analysis: theory Norm_Arith

13:15:19 HOL-Library: theory Old_Datatype

13:15:19 HOL-Analysis: theory Topology_Euclidean_Space

13:15:19 Jinja: theory DefAss

13:15:20 Jinja: theory J1

13:15:20 HOL-Library: theory DAList_Multiset

13:15:20 HOL-Library: theory Factorial_Ring

13:15:21 HOL-Library: theory Multiset_Order

13:15:21 HOL-Library: theory Permutation

13:15:21 HOL-Analysis: theory Measurable

13:15:21 HOL-Library: theory Permutations

13:15:22 Jinja: theory execute_Bigstep

13:15:22 HOL-Analysis: theory Measure_Space

13:15:23 HOL-Library: theory Countable

13:15:23 Timing HOL-Nominal (2 threads, 12.802s elapsed time, 24.888s cpu time, 0.876s GC time, factor 1.94)

13:15:23 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Nominal

13:15:23 Finished HOL-Nominal (0:00:28 elapsed time, 0:00:48 cpu time, factor 1.68)

13:15:23 Building LatticeProperties ...

13:15:23 Jinja: theory WellType

13:15:24 HOL-Library: theory Countable_Set

13:15:24 LatticeProperties: theory Conj_Disj

13:15:24 LatticeProperties: theory Lattice_Prop

13:15:24 Jinja: theory Annotate

13:15:25 LatticeProperties: theory WellFoundedTransitive

13:15:25 LatticeProperties: theory Modular_Distrib_Lattice

13:15:25 HOL-Library: theory Countable_Complete_Lattices

13:15:25 Jinja: theory WellTypeRT

13:15:25 LatticeProperties: theory Complete_Lattice_Prop

13:15:25 HOL-Analysis: theory Caratheodory

13:15:26 Jinja: theory execute_WellType

13:15:26 HOL-Analysis: theory Summation_Tests

13:15:27 LatticeProperties: theory Lattice_Ordered_Group

13:15:28 HOL-Library: theory Countable_Set_Type

13:15:28 HOL-Library: theory Euclidean_Algorithm

13:15:29 Jinja: theory WellForm

13:15:29 Jinja: theory PCompiler

13:15:29 HOL-Analysis: theory Bounded_Linear_Function

13:15:29 HOL-Analysis: theory Convex_Euclidean_Space

13:15:29 Jinja: theory Compiler1

13:15:30 Jinja: theory Compiler2

13:15:30 HOL-Library: theory Old_Recdef

13:15:31 Jinja: theory Correctness2

13:15:31 HOL-Analysis: theory Extended_Real_Limits

13:15:31 HOL-Library: theory Option_ord

13:15:31 HOL-Library: theory Parallel

13:15:32 HOL-Analysis: theory Tagged_Division

13:15:32 HOL-Library: theory Perm

13:15:33 Jinja: theory WWellForm

13:15:33 Jinja: theory Equivalence

13:15:33 HOL-Library: theory Phantom_Type

13:15:33 HOL-Analysis: theory Uniform_Limit

13:15:34 HOL-Library: theory Cardinality

13:15:34 HOL-Algebra: theory Congruence

13:15:34 HOL-Algebra: theory Exponent

13:15:34 Jinja: theory Progress

13:15:35 HOL-Library: theory FinFun

13:15:35 HOL-Algebra: theory Lattice

13:15:35 HOL-Analysis: theory Continuous_Extension

13:15:36 HOL-Analysis: theory Path_Connected

13:15:36 Jinja: theory JWellForm

13:15:36 Jinja: theory J1WellForm

13:15:37 HOL-Algebra: theory Group

13:15:37 HOL-Library: theory Normalized_Fraction

13:15:37 HOL-Library: theory Numeral_Type

13:15:38 Jinja: theory Correctness1

13:15:38 HOL-Library: theory Predicate_Compile_Alternative_Defs

13:15:38 Jinja: theory Compiler

13:15:38 HOL-Library: theory Predicate_Compile_Quickcheck

13:15:38 Jinja: theory TypeSafe

13:15:38 HOL-Library: theory Type_Length

13:15:39 HOL-Library: theory Product_Lexorder

13:15:39 HOL-Library: theory Saturated

13:15:39 HOL-Algebra: theory Bij

13:15:39 HOL-Library: theory Product_Plus

13:15:39 HOL-Algebra: theory Coset

13:15:39 HOL-Library: theory Product_Order

13:15:39 HOL-Library: theory Quotient_Syntax

13:15:39 HOL-Library: theory Quotient_Option

13:15:39 HOL-Library: theory Quotient_Product

13:15:39 Jinja: theory SemiType

13:15:39 HOL-Library: theory Finite_Lattice

13:15:39 HOL-Library: theory Quotient_Set

13:15:39 HOL-Library: theory Quotient_List

13:15:40 Jinja: theory JVM_SemiType

13:15:40 HOL-Analysis: theory Homeomorphism

13:15:40 Jinja: theory Effect

13:15:40 HOL-Algebra: theory FiniteProduct

13:15:40 HOL-Library: theory Quotient_Sum

13:15:40 HOL-Library: theory Quotient_Type

13:15:40 HOL-Library: theory RBT_Impl

13:15:40 HOL-Analysis: theory Brouwer_Fixpoint

13:15:41 HOL-Algebra: theory Ring

13:15:42 HOL-Algebra: theory Sylow

13:15:42 Timing HOL-Word (2 threads, 24.432s elapsed time, 47.848s cpu time, 1.760s GC time, factor 1.96)

13:15:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Word

13:15:42 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Word/document.pdf

13:15:42 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Word/outline.pdf

13:15:42 Finished HOL-Word (0:00:47 elapsed time, 0:01:23 cpu time, factor 1.74)

13:15:42 Building Kleene_Algebra ...

13:15:42 HOL-Analysis: theory Derivative

13:15:43 HOL-Library: theory Ramsey

13:15:43 HOL-Algebra: theory Divisibility

13:15:43 HOL-Library: theory Reflection

13:15:43 HOL-Library: theory Refute

13:15:43 Timing LatticeProperties (2 threads, 4.384s elapsed time, 9.808s cpu time, 0.128s GC time, factor 2.24)

13:15:43 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LatticeProperties

13:15:43 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LatticeProperties/document.pdf

13:15:43 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LatticeProperties/outline.pdf

13:15:43 Finished LatticeProperties (0:00:20 elapsed time, 0:00:33 cpu time, factor 1.65)

13:15:43 Building Simpl ...

13:15:44 HOL-Library: theory Rewrite

13:15:44 Kleene_Algebra: theory Signatures

13:15:44 Kleene_Algebra: theory Dioid

13:15:44 HOL-Library: theory Set_Algebras

13:15:44 HOL-Library: theory Simps_Case_Conv

13:15:45 HOL-Analysis: theory Cartesian_Euclidean_Space

13:15:45 HOL-Library: theory Extended

13:15:45 HOL-Algebra: theory AbelCoset

13:15:45 HOL-Analysis: theory Weierstrass_Theorems

13:15:45 Timing HOLCF (2 threads, 25.771s elapsed time, 49.328s cpu time, 2.252s GC time, factor 1.91)

13:15:45 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF

13:15:45 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF/document.pdf

13:15:45 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOLCF/outline.pdf

13:15:45 Finished HOLCF (0:00:50 elapsed time, 0:01:27 cpu time, factor 1.73)

13:15:45 Simpl: theory DistinctTreeProver

13:15:45 Simpl: theory LaTeXsugar

13:15:45 Building HOL-Cardinals ...

13:15:45 Simpl: theory Multiset

13:15:46 HOL-Algebra: theory Module

13:15:46 HOL-Cardinals: theory Order_Union

13:15:46 HOL-Cardinals: theory Cardinal_Notations

13:15:47 Simpl: theory Generalise

13:15:47 HOL-Library: theory State_Monad

13:15:47 HOL-Cardinals: theory Fun_More

13:15:47 HOL-Cardinals: theory Order_Relation_More

13:15:47 HOL-Library: theory Sublist

13:15:47 Simpl: theory StateFun

13:15:47 HOL-Cardinals: theory Wellorder_Extension

13:15:47 Simpl: theory StateSpaceLocale

13:15:47 HOL-Cardinals: theory Wellfounded_More

13:15:47 HOL-Cardinals: theory Wellorder_Relation

13:15:47 Simpl: theory StateSpaceSyntax

13:15:47 HOL-Analysis: theory Determinants

13:15:47 HOL-Analysis: theory Fashoda_Theorem

13:15:47 Simpl: theory Old_Recdef

13:15:47 HOL-Cardinals: theory Wellorder_Embedding

13:15:48 HOL-Library: theory Prefix_Order

13:15:48 HOL-Cardinals: theory Wellorder_Constructions

13:15:48 HOL-Library: theory Sublist_Order

13:15:48 HOL-Analysis: theory Ordered_Euclidean_Space

13:15:48 HOL-Library: theory Polynomial

13:15:48 HOL-Analysis: theory Polytope

13:15:49 Simpl: theory Language

13:15:49 HOL-Cardinals: theory Cardinal_Order_Relation

13:15:49 HOL-Cardinals: theory Ordinal_Arithmetic

13:15:50 HOL-Cardinals: theory Cardinal_Arithmetic

13:15:50 HOL-Cardinals: theory Cardinals

13:15:51 Simpl: theory Permutation

13:15:51 HOL-Cardinals: theory Bounded_Set

13:15:51 Simpl: theory Simpl_Heap

13:15:51 Simpl: theory HeapList

13:15:51 Jinja: theory BVSpec

13:15:51 Jinja: theory BVConform

13:15:52 HOL-Algebra: theory Ideal

13:15:52 Jinja: theory BVSpecTypeSafe

13:15:52 Jinja: theory TypeComp

13:15:53 HOL-Analysis: theory Borel_Space

13:15:53 HOL-Library: theory BigO

13:15:54 Jinja: theory BVNoTypeError

13:15:54 Jinja: theory EffectMono

13:15:54 Jinja: theory Typing_Framework

13:15:54 HOL-Library: theory Bool_List_Representation

13:15:54 Jinja: theory SemilatAlg

13:15:55 Jinja: theory Kildall

13:15:55 Jinja: theory LBVSpec

13:15:55 Jinja: theory Typing_Framework_err

13:15:55 Jinja: theory TF_JVM

13:15:55 Jinja: theory LBVComplete

13:15:56 HOL-Library: theory Code_Real_Approx_By_Float

13:15:56 Jinja: theory LBVCorrect

13:15:56 Jinja: theory Abstract_BV

13:15:56 HOL-Analysis: theory Nonnegative_Lebesgue_Integration

13:15:56 Jinja: theory BVExec

13:15:57 Jinja: theory LBVJVM

13:15:57 HOL-Library: theory Diagonal_Subsequence

13:15:57 HOL-Algebra: theory RingHom

13:15:57 HOL-Library: theory Formal_Power_Series

13:15:57 Jinja: theory BVExample

13:15:57 Kleene_Algebra: theory Conway

13:15:57 Kleene_Algebra: theory Dioid_Models

13:15:58 HOL-Analysis: theory Regularity

13:15:58 Simpl: theory Semantic

13:15:58 Jinja: theory Jinja

13:15:59 HOL-Algebra: theory QuotRing

13:15:59 HOL-Algebra: theory UnivPoly

13:15:59 HOL-Analysis: theory Binary_Product_Measure

13:15:59 HOL-Algebra: theory IntRing

13:16:00 HOL-Analysis: theory Embed_Measure

13:16:00 HOL-Analysis: theory Finite_Product_Measure

13:16:01 HOL-Library: theory Polynomial_FPS

13:16:02 HOL-Analysis: theory Bochner_Integration

13:16:02 Simpl: theory HoarePartialDef

13:16:02 Simpl: theory Termination

13:16:02 HOL-Library: theory Fundamental_Theorem_Algebra

13:16:03 HOL-Library: theory Indicator_Function

13:16:03 Simpl: theory HoarePartialProps

13:16:03 Simpl: theory HoareTotalDef

13:16:03 HOL-Library: theory Lattice_Algebras

13:16:04 Kleene_Algebra: theory Finite_Suprema

13:16:04 HOL-Analysis: theory Complete_Measure

13:16:04 Kleene_Algebra: theory Inf_Matrix

13:16:04 HOL-Analysis: theory Radon_Nikodym

13:16:04 Simpl: theory HoarePartial

13:16:04 Simpl: theory AlternativeSmallStep

13:16:04 HOL-Analysis: theory Set_Integral

13:16:05 Kleene_Algebra: theory Matrix

13:16:05 HOL-Analysis: theory Lebesgue_Measure

13:16:06 Simpl: theory SmallStep

13:16:06 Kleene_Algebra: theory Kleene_Algebra

13:16:07 HOL-Analysis: theory Henstock_Kurzweil_Integration

13:16:07 Simpl: theory HoareTotalProps

13:16:09 Simpl: theory Compose

13:16:09 Simpl: theory HoareTotal

13:16:09 HOL-Library: theory Liminf_Limsup

13:16:10 HOL-Library: theory Log_Nat

13:16:10 HOL-Analysis: theory Bounded_Continuous_Function

13:16:10 Simpl: theory Hoare

13:16:10 HOL-Library: theory Float

13:16:11 HOL-Analysis: theory Equivalence_Lebesgue_Henstock_Integration

13:16:11 Simpl: theory Closure

13:16:11 Simpl: theory StateSpace

13:16:11 HOL-Analysis: theory Integral_Test

13:16:12 Simpl: theory Vcg

13:16:12 HOL-Analysis: theory Complex_Analysis_Basics

13:16:12 HOL-Analysis: theory Interval_Integral

13:16:13 Kleene_Algebra: theory DRA

13:16:13 Kleene_Algebra: theory Omega_Algebra

13:16:13 HOL-Analysis: theory Lebesgue_Integral_Substitution

13:16:13 HOL-Library: theory Lub_Glb

13:16:14 HOL-Analysis: theory FurtherTopology

13:16:14 HOL-Library: theory Multiset_Permutations

13:16:14 HOL-Analysis: theory Complex_Transcendental

13:16:14 Simpl: theory ProcParEx

13:16:15 Simpl: theory ProcParExSP

13:16:15 Kleene_Algebra: theory PHL_KA

13:16:15 HOL-Library: theory Nonpos_Ints

13:16:15 Simpl: theory XVcg

13:16:15 HOL-Library: theory OptionalSugar

13:16:15 Simpl: theory XVcgEx

13:16:16 HOL-Library: theory Order_Continuity

13:16:16 Kleene_Algebra: theory PHL_DRA

13:16:16 Kleene_Algebra: theory Kleene_Algebra_Models

13:16:16 HOL-Analysis: theory Generalised_Binomial_Theorem

13:16:16 HOL-Analysis: theory Harmonic_Numbers

13:16:16 Simpl: theory ClosureEx

13:16:16 Simpl: theory ComposeEx

13:16:16 Kleene_Algebra: theory Formal_Power_Series

13:16:17 HOL-Analysis: theory Cauchy_Integral_Theorem

13:16:17 HOL-Library: theory Extended_Nat

13:16:17 HOL-Library: theory RBT

13:16:17 HOL-Analysis: theory Gamma_Function

13:16:18 Simpl: theory Quicksort

13:16:18 HOL-Library: theory Extended_Real

13:16:18 Simpl: theory SyntaxTest

13:16:18 HOL-Library: theory RBT_Mapping

13:16:18 HOL-Library: theory RBT_Set

13:16:19 Timing Abstract-Rewriting (2 threads, 51.890s elapsed time, 102.116s cpu time, 3.436s GC time, factor 1.97)

13:16:19 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Abstract-Rewriting

13:16:19 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Abstract-Rewriting/document.pdf

13:16:19 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Abstract-Rewriting/outline.pdf

13:16:19 Finished Abstract-Rewriting (0:01:24 elapsed time, 0:02:36 cpu time, factor 1.86)

13:16:19 Building Koenigsberg_Friendship_Base ...

13:16:19 Simpl: theory UserGuide

13:16:19 Simpl: theory VcgEx

13:16:19 HOL-Library: theory Linear_Temporal_Logic_on_Streams

13:16:20 Koenigsberg_Friendship_Base: theory AList

13:16:20 Koenigsberg_Friendship_Base: theory Congruence

13:16:21 Kleene_Algebra: theory Omega_Algebra_Models

13:16:21 HOL-Analysis: theory Conformal_Mappings

13:16:21 HOL-Library: theory Periodic_Fun

13:16:22 HOL-Library: theory Polynomial_Factorial

13:16:22 Koenigsberg_Friendship_Base: theory Lattice

13:16:22 HOL-Library: theory Extended_Nonnegative_Real

13:16:22 Koenigsberg_Friendship_Base: theory DAList

13:16:23 Simpl: theory VcgExSP

13:16:23 HOL-Analysis: theory Analysis

13:16:24 Simpl: theory VcgExTotal

13:16:24 Koenigsberg_Friendship_Base: theory FuncSet

13:16:24 Koenigsberg_Friendship_Base: theory Fib

13:16:25 HOL-Library: theory Quadratic_Discriminant

13:16:25 Koenigsberg_Friendship_Base: theory Graph

13:16:25 Koenigsberg_Friendship_Base: theory Group

13:16:25 HOL-Library: theory Sum_of_Squares

13:16:25 HOL-Library: theory Transitive_Closure_Table

13:16:26 Koenigsberg_Friendship_Base: theory Multiset

13:16:26 HOL-Library: theory Tree

13:16:27 Koenigsberg_Friendship_Base: theory FiniteProduct

13:16:27 Simpl: theory Simpl

13:16:28 Koenigsberg_Friendship_Base: theory Ring

13:16:28 HOL-Library: theory While_Combinator

13:16:29 HOL-Library: theory Bourbaki_Witt_Fixpoint

13:16:29 HOL-Library: theory Word_Miscellaneous

13:16:29 HOL-Library: theory Tree_Multiset

13:16:30 HOL-Library: theory Word

13:16:30 HOL-Library: theory Preorder

13:16:30 HOL-Library: theory Function_Growth

13:16:31 Koenigsberg_Friendship_Base: theory Factorial_Ring

13:16:31 HOL-Library: theory Library

13:16:32 Koenigsberg_Friendship_Base: theory MiscAlgebra

13:16:36 HOL-Library: theory Old_SMT

13:16:38 Timing HOL-Cardinals (2 threads, 34.812s elapsed time, 70.188s cpu time, 2.084s GC time, factor 2.02)

13:16:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Cardinals

13:16:38 Finished HOL-Cardinals (0:00:53 elapsed time, 0:01:37 cpu time, factor 1.83)

13:16:38 Building Incompleteness ...

13:16:40 Incompleteness: theory FSet

13:16:40 Incompleteness: theory Infinite_Set

13:16:41 Incompleteness: theory Multiset

13:16:41 Koenigsberg_Friendship_Base: theory Euclidean_Algorithm

13:16:44 Incompleteness: theory Nat_Bijection

13:16:45 Incompleteness: theory HF

13:16:46 Incompleteness: theory Old_Datatype

13:16:46 Incompleteness: theory Ordinal

13:16:46 Incompleteness: theory Rank

13:16:47 Incompleteness: theory OrdArith

13:16:47 Incompleteness: theory Phantom_Type

13:16:48 Incompleteness: theory Quotient_Syntax

13:16:48 Incompleteness: theory Quotient_Option

13:16:48 Incompleteness: theory Quotient_Product

13:16:48 Incompleteness: theory Quotient_Set

13:16:48 Incompleteness: theory Quotient_List

13:16:48 Incompleteness: theory Cardinality

13:16:49 Incompleteness: theory FinFun

13:16:50 Koenigsberg_Friendship_Base: theory Primes

13:16:51 Koenigsberg_Friendship_Base: theory Cong

13:16:51 Koenigsberg_Friendship_Base: theory Eratosthenes

13:16:52 Koenigsberg_Friendship_Base: theory Residues

13:16:52 Incompleteness: theory Nominal2_Base

13:16:54 Koenigsberg_Friendship_Base: theory Number_Theory

13:16:57 Incompleteness: theory Nominal2_Abs

13:17:00 Incompleteness: theory Nominal2_FCB

13:17:00 Incompleteness: theory Nominal2

13:17:12 Timing Kleene_Algebra (2 threads, 54.589s elapsed time, 97.832s cpu time, 3.668s GC time, factor 1.79)

13:17:12 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Kleene_Algebra

13:17:12 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Kleene_Algebra/document.pdf

13:17:12 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Kleene_Algebra/outline.pdf

13:17:12 Finished Kleene_Algebra (0:01:29 elapsed time, 0:02:32 cpu time, factor 1.70)

13:17:12 Building Automatic_Refinement ...

13:17:14 Automatic_Refinement: theory Infinite_Set

13:17:14 Automatic_Refinement: theory Foldi

13:17:14 Automatic_Refinement: theory Multiset

13:17:14 Automatic_Refinement: theory Omega_Words_Fun

13:17:15 Automatic_Refinement: theory Option_ord

13:17:16 Automatic_Refinement: theory Prio_List

13:17:16 Automatic_Refinement: theory Refine_Util

13:17:16 Automatic_Refinement: theory Anti_Unification

13:17:16 Automatic_Refinement: theory Attr_Comb

13:17:16 Automatic_Refinement: theory Named_Sorted_Thms

13:17:16 Automatic_Refinement: theory Mk_Term_Antiquot

13:17:16 Automatic_Refinement: theory Mpat_Antiquot

13:17:17 Automatic_Refinement: theory Indep_Vars

13:17:17 Automatic_Refinement: theory Mk_Record_Simp

13:17:17 Automatic_Refinement: theory Tagged_Solver

13:17:17 Automatic_Refinement: theory Select_Solve

13:17:20 Automatic_Refinement: theory List_More

13:17:20 Automatic_Refinement: theory Quicksort

13:17:20 Automatic_Refinement: theory Misc

13:17:26 Automatic_Refinement: theory Digraph_Basic

13:17:27 Automatic_Refinement: theory Refine_Lib

13:17:35 Timing HOL-Algebra (2 threads, 115.504s elapsed time, 229.932s cpu time, 9.576s GC time, factor 1.99)

13:17:35 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Algebra

13:17:35 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Algebra/document.pdf

13:17:35 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Algebra/outline.pdf

13:17:35 Finished HOL-Algebra (0:02:40 elapsed time, 0:05:00 cpu time, factor 1.87)

13:17:36 Building Cauchy ...

13:17:37 Cauchy: theory CauchySchwarz

13:17:37 Cauchy: theory CauchysMeanTheorem

13:17:37 Incompleteness: theory SyntaxN

13:17:44 Incompleteness: theory Coding

13:17:44 Incompleteness: theory Predicates

13:17:46 Incompleteness: theory Sigma

13:17:52 Incompleteness: theory Coding_Predicates

13:17:57 Incompleteness: theory Functions

13:17:57 Incompleteness: theory Pf_Predicates

13:18:00 Timing Cauchy (2 threads, 7.323s elapsed time, 15.440s cpu time, 0.088s GC time, factor 2.11)

13:18:00 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Cauchy

13:18:00 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Cauchy/document.pdf

13:18:00 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Cauchy/outline.pdf

13:18:00 Finished Cauchy (0:00:23 elapsed time, 0:00:39 cpu time, factor 1.67)

13:18:00 Building Dependent_SIFUM_Type_Systems ...

13:18:00 Incompleteness: theory Goedel_I

13:18:00 Incompleteness: theory II_Prelims

13:18:00 Automatic_Refinement: theory Param_Chapter

13:18:00 Automatic_Refinement: theory Relators

13:18:01 Automatic_Refinement: theory Param_Tool

13:18:01 Automatic_Refinement: theory Param_HOL

13:18:01 Dependent_SIFUM_Type_Systems: theory Preliminaries

13:18:02 Automatic_Refinement: theory Parametricity

13:18:02 Incompleteness: theory Pseudo_Coding

13:18:02 Incompleteness: theory Quote

13:18:02 Automatic_Refinement: theory Autoref_Data

13:18:02 Automatic_Refinement: theory Autoref_Phases

13:18:02 Automatic_Refinement: theory Autoref_Tagging

13:18:03 Dependent_SIFUM_Type_Systems: theory Language

13:18:03 Automatic_Refinement: theory Autoref_Id_Ops

13:18:03 Dependent_SIFUM_Type_Systems: theory Security

13:18:03 Incompleteness: theory Goedel_II

13:18:04 Automatic_Refinement: theory Autoref_Fix_Rel

13:18:04 Automatic_Refinement: theory Autoref_Translate

13:18:04 Automatic_Refinement: theory Autoref_Relator_Interface

13:18:04 Automatic_Refinement: theory Autoref_Gen_Algo

13:18:05 Automatic_Refinement: theory Autoref_Chapter

13:18:05 Automatic_Refinement: theory Autoref_Tool

13:18:05 Automatic_Refinement: theory Autoref_Bindings_HOL

13:18:07 Dependent_SIFUM_Type_Systems: theory Compositionality

13:18:09 Dependent_SIFUM_Type_Systems: theory LocallySoundModeUse

13:18:09 Dependent_SIFUM_Type_Systems: theory TypeSystem

13:18:09 Automatic_Refinement: theory Automatic_Refinement

13:18:14 Timing Koenigsberg_Friendship_Base (2 threads, 81.077s elapsed time, 161.936s cpu time, 8.120s GC time, factor 2.00)

13:18:14 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Koenigsberg_Friendship_Base

13:18:14 Finished Koenigsberg_Friendship_Base (0:01:54 elapsed time, 0:03:33 cpu time, factor 1.87)

13:18:14 Building Discrete_Summation ...

13:18:15 Discrete_Summation: theory Stirling

13:18:15 Discrete_Summation: theory Discrete_Summation

13:18:16 Discrete_Summation: theory Factorials

13:18:16 Discrete_Summation: theory Summation_Conversion

13:18:17 Discrete_Summation: theory Examples

13:18:36 Timing Automatic_Refinement (2 threads, 55.471s elapsed time, 109.596s cpu time, 3.504s GC time, factor 1.98)

13:18:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Automatic_Refinement

13:18:36 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Automatic_Refinement/document.pdf

13:18:36 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Automatic_Refinement/outline.pdf

13:18:36 Finished Automatic_Refinement (0:01:22 elapsed time, 0:02:31 cpu time, factor 1.83)

13:18:36 Timing Discrete_Summation (2 threads, 5.586s elapsed time, 11.156s cpu time, 0.076s GC time, factor 2.00)

13:18:36 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Discrete_Summation

13:18:36 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Discrete_Summation/document.pdf

13:18:36 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Discrete_Summation/outline.pdf

13:18:36 Finished Discrete_Summation (0:00:21 elapsed time, 0:00:34 cpu time, factor 1.62)

13:18:36 Building Refine_Monadic ...

13:18:36 Building Graph_Theory ...

13:18:37 Graph_Theory: theory Infinite_Set

13:18:37 Graph_Theory: theory Nat_Bijection

13:18:38 Refine_Monadic: theory Adhoc_Overloading

13:18:38 Refine_Monadic: theory Lattice_Syntax

13:18:38 Refine_Monadic: theory Bit

13:18:38 Refine_Monadic: theory Bits

13:18:38 Graph_Theory: theory Old_Datatype

13:18:38 Refine_Monadic: theory Boolean_Algebra

13:18:38 Graph_Theory: theory Liminf_Limsup

13:18:39 Refine_Monadic: theory Bits_Bit

13:18:39 Refine_Monadic: theory Misc_Numeric

13:18:39 Refine_Monadic: theory Bit_Representation

13:18:39 Refine_Monadic: theory Misc_Typedef

13:18:39 Refine_Monadic: theory Monad_Syntax

13:18:39 Refine_Monadic: theory Phantom_Type

13:18:40 Refine_Monadic: theory Bits_Int

13:18:40 Graph_Theory: theory Countable

13:18:40 Refine_Monadic: theory Cardinality

13:18:41 Refine_Monadic: theory Bool_List_Representation

13:18:41 Graph_Theory: theory Countable_Set

13:18:41 Refine_Monadic: theory Numeral_Type

13:18:42 Graph_Theory: theory Countable_Complete_Lattices

13:18:43 Refine_Monadic: theory Type_Length

13:18:43 Refine_Monadic: theory While_Combinator

13:18:43 Refine_Monadic: theory Word_Miscellaneous

13:18:44 Refine_Monadic: theory Word

13:18:45 Graph_Theory: theory Order_Continuity

13:18:46 Graph_Theory: theory Extended_Nat

13:18:47 Graph_Theory: theory Extended_Real

13:19:04 Refine_Monadic: theory Refine_Chapter

13:19:04 Refine_Monadic: theory Example_Chapter

13:19:04 Refine_Monadic: theory Refine_Mono_Prover

13:19:05 Refine_Monadic: theory Refine_Misc

13:19:05 Refine_Monadic: theory RefineG_Domain

13:19:05 Refine_Monadic: theory RefineG_Transfer

13:19:06 Refine_Monadic: theory RefineG_Assert

13:19:06 Refine_Monadic: theory RefineG_Recursion

13:19:06 Refine_Monadic: theory Refine_Basic

13:19:07 Refine_Monadic: theory RefineG_While

13:19:07 Refine_Monadic: theory Refine_Det

13:19:10 Refine_Monadic: theory Refine_Heuristics

13:19:10 Refine_Monadic: theory Refine_Leof

13:19:10 Refine_Monadic: theory Refine_Pfun

13:19:10 Refine_Monadic: theory Refine_While

13:19:12 Refine_Monadic: theory Refine_Transfer

13:19:12 Refine_Monadic: theory Autoref_Monadic

13:19:12 Refine_Monadic: theory Refine_Automation

13:19:12 Refine_Monadic: theory Refine_Foreach

13:19:14 Graph_Theory: theory FuncSet

13:19:14 Graph_Theory: theory Disjoint_Sets

13:19:14 Graph_Theory: theory Multiset

13:19:14 Graph_Theory: theory Rewrite

13:19:15 Refine_Monadic: theory Refine_Monadic

13:19:15 Graph_Theory: theory Rtrancl_On

13:19:15 Graph_Theory: theory Stuff

13:19:15 Refine_Monadic: theory Breadth_First_Search

13:19:15 Graph_Theory: theory Digraph

13:19:15 Refine_Monadic: theory WordRefine

13:19:17 Refine_Monadic: theory Examples

13:19:17 Graph_Theory: theory Arc_Walk

13:19:19 Graph_Theory: theory Permutations

13:19:19 Graph_Theory: theory Vertex_Walk

13:19:20 Graph_Theory: theory Funpow

13:19:21 Graph_Theory: theory Bidirected_Digraph

13:19:21 Graph_Theory: theory Pair_Digraph

13:19:21 Graph_Theory: theory Weighted_Graph

13:19:22 Graph_Theory: theory Shortest_Path

13:19:28 Graph_Theory: theory Digraph_Component

13:19:31 Graph_Theory: theory Digraph_Component_Vwalk

13:19:31 Graph_Theory: theory Digraph_Isomorphism

13:19:32 Graph_Theory: theory Subdivision

13:19:33 Graph_Theory: theory Euler

13:19:33 Graph_Theory: theory Kuratowski

13:19:38 Graph_Theory: theory Graph_Theory

13:19:47 Timing Simpl (2 threads, 163.519s elapsed time, 325.228s cpu time, 15.048s GC time, factor 1.99)

13:19:47 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Simpl

13:19:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Simpl/document.pdf

13:19:47 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Simpl/outline.pdf

13:19:47 Finished Simpl (0:04:04 elapsed time, 0:07:34 cpu time, factor 1.86)

13:19:48 Building JNF-HOL-Lib ...

13:19:50 JNF-HOL-Lib: theory Adhoc_Overloading

13:19:50 JNF-HOL-Lib: theory Lattice_Syntax

13:19:50 JNF-HOL-Lib: theory Order_Union

13:19:51 JNF-HOL-Lib: theory AList

13:19:51 JNF-HOL-Lib: theory Char_ord

13:19:51 JNF-HOL-Lib: theory Code_Abstract_Nat

13:19:51 JNF-HOL-Lib: theory Code_Binary_Nat

13:19:51 JNF-HOL-Lib: theory Code_Target_Nat

13:19:52 JNF-HOL-Lib: theory Code_Char

13:19:52 JNF-HOL-Lib: theory Disjoint_Sets

13:19:52 JNF-HOL-Lib: theory Fraction_Field

13:19:53 JNF-HOL-Lib: theory DAList

13:19:53 Dependent_SIFUM_Type_Systems: theory Example

13:19:53 Dependent_SIFUM_Type_Systems: theory Eisbach

13:19:53 Dependent_SIFUM_Type_Systems: theory Eisbach_Tools

13:19:53 Dependent_SIFUM_Type_Systems: theory TypeSystemTactics

13:19:53 JNF-HOL-Lib: theory Code_Target_Int

13:19:54 JNF-HOL-Lib: theory Code_Target_Numeral

13:19:54 JNF-HOL-Lib: theory IArray

13:19:54 JNF-HOL-Lib: theory Infinite_Set

13:19:55 JNF-HOL-Lib: theory List_lexord

13:19:55 JNF-HOL-Lib: theory Mapping

13:19:55 Dependent_SIFUM_Type_Systems: theory Example_Swap_Add

13:19:55 JNF-HOL-Lib: theory Monad_Syntax

13:19:55 JNF-HOL-Lib: theory More_List

13:19:56 JNF-HOL-Lib: theory DAList_Multiset

13:19:57 JNF-HOL-Lib: theory Permutations

13:19:57 JNF-HOL-Lib: theory Phantom_Type

13:19:57 Dependent_SIFUM_Type_Systems: theory Example_TypeSystem

13:19:57 JNF-HOL-Lib: theory Cardinality

13:19:58 JNF-HOL-Lib: theory RBT_Impl

13:19:58 JNF-HOL-Lib: theory Ramsey

13:19:59 JNF-HOL-Lib: theory Simps_Case_Conv

13:19:59 JNF-HOL-Lib: theory Polynomial

13:20:05 JNF-HOL-Lib: theory Fundamental_Theorem_Algebra

13:20:06 JNF-HOL-Lib: theory Wellorder_Extension

13:20:06 JNF-HOL-Lib: theory While_Combinator

13:20:13 Timing Refine_Monadic (2 threads, 59.858s elapsed time, 119.832s cpu time, 4.600s GC time, factor 2.00)

13:20:13 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Refine_Monadic

13:20:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Refine_Monadic/document.pdf

13:20:13 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Refine_Monadic/outline.pdf

13:20:13 Finished Refine_Monadic (0:01:37 elapsed time, 0:02:57 cpu time, factor 1.82)

13:20:14 Building Collections ...

13:20:16 Collections: theory AList

13:20:16 Collections: theory Code_Abstract_Nat

13:20:17 Collections: theory Code_Target_Nat

13:20:17 Collections: theory Dlist

13:20:18 Collections: theory FingerTree

13:20:19 Collections: theory Code_Target_Int

13:20:19 Collections: theory Code_Target_Numeral

13:20:19 Collections: theory ICF_Tools

13:20:19 Collections: theory BinomialHeap

13:20:23 Collections: theory SetIterator

13:20:26 Collections: theory Ord_Code_Preproc

13:20:26 Collections: theory Locale_Code

13:20:26 Collections: theory Partial_Equivalence_Relation

13:20:26 Collections: theory RBT_Impl

13:20:34 Collections: theory Record_Intf

13:20:35 Collections: theory Idx_Iterator

13:20:35 Collections: theory SetAbstractionIterator

13:20:36 Collections: theory SetIteratorOperations

13:20:38 Collections: theory Assoc_List

13:20:39 Collections: theory Diff_Array

13:20:41 Collections: theory Dlist_add

13:20:41 Collections: theory Proper_Iterator

13:20:41 Collections: theory It_to_It

13:20:42 Collections: theory SetIteratorGA

13:20:43 Collections: theory SkewBinomialHeap

13:20:54 Collections: theory Sorted_List_Operations

13:20:55 Collections: theory More_Bits_Int

13:20:58 Collections: theory Bits_Integer

13:21:08 Collections: theory DatRef

13:21:09 Collections: theory Gen_Iterator

13:21:10 Collections: theory Iterator

13:21:10 Collections: theory ICF_Spec_Base

13:21:11 Collections: theory MapSpec

13:21:11 Collections: theory Code_Target_Bits_Int

13:21:11 Collections: theory Code_Target_ICF

13:21:12 Collections: theory Locale_Code_Ex

13:21:14 Collections: theory RBT_add

13:21:15 Collections: theory Robdd

13:21:15 Collections: theory Word_Misc

13:21:16 Collections: theory Uint32

13:21:19 Collections: theory HashCode

13:21:30 Timing Graph_Theory (2 threads, 131.402s elapsed time, 262.300s cpu time, 8.976s GC time, factor 2.00)

13:21:30 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Graph_Theory

13:21:30 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Graph_Theory/document.pdf

13:21:30 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Graph_Theory/outline.pdf

13:21:30 Finished Graph_Theory (0:02:54 elapsed time, 0:05:27 cpu time, factor 1.88)

13:21:31 Building KAT_and_DRA ...

13:21:33 KAT_and_DRA: theory DRAT2

13:21:33 KAT_and_DRA: theory KAT2

13:21:33 KAT_and_DRA: theory Test_Dioid

13:21:41 KAT_and_DRA: theory Conway_Tests

13:21:43 KAT_and_DRA: theory KAT

13:21:46 KAT_and_DRA: theory DRAT

13:21:46 Timing Dependent_SIFUM_Type_Systems (2 threads, 165.618s elapsed time, 320.716s cpu time, 10.612s GC time, factor 1.94)

13:21:46 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Dependent_SIFUM_Type_Systems

13:21:46 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Dependent_SIFUM_Type_Systems/document.pdf

13:21:46 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Dependent_SIFUM_Type_Systems/outline.pdf

13:21:46 Finished Dependent_SIFUM_Type_Systems (0:03:46 elapsed time, 0:06:55 cpu time, factor 1.83)

13:21:47 KAT_and_DRA: theory KAT_Models

13:21:47 Building Marriage ...

13:21:47 KAT_and_DRA: theory PHL_KAT

13:21:48 Marriage: theory Marriage

13:21:48 KAT_and_DRA: theory DRA_Models

13:21:49 KAT_and_DRA: theory FolkTheorem

13:21:52 KAT_and_DRA: theory PHL_DRAT

13:22:08 Timing Marriage (2 threads, 4.727s elapsed time, 8.888s cpu time, 0.048s GC time, factor 1.88)

13:22:08 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Marriage

13:22:08 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Marriage/document.pdf

13:22:08 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Marriage/outline.pdf

13:22:08 Finished Marriage (0:00:20 elapsed time, 0:00:32 cpu time, factor 1.56)

13:22:08 Building Matrix ...

13:22:10 Matrix: theory FuncSet

13:22:10 Matrix: theory Congruence

13:22:11 Matrix: theory Lattice

13:22:13 Matrix: theory Group

13:22:15 Matrix: theory FiniteProduct

13:22:16 Matrix: theory Ring

13:22:28 Timing JNF-HOL-Lib (2 threads, 105.856s elapsed time, 208.580s cpu time, 10.588s GC time, factor 1.97)

13:22:28 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/JNF-HOL-Lib

13:22:28 Finished JNF-HOL-Lib (0:02:40 elapsed time, 0:04:53 cpu time, factor 1.83)

13:22:29 Building JNF-AFP-Lib ...

13:22:31 Matrix: theory Utility

13:22:31 Matrix: theory Ordered_Semiring

13:22:32 JNF-AFP-Lib: theory Comparator

13:22:32 JNF-AFP-Lib: theory Derive_Manager

13:22:32 JNF-AFP-Lib: theory Equal

13:22:32 JNF-AFP-Lib: theory Closure_Set

13:22:32 JNF-AFP-Lib: theory Extend_Partial_Order

13:22:33 Matrix: theory Matrix_Arith

13:22:33 JNF-AFP-Lib: theory FunctionLemmas

13:22:33 JNF-AFP-Lib: theory Generator_Aux

13:22:33 JNF-AFP-Lib: theory Equality_Generator

13:22:34 JNF-AFP-Lib: theory Compare

13:22:34 JNF-AFP-Lib: theory Comparator_Generator

13:22:34 JNF-AFP-Lib: theory Equality_Instances

13:22:34 JNF-AFP-Lib: theory Compare_Generator

13:22:34 JNF-AFP-Lib: theory IArray_Addenda

13:22:34 Matrix: theory Matrix_Comparison

13:22:35 JNF-AFP-Lib: theory IArray_Haskell

13:22:35 JNF-AFP-Lib: theory List_Fusion

13:22:35 JNF-AFP-Lib: theory Compare_Instances

13:22:35 JNF-AFP-Lib: theory Containers_Auxiliary

13:22:36 JNF-AFP-Lib: theory Normalized_Fraction

13:22:36 Matrix: theory Matrix

13:22:36 JNF-AFP-Lib: theory Lexicographic_Order

13:22:37 JNF-AFP-Lib: theory Set_Linorder

13:22:37 JNF-AFP-Lib: theory Containers_Generator

13:22:37 JNF-AFP-Lib: theory Collection_Enum

13:22:38 JNF-AFP-Lib: theory Collection_Eq

13:22:38 Timing KAT_and_DRA (2 threads, 43.142s elapsed time, 82.764s cpu time, 2.400s GC time, factor 1.92)

13:22:38 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/KAT_and_DRA

13:22:38 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/KAT_and_DRA/document.pdf

13:22:38 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/KAT_and_DRA/outline.pdf

13:22:38 Finished KAT_and_DRA (0:01:07 elapsed time, 0:02:13 cpu time, factor 1.99)

13:22:39 Building Multivariate_Polynomials ...

13:22:39 JNF-AFP-Lib: theory DList_Set

13:22:40 Multivariate_Polynomials: theory AList

13:22:40 JNF-AFP-Lib: theory RBT_Comparator_Impl

13:22:44 Multivariate_Polynomials: theory Power_Products

13:22:45 JNF-AFP-Lib: theory RBT_ext

13:22:46 Multivariate_Polynomials: theory Abstract_Poly

13:22:47 JNF-AFP-Lib: theory Regular_Set

13:22:48 JNF-AFP-Lib: theory Collection_Order

13:22:49 Multivariate_Polynomials: theory Poly_Lists

13:22:50 JNF-AFP-Lib: theory RBT_Mapping2

13:22:51 JNF-AFP-Lib: theory Regular_Exp

13:22:52 JNF-AFP-Lib: theory RBT_Set2

13:22:53 Collections: theory GenCF_Chapter

13:22:53 Collections: theory GenCF_Gen_Chapter

13:22:53 Collections: theory GenCF_Impl_Chapter

13:22:53 Collections: theory GenCF_Intf_Chapter

13:22:53 Collections: theory Product_Lexorder

13:22:53 Collections: theory Intf_Comp

13:22:53 Collections: theory Impl_Array_Stack

13:22:54 JNF-AFP-Lib: theory RingModuleFacts

13:22:54 JNF-AFP-Lib: theory NDerivative

13:22:54 Collections: theory Array_Iterator

13:22:55 Collections: theory Intf_Map

13:22:55 Collections: theory Gen_Comp

13:22:55 Collections: theory Gen_Map

13:22:55 Collections: theory Impl_RBT_Map

13:22:56 JNF-AFP-Lib: theory Relation_Interpretation

13:22:56 JNF-AFP-Lib: theory MonoidSums

13:22:56 Collections: theory Impl_Array_Map

13:22:56 JNF-AFP-Lib: theory LinearCombinations

13:22:57 Collections: theory Impl_List_Map

13:22:58 Collections: theory Intf_Set

13:22:58 JNF-AFP-Lib: theory Seq

13:22:58 Collections: theory Gen_Map2Set

13:22:59 JNF-AFP-Lib: theory Show

13:23:00 Collections: theory Gen_Set

13:23:00 JNF-AFP-Lib: theory Show_Instances

13:23:01 Collections: theory Impl_Cfun_Set

13:23:01 Collections: theory Impl_List_Set

13:23:01 Collections: theory Intf_Hash

13:23:02 JNF-AFP-Lib: theory Missing_Unsorted

13:23:02 Collections: theory Impl_Array_Hash_Map

13:23:03 JNF-AFP-Lib: theory Polynomial_Factorial

13:23:07 JNF-AFP-Lib: theory SumSpaces

13:23:07 JNF-AFP-Lib: theory Missing_Polynomial

13:23:08 JNF-AFP-Lib: theory Set_Impl

13:23:08 JNF-AFP-Lib: theory Utility

13:23:09 JNF-AFP-Lib: theory VectorSpace

13:23:10 Timing HOL-Library (2 threads, 361.509s elapsed time, 713.900s cpu time, 49.044s GC time, factor 1.97)

13:23:10 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Library

13:23:10 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Library/document.pdf

13:23:10 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/HOL/HOL-Library/outline.pdf

13:23:10 Finished HOL-Library (0:08:16 elapsed time, 0:15:29 cpu time, factor 1.87)

13:23:12 Building Coinductive ...

13:23:16 Coinductive: theory Primes

13:23:16 Coinductive: theory L2_Norm

13:23:16 Coinductive: theory Inner_Product

13:23:17 Coinductive: theory Norm_Arith

13:23:18 Coinductive: theory Product_Vector

13:23:18 Coinductive: theory Euclidean_Space

13:23:19 JNF-AFP-Lib: theory Equivalence_Checking

13:23:19 JNF-AFP-Lib: theory Regexp_Method

13:23:20 Timing Jinja (2 threads, 408.549s elapsed time, 806.164s cpu time, 24.624s GC time, factor 1.97)

13:23:20 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jinja

13:23:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jinja/document.pdf

13:23:20 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jinja/outline.pdf

13:23:20 Finished Jinja (0:08:26 elapsed time, 0:16:06 cpu time, factor 1.91)

13:23:20 JNF-AFP-Lib: theory Abstract_Rewriting

13:23:20 Coinductive: theory Linear_Algebra

13:23:21 Building Deriving ...

13:23:22 JNF-AFP-Lib: theory Relative_Rewriting

13:23:24 Coinductive: theory Topology_Euclidean_Space

13:23:24 JNF-AFP-Lib: theory SN_Orders

13:23:25 Deriving: theory More_Bits_Int

13:23:26 JNF-AFP-Lib: theory Ordered_Semiring

13:23:26 JNF-AFP-Lib: theory SN_Order_Carrier

13:23:27 Timing Matrix (2 threads, 51.076s elapsed time, 103.340s cpu time, 2.952s GC time, factor 2.02)

13:23:27 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Matrix

13:23:27 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Matrix/document.pdf

13:23:27 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Matrix/outline.pdf

13:23:27 Finished Matrix (0:01:18 elapsed time, 0:02:25 cpu time, factor 1.85)

13:23:27 Building LTL ...

13:23:27 JNF-AFP-Lib: theory Ring_Hom

13:23:27 Deriving: theory Bits_Integer

13:23:27 Deriving: theory Word_Misc

13:23:29 Timing Multivariate_Polynomials (2 threads, 29.112s elapsed time, 59.376s cpu time, 1.336s GC time, factor 2.04)

13:23:29 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Multivariate_Polynomials

13:23:29 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Multivariate_Polynomials/document.pdf

13:23:29 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Multivariate_Polynomials/outline.pdf

13:23:29 Finished Multivariate_Polynomials (0:00:50 elapsed time, 0:01:31 cpu time, factor 1.82)

13:23:29 Building Slicing ...

13:23:31 LTL: theory LTL

13:23:32 Slicing: theory AuxLemmas

13:23:32 Slicing: theory BitVector

13:23:32 Slicing: theory BasicDefs

13:23:32 Slicing: theory Com

13:23:34 Coinductive: theory Extended_Real_Limits

13:23:34 Slicing: theory CFG

13:23:34 Slicing: theory CFGExit

13:23:34 Slicing: theory Postdomination

13:23:35 Slicing: theory DynStandardControlDependence

13:23:35 Slicing: theory DynWeakControlDependence

13:23:35 Slicing: theory StandardControlDependence

13:23:36 Slicing: theory WeakControlDependence

13:23:36 Slicing: theory CFG_wf

13:23:36 Slicing: theory CFGExit_wf

13:23:36 Collections: theory Impl_Bit_Set

13:23:36 Collections: theory Uint

13:23:36 Slicing: theory DynDataDependence

13:23:37 Slicing: theory DataDependence

13:23:37 Slicing: theory DynPDG

13:23:37 Slicing: theory PDG

13:23:39 Slicing: theory DependentLiveVariables

13:23:39 Collections: theory Gen_Hash

13:23:39 Collections: theory Impl_Uv_Set

13:23:39 Slicing: theory Distance

13:23:39 Slicing: theory Observable

13:23:39 Slicing: theory SemanticsCFG

13:23:39 Slicing: theory WeakOrderDependence

13:23:40 Slicing: theory Slice

13:23:40 Slicing: theory ControlDependenceRelations

13:23:40 Slicing: theory DynSlice

13:23:41 Slicing: theory Labels

13:23:41 Deriving: theory Code_Target_Bits_Int

13:23:41 Deriving: theory Uint32

13:23:42 Slicing: theory Semantics

13:23:42 Deriving: theory Code_Target_ICF

13:23:42 Slicing: theory CDepInstantiations

13:23:42 Slicing: theory WCFG

13:23:43 Slicing: theory JVMCFG

13:23:43 LTL: theory LTL_Rewrite

13:23:43 Slicing: theory Interpretation

13:23:43 Slicing: theory WellFormed

13:23:44 Deriving: theory HashCode

13:23:45 Slicing: theory AdditionalLemmas

13:23:45 Slicing: theory DynamicControlDependences

13:23:45 Slicing: theory WEquivalence

13:23:45 Slicing: theory SemanticsWellFormed

13:23:46 Slicing: theory StaticControlDependences

13:23:49 LTL: theory LTL_Example

13:23:51 Slicing: theory JVMInterpretation

13:23:51 Deriving: theory Comparator

13:23:51 Deriving: theory Derive_Manager

13:23:51 Deriving: theory Generator_Aux

13:23:51 Deriving: theory Equality_Generator

13:23:52 Deriving: theory Equality_Instances

13:23:52 Deriving: theory Countable_Generator

13:23:52 Deriving: theory Compare

13:23:52 Deriving: theory Comparator_Generator

13:23:53 Slicing: theory JVMCFG_wf

13:23:53 Slicing: theory JVMPostdomination

13:23:53 Deriving: theory RBT_Comparator_Impl

13:23:53 Deriving: theory Compare_Generator

13:23:54 Slicing: theory SemanticsWF

13:23:54 Deriving: theory Compare_Instances

13:23:55 Deriving: theory Compare_Rat

13:23:55 Deriving: theory Compare_Real

13:23:56 Collections: theory GenCF

13:23:56 Deriving: theory Compare_Order_Instances

13:23:56 Deriving: theory RBT_Compare_Order_Impl

13:23:57 Deriving: theory Hash_Generator

13:23:58 Slicing: theory JVMControlDependences

13:23:59 Deriving: theory Hash_Instances

13:23:59 Slicing: theory Slicing

13:23:59 Deriving: theory Derive

13:24:00 Deriving: theory Derive_Examples

13:24:40 Coinductive: theory Resumption

13:24:40 Coinductive: theory Coinductive_Nat

13:24:41 Coinductive: theory Coinductive_List

13:24:41 Coinductive: theory CCPO_Topology

13:24:42 Timing LTL (2 threads, 32.238s elapsed time, 57.872s cpu time, 2.232s GC time, factor 1.80)

13:24:42 Browser info at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LTL

13:24:42 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LTL/document.pdf

13:24:42 Document at /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/LTL/outline.pdf

13:24:42 Finished LTL (0:01:14 elapsed time, 0:02:02 cpu time, factor 1.63)

13:24:43 Building MSO_Regex_Equivalence ...

13:24:47 MSO_Regex_Equivalence: theory Comparator

13:24:47 MSO_Regex_Equivalence: theory Derive_Manager