15:44:05 Started by an SCM change

15:44:05 [EnvInject] - Loading node environment variables.

15:44:05 Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-all

15:44:05 [isabelle-all] $ hg showconfig paths.default

15:44:05 [isabelle-all] $ hg pull --rev default

15:44:06 pulling from http://isabelle.in.tum.de/repos/isabelle/

15:44:06 no changes found

15:44:06 [isabelle-all] $ hg update --clean --rev default

15:44:06 12 files updated, 0 files merged, 0 files removed, 0 files unresolved

15:44:06 [isabelle-all] $ hg log --rev . --template {node}

15:44:06 [isabelle-all] $ hg log --rev . --template {rev}

15:44:06 [isabelle-all] $ hg log --rev 9497a6334a26752d09d58b7b934d639ea8f9e846 --template exists\n

15:44:06 exists

15:44:06 [isabelle-all] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(9497a6334a26752d09d58b7b934d639ea8f9e846)" --encoding UTF-8 --encodingmode replace

15:44:06 [afp] $ hg showconfig paths.default

15:44:06 [afp] $ hg pull --rev default

15:44:07 pulling from https://bitbucket.org/isa-afp/afp-devel/

15:44:07 no changes found

15:44:08 [afp] $ hg update --clean --rev default

15:44:08 478 files updated, 0 files merged, 0 files removed, 0 files unresolved

15:44:08 [afp] $ hg --config extensions.purge= clean --all

15:44:08 [afp] $ hg log --rev . --template {node}

15:44:08 [afp] $ hg log --rev . --template {rev}

15:44:08 [afp] $ hg log --rev ec3ff55171a95c2b44120d974b239e8d9bbcf65f --template exists\n

15:44:08 exists

15:44:08 [afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(ec3ff55171a95c2b44120d974b239e8d9bbcf65f)" --encoding UTF-8 --encodingmode replace

15:44:08 No emails were triggered.

15:44:08 [isabelle-all] $ /bin/sh -xe /tmp/jenkins8686717715024695347.sh

15:44:08 + Admin/jenkins/run_build all

15:44:08 + set -e

15:44:08 + PROFILE=all

15:44:08 + shift

15:44:08 + bin/isabelle components -a

15:44:08 + bin/isabelle jedit -bf

15:44:09 ### Building Isabelle/Scala ...

15:44:37 ### Building Isabelle/jEdit ...

15:44:54 + bin/isabelle ocaml_setup

15:44:54 # Run eval $(opam env) to update the current shell environment

15:44:55 [NOTE] It seems you have not updated your repositories for a while. Consider updating them with:

15:44:55 opam update

15:44:55

15:44:55 [NOTE] Package zarith is already installed (current version is 1.7).

15:44:55 + bin/isabelle ghc_setup

15:44:55 stack will use a sandboxed GHC it installed

15:44:55 For more information on paths, see 'stack path' and 'stack exec env'

15:44:55 To use this GHC and packages outside of a project, consider using:

15:44:55 stack ghc, stack ghci, stack runghc, or stack exec

15:44:56 The Glorious Glasgow Haskell Compilation System, version 8.4.4

15:44:56 + bin/isabelle ci_build_all

15:45:02

15:45:02 === CONFIGURATION ===

15:45:02

15:45:02 ISABELLE_BUILD_OPTIONS=""

15:45:02

15:45:02 ML_PLATFORM="x86_64_32-linux"

15:45:02 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64_32-linux"

15:45:02 ML_SYSTEM="polyml-5.8"

15:45:02 ML_OPTIONS="-H 4000 --maxheap 8G"

15:45:02 jobs = 10, threads = 4, numa = false

15:45:02

15:45:02 === BUILD ===

15:45:02

15:45:02 Build started at Sat, 22 Jun 2019 13:45:02 GMT

15:45:02 Isabelle id 4a327c061870

15:45:02 AFP id ec3ff55171a9

15:45:02

15:45:02 === LOG ===

15:45:02

15:45:03 Session Pure/Pure

15:45:04 Session CTT/CTT

15:45:04 Session Cube/Cube

15:45:04 Session FOL/FOL

15:45:04 Session CCL/CCL

15:45:04 Session FOL/FOL-ex

15:45:04 Session FOLP/FOLP

15:45:04 Session FOLP/FOLP-ex

15:45:04 Session HOL/HOL (main)

15:45:05 Session AFP/AVL-Trees (AFP)

15:45:05 Session AFP/AWN (AFP)

15:45:05 Session AFP/Abortable_Linearizable_Modules (AFP)

15:45:05 Session AFP/Abstract-Hoare-Logics (AFP)

15:45:05 Session AFP/AnselmGod (AFP)

15:45:05 Session AFP/AxiomaticCategoryTheory (AFP)

15:45:05 Session AFP/BinarySearchTree (AFP)

15:45:05 Session AFP/Binomial-Queues (AFP)

15:45:05 Session AFP/Bondy (AFP)

15:45:05 Session AFP/Bounded_Deducibility_Security (AFP)

15:45:05 Session AFP/BytecodeLogicJmlTypes (AFP)

15:45:05 Session AFP/CISC-Kernel (AFP)

15:45:05 Session AFP/CYK (AFP)

15:45:05 Session AFP/Cauchy (AFP)

15:45:05 Session AFP/Sqrt_Babylonian (AFP)

15:45:05 Session Doc/Classes (doc)

15:45:05 Session AFP/ClockSynchInst (AFP)

15:45:05 Session AFP/Compiling-Exceptions-Correctly (AFP)

15:45:05 Session AFP/ComponentDependencies (AFP)

15:45:05 Session AFP/Concurrent_Revisions (AFP)

15:45:05 Session AFP/Constructor_Funs (AFP)

15:45:05 Session AFP/CryptoBasedCompositionalProperties (AFP)

15:45:06 Session AFP/DPT-SAT-Solver (AFP)

15:45:06 Session AFP/Depth-First-Search (AFP)

15:45:06 Session AFP/Diophantine_Eqns_Lin_Hom (AFP)

15:45:06 Session AFP/DiskPaxos (AFP)

15:45:06 Session AFP/Example-Submission (AFP)

15:45:06 Session AFP/FFT (AFP)

15:45:06 Session AFP/FLP (AFP)

15:45:06 Session AFP/FeatherweightJava (AFP)

15:45:06 Session AFP/Featherweight_OCL (AFP)

15:45:06 Session AFP/FileRefinement (AFP)

15:45:06 Session AFP/FocusStreamsCaseStudies (AFP)

15:45:06 Session AFP/Free-Boolean-Algebra (AFP)

15:45:06 Session AFP/FunWithFunctions (AFP)

15:45:06 Session AFP/FunWithTilings (AFP)

15:45:06 Session Doc/Functions (doc)

15:45:06 Session AFP/GPU_Kernel_PL (AFP)

15:45:06 Session AFP/Gauss-Jordan-Elim-Fun (AFP)

15:45:06 Session AFP/GenClock (AFP)

15:45:06 Session AFP/General-Triangle (AFP)

15:45:06 Session AFP/Generic_Deriving (AFP)

15:45:06 Session AFP/GewirthPGCProof (AFP)

15:45:06 Session AFP/GoedelGod (AFP)

15:45:06 Session HOL/HOL-Cardinals (timing)

15:45:06 Session AFP/Binding_Syntax_Theory (AFP)

15:45:06 Session AFP/Ordinals_and_Cardinals (AFP)

15:45:06 Session HOL/HOL-Eisbach

15:45:06 Session AFP/Allen_Calculus (AFP)

15:45:07 Session AFP/Dependent_SIFUM_Type_Systems (AFP)

15:45:07 Session AFP/Dependent_SIFUM_Refinement (AFP)

15:45:07 Session Doc/Eisbach (doc)

15:45:07 Session HOL/HOL-Hoare

15:45:07 Session AFP/Case_Labeling (AFP)

15:45:07 Session HOL/HOL-Hoare_Parallel (timing)

15:45:07 Session HOL/HOL-IMPP

15:45:07 Session HOL/HOL-IOA

15:45:07 Session HOL/HOL-Import

15:45:07 Session HOL/HOL-Lattice

15:45:07 Session HOL/HOL-Library (main timing)

15:45:07 Session AFP/ArrowImpossibilityGS (AFP)

15:45:08 Session AFP/Auto2_HOL (AFP)

15:45:08 Session AFP/BNF_CC (AFP)

15:45:08 Session AFP/BNF_Operations (AFP)

15:45:08 Session AFP/Binomial-Heaps (AFP)

15:45:08 Session AFP/Boolean_Expression_Checkers (AFP)

15:45:08 Session AFP/Buildings (AFP)

15:45:08 Session AFP/CRDT (AFP)

15:45:08 Session AFP/IMAP-CRDT (AFP)

15:45:08 Session AFP/Card_Multisets (AFP)

15:45:09 Session AFP/Card_Number_Partitions (AFP)

15:45:09 Session AFP/Category (AFP)

15:45:09 Session AFP/Category3 (AFP)

15:45:09 Session AFP/MonoidalCategory (AFP)

15:45:09 Session Doc/Codegen (doc)

15:45:09 Session AFP/CofGroups (AFP)

15:45:09 Session AFP/Completeness (AFP)

15:45:09 Session AFP/ConcurrentIMP (AFP)

15:45:10 Session AFP/Concurrent_Ref_Alg (AFP)

15:45:10 Session AFP/CoreC++ (AFP)

15:45:10 Session AFP/Core_DOM (AFP)

15:45:10 Session Doc/Datatypes (doc)

15:45:10 Session Doc/Corec (doc)

15:45:10 Session AFP/Decl_Sem_Fun_PL (AFP)

15:45:10 Session AFP/Derangements (AFP)

15:45:10 Session AFP/Discrete_Summation (AFP)

15:45:11 Session AFP/Card_Partitions (AFP)

15:45:11 Session AFP/Bell_Numbers_Spivey (AFP)

15:45:11 Session AFP/Card_Equiv_Relations (AFP)

15:45:11 Session AFP/Efficient-Mergesort (AFP)

15:45:11 Session AFP/Encodability_Process_Calculi (AFP)

15:45:11 Session AFP/Epistemic_Logic (AFP)

15:45:11 Session AFP/Euler_Partition (AFP)

15:45:11 Session AFP/FOL-Fitting (AFP)

15:45:11 Session AFP/FOL_Harrison (AFP)

15:45:11 Session AFP/Factored_Transition_System_Bounding (AFP)

15:45:11 Session AFP/Falling_Factorial_Sum (AFP)

15:45:12 Session AFP/FinFun (AFP)

15:45:12 Session AFP/Finger-Trees (AFP)

15:45:12 Session AFP/Graph_Saturation (AFP)

15:45:12 Session AFP/Graph_Theory (AFP)

15:45:12 Session AFP/ShortestPath (AFP)

15:45:12 Session AFP/Group-Ring-Module (AFP)

15:45:12 Session AFP/Valuation (AFP)

15:45:12 Session HOL/HOL-Auth (timing)

15:45:12 Session HOL/HOL-UNITY (timing)

15:45:12 Session HOL/HOL-Bali (timing)

15:45:12 Session HOL/HOL-Computational_Algebra (main timing)

15:45:12 Session AFP/Descartes_Sign_Rule (AFP)

15:45:13 Session HOL/HOL-Algebra (main timing)

15:45:13 Session HOL/HOL-Decision_Procs (timing)

15:45:13 Session HOL/HOL-Quotient_Examples (timing)

15:45:13 Session AFP/Localization_Ring (AFP)

15:45:13 Session AFP/Orbit_Stabiliser (AFP)

15:45:14 Session AFP/Perfect-Number-Thm (AFP)

15:45:14 Session AFP/Secondary_Sylow (AFP)

15:45:14 Session AFP/Jordan_Hoelder (AFP)

15:45:14 Session AFP/VectorSpace (AFP)

15:45:14 Session HOL/HOL-Analysis (main timing)

15:45:14 Session AFP/Bernoulli (AFP)

15:45:15 Session AFP/Cartan_FP (AFP)

15:45:15 Session AFP/Cayley_Hamilton (AFP)

15:45:15 Session AFP/Coinductive (AFP)

15:45:15 Session AFP/DynamicArchitectures (AFP)

15:45:15 Session AFP/Architectural_Design_Patterns (AFP)

15:45:15 Session AFP/Lazy-Lists-II (AFP)

15:45:15 Session AFP/Stream_Fusion_Code (AFP)

15:45:15 Session AFP/Topology (AFP)

15:45:15 Session AFP/First_Welfare_Theorem (AFP)

15:45:15 Session AFP/Green (AFP)

15:45:15 Session HOL/HOL-Analysis-ex

15:45:16 Session HOL/HOL-Homology (timing)

15:45:16 Session HOL/HOL-Probability (main timing)

15:45:16 Session AFP/Buffons_Needle (AFP)

15:45:16 Session AFP/Density_Compiler (AFP)

15:45:16 Session AFP/DiscretePricing (AFP)

15:45:16 Session AFP/Ergodic_Theory (AFP)

15:45:16 Session AFP/Gromov_Hyperbolicity (AFP)

15:45:17 Session AFP/Fisher_Yates (AFP)

15:45:17 Session AFP/Girth_Chromatic (AFP)

15:45:17 Session AFP/Random_Graph_Subgraph_Threshold (AFP)

15:45:17 Session HOL/HOL-Probability-ex (timing)

15:45:17 Session AFP/Lp (AFP)

15:45:17 Session AFP/Markov_Models (AFP)

15:45:18 Session AFP/Monad_Normalisation (AFP)

15:45:18 Session AFP/Monomorphic_Monad (AFP)

15:45:18 Session AFP/Neumann_Morgenstern_Utility (AFP)

15:45:18 Session AFP/Probabilistic_Noninterference (AFP)

15:45:18 Session AFP/Probabilistic_System_Zoo (AFP)

15:45:18 Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)

15:45:18 Session AFP/Source_Coding_Theorem (AFP)

15:45:18 Session AFP/Irrationality_J_Hancl (AFP)

15:45:19 Session AFP/Kuratowski_Closure_Complement (AFP)

15:45:19 Session AFP/Lower_Semicontinuous (AFP)

15:45:19 Session AFP/Minkowskis_Theorem (AFP)

15:45:19 Session AFP/Octonions (AFP)

15:45:19 Session AFP/Probabilistic_System_Zoo-BNFs (AFP)

15:45:19 Session AFP/Ptolemys_Theorem (AFP)

15:45:19 Session AFP/Quaternions (AFP)

15:45:19 Session AFP/Rank_Nullity_Theorem (AFP)

15:45:19 Session AFP/Gauss_Jordan (AFP)

15:45:19 Session AFP/Echelon_Form (AFP)

15:45:19 Session AFP/Hermite (AFP)

15:45:19 Session AFP/Tarskis_Geometry (AFP)

15:45:20 Session AFP/Triangle (AFP)

15:45:20 Session AFP/Chord_Segments (AFP)

15:45:20 Session AFP/Stewart_Apollonius (AFP)

15:45:20 Session AFP/pGCL (AFP)

15:45:20 Session HOL/HOL-Isar_Examples

15:45:20 Session HOL/HOL-Nonstandard_Analysis (timing)

15:45:20 Session HOL/HOL-Nonstandard_Analysis-Examples (timing)

15:45:20 Session HOL/HOL-Number_Theory (main timing)

15:45:20 Session AFP/E_Transcendental (AFP)

15:45:21 Session AFP/Elliptic_Curves_Group_Law (AFP)

15:45:21 Session AFP/Fermat3_4 (AFP)

15:45:21 Session HOL/HOL-Data_Structures (timing)

15:45:21 Session HOL/HOL-ex (timing)

15:45:21 Session AFP/Automatic_Refinement (AFP)

15:45:22 Session HOL/HOL-Codegenerator_Test

15:45:22 Session AFP/Lehmer (AFP)

15:45:22 Session AFP/Pratt_Certificate (AFP)

15:45:22 Session AFP/Bertrands_Postulate (AFP)

15:45:23 Session AFP/Prime_Harmonic_Series (AFP)

15:45:23 Session AFP/RSAPSS (AFP)

15:45:23 Session AFP/SumSquares (AFP)

15:45:23 Session AFP/Liouville_Numbers (AFP)

15:45:23 Session AFP/Mason_Stothers (AFP)

15:45:23 Session AFP/Polynomial_Interpolation (AFP)

15:45:23 Session AFP/Probabilistic_Prime_Tests (AFP)

15:45:23 Session AFP/Rep_Fin_Groups (AFP)

15:45:23 Session AFP/Sturm_Sequences (AFP)

15:45:24 Session AFP/Special_Function_Bounds (AFP)

15:45:24 Session AFP/Sturm_Tarski (AFP)

15:45:24 Session AFP/Budan_Fourier (AFP)

15:45:24 Session AFP/Winding_Number_Eval (AFP)

15:45:24 Session AFP/Count_Complex_Roots (AFP)

15:45:24 Session HOL/HOL-Corec_Examples (timing)

15:45:24 Session HOL/HOL-Datatype_Examples (timing)

15:45:24 Session HOL/HOL-Hahn_Banach

15:45:24 Session HOL/HOL-IMP (timing)

15:45:24 Session AFP/Abs_Int_ITP2012 (AFP)

15:45:25 Session HOL/HOL-Imperative_HOL (timing)

15:45:25 Session AFP/Auto2_Imperative_HOL (AFP)

15:45:25 Session AFP/Imperative_Insertion_Sort (AFP)

15:45:25 Session HOL/HOL-Induct

15:45:25 Session HOL/HOL-Matrix_LP

15:45:25 Session HOL/HOL-Metis_Examples (timing)

15:45:25 Session HOL/HOL-MicroJava (timing)

15:45:25 Session HOL/HOL-Mutabelle

15:45:25 Session HOL/HOL-Nitpick_Examples

15:45:25 Session HOL/HOL-Nominal

15:45:26 Session AFP/CCS (AFP)

15:45:26 Session HOL/HOL-Nominal-Examples (timing)

15:45:26 Session AFP/Lam-ml-Normalization (AFP)

15:45:26 Session AFP/Pi_Calculus (AFP)

15:45:26 Session AFP/Psi_Calculi (AFP)

15:45:26 Session AFP/SequentInvertibility (AFP)

15:45:26 Session HOL/HOL-Predicate_Compile_Examples (timing)

15:45:26 Session HOL/HOL-Quickcheck_Examples (timing)

15:45:26 Session HOL/HOL-SET_Protocol (timing)

15:45:27 Session HOL/HOL-TPTP

15:45:27 Session HOL/HOL-Unix

15:45:27 Session HOL/HOL-ZF

15:45:27 Session AFP/Category2 (AFP)

15:45:27 Session AFP/HereditarilyFinite (AFP)

15:45:27 Session AFP/HyperCTL (AFP)

15:45:27 Session AFP/Integration (AFP)

15:45:27 Session AFP/Isabelle_Meta_Model (AFP)

15:45:27 Session AFP/LTL (AFP)

15:45:27 Session AFP/Stuttering_Equivalence (AFP)

15:45:27 Session AFP/Lambda_Free_RPOs (AFP)

15:45:27 Session AFP/Lambda_Free_EPO (AFP)

15:45:27 Session AFP/Landau_Symbols (AFP)

15:45:27 Session AFP/Akra_Bazzi (AFP)

15:45:28 Session AFP/Catalan_Numbers (AFP)

15:45:28 Session AFP/Error_Function (AFP)

15:45:28 Session AFP/Euler_MacLaurin (AFP)

15:45:28 Session AFP/Stirling_Formula (AFP)

15:45:28 Session AFP/LightweightJava (AFP)

15:45:28 Session AFP/LinearQuantifierElim (AFP)

15:45:28 Session AFP/List-Infinite (AFP)

15:45:28 Session AFP/Nat-Interval-Logic (AFP)

15:45:28 Session AFP/AutoFocus-Stream (AFP)

15:45:29 Session AFP/MuchAdoAboutTwo (AFP)

15:45:29 Session AFP/Optics (AFP)

15:45:29 Session AFP/UTP-Toolkit (AFP)

15:45:29 Session AFP/UTP (AFP)

15:45:29 Session AFP/Order_Lattice_Props (AFP)

15:45:29 Session AFP/POPLmark-deBruijn (AFP)

15:45:29 Session AFP/Pairing_Heap (AFP)

15:45:29 Session AFP/Password_Authentication_Protocol (AFP)

15:45:29 Session AFP/Pell (AFP)

15:45:29 Session AFP/Presburger-Automata (AFP)

15:45:29 Session AFP/Priority_Queue_Braun (AFP)

15:45:29 Session AFP/Program-Conflict-Analysis (AFP)

15:45:29 Session AFP/Regular-Sets (AFP)

15:45:30 Session AFP/Abstract-Rewriting (AFP)

15:45:30 Session AFP/Decreasing-Diagrams (AFP)

15:45:30 Session AFP/First_Order_Terms (AFP)

15:45:30 Session AFP/Matrix (AFP)

15:45:30 Session AFP/Matrix_Tensor (AFP)

15:45:30 Session AFP/Knot_Theory (AFP)

15:45:30 Session AFP/Coinductive_Languages (AFP)

15:45:30 Session AFP/Finite_Automata_HF (AFP)

15:45:30 Session AFP/Functional-Automata (AFP)

15:45:30 Session AFP/Posix-Lexing (AFP)

15:45:30 Session AFP/Ribbon_Proofs (AFP)

15:45:30 Session AFP/SATSolverVerification (AFP)

15:45:31 Session AFP/Safe_OCL (AFP)

15:45:31 Session AFP/Selection_Heap_Sort (AFP)

15:45:31 Session AFP/Simplex (AFP)

15:45:31 Session AFP/Skew_Heap (AFP)

15:45:31 Session AFP/Sort_Encodings (AFP)

15:45:31 Session AFP/Splay_Tree (AFP)

15:45:31 Session AFP/Amortized_Complexity (AFP)

15:45:31 Session AFP/Dynamic_Tables (AFP)

15:45:31 Session AFP/Root_Balanced_Tree (AFP)

15:45:32 Session AFP/Stable_Matching (AFP)

15:45:32 Session AFP/SuperCalc (AFP)

15:45:32 Session AFP/Tail_Recursive_Functions (AFP)

15:45:32 Session AFP/TortoiseHare (AFP)

15:45:32 Session AFP/Trie (AFP)

15:45:32 Session AFP/Flyspeck-Tame (AFP)

15:45:32 Session AFP/Twelvefold_Way (AFP)

15:45:32 Session AFP/Vickrey_Clarke_Groves (AFP)

15:45:32 Session HOL/HOL-Mirabelle

15:45:32 Session HOL/HOL-Mirabelle-ex

15:45:32 Session HOL/HOL-NanoJava

15:45:32 Session HOL/HOL-Prolog

15:45:33 Session HOL/HOL-Real_Asymp

15:45:33 Session HOL/HOL-Real_Asymp-Manual

15:45:33 Session HOL/HOL-Statespace

15:45:33 Session HOL/HOL-TLA

15:45:33 Session HOL/HOL-TLA-Buffer

15:45:33 Session HOL/HOL-TLA-Inc

15:45:33 Session HOL/HOL-TLA-Memory

15:45:33 Session HOL/HOL-Types_To_Sets

15:45:33 Session AFP/Smooth_Manifolds (AFP)

15:45:33 Session HOL/HOL-Word (main timing)

15:45:34 Session HOL/HOL-SPARK

15:45:34 Session HOL/HOL-SPARK-Examples

15:45:34 Session AFP/RIPEMD-160-SPARK (AFP)

15:45:34 Session HOL/HOL-SPARK-Manual

15:45:34 Session HOL/HOL-Word-SMT_Examples (timing)

15:45:34 Session AFP/Kleene_Algebra (AFP)

15:45:34 Session AFP/KAT_and_DRA (AFP)

15:45:34 Session AFP/Multirelations (AFP)

15:45:34 Session AFP/Quantales (AFP)

15:45:34 Session AFP/Transformer_Semantics (AFP)

15:45:34 Session AFP/Regular_Algebras (AFP)

15:45:34 Session AFP/Relation_Algebra (AFP)

15:45:34 Session AFP/Residuated_Lattices (AFP)

15:45:35 Session AFP/LEM (AFP)

15:45:35 Session AFP/Native_Word (AFP)

15:45:35 Session AFP/WebAssembly (AFP)

15:45:35 Session AFP/Refine_Monadic (AFP)

15:45:36 Session AFP/Collections (AFP)

15:45:36 Session AFP/Abstract_Completeness (AFP)

15:45:36 Session AFP/Abstract_Soundness (AFP)

15:45:36 Session AFP/Incredible_Proof_Machine (AFP)

15:45:36 Session AFP/Deriving (AFP)

15:45:37 Session AFP/CAVA_Base (AFP)

15:45:37 Session AFP/CAVA_Automata (AFP)

15:45:37 Session AFP/DFS_Framework (AFP)

15:45:37 Session AFP/Gabow_SCC (AFP)

15:45:37 Session AFP/LTL_to_GBA (AFP)

15:45:37 Session AFP/Promela (AFP)

15:45:38 Session AFP/Containers (AFP)

15:45:38 Session AFP/Collections_Examples (AFP)

15:45:38 Session AFP/Containers-Benchmarks (AFP)

15:45:39 Session AFP/Datatype_Order_Generator (AFP)

15:45:39 Session AFP/Old_Datatype_Show (AFP)

15:45:39 Session AFP/Show (AFP)

15:45:39 Session AFP/JNF-AFP-Lib (AFP)

15:45:40 Session AFP/Real_Impl (AFP)

15:45:40 Session AFP/QR_Decomposition (AFP)

15:45:40 Session AFP/Dijkstra_Shortest_Path (AFP)

15:45:40 Session AFP/Koenigsberg_Friendship (AFP)

15:45:41 Session AFP/Transition_Systems_and_Automata (AFP)

15:45:41 Session AFP/Buchi_Complementation (AFP)

15:45:41 Session AFP/LTL_Master_Theorem (AFP)

15:45:41 Session AFP/Partial_Order_Reduction (AFP)

15:45:42 Session AFP/SM_Base (AFP)

15:45:42 Session AFP/SM (AFP)

15:45:42 Session AFP/CAVA_Setup (AFP)

15:45:43 Session AFP/CAVA_LTL_Modelchecker (AFP)

15:45:43 Session AFP/Transitive-Closure (AFP)

15:45:43 Session AFP/KBPs (AFP)

15:45:43 Session AFP/Tree-Automata (AFP)

15:45:43 Session AFP/SPARCv8 (AFP)

15:45:43 Session AFP/Separation_Algebra (AFP)

15:45:43 Session AFP/Separata (AFP)

15:45:44 Session AFP/Separation_Logic_Imperative_HOL (AFP)

15:45:44 Session AFP/Sepref_Prereq (AFP)

15:45:44 Session AFP/ROBDD (AFP)

15:45:45 Session AFP/UpDown_Scheme (AFP)

15:45:45 Session AFP/Word_Lib (AFP)

15:45:45 Session AFP/Complx (AFP)

15:45:45 Session AFP/IEEE_Floating_Point (AFP)

15:45:45 Session AFP/CakeML (AFP)

15:45:45 Session AFP/IP_Addresses (AFP)

15:45:46 Session AFP/Simple_Firewall (AFP)

15:45:46 Session AFP/Routing (AFP)

15:45:46 Session AFP/Iptables_Semantics (AFP)

15:45:46 Session AFP/Iptables_Semantics_Examples (AFP)

15:45:46 Session AFP/LOFT (AFP)

15:45:46 Session HOL/HOLCF (main timing)

15:45:46 Session AFP/Circus (AFP)

15:45:47 Session AFP/HOL-CSP (AFP)

15:45:47 Session HOL/HOLCF-IMP

15:45:47 Session HOL/HOLCF-Library

15:45:47 Session HOL/HOLCF-FOCUS

15:45:47 Session HOL/HOLCF-ex

15:45:47 Session AFP/PCF (AFP)

15:45:47 Session AFP/HOLCF-Prelude (AFP)

15:45:47 Session HOL/HOLCF-Tutorial

15:45:47 Session HOL/IOA (timing)

15:45:47 Session HOL/IOA-ABP

15:45:48 Session HOL/IOA-NTP

15:45:48 Session HOL/IOA-Storage

15:45:48 Session HOL/IOA-ex

15:45:48 Session AFP/Shivers-CFA (AFP)

15:45:48 Session AFP/Stream-Fusion (AFP)

15:45:48 Session AFP/Tycon (AFP)

15:45:48 Session AFP/WorkerWrapper (AFP)

15:45:48 Session AFP/Heard_Of (AFP)

15:45:48 Session AFP/Consensus_Refined (AFP)

15:45:48 Session AFP/Hoare_Time (AFP)

15:45:48 Session AFP/HotelKeyCards (AFP)

15:45:48 Session Doc/How_to_Prove_it (no_doc)

15:45:48 Session AFP/Huffman (AFP)

15:45:48 Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)

15:45:48 Session AFP/IMP2 (AFP)

15:45:49 Session Doc/Implementation (doc)

15:45:49 Session AFP/Impossible_Geometry (AFP)

15:45:49 Session AFP/Inductive_Confidentiality (AFP)

15:45:49 Session AFP/InfPathElimination (AFP)

15:45:49 Session Doc/Isar_Ref (doc)

15:45:49 Session Doc/JEdit (doc)

15:45:49 Session AFP/JiveDataStoreModel (AFP)

15:45:49 Session AFP/KAD (AFP)

15:45:50 Session AFP/Algebraic_VCs (AFP)

15:45:50 Session AFP/Key_Agreement_Strong_Adversaries (AFP)

15:45:50 Session AFP/LambdaMu (AFP)

15:45:50 Session AFP/LatticeProperties (AFP)

15:45:50 Session AFP/DataRefinementIBP (AFP)

15:45:50 Session AFP/GraphMarkingIBP (AFP)

15:45:50 Session AFP/Lazy_Case (AFP)

15:45:50 Session AFP/Dict_Construction (AFP)

15:45:50 Session AFP/Lifting_Definition_Option (AFP)

15:45:50 Session AFP/List-Index (AFP)

15:45:50 Session AFP/Affine_Arithmetic (AFP)

15:45:51 Session AFP/Taylor_Models (AFP)

15:45:51 Session AFP/Comparison_Sort_Lower_Bound (AFP)

15:45:51 Session AFP/Formula_Derivatives (AFP)

15:45:51 Session AFP/Formula_Derivatives-Examples (AFP)

15:45:51 Session AFP/Higher_Order_Terms (AFP)

15:45:52 Session AFP/Jinja (AFP)

15:45:52 Session AFP/HRB-Slicing (AFP)

15:45:52 Session AFP/InformationFlowSlicing_Inter (AFP)

15:45:52 Session AFP/Slicing (AFP)

15:45:52 Session AFP/Formal_SSA (AFP)

15:45:53 Session AFP/Minimal_SSA (AFP)

15:45:53 Session AFP/InformationFlowSlicing (AFP)

15:45:53 Session AFP/LTL_to_DRA (AFP)

15:45:53 Session AFP/List_Update (AFP)

15:45:53 Session AFP/Ordinary_Differential_Equations (AFP)

15:45:54 Session AFP/Differential_Dynamic_Logic (AFP)

15:45:54 Session AFP/HOL-ODE-Numerics (AFP)

15:45:55 Session AFP/HOL-ODE-ARCH-COMP (AFP)

15:45:55 Session AFP/HOL-ODE-Examples (AFP large)

15:45:55 Session AFP/Lorenz_Approximation (AFP)

15:45:55 Session AFP/Lorenz_C0 (AFP large)

15:45:55 Session AFP/Lorenz_C1 (AFP large)

15:45:55 Session AFP/Quick_Sort_Cost (AFP)

15:45:56 Session AFP/Random_BSTs (AFP)

15:45:56 Session AFP/Randomised_BSTs (AFP)

15:45:56 Session AFP/Treaps (AFP)

15:45:56 Session AFP/Randomised_Social_Choice (AFP)

15:45:56 Session AFP/Fishburn_Impossibility (AFP)

15:45:56 Session AFP/SDS_Impossibility (AFP)

15:45:57 Session AFP/Refine_Imperative_HOL (AFP)

15:45:57 Session AFP/Floyd_Warshall (AFP)

15:45:57 Session AFP/Sepref_Basic (AFP)

15:45:57 Session AFP/Sepref_IICF (AFP)

15:45:58 Session AFP/Flow_Networks (AFP)

15:45:58 Session AFP/EdmondsKarp_Maxflow (AFP)

15:45:58 Session AFP/MFMC_Countable (AFP)

15:45:58 Session AFP/Prpu_Maxflow (AFP)

15:45:59 Session AFP/Knuth_Morris_Pratt (AFP)

15:45:59 Session AFP/VerifyThis2018 (AFP)

15:45:59 Session AFP/List_Interleaving (AFP)

15:45:59 Session AFP/List_Inversions (AFP)

15:45:59 Session AFP/LocalLexing (AFP)

15:45:59 Session Doc/Locales (doc)

15:45:59 Session AFP/Lowe_Ontological_Argument (AFP)

15:45:59 Session AFP/MSO_Regex_Equivalence (AFP)

15:46:00 Session Doc/Main (doc)

15:46:00 Session AFP/Marriage (AFP)

15:46:00 Session AFP/Latin_Square (AFP)

15:46:00 Session AFP/Matroids (AFP)

15:46:00 Session AFP/Kruskal (AFP)

15:46:00 Session AFP/Max-Card-Matching (AFP)

15:46:00 Session AFP/Median_Of_Medians_Selection (AFP)

15:46:01 Session AFP/KD_Tree (AFP)

15:46:01 Session AFP/Menger (AFP)

15:46:01 Session AFP/MiniML (AFP)

15:46:01 Session AFP/Modular_Assembly_Kit_Security (AFP)

15:46:01 Session AFP/Monad_Memo_DP (AFP)

15:46:01 Session AFP/Hidden_Markov_Models (AFP)

15:46:01 Session AFP/Optimal_BST (AFP)

15:46:01 Session AFP/MonoBoolTranAlgebra (AFP)

15:46:01 Session AFP/Name_Carrying_Type_Inference (AFP)

15:46:02 Session AFP/Network_Security_Policy_Verification (AFP)

15:46:02 Session AFP/No_FTL_observers (AFP)

15:46:02 Session AFP/Nominal2 (AFP)

15:46:02 Session AFP/Incompleteness (AFP)

15:46:03 Session AFP/Surprise_Paradox (AFP)

15:46:03 Session AFP/LambdaAuth (AFP)

15:46:03 Session AFP/Launchbury (AFP)

15:46:03 Session AFP/Call_Arity (AFP)

15:46:03 Session AFP/Modal_Logics_for_NTS (AFP)

15:46:04 Session AFP/Rewriting_Z (AFP)

15:46:04 Session AFP/Noninterference_CSP (AFP)

15:46:04 Session AFP/Noninterference_Ipurge_Unwinding (AFP)

15:46:04 Session AFP/Noninterference_Generic_Unwinding (AFP)

15:46:04 Session AFP/Noninterference_Inductive_Unwinding (AFP)

15:46:04 Session AFP/Noninterference_Sequential_Composition (AFP)

15:46:04 Session AFP/Noninterference_Concurrent_Composition (AFP)

15:46:04 Session AFP/NormByEval (AFP)

15:46:04 Session AFP/OpSets (AFP)

15:46:04 Session AFP/Open_Induction (AFP)

15:46:04 Session AFP/Well_Quasi_Orders (AFP)

15:46:04 Session AFP/Decreasing-Diagrams-II (AFP)

15:46:04 Session AFP/Myhill-Nerode (AFP)

15:46:04 Session AFP/Polynomials (AFP)

15:46:05 Session AFP/Symmetric_Polynomials (AFP)

15:46:05 Session AFP/Pi_Transcendental (AFP)

15:46:05 Session AFP/Ordinal (AFP)

15:46:06 Session AFP/Nested_Multisets_Ordinals (AFP)

15:46:06 Session AFP/Lambda_Free_KBOs (AFP)

15:46:06 Session AFP/Ordered_Resolution_Prover (AFP)

15:46:06 Session AFP/PLM (AFP)

15:46:06 Session AFP/PSemigroupsConvolution (AFP)

15:46:06 Session AFP/Paraconsistency (AFP)

15:46:07 Session AFP/Parity_Game (AFP)

15:46:07 Session AFP/Partial_Function_MR (AFP)

15:46:07 Session AFP/Certification_Monads (AFP)

15:46:07 Session AFP/XML (AFP)

15:46:08 Session AFP/Polynomial_Factorization (AFP)

15:46:08 Session AFP/Dirichlet_Series (AFP)

15:46:09 Session AFP/Zeta_Function (AFP)

15:46:09 Session AFP/Dirichlet_L (AFP)

15:46:10 Session AFP/Prime_Number_Theorem (AFP)

15:46:10 Session AFP/Prime_Distribution_Elementary (AFP)

15:46:10 Session AFP/Transcendence_Series_Hancl_Rucki (AFP)

15:46:11 Session AFP/Functional_Ordered_Resolution_Prover (AFP)

15:46:11 Session AFP/Jordan_Normal_Form (AFP)

15:46:12 Session AFP/Deep_Learning (AFP)

15:46:12 Session AFP/Farkas (AFP)

15:46:12 Session AFP/Groebner_Bases (AFP)

15:46:13 Session AFP/Signature_Groebner (AFP)

15:46:13 Session AFP/QHLProver (AFP)

15:46:14 Session AFP/Linear_Recurrences (AFP)

15:46:14 Session AFP/Perron_Frobenius (AFP)

15:46:15 Session AFP/Stochastic_Matrices (AFP)

15:46:15 Session AFP/Subresultants (AFP)

15:46:16 Session AFP/Pre_BZ (AFP)

15:46:16 Session AFP/Berlekamp_Zassenhaus (AFP)

15:46:16 Session AFP/Algebraic_Numbers (AFP)

15:46:17 Session AFP/LLL_Basis_Reduction (AFP)

15:46:17 Session AFP/LLL_Factorization (AFP)

15:46:17 Session AFP/Linear_Recurrences_Solver (AFP)

15:46:18 Session AFP/Probabilistic_While (AFP)

15:46:18 Session AFP/Pop_Refinement (AFP)

15:46:18 Session AFP/Possibilistic_Noninterference (AFP)

15:46:18 Session Doc/Prog_Prove (doc)

15:46:18 Session AFP/Projective_Geometry (AFP)

15:46:18 Session AFP/Proof_Strategy_Language (AFP)

15:46:18 Session AFP/PropResPI (AFP)

15:46:18 Session AFP/Propositional_Proof_Systems (AFP)

15:46:18 Session AFP/PseudoHoops (AFP)

15:46:18 Session AFP/Ramsey-Infinite (AFP)

15:46:18 Session AFP/Recursion-Theory-I (AFP)

15:46:19 Session AFP/Minsky_Machines (AFP)

15:46:19 Session AFP/RefinementReactive (AFP)

15:46:19 Session AFP/Resolution_FOL (AFP)

15:46:19 Session AFP/Robbins-Conjecture (AFP)

15:46:19 Session AFP/Roy_Floyd_Warshall (AFP)

15:46:19 Session AFP/SIFPL (AFP)

15:46:19 Session AFP/SIFUM_Type_Systems (AFP)

15:46:19 Session AFP/Security_Protocol_Refinement (AFP)

15:46:20 Session AFP/SenSocialChoice (AFP)

15:46:20 Session AFP/Simpl (AFP)

15:46:20 Session AFP/BDD (AFP)

15:46:20 Session AFP/Planarity_Certificates (AFP)

15:46:20 Session AFP/Statecharts (AFP)

15:46:20 Session AFP/Stone_Algebras (AFP)

15:46:20 Session AFP/Stone_Relation_Algebras (AFP)

15:46:20 Session AFP/Stone_Kleene_Relation_Algebras (AFP)

15:46:21 Session AFP/Aggregation_Algebras (AFP)

15:46:21 Session AFP/Store_Buffer_Reduction (AFP)

15:46:21 Session AFP/Strong_Security (AFP)

15:46:21 Session Doc/Sugar (doc)

15:46:21 Session AFP/TLA (AFP)

15:46:21 Session AFP/Timed_Automata (AFP)

15:46:21 Session AFP/Probabilistic_Timed_Automata (AFP)

15:46:21 Session AFP/Transitive-Closure-II (AFP)

15:46:21 Session AFP/Tree_Decomposition (AFP)

15:46:21 Session Doc/Tutorial (doc)

15:46:21 Session Doc/Typeclass_Hierarchy (doc)

15:46:22 Session AFP/Types_Tableaus_and_Goedels_God (AFP)

15:46:22 Session AFP/UPF (AFP)

15:46:22 Session AFP/UPF_Firewall (AFP)

15:46:22 Session AFP/Universal_Turing_Machine (AFP)

15:46:22 Session AFP/Verified-Prover (AFP)

15:46:22 Session AFP/VolpanoSmith (AFP)

15:46:22 Session AFP/WHATandWHERE_Security (AFP)

15:46:22 Session AFP/Weight_Balanced_Trees (AFP)

15:46:22 Session HOL/HOL-Proofs (timing)

15:46:23 Session HOL/HOL-Proofs-Extraction (timing)

15:46:23 Session HOL/HOL-Proofs-Lambda (timing)

15:46:23 Session AFP/Applicative_Lifting (AFP)

15:46:24 Session AFP/CryptHOL (AFP)

15:46:24 Session AFP/Constructive_Cryptography (AFP)

15:46:24 Session AFP/Game_Based_Crypto (AFP)

15:46:25 Session AFP/Multi_Party_Computation (AFP)

15:46:25 Session AFP/Free-Groups (AFP)

15:46:25 Session AFP/Locally-Nameless-Sigma (AFP)

15:46:26 Session AFP/Stern_Brocot (AFP)

15:46:26 Session HOL/HOL-Proofs-ex

15:46:26 Session Tools/Haskell

15:46:26 Session Doc/Intro (doc)

15:46:26 Session LCF/LCF

15:46:26 Session Doc/Logics (doc)

15:46:26 Session Doc/Nitpick (doc)

15:46:26 Session Tools/SML

15:46:26 Session Sequents/Sequents

15:46:26 Session Doc/Sledgehammer (doc)

15:46:26 Session Tools/Spec_Check

15:46:26 Session AFP/Regex_Equivalence (AFP)

15:46:26 Session Doc/System (doc)

15:46:26 Session ZF/ZF (main timing)

15:46:26 Session Doc/Logics_ZF (doc)

15:46:27 Session ZF/ZF-AC

15:46:27 Session ZF/ZF-Coind

15:46:27 Session ZF/ZF-Constructible

15:46:27 Session ZF/ZF-IMP

15:46:27 Session ZF/ZF-Induct

15:46:27 Session ZF/ZF-UNITY (timing)

15:46:27 Session ZF/ZF-Resid

15:46:27 Session ZF/ZF-ex

15:46:42 Building HOL ...

15:46:42 Building HOL-Proofs ...

15:46:44 HOL: theory HOL.Code_Generator

15:46:44 HOL-Proofs: theory HOL.Code_Generator

15:46:48 HOL: theory HOL.HOL

15:46:48 HOL-Proofs: theory HOL.HOL

15:46:52 HOL: theory HOL.Argo

15:46:52 HOL: theory HOL.Ctr_Sugar

15:46:52 HOL: theory HOL.Orderings

15:46:53 HOL-Proofs: theory HOL.Argo

15:46:53 HOL-Proofs: theory HOL.Ctr_Sugar

15:46:53 HOL-Proofs: theory HOL.Orderings

15:46:54 HOL: theory HOL.Groups

15:46:55 HOL: theory HOL.SAT

15:46:56 HOL-Proofs: theory HOL.SAT

15:46:56 HOL-Proofs: theory HOL.Groups

15:46:57 HOL: theory HOL.Lattices

15:46:59 HOL-Proofs: theory HOL.Lattices

15:46:59 HOL: theory HOL.Set

15:47:01 HOL: theory HOL.Fun

15:47:01 HOL: theory HOL.Typedef

15:47:01 HOL: theory HOL.Complete_Lattices

15:47:01 HOL: theory HOL.Rings

15:47:03 HOL-Proofs: theory HOL.Set

15:47:04 HOL: theory HOL.Inductive

15:47:06 HOL: theory HOL.Product_Type

15:47:06 HOL: theory HOL.Sum_Type

15:47:07 HOL-Proofs: theory HOL.Fun

15:47:07 HOL-Proofs: theory HOL.Typedef

15:47:08 HOL: theory HOL.Complete_Partial_Order

15:47:09 HOL-Proofs: theory HOL.Complete_Lattices

15:47:09 HOL-Proofs: theory HOL.Rings

15:47:13 HOL: theory HOL.Nat

15:47:14 HOL-Proofs: theory HOL.Inductive

15:47:15 HOL: theory HOL.Fields

15:47:15 HOL: theory HOL.Meson

15:47:16 HOL: theory HOL.ATP

15:47:17 HOL-Proofs: theory HOL.Product_Type

15:47:17 HOL-Proofs: theory HOL.Sum_Type

15:47:19 HOL: theory HOL.Metis

15:47:19 HOL-Proofs: theory HOL.Complete_Partial_Order

15:47:20 HOL: theory HOL.Finite_Set

15:47:22 HOL: theory HOL.Relation

15:47:23 HOL: theory HOL.Transitive_Closure

15:47:24 HOL: theory HOL.Wellfounded

15:47:25 HOL: theory HOL.Fun_Def_Base

15:47:25 HOL: theory HOL.Hilbert_Choice

15:47:25 HOL-Proofs: theory HOL.Nat

15:47:25 HOL: theory HOL.Wfrec

15:47:25 HOL: theory HOL.Order_Relation

15:47:25 HOL: theory HOL.BNF_Wellorder_Relation

15:47:26 HOL: theory HOL.BNF_Wellorder_Embedding

15:47:26 HOL: theory HOL.Zorn

15:47:26 HOL: theory HOL.BNF_Wellorder_Constructions

15:47:27 HOL: theory HOL.BNF_Cardinal_Order_Relation

15:47:27 HOL: theory HOL.BNF_Cardinal_Arithmetic

15:47:28 HOL: theory HOL.BNF_Def

15:47:29 HOL-Proofs: theory HOL.Fields

15:47:29 HOL-Proofs: theory HOL.Meson

15:47:30 HOL-Proofs: theory HOL.ATP

15:47:31 HOL: theory HOL.BNF_Composition

15:47:31 HOL: theory HOL.Basic_BNFs

15:47:32 HOL: theory HOL.BNF_Fixpoint_Base

15:47:33 HOL-Proofs: theory HOL.Metis

15:47:36 HOL: theory HOL.BNF_Least_Fixpoint

15:47:37 HOL-Proofs: theory HOL.Finite_Set

15:47:40 HOL: theory HOL.Basic_BNF_LFPs

15:47:40 HOL: theory HOL.Transfer

15:47:41 HOL: theory HOL.Num

15:47:44 HOL: theory HOL.Power

15:47:46 HOL: theory HOL.Groups_Big

15:47:49 HOL: theory HOL.Equiv_Relations

15:47:49 HOL: theory HOL.Lifting

15:47:50 HOL-Proofs: theory HOL.Relation

15:47:51 HOL: theory HOL.Lifting_Set

15:47:51 HOL: theory HOL.Option

15:47:51 HOL: theory HOL.Quotient

15:47:52 HOL: theory HOL.Extraction

15:47:52 HOL: theory HOL.Lattices_Big

15:47:52 HOL: theory HOL.Partial_Function

15:47:52 HOL-Proofs: theory HOL.Transitive_Closure

15:47:53 HOL: theory HOL.Fun_Def

15:47:54 HOL: theory HOL.Int

15:47:57 HOL-Proofs: theory HOL.Wellfounded

15:47:58 HOL: theory HOL.Euclidean_Division

15:47:59 HOL-Proofs: theory HOL.Fun_Def_Base

15:47:59 HOL-Proofs: theory HOL.Hilbert_Choice

15:47:59 HOL-Proofs: theory HOL.Wfrec

15:47:59 HOL-Proofs: theory HOL.Order_Relation

15:48:01 HOL-Proofs: theory HOL.BNF_Wellorder_Relation

15:48:03 HOL-Proofs: theory HOL.BNF_Wellorder_Embedding

15:48:03 HOL-Proofs: theory HOL.Zorn

15:48:04 HOL: theory HOL.Parity

15:48:05 HOL-Proofs: theory HOL.BNF_Wellorder_Constructions

15:48:09 HOL: theory HOL.Divides

15:48:10 HOL-Proofs: theory HOL.BNF_Cardinal_Order_Relation

15:48:12 HOL: theory HOL.Code_Numeral

15:48:12 HOL: theory HOL.Numeral_Simprocs

15:48:12 HOL: theory HOL.SMT

15:48:12 HOL: theory HOL.Set_Interval

15:48:13 HOL: theory HOL.Semiring_Normalization

15:48:15 HOL-Proofs: theory HOL.BNF_Cardinal_Arithmetic

15:48:16 HOL: theory HOL.Groebner_Basis

15:48:17 HOL-Proofs: theory HOL.BNF_Def

15:48:17 HOL: theory HOL.Conditionally_Complete_Lattices

15:48:17 HOL: theory HOL.Filter

15:48:18 HOL: theory HOL.Presburger

15:48:20 HOL-Proofs: theory HOL.BNF_Composition

15:48:20 HOL-Proofs: theory HOL.Basic_BNFs

15:48:21 HOL: theory HOL.Sledgehammer

15:48:21 HOL-Proofs: theory HOL.BNF_Fixpoint_Base

15:48:23 HOL: theory HOL.List

15:48:25 HOL-Proofs: theory HOL.BNF_Least_Fixpoint

15:48:30 HOL-Proofs: theory HOL.Basic_BNF_LFPs

15:48:30 HOL-Proofs: theory HOL.Transfer

15:48:31 HOL: theory HOL.Groups_List

15:48:31 HOL: theory HOL.Map

15:48:32 HOL-Proofs: theory HOL.Num

15:48:32 HOL: theory HOL.Factorial

15:48:33 HOL: theory HOL.GCD

15:48:33 HOL: theory HOL.Enum

15:48:34 HOL: theory HOL.Binomial

15:48:34 HOL: theory HOL.Random

15:48:36 HOL-Proofs: theory HOL.Power

15:48:36 HOL: theory HOL.String

15:48:38 HOL: theory HOL.BNF_Greatest_Fixpoint

15:48:38 HOL: theory HOL.Predicate

15:48:38 HOL: theory HOL.Typerep

15:48:39 HOL: theory HOL.Lazy_Sequence

15:48:40 HOL: theory HOL.Limited_Sequence

15:48:40 HOL-Proofs: theory HOL.Groups_Big

15:48:40 HOL: theory HOL.Code_Evaluation

15:48:41 HOL: theory HOL.Quickcheck_Random

15:48:43 HOL: theory HOL.Quickcheck_Exhaustive

15:48:43 HOL: theory HOL.Quickcheck_Narrowing

15:48:44 HOL: theory HOL.Random_Pred

15:48:44 HOL: theory HOL.Random_Sequence

15:48:47 HOL: theory HOL.Record

15:48:47 HOL: theory HOL.Predicate_Compile

15:48:48 HOL-Proofs: theory HOL.Equiv_Relations

15:48:49 HOL: theory HOL.Nitpick

15:48:50 HOL-Proofs: theory HOL.Lifting

15:48:53 HOL-Proofs: theory HOL.Lifting_Set

15:48:53 HOL-Proofs: theory HOL.Option

15:48:53 HOL-Proofs: theory HOL.Quotient

15:48:55 HOL-Proofs: theory HOL.Extraction

15:48:55 HOL-Proofs: theory HOL.Lattices_Big

15:48:55 HOL-Proofs: theory HOL.Partial_Function

15:48:56 HOL: theory HOL.Nunchaku

15:48:57 HOL: theory Main

15:48:59 HOL-Proofs: theory HOL.Fun_Def

15:48:59 HOL: theory HOL.Archimedean_Field

15:48:59 HOL: theory HOL.Hull

15:48:59 HOL: theory HOL.Topological_Spaces

15:48:59 HOL: theory HOL.Modules

15:49:00 HOL: theory HOL.Vector_Spaces

15:49:01 HOL-Proofs: theory HOL.Int

15:49:06 HOL: theory HOL.Rat

15:49:08 HOL-Proofs: theory HOL.Euclidean_Division

15:49:08 HOL: theory HOL.Real

15:49:10 HOL: theory HOL.Real_Vector_Spaces

15:49:20 HOL-Proofs: theory HOL.Parity

15:49:26 HOL: theory HOL.Inequalities

15:49:26 HOL: theory HOL.Limits

15:49:27 HOL-Proofs: theory HOL.Divides

15:49:32 HOL: theory HOL.Deriv

15:49:33 HOL: theory HOL.Series

15:49:33 HOL-Proofs: theory HOL.Code_Numeral

15:49:33 HOL-Proofs: theory HOL.Numeral_Simprocs

15:49:33 HOL-Proofs: theory HOL.SMT

15:49:33 HOL-Proofs: theory HOL.Set_Interval

15:49:34 HOL: theory HOL.NthRoot

15:49:35 HOL: theory HOL.Transcendental

15:49:40 HOL: theory HOL.Complex

15:49:40 HOL: theory HOL.MacLaurin

15:49:41 HOL: theory Complex_Main

15:49:47 HOL-Proofs: theory HOL.Semiring_Normalization

15:49:49 HOL-Proofs: theory HOL.Conditionally_Complete_Lattices

15:49:49 HOL-Proofs: theory HOL.Filter

15:49:52 HOL-Proofs: theory HOL.Groebner_Basis

15:49:54 HOL-Proofs: theory HOL.Presburger

15:50:07 HOL-Proofs: theory HOL.Sledgehammer

15:50:09 Timing HOL (4 threads, 192.863s elapsed time, 589.516s cpu time, 38.540s GC time, factor 3.06)

15:50:09 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL

15:50:09 HOL FAILED

15:50:09 (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64_32-linux/log/HOL)

15:50:09 ### closed (\<Inter> (?B ` ?A))

15:50:09 ### Rule already declared as introduction (intro)

15:50:09 ### \<forall>S\<in>?K. closed S \<Longrightarrow> closed (\<Inter> ?K)

15:50:09 ### Rule already declared as introduction (intro)

15:50:09 ### \<lbrakk>finite ?S; \<forall>T\<in>?S. closed T\<rbrakk>

15:50:09 ### \<Longrightarrow> closed (\<Union> ?S)

15:50:09 ### Rule already declared as introduction (intro)

15:50:09 ### \<lbrakk>finite ?A; \<forall>x\<in>?A. closed (?B x)\<rbrakk>

15:50:09 ### \<Longrightarrow> closed (\<Union> (?B ` ?A))

15:50:09 ### Rule already declared as introduction (intro)

15:50:09 ### \<lbrakk>open ?S; closed ?T\<rbrakk> \<Longrightarrow> open (?S - ?T)

15:50:09 ### Rule already declared as introduction (intro)

15:50:09 ### \<lbrakk>closed ?S; open ?T\<rbrakk> \<Longrightarrow> closed (?S - ?T)

15:50:09 ### Rule already declared as introduction (intro)

15:50:09 ### closed ?S \<Longrightarrow> open (- ?S)

15:50:09 ### Rule already declared as introduction (intro)

15:50:09 ### open ?S \<Longrightarrow> closed (- ?S)

15:50:09 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL/outline -o pdf -n outline -t /proof,/ML

15:50:09 isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL/document -o pdf -n document

15:50:09 *** Latex error (line 86 of "~~/src/HOL/Fields.thy"):

15:50:09 *** Missing $ inserted.

15:50:09 *** <inserted text>

15:50:09 *** $

15:50:09 *** }

15:50:09 *** Latex error (line 86 of "~~/src/HOL/Fields.thy"):

15:50:09 *** Extra }, or forgotten $.

15:50:09 *** \isamarkupcmt #1->{\isastylecmt --- #1}

15:50:09 ***

15:50:09 *** }

15:50:09 *** Latex error (line 86 of "~~/src/HOL/Fields.thy"):

15:50:09 *** Missing $ inserted.

15:50:09 *** <inserted text>

15:50:09 *** $

15:50:09 *** \isanewline

15:50:09 *** Latex error (line 1333 of "~~/src/HOL/Fields.thy"):

15:50:09 *** Missing } inserted.

15:50:09 *** <inserted text>

15:50:09 *** }

15:50:09 *** \end{isabellebody}

15:50:09 *** Failed to build document in "/media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL/document"

15:50:09 HOL-Analysis CANCELLED

15:50:09 Ordinary_Differential_Equations CANCELLED

15:50:09 HOL-ODE-Numerics CANCELLED

15:50:09 Lorenz_Approximation CANCELLED

15:50:09 Lorenz_C0 CANCELLED

15:50:09 Automatic_Refinement CANCELLED

15:50:09 HOL-Library CANCELLED

15:50:09 Refine_Monadic CANCELLED

15:50:09 Collections CANCELLED

15:50:09 HOL-Computational_Algebra CANCELLED

15:50:09 HOL-Algebra CANCELLED

15:50:09 CAVA_Base CANCELLED

15:50:09 CAVA_Automata CANCELLED

15:50:09 CAVA_Setup CANCELLED

15:50:09 JNF-AFP-Lib CANCELLED

15:50:09 HOL-Word CANCELLED

15:50:09 Word_Lib CANCELLED

15:50:09 Jordan_Normal_Form CANCELLED

15:50:09 IP_Addresses CANCELLED

15:50:09 Simple_Firewall CANCELLED

15:50:09 Routing CANCELLED

15:50:09 Category3 CANCELLED

15:50:09 Iptables_Semantics CANCELLED

15:50:10 Subresultants CANCELLED

15:50:10 HOL-ODE-ARCH-COMP CANCELLED

15:50:10 Pre_BZ CANCELLED

15:50:10 HOL-ODE-Examples CANCELLED

15:50:10 HereditarilyFinite CANCELLED

15:50:10 Incompleteness CANCELLED

15:50:10 Native_Word CANCELLED

15:50:10 Jinja CANCELLED

15:50:10 HOL-Number_Theory CANCELLED

15:50:10 MSO_Regex_Equivalence CANCELLED

15:50:10 Iptables_Semantics_Examples CANCELLED

15:50:10 Berlekamp_Zassenhaus CANCELLED

15:50:10 HOL-Probability CANCELLED

15:50:10 CAVA_LTL_Modelchecker CANCELLED

15:50:10 HOL-Codegenerator_Test CANCELLED

15:50:10 HOL-Nominal CANCELLED

15:50:10 Groebner_Bases CANCELLED

15:50:10 HOL-Nominal-Examples CANCELLED

15:50:10 HOL-ex CANCELLED

15:50:10 HOL-Decision_Procs CANCELLED

15:50:10 Echelon_Form CANCELLED

15:50:10 LEM CANCELLED

15:50:10 Sepref_Prereq CANCELLED

15:50:10 Affine_Arithmetic CANCELLED

15:50:10 Algebraic_Numbers CANCELLED

15:50:10 CakeML CANCELLED

15:50:10 Formal_SSA CANCELLED

15:50:10 Sepref_Basic CANCELLED

15:50:10 HRB-Slicing CANCELLED

15:50:10 Markov_Models CANCELLED

15:50:10 HOL-Data_Structures CANCELLED

15:50:10 Sepref_IICF CANCELLED

15:50:10 Auto2_HOL CANCELLED

15:50:10 Psi_Calculi CANCELLED

15:50:10 Slicing CANCELLED

15:50:10 MonoidalCategory CANCELLED

15:50:10 Dirichlet_Series CANCELLED

15:50:10 Security_Protocol_Refinement CANCELLED

15:50:10 SM_Base CANCELLED

15:50:10 Deriving CANCELLED

15:50:10 Auto2_Imperative_HOL CANCELLED

15:50:10 Kleene_Algebra CANCELLED

15:50:10 Transition_Systems_and_Automata CANCELLED

15:50:10 Stone_Algebras CANCELLED

15:50:10 Formula_Derivatives CANCELLED

15:50:10 Probabilistic_While CANCELLED

15:50:10 Network_Security_Policy_Verification CANCELLED

15:50:10 Flow_Networks CANCELLED

15:50:10 KAT_and_DRA CANCELLED

15:50:10 Containers CANCELLED

15:50:10 HOLCF CANCELLED

15:50:10 Stochastic_Matrices CANCELLED

15:50:10 CryptHOL CANCELLED

15:50:10 HOL-CSP CANCELLED

15:50:10 Refine_Imperative_HOL CANCELLED

15:50:10 Proof_Strategy_Language CANCELLED

15:50:10 Stone_Relation_Algebras CANCELLED

15:50:10 Core_DOM CANCELLED

15:50:10 Algebraic_VCs CANCELLED

15:50:10 Linear_Recurrences_Solver CANCELLED

15:50:10 Complx CANCELLED

15:50:10 LLL_Basis_Reduction CANCELLED

15:50:10 Key_Agreement_Strong_Adversaries CANCELLED

15:50:10 Probabilistic_Prime_Tests CANCELLED

15:50:10 Differential_Dynamic_Logic CANCELLED

15:50:10 Dependent_SIFUM_Type_Systems CANCELLED

15:50:10 HOL-Corec_Examples CANCELLED

15:50:10 SPARCv8 CANCELLED

15:50:10 Perron_Frobenius CANCELLED

15:50:10 Transcendence_Series_Hancl_Rucki CANCELLED

15:50:10 Universal_Turing_Machine CANCELLED

15:50:10 No_FTL_observers CANCELLED

15:50:10 Group-Ring-Module CANCELLED

15:50:10 Count_Complex_Roots CANCELLED

15:50:10 Simpl CANCELLED

15:50:10 Promela CANCELLED

15:50:10 Probabilistic_Timed_Automata CANCELLED

15:50:10 Datatype_Order_Generator CANCELLED

15:50:10 Isabelle_Meta_Model CANCELLED

15:50:10 Stone_Kleene_Relation_Algebras CANCELLED

15:50:10 SM CANCELLED

15:50:10 QR_Decomposition CANCELLED

15:50:10 CoreC++ CANCELLED

15:50:10 HOL-Nitpick_Examples CANCELLED

15:50:10 Game_Based_Crypto CANCELLED

15:50:10 Simplex CANCELLED

15:50:10 KAD CANCELLED

15:50:10 Deep_Learning CANCELLED

15:50:10 LTL_to_GBA CANCELLED

15:50:10 Nominal2 CANCELLED

15:50:10 E_Transcendental CANCELLED

15:50:10 Abstract-Rewriting CANCELLED

15:50:10 Prpu_Maxflow CANCELLED

15:50:10 HOL-Auth CANCELLED

15:50:10 DFS_Framework CANCELLED

15:50:10 Timed_Automata CANCELLED

15:50:10 LOFT CANCELLED

15:50:10 Containers-Benchmarks CANCELLED

15:50:10 Safe_OCL CANCELLED

15:50:10 Collections_Examples CANCELLED

15:50:10 Featherweight_OCL CANCELLED

15:50:10 Modal_Logics_for_NTS CANCELLED

15:50:10 Multi_Party_Computation CANCELLED

15:50:10 Monad_Memo_DP CANCELLED

15:50:10 Order_Lattice_Props CANCELLED

15:50:10 LTL CANCELLED

15:50:10 Allen_Calculus CANCELLED

15:50:10 Datatypes CANCELLED

15:50:10 Polynomials CANCELLED

15:50:10 Zeta_Function CANCELLED

15:50:10 Store_Buffer_Reduction CANCELLED

15:50:10 KBPs CANCELLED

15:50:10 Coinductive CANCELLED

15:50:10 Gabow_SCC CANCELLED

15:50:10 Constructive_Cryptography CANCELLED

15:50:10 Dependent_SIFUM_Refinement CANCELLED

15:50:10 HOL-Quickcheck_Examples CANCELLED

15:50:10 HOL-Homology CANCELLED

15:50:10 Density_Compiler CANCELLED

15:50:10 Ordinal CANCELLED

15:50:10 Gromov_Hyperbolicity CANCELLED

15:50:10 InfPathElimination CANCELLED

15:50:10 Functional_Ordered_Resolution_Prover CANCELLED

15:50:10 Planarity_Certificates CANCELLED

15:50:10 Stable_Matching CANCELLED

15:50:10 Taylor_Models CANCELLED

15:50:10 Nested_Multisets_Ordinals CANCELLED

15:50:10 Flyspeck-Tame CANCELLED

15:50:10 HOL-Datatype_Examples CANCELLED

15:50:10 HOL-Cardinals CANCELLED

15:50:10 PseudoHoops CANCELLED

15:50:10 HOL-Hoare_Parallel CANCELLED

15:50:10 UPF CANCELLED

15:50:10 Hermite CANCELLED

15:50:10 Rep_Fin_Groups CANCELLED

15:50:10 Matrix CANCELLED

15:50:10 Launchbury CANCELLED

15:50:10 IMP2 CANCELLED

15:50:10 Paraconsistency CANCELLED

15:50:10 Resolution_FOL CANCELLED

15:50:10 WebAssembly CANCELLED

15:50:10 Binding_Syntax_Theory CANCELLED

15:50:10 Hoare_Time CANCELLED

15:50:10 Quantales CANCELLED

15:50:10 Vickrey_Clarke_Groves CANCELLED

15:50:10 HOL-IMP CANCELLED

15:50:10 HOL-MicroJava CANCELLED

15:50:10 EdmondsKarp_Maxflow CANCELLED

15:50:10 Aggregation_Algebras CANCELLED

15:50:10 HOL-Bali CANCELLED

15:50:10 Regular_Algebras CANCELLED

15:50:10 Winding_Number_Eval CANCELLED

15:50:10 Separation_Logic_Imperative_HOL CANCELLED

15:50:10 LTL_to_DRA CANCELLED

15:50:10 Abortable_Linearizable_Modules CANCELLED

15:50:10 Multirelations CANCELLED

15:50:10 List_Update CANCELLED

15:50:10 Buildings CANCELLED

15:50:10 UPF_Firewall CANCELLED

15:50:10 Prime_Harmonic_Series CANCELLED

15:50:10 List-Infinite CANCELLED

15:50:10 Signature_Groebner CANCELLED

15:50:10 Factored_Transition_System_Bounding CANCELLED

15:50:10 HOL-Word-SMT_Examples CANCELLED

15:50:10 Linear_Recurrences CANCELLED

15:50:10 Propositional_Proof_Systems CANCELLED

15:50:10 Matrix_Tensor CANCELLED

15:50:10 Password_Authentication_Protocol CANCELLED

15:50:10 Ergodic_Theory CANCELLED

15:50:10 Gauss_Jordan CANCELLED

15:50:10 Dijkstra_Shortest_Path CANCELLED

15:50:10 Green CANCELLED

15:50:10 BytecodeLogicJmlTypes CANCELLED

15:50:10 Dirichlet_L CANCELLED

15:50:10 HOL-Real_Asymp CANCELLED

15:50:10 Akra_Bazzi CANCELLED

15:50:10 Girth_Chromatic CANCELLED

15:50:10 Farkas CANCELLED

15:50:10 Sturm_Sequences CANCELLED

15:50:10 Hidden_Markov_Models CANCELLED

15:50:10 MFMC_Countable CANCELLED

15:50:10 Corec CANCELLED

15:50:10 Applicative_Lifting CANCELLED

15:50:10 Probabilistic_Noninterference CANCELLED

15:50:10 Abs_Int_ITP2012 CANCELLED

15:50:10 DiscretePricing CANCELLED

15:50:10 Pi_Transcendental CANCELLED

15:50:10 Cauchy CANCELLED

15:50:10 Free-Groups CANCELLED

15:50:10 Root_Balanced_Tree CANCELLED

15:50:10 Nat-Interval-Logic CANCELLED

15:50:10 Splay_Tree CANCELLED

15:50:10 Lambda_Free_KBOs CANCELLED

15:50:10 Sqrt_Babylonian CANCELLED

15:50:10 AWN CANCELLED

15:50:10 Parity_Game CANCELLED

15:50:10 LambdaAuth CANCELLED

15:50:10 HOL-Predicate_Compile_Examples CANCELLED

15:50:10 ComponentDependencies CANCELLED

15:50:10 Irrationality_J_Hancl CANCELLED

15:50:10 Regular-Sets CANCELLED

15:50:10 Symmetric_Polynomials CANCELLED

15:50:10 HOL-Imperative_HOL CANCELLED

15:50:10 LTL_Master_Theorem CANCELLED

15:50:10 Codegen CANCELLED

15:50:10 QHLProver CANCELLED

15:50:10 Sort_Encodings CANCELLED

15:50:10 Amortized_Complexity CANCELLED

15:50:10 LocalLexing CANCELLED

15:50:10 Real_Impl CANCELLED

15:50:10 Twelvefold_Way CANCELLED

15:50:10 UTP-Toolkit CANCELLED

15:50:10 LLL_Factorization CANCELLED

15:50:10 Polynomial_Factorization CANCELLED

15:50:10 Regex_Equivalence CANCELLED

15:50:10 Elliptic_Curves_Group_Law CANCELLED

15:50:10 Tree-Automata CANCELLED

15:50:10 Encodability_Process_Calculi CANCELLED

15:50:10 SATSolverVerification CANCELLED

15:50:10 Relation_Algebra CANCELLED

15:50:10 SIFUM_Type_Systems CANCELLED

15:50:10 Randomised_Social_Choice CANCELLED

15:50:10 Pi_Calculus CANCELLED

15:50:10 Generic_Deriving CANCELLED

15:50:10 HOLCF-Library CANCELLED

15:50:10 Higher_Order_Terms CANCELLED

15:50:10 LightweightJava CANCELLED

15:50:10 Stern_Brocot CANCELLED

15:50:10 BDD CANCELLED

15:50:10 Call_Arity CANCELLED

15:50:10 VerifyThis2018 CANCELLED

15:50:10 AutoFocus-Stream CANCELLED

15:50:10 HOL-SET_Protocol CANCELLED

15:50:10 Knot_Theory CANCELLED

15:50:10 Partial_Order_Reduction CANCELLED

15:50:10 Statecharts CANCELLED

15:50:10 Smooth_Manifolds CANCELLED

15:50:10 Dict_Construction CANCELLED

15:50:10 Bertrands_Postulate CANCELLED

15:50:10 Buchi_Complementation CANCELLED

15:50:10 Probabilistic_System_Zoo CANCELLED

15:50:10 Treaps CANCELLED

15:50:10 Ordered_Resolution_Prover CANCELLED

15:50:10 Hybrid_Multi_Lane_Spatial_Logic CANCELLED

15:50:10 HOL-Quotient_Examples CANCELLED

15:50:10 LinearQuantifierElim CANCELLED

15:50:10 PCF CANCELLED

15:50:10 Koenigsberg_Friendship CANCELLED

15:50:10 Prime_Distribution_Elementary CANCELLED

15:50:10 HOLCF-Prelude CANCELLED

15:50:10 SDS_Impossibility CANCELLED

15:50:10 SequentInvertibility CANCELLED

15:50:10 Probabilistic_System_Zoo-Non_BNFs CANCELLED

15:50:10 Concurrent_Revisions CANCELLED

15:50:10 DynamicArchitectures CANCELLED

15:50:10 HOL-UNITY CANCELLED

15:50:10 Circus CANCELLED

15:50:10 Monomorphic_Monad CANCELLED

15:50:10 Graph_Theory CANCELLED

15:50:10 UTP CANCELLED

15:50:10 Valuation CANCELLED

15:50:10 SIFPL CANCELLED

15:50:10 Possibilistic_Noninterference CANCELLED

15:50:10 CRDT CANCELLED

15:50:10 Special_Function_Bounds CANCELLED

15:50:10 Residuated_Lattices CANCELLED

15:50:10 Noninterference_CSP CANCELLED

15:50:10 VectorSpace CANCELLED

15:50:10 Quick_Sort_Cost CANCELLED

15:50:10 Tarskis_Geometry CANCELLED

15:50:10 SuperCalc CANCELLED

15:50:10 GewirthPGCProof CANCELLED

15:50:10 Incredible_Proof_Machine CANCELLED

15:50:10 UpDown_Scheme CANCELLED

15:50:10 Kruskal CANCELLED

15:50:10 Prime_Number_Theorem CANCELLED

15:50:10 Stirling_Formula CANCELLED

15:50:10 Formula_Derivatives-Examples CANCELLED

15:50:10 Localization_Ring CANCELLED

15:50:10 Decl_Sem_Fun_PL CANCELLED

15:50:10 DiskPaxos CANCELLED

15:50:10 Graph_Saturation CANCELLED

15:50:10 Noninterference_Ipurge_Unwinding CANCELLED

15:50:10 Locally-Nameless-Sigma CANCELLED

15:50:10 Rewriting_Z CANCELLED

15:50:10 Architectural_Design_Patterns CANCELLED

15:50:10 Consensus_Refined CANCELLED

15:50:10 Heard_Of CANCELLED

15:50:10 Myhill-Nerode CANCELLED

15:50:10 Median_Of_Medians_Selection CANCELLED

15:50:10 ROBDD CANCELLED

15:50:10 PLM CANCELLED

15:50:10 Lp CANCELLED

15:50:10 HOL-Hoare CANCELLED

15:50:10 IEEE_Floating_Point CANCELLED

15:50:10 WHATandWHERE_Security CANCELLED

15:50:10 HOL-Metis_Examples CANCELLED

15:50:10 HOL-Analysis-ex CANCELLED

15:50:10 Quaternions CANCELLED

15:50:10 Presburger-Automata CANCELLED

15:50:10 Trie CANCELLED

15:50:10 Projective_Geometry CANCELLED

15:50:10 Well_Quasi_Orders CANCELLED

15:50:10 Shivers-CFA CANCELLED

15:50:10 Modular_Assembly_Kit_Security CANCELLED

15:50:10 pGCL CANCELLED

15:50:10 Noninterference_Sequential_Composition CANCELLED

15:50:10 Abstract_Completeness CANCELLED

15:50:10 ConcurrentIMP CANCELLED

15:50:10 Lambda_Free_EPO CANCELLED

15:50:10 NormByEval CANCELLED

15:50:10 Noninterference_Generic_Unwinding CANCELLED

15:50:10 Fishburn_Impossibility CANCELLED

15:50:10 Priority_Queue_Braun CANCELLED

15:50:10 Show CANCELLED

15:50:10 Tutorial CANCELLED

15:50:10 HOL-Statespace CANCELLED

15:50:10 Budan_Fourier CANCELLED

15:50:10 XML CANCELLED

15:50:10 AxiomaticCategoryTheory CANCELLED

15:50:10 HOL-SPARK CANCELLED

15:50:10 Diophantine_Eqns_Lin_Hom CANCELLED

15:50:10 PSemigroupsConvolution CANCELLED

15:50:10 HOL-Eisbach CANCELLED

15:50:10 FocusStreamsCaseStudies CANCELLED

15:50:10 Kuratowski_Closure_Complement CANCELLED

15:50:10 Octonions CANCELLED

15:50:10 FOL_Harrison CANCELLED

15:50:10 IOA CANCELLED

15:50:10 Program-Conflict-Analysis CANCELLED

15:50:10 InformationFlowSlicing_Inter CANCELLED

15:50:10 IMAP-CRDT CANCELLED

15:50:10 Knuth_Morris_Pratt CANCELLED

15:50:10 FOL-Fitting CANCELLED

15:50:10 PropResPI CANCELLED

15:50:10 Isar_Ref CANCELLED

15:50:10 GraphMarkingIBP CANCELLED

15:50:10 Boolean_Expression_Checkers CANCELLED

15:50:10 Finger-Trees CANCELLED

15:50:10 Euler_MacLaurin CANCELLED

15:50:10 Pell CANCELLED

15:50:10 HOL-SPARK-Examples CANCELLED

15:50:10 SenSocialChoice CANCELLED

15:50:10 OpSets CANCELLED

15:50:10 Types_Tableaus_and_Goedels_God CANCELLED

15:50:10 Probabilistic_System_Zoo-BNFs CANCELLED

15:50:10 Finite_Automata_HF CANCELLED

15:50:10 Binomial-Heaps CANCELLED

15:50:10 Random_BSTs CANCELLED

15:50:10 FLP CANCELLED

15:50:10 CCS CANCELLED

15:50:10 Posix-Lexing CANCELLED

15:50:10 HOL-Proofs: theory HOL.List

15:50:10 Ribbon_Proofs CANCELLED

15:50:10 RSAPSS CANCELLED

15:50:10 Decreasing-Diagrams-II CANCELLED

15:50:10 Optics CANCELLED

15:50:10 POPLmark-deBruijn CANCELLED

15:50:10 Polynomial_Interpolation CANCELLED

15:50:10 Sturm_Tarski CANCELLED

15:50:10 Functional-Automata CANCELLED

15:50:10 BNF_CC CANCELLED

15:50:10 Coinductive_Languages CANCELLED

15:50:10 HOL-Types_To_Sets CANCELLED

15:50:10 Weight_Balanced_Trees CANCELLED

15:50:10 Floyd_Warshall CANCELLED

15:50:10 HOLCF-Tutorial CANCELLED

15:50:10 FunWithTilings CANCELLED

15:50:10 Transitive-Closure-II CANCELLED

15:50:10 Separation_Algebra CANCELLED

15:50:10 Minsky_Machines CANCELLED

15:50:10 Name_Carrying_Type_Inference CANCELLED

15:50:10 Decreasing-Diagrams CANCELLED

15:50:10 CISC-Kernel CANCELLED

15:50:10 KD_Tree CANCELLED

15:50:10 Inductive_Confidentiality CANCELLED

15:50:10 Abstract_Soundness CANCELLED

15:50:10 Stream_Fusion_Code CANCELLED

15:50:10 List_Inversions CANCELLED

15:50:10 HOL-Nonstandard_Analysis CANCELLED

15:50:10 Cayley_Hamilton CANCELLED

15:50:10 Completeness CANCELLED

15:50:10 Derangements CANCELLED

15:50:10 Old_Datatype_Show CANCELLED

15:50:10 Lowe_Ontological_Argument CANCELLED

15:50:10 HOL-Mirabelle CANCELLED

15:50:10 Neumann_Morgenstern_Utility CANCELLED

15:50:10 Optimal_BST CANCELLED

15:50:10 Constructor_Funs CANCELLED

15:50:10 Catalan_Numbers CANCELLED

15:50:10 Pratt_Certificate CANCELLED

15:50:10 HOL-Mirabelle-ex CANCELLED

15:50:10 HOL-TLA CANCELLED

15:50:10 Category2 CANCELLED

15:50:10 AVL-Trees CANCELLED

15:50:10 Error_Function CANCELLED

15:50:10 HOL-Induct CANCELLED

15:50:10 Bell_Numbers_Spivey CANCELLED

15:50:10 TLA CANCELLED

15:50:10 Jordan_Hoelder CANCELLED

15:50:10 Lambda_Free_RPOs CANCELLED

15:50:10 JiveDataStoreModel CANCELLED

15:50:10 Euler_Partition CANCELLED

15:50:10 CryptoBasedCompositionalProperties CANCELLED

15:50:10 BNF_Operations CANCELLED

15:50:10 HOL-TLA-Memory CANCELLED

15:50:10 Fermat3_4 CANCELLED

15:50:10 Recursion-Theory-I CANCELLED

15:50:10 Strong_Security CANCELLED

15:50:10 MiniML CANCELLED

15:50:10 Orbit_Stabiliser CANCELLED

15:50:10 HyperCTL CANCELLED

15:50:10 HOL-Probability-ex CANCELLED

15:50:10 Stream-Fusion CANCELLED

15:50:10 Randomised_BSTs CANCELLED

15:50:10 Lam-ml-Normalization CANCELLED

15:50:10 FeatherweightJava CANCELLED

15:50:10 Robbins-Conjecture CANCELLED

15:50:10 Efficient-Mergesort CANCELLED

15:50:10 Transformer_Semantics CANCELLED

15:50:10 Separata CANCELLED

15:50:10 RefinementReactive CANCELLED

15:50:10 Landau_Symbols CANCELLED

15:50:10 Huffman CANCELLED

15:50:10 MonoBoolTranAlgebra CANCELLED

15:50:10 Card_Multisets CANCELLED

15:50:10 HOL-Matrix_LP CANCELLED

15:50:10 GoedelGod CANCELLED

15:50:10 WorkerWrapper CANCELLED

15:50:10 Impossible_Geometry CANCELLED

15:50:10 VolpanoSmith CANCELLED

15:50:10 Noninterference_Concurrent_Composition CANCELLED

15:50:10 Bernoulli CANCELLED

15:50:10 Typeclass_Hierarchy CANCELLED

15:50:10 GPU_Kernel_PL CANCELLED

15:50:10 Random_Graph_Subgraph_Threshold CANCELLED

15:50:10 Integration CANCELLED

15:50:10 Abstract-Hoare-Logics CANCELLED

15:50:10 LambdaMu CANCELLED

15:50:10 Rank_Nullity_Theorem CANCELLED

15:50:10 First_Order_Terms CANCELLED

15:50:10 First_Welfare_Theorem CANCELLED

15:50:10 Selection_Heap_Sort CANCELLED

15:50:10 FileRefinement CANCELLED

15:50:10 Verified-Prover CANCELLED

15:50:10 Minimal_SSA CANCELLED

15:50:10 Tycon CANCELLED

15:50:10 FinFun CANCELLED

15:50:10 Pop_Refinement CANCELLED

15:50:10 Comparison_Sort_Lower_Bound CANCELLED

15:50:10 Noninterference_Inductive_Unwinding CANCELLED

15:50:10 InformationFlowSlicing CANCELLED

15:50:10 Menger CANCELLED

15:50:10 IOA-NTP CANCELLED

15:50:10 Concurrent_Ref_Alg CANCELLED

15:50:10 Card_Partitions CANCELLED

15:50:10 Partial_Function_MR CANCELLED

15:50:10 HOL-TPTP CANCELLED

15:50:10 Epistemic_Logic CANCELLED

15:50:10 HOLCF-IMP CANCELLED

15:50:10 HOL-Unix CANCELLED

15:50:10 Binomial-Queues CANCELLED

15:50:10 HOL-NanoJava CANCELLED

15:50:10 SumSquares CANCELLED

15:50:10 Latin_Square CANCELLED

15:50:10 Tree_Decomposition CANCELLED

15:50:10 ShortestPath CANCELLED

15:50:10 Ramsey-Infinite CANCELLED

15:50:10 IOA-ABP CANCELLED

15:50:10 Bounded_Deducibility_Security CANCELLED

15:50:10 Dynamic_Tables CANCELLED

15:50:10 Topology CANCELLED

15:50:10 Matroids CANCELLED

15:50:10 HotelKeyCards CANCELLED

15:50:10 Tail_Recursive_Functions CANCELLED

15:50:10 MuchAdoAboutTwo CANCELLED

15:50:10 Prog_Prove CANCELLED

15:50:10 Chord_Segments CANCELLED

15:50:10 Lower_Semicontinuous CANCELLED

15:50:10 HOL-IMPP CANCELLED

15:50:10 Stewart_Apollonius CANCELLED

15:50:10 Triangle CANCELLED

15:50:10 ArrowImpossibilityGS CANCELLED

15:50:10 Imperative_Insertion_Sort CANCELLED

15:50:10 Compiling-Exceptions-Correctly CANCELLED

15:50:10 Category CANCELLED

15:50:10 Certification_Monads CANCELLED

15:50:10 Buffons_Needle CANCELLED

15:50:10 Source_Coding_Theorem CANCELLED

15:50:10 Falling_Factorial_Sum CANCELLED

15:50:10 TortoiseHare CANCELLED

15:50:10 HOL-Hahn_Banach CANCELLED

15:50:10 Lazy_Case CANCELLED

15:50:10 DPT-SAT-Solver CANCELLED

15:50:10 HOL-Isar_Examples CANCELLED

15:50:10 Case_Labeling CANCELLED

15:50:10 Secondary_Sylow CANCELLED

15:50:10 CYK CANCELLED

15:50:10 HOL-SPARK-Manual CANCELLED

15:50:10 Pairing_Heap CANCELLED

15:50:10 HOLCF-FOCUS CANCELLED

15:50:10 LatticeProperties CANCELLED

15:50:10 Functions CANCELLED

15:50:10 HOLCF-ex CANCELLED

15:50:10 Transitive-Closure CANCELLED

15:50:10 DataRefinementIBP CANCELLED

15:50:10 Lifting_Definition_Option CANCELLED

15:50:10 Stuttering_Equivalence CANCELLED

15:50:10 Implementation CANCELLED

15:50:10 Fisher_Yates CANCELLED

15:50:10 HOL-ZF CANCELLED

15:50:10 Card_Number_Partitions CANCELLED

15:50:10 List_Interleaving CANCELLED

15:50:10 Mason_Stothers CANCELLED

15:50:10 Eisbach CANCELLED

15:50:10 HOL-IOA CANCELLED

15:50:10 Gauss-Jordan-Elim-Fun CANCELLED

15:50:10 BinarySearchTree CANCELLED

15:50:10 Surprise_Paradox CANCELLED

15:50:10 ClockSynchInst CANCELLED

15:50:10 GenClock CANCELLED

15:50:10 Discrete_Summation CANCELLED

15:50:10 HOL-Nonstandard_Analysis-Examples CANCELLED

15:50:10 Classes CANCELLED

15:50:10 HOL-Lattice CANCELLED

15:50:10 Descartes_Sign_Rule CANCELLED

15:50:10 List-Index CANCELLED

15:50:10 Lazy-Lists-II CANCELLED

15:50:10 HOL-TLA-Inc CANCELLED

15:50:10 Open_Induction CANCELLED

15:50:10 IOA-Storage CANCELLED

15:50:10 Marriage CANCELLED

15:50:10 Cartan_FP CANCELLED

15:50:10 Max-Card-Matching CANCELLED

15:50:10 Liouville_Numbers CANCELLED

15:50:10 Skew_Heap CANCELLED

15:50:10 RIPEMD-160-SPARK CANCELLED

15:50:10 Locales CANCELLED

15:50:10 Perfect-Number-Thm CANCELLED

15:50:10 AnselmGod CANCELLED

15:50:10 Ptolemys_Theorem CANCELLED

15:50:10 Minkowskis_Theorem CANCELLED

15:50:10 Main CANCELLED

15:50:10 CofGroups CANCELLED

15:50:10 Lehmer CANCELLED

15:50:10 Lorenz_C1 CANCELLED

15:50:10 FunWithFunctions CANCELLED

15:50:10 Monad_Normalisation CANCELLED

15:50:10 Free-Boolean-Algebra CANCELLED

15:50:10 HOL-Import CANCELLED

15:50:10 Sugar CANCELLED

15:50:10 FFT CANCELLED

15:50:10 Depth-First-Search CANCELLED

15:50:10 IOA-ex CANCELLED

15:50:10 HOL-Mutabelle CANCELLED

15:50:10 Roy_Floyd_Warshall CANCELLED

15:50:10 JEdit CANCELLED

15:50:10 Card_Equiv_Relations CANCELLED

15:50:10 Bondy CANCELLED

15:50:10 General-Triangle CANCELLED

15:50:10 HOL-Real_Asymp-Manual CANCELLED

15:50:10 HOL-TLA-Buffer CANCELLED

15:50:10 How_to_Prove_it CANCELLED

15:50:10 HOL-Prolog CANCELLED

15:50:10 Example-Submission CANCELLED

15:50:10 Ordinals_and_Cardinals CANCELLED

15:51:13 HOL-Proofs: theory HOL.Groups_List

15:51:13 HOL-Proofs: theory HOL.Map

15:51:16 HOL-Proofs: theory HOL.Factorial

15:51:16 HOL-Proofs: theory HOL.GCD

15:51:19 HOL-Proofs: theory HOL.Binomial

15:51:31 HOL-Proofs: theory HOL.Enum

15:51:36 HOL-Proofs: theory HOL.Random

15:52:05 HOL-Proofs: theory HOL.String

15:52:51 HOL-Proofs: theory HOL.BNF_Greatest_Fixpoint

15:52:52 HOL-Proofs: theory HOL.Predicate

15:52:55 HOL-Proofs: theory HOL.Lazy_Sequence

15:52:57 HOL-Proofs: theory HOL.Limited_Sequence

15:52:57 HOL-Proofs: theory HOL.Typerep

15:52:58 HOL-Proofs: theory HOL.Code_Evaluation

15:52:59 HOL-Proofs: theory HOL.Quickcheck_Random

15:53:01 HOL-Proofs: theory HOL.Quickcheck_Exhaustive

15:53:01 HOL-Proofs: theory HOL.Quickcheck_Narrowing

15:53:01 HOL-Proofs: theory HOL.Random_Pred

15:53:03 HOL-Proofs: theory HOL.Random_Sequence

15:53:06 HOL-Proofs: theory HOL.Record

15:53:06 HOL-Proofs: theory HOL.Predicate_Compile

15:53:08 HOL-Proofs: theory HOL.Nitpick

15:53:14 HOL-Proofs: theory HOL.Nunchaku

15:53:15 HOL-Proofs: theory Main

15:53:17 HOL-Proofs: theory HOL-Library.Realizers

15:56:58 Timing HOL-Proofs (4 threads, 562.336s elapsed time, 1273.340s cpu time, 117.648s GC time, factor 2.26)

15:56:58 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs

15:56:58 Finished HOL-Proofs (0:10:14 elapsed time, 0:22:50 cpu time, factor 2.23)

15:56:58 Running HOL-Proofs-Lambda ...

15:56:58 Running HOL-Proofs-Extraction ...

15:56:58 Running HOL-Proofs-ex ...

15:56:59 HOL-Proofs-ex: theory HOL-Proofs-ex.Hilbert_Classical

15:56:59 HOL-Proofs-ex: theory HOL-Proofs-ex.Proof_Terms

15:56:59 HOL-Proofs-ex: theory HOL-Isar_Examples.Drinker

15:56:59 HOL-Proofs-Lambda: theory HOL-Library.Code_Target_Int

15:56:59 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Commutation

15:56:59 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Lambda

15:56:59 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListOrder

15:56:59 HOL-Proofs-ex: theory HOL-Proofs-ex.XML_Data

15:56:59 HOL-Proofs-Extraction: theory HOL-Library.Cancellation

15:56:59 HOL-Proofs-Extraction: theory HOL-Library.Code_Abstract_Nat

15:56:59 HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Int

15:56:59 HOL-Proofs-Extraction: theory HOL-Library.Open_State_Syntax

15:57:00 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Warshall

15:57:00 HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Nat

15:57:00 HOL-Proofs-Extraction: theory HOL-Library.Multiset

15:57:00 Timing HOL-Proofs-ex (4 threads, 0.849s elapsed time, 1.832s cpu time, 0.000s GC time, factor 2.16)

15:57:00 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-ex

15:57:00 Finished HOL-Proofs-ex (0:00:01 elapsed time)

15:57:01 HOL-Proofs-Extraction: theory HOL-Library.Code_Target_Numeral

15:57:01 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman

15:57:01 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListApplication

15:57:01 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ParRed

15:57:02 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.LambdaType

15:57:02 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.ListBeta

15:57:03 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Higman_Extraction

15:57:03 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Util

15:57:03 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Pigeonhole

15:57:04 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Eta

15:57:04 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.InductTermi

15:57:04 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.NormalForm

15:57:04 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.StrongNorm

15:57:04 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.Standardization

15:57:04 HOL-Proofs-Lambda: theory HOL-Proofs-Lambda.WeakNorm

15:57:16 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.QuotRem

15:57:19 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Greatest_Common_Divisor

15:57:21 HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Factorial_Ring

15:57:36 HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Euclidean_Algorithm

15:57:46 HOL-Proofs-Extraction: theory HOL-Computational_Algebra.Primes

15:57:57 HOL-Proofs-Extraction: theory HOL-Proofs-Extraction.Euclid

15:58:32 Timing HOL-Proofs-Extraction (4 threads, 89.075s elapsed time, 188.452s cpu time, 8.760s GC time, factor 2.12)

15:58:32 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Extraction

15:58:32 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Extraction/document.pdf

15:58:32 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Extraction/outline.pdf

15:58:32 Finished HOL-Proofs-Extraction (0:01:33 elapsed time, 0:03:16 cpu time, factor 2.12)

15:58:50 Timing HOL-Proofs-Lambda (4 threads, 106.721s elapsed time, 136.516s cpu time, 4.844s GC time, factor 1.28)

15:58:50 Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Lambda

15:58:50 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Lambda/document.pdf

15:58:50 Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Proofs-Lambda/outline.pdf

15:58:50 Finished HOL-Proofs-Lambda (0:01:51 elapsed time, 0:02:26 cpu time, factor 1.31)

15:58:50 Unfinished session(s): AVL-Trees, AWN, Abortable_Linearizable_Modules, Abs_Int_ITP2012, Abstract-Hoare-Logics, Abstract-Rewriting, Abstract_Completeness, Abstract_Soundness, Affine_Arithmetic, Aggregation_Algebras, Akra_Bazzi, Algebraic_Numbers, Algebraic_VCs, Allen_Calculus, Amortized_Complexity, AnselmGod, Applicative_Lifting, Architectural_Design_Patterns, ArrowImpossibilityGS, Auto2_HOL, Auto2_Imperative_HOL, AutoFocus-Stream, Automatic_Refinement, AxiomaticCategoryTheory, BDD, BNF_CC, BNF_Operations, Bell_Numbers_Spivey, Berlekamp_Zassenhaus, Bernoulli, Bertrands_Postulate, BinarySearchTree, Binding_Syntax_Theory, Binomial-Heaps, Binomial-Queues, Bondy, Boolean_Expression_Checkers, Bounded_Deducibility_Security, Buchi_Complementation, Budan_Fourier, Buffons_Needle, Buildings, BytecodeLogicJmlTypes, CAVA_Automata, CAVA_Base, CAVA_LTL_Modelchecker, CAVA_Setup, CCS, CISC-Kernel, CRDT, CYK, CakeML, Call_Arity, Card_Equiv_Relations, Card_Multisets, Card_Number_Partitions, Card_Partitions, Cartan_FP, Case_Labeling, Catalan_Numbers, Category, Category2, Category3, Cauchy, Cayley_Hamilton, Certification_Monads, Chord_Segments, Circus, Classes, ClockSynchInst, Codegen, CofGroups, Coinductive, Coinductive_Languages, Collections, Collections_Examples, Comparison_Sort_Lower_Bound, Compiling-Exceptions-Correctly, Completeness, Complx, ComponentDependencies, ConcurrentIMP, Concurrent_Ref_Alg, Concurrent_Revisions, Consensus_Refined, Constructive_Cryptography, Constructor_Funs, Containers, Containers-Benchmarks, CoreC++, Core_DOM, Corec, Count_Complex_Roots, CryptHOL, CryptoBasedCompositionalProperties, DFS_Framework, DPT-SAT-Solver, DataRefinementIBP, Datatype_Order_Generator, Datatypes, Decl_Sem_Fun_PL, Decreasing-Diagrams, Decreasing-Diagrams-II, Deep_Learning, Density_Compiler, Dependent_SIFUM_Refinement, Dependent_SIFUM_Type_Systems, Depth-First-Search, Derangements, Deriving, Descartes_Sign_Rule, Dict_Construction, Differential_Dynamic_Logic, Dijkstra_Shortest_Path, Diophantine_Eqns_Lin_Hom, Dirichlet_L, Dirichlet_Series, DiscretePricing, Discrete_Summation, DiskPaxos, DynamicArchitectures, Dynamic_Tables, E_Transcendental, Echelon_Form, EdmondsKarp_Maxflow, Efficient-Mergesort, Eisbach, Elliptic_Curves_Group_Law, Encodability_Process_Calculi, Epistemic_Logic, Ergodic_Theory, Error_Function, Euler_MacLaurin, Euler_Partition, Example-Submission, FFT, FLP, FOL-Fitting, FOL_Harrison, Factored_Transition_System_Bounding, Falling_Factorial_Sum, Farkas, FeatherweightJava, Featherweight_OCL, Fermat3_4, FileRefinement, FinFun, Finger-Trees, Finite_Automata_HF, First_Order_Terms, First_Welfare_Theorem, Fishburn_Impossibility, Fisher_Yates, Flow_Networks, Floyd_Warshall, Flyspeck-Tame, FocusStreamsCaseStudies, Formal_SSA, Formula_Derivatives, Formula_Derivatives-Examples, Free-Boolean-Algebra, Free-Groups, FunWithFunctions, FunWithTilings, Functional-Automata, Functional_Ordered_Resolution_Prover, Functions, GPU_Kernel_PL, Gabow_SCC, Game_Based_Crypto, Gauss-Jordan-Elim-Fun, Gauss_Jordan, GenClock, General-Triangle, Generic_Deriving, GewirthPGCProof, Girth_Chromatic, GoedelGod, GraphMarkingIBP, Graph_Saturation, Graph_Theory, Green, Groebner_Bases, Gromov_Hyperbolicity, Group-Ring-Module, HOL, HOL-Algebra, HOL-Analysis, HOL-Analysis-ex, HOL-Auth, HOL-Bali, HOL-CSP, HOL-Cardinals, HOL-Codegenerator_Test, HOL-Computational_Algebra, HOL-Corec_Examples, HOL-Data_Structures, HOL-Datatype_Examples, HOL-Decision_Procs, HOL-Eisbach, HOL-Hahn_Banach, HOL-Hoare, HOL-Hoare_Parallel, HOL-Homology, HOL-IMP, HOL-IMPP, HOL-IOA, HOL-Imperative_HOL, HOL-Import, HOL-Induct, HOL-Isar_Examples, HOL-Lattice, HOL-Library, HOL-Matrix_LP, HOL-Metis_Examples, HOL-MicroJava, HOL-Mirabelle, HOL-Mirabelle-ex, HOL-Mutabelle, HOL-NanoJava, HOL-Nitpick_Examples, HOL-Nominal, HOL-Nominal-Examples, HOL-Nonstandard_Analysis, HOL-Nonstandard_Analysis-Examples, HOL-Number_Theory, HOL-ODE-ARCH-COMP, HOL-ODE-Examples, HOL-ODE-Numerics, HOL-Predicate_Compile_Examples, HOL-Probability, HOL-Probability-ex, HOL-Prolog, HOL-Quickcheck_Examples, HOL-Quotient_Examples, HOL-Real_Asymp, HOL-Real_Asymp-Manual, HOL-SET_Protocol, HOL-SPARK, HOL-SPARK-Examples, HOL-SPARK-Manual, HOL-Statespace, HOL-TLA, HOL-TLA-Buffer, HOL-TLA-Inc, HOL-TLA-Memory, HOL-TPTP, HOL-Types_To_Sets, HOL-UNITY, HOL-Unix, HOL-Word, HOL-Word-SMT_Examples, HOL-ZF, HOL-ex, HOLCF, HOLCF-FOCUS, HOLCF-IMP, HOLCF-Library, HOLCF-Prelude, HOLCF-Tutorial, HOLCF-ex, HRB-Slicing, Heard_Of, HereditarilyFinite, Hermite, Hidden_Markov_Models, Higher_Order_Terms, Hoare_Time, HotelKeyCards, How_to_Prove_it, Huffman, Hybrid_Multi_Lane_Spatial_Logic, HyperCTL, IEEE_Floating_Point, IMAP-CRDT, IMP2, IOA, IOA-ABP, IOA-NTP, IOA-Storage, IOA-ex, IP_Addresses, Imperative_Insertion_Sort, Implementation, Impossible_Geometry, Incompleteness, Incredible_Proof_Machine, Inductive_Confidentiality, InfPathElimination, InformationFlowSlicing, InformationFlowSlicing_Inter, Integration, Iptables_Semantics, Iptables_Semantics_Examples, Irrationality_J_Hancl, Isabelle_Meta_Model, Isar_Ref, JEdit, JNF-AFP-Lib, Jinja, JiveDataStoreModel, Jordan_Hoelder, Jordan_Normal_Form, KAD, KAT_and_DRA, KBPs, KD_Tree, Key_Agreement_Strong_Adversaries, Kleene_Algebra, Knot_Theory, Knuth_Morris_Pratt, Koenigsberg_Friendship, Kruskal, Kuratowski_Closure_Complement, LEM, LLL_Basis_Reduction, LLL_Factorization, LOFT, LTL, LTL_Master_Theorem, LTL_to_DRA, LTL_to_GBA, Lam-ml-Normalization, LambdaAuth, LambdaMu, Lambda_Free_EPO, Lambda_Free_KBOs, Lambda_Free_RPOs, Landau_Symbols, Latin_Square, LatticeProperties, Launchbury, Lazy-Lists-II, Lazy_Case, Lehmer, Lifting_Definition_Option, LightweightJava, LinearQuantifierElim, Linear_Recurrences, Linear_Recurrences_Solver, Liouville_Numbers, List-Index, List-Infinite, List_Interleaving, List_Inversions, List_Update, LocalLexing, Locales, Localization_Ring, Locally-Nameless-Sigma, Lorenz_Approximation, Lorenz_C0, Lorenz_C1, Lowe_Ontological_Argument, Lower_Semicontinuous, Lp, MFMC_Countable, MSO_Regex_Equivalence, Main, Markov_Models, Marriage, Mason_Stothers, Matrix, Matrix_Tensor, Matroids, Max-Card-Matching, Median_Of_Medians_Selection, Menger, MiniML, Minimal_SSA, Minkowskis_Theorem, Minsky_Machines, Modal_Logics_for_NTS, Modular_Assembly_Kit_Security, Monad_Memo_DP, Monad_Normalisation, MonoBoolTranAlgebra, MonoidalCategory, Monomorphic_Monad, MuchAdoAboutTwo, Multi_Party_Computation, Multirelations, Myhill-Nerode, Name_Carrying_Type_Inference, Nat-Interval-Logic, Native_Word, Nested_Multisets_Ordinals, Network_Security_Policy_Verification, Neumann_Morgenstern_Utility, No_FTL_observers, Nominal2, Noninterference_CSP, Noninterference_Concurrent_Composition, Noninterference_Generic_Unwinding, Noninterference_Inductive_Unwinding, Noninterference_Ipurge_Unwinding, Noninterference_Sequential_Composition, NormByEval, Octonions, Old_Datatype_Show, OpSets, Open_Induction, Optics, Optimal_BST, Orbit_Stabiliser, Order_Lattice_Props, Ordered_Resolution_Prover, Ordinal, Ordinals_and_Cardinals, Ordinary_Differential_Equations, PCF, PLM, POPLmark-deBruijn, PSemigroupsConvolution, Pairing_Heap, Paraconsistency, Parity_Game, Partial_Function_MR, Partial_Order_Reduction, Password_Authentication_Protocol, Pell, Perfect-Number-Thm, Perron_Frobenius, Pi_Calculus, Pi_Transcendental, Planarity_Certificates, Polynomial_Factorization, Polynomial_Interpolation, Polynomials, Pop_Refinement, Posix-Lexing, Possibilistic_Noninterference, Pratt_Certificate, Pre_BZ, Presburger-Automata, Prime_Distribution_Elementary, Prime_Harmonic_Series, Prime_Number_Theorem, Priority_Queue_Braun, Probabilistic_Noninterference, Probabilistic_Prime_Tests, Probabilistic_System_Zoo, Probabilistic_System_Zoo-BNFs, Probabilistic_System_Zoo-Non_BNFs, Probabilistic_Timed_Automata, Probabilistic_While, Prog_Prove, Program-Conflict-Analysis, Projective_Geometry, Promela, Proof_Strategy_Language, PropResPI, Propositional_Proof_Systems, Prpu_Maxflow, PseudoHoops, Psi_Calculi, Ptolemys_Theorem, QHLProver, QR_Decomposition, Quantales, Quaternions, Quick_Sort_Cost, RIPEMD-160-SPARK, ROBDD, RSAPSS, Ramsey-Infinite, Random_BSTs, Random_Graph_Subgraph_Threshold, Randomised_BSTs, Randomised_Social_Choice, Rank_Nullity_Theorem, Real_Impl, Recursion-Theory-I, Refine_Imperative_HOL, Refine_Monadic, RefinementReactive, Regex_Equivalence, Regular-Sets, Regular_Algebras, Relation_Algebra, Rep_Fin_Groups, Residuated_Lattices, Resolution_FOL, Rewriting_Z, Ribbon_Proofs, Robbins-Conjecture, Root_Balanced_Tree, Routing, Roy_Floyd_Warshall, SATSolverVerification, SDS_Impossibility, SIFPL, SIFUM_Type_Systems, SM, SM_Base, SPARCv8, Safe_OCL, Secondary_Sylow, Security_Protocol_Refinement, Selection_Heap_Sort, SenSocialChoice, Separata, Separation_Algebra, Separation_Logic_Imperative_HOL, Sepref_Basic, Sepref_IICF, Sepref_Prereq, SequentInvertibility, Shivers-CFA, ShortestPath, Show, Signature_Groebner, Simpl, Simple_Firewall, Simplex, Skew_Heap, Slicing, Smooth_Manifolds, Sort_Encodings, Source_Coding_Theorem, Special_Function_Bounds, Splay_Tree, Sqrt_Babylonian, Stable_Matching, Statecharts, Stern_Brocot, Stewart_Apollonius, Stirling_Formula, Stochastic_Matrices, Stone_Algebras, Stone_Kleene_Relation_Algebras, Stone_Relation_Algebras, Store_Buffer_Reduction, Stream-Fusion, Stream_Fusion_Code, Strong_Security, Sturm_Sequences, Sturm_Tarski, Stuttering_Equivalence, Subresultants, Sugar, SumSquares, SuperCalc, Surprise_Paradox, Symmetric_Polynomials, TLA, Tail_Recursive_Functions, Tarskis_Geometry, Taylor_Models, Timed_Automata, Topology, TortoiseHare, Transcendence_Series_Hancl_Rucki, Transformer_Semantics, Transition_Systems_and_Automata, Transitive-Closure, Transitive-Closure-II, Treaps, Tree-Automata, Tree_Decomposition, Triangle, Trie, Tutorial, Twelvefold_Way, Tycon, Typeclass_Hierarchy, Types_Tableaus_and_Goedels_God, UPF, UPF_Firewall, UTP, UTP-Toolkit, Universal_Turing_Machine, UpDown_Scheme, Valuation, VectorSpace, Verified-Prover, VerifyThis2018, Vickrey_Clarke_Groves, VolpanoSmith, WHATandWHERE_Security, WebAssembly, Weight_Balanced_Trees, Well_Quasi_Orders, Winding_Number_Eval, Word_Lib, WorkerWrapper, XML, Zeta_Function, pGCL

15:58:50

15:58:50 === TIMING ===

15:58:50

15:58:50 Group AFP: 0:00:00 elapsed time

15:58:50 Group main: 0:03:26 elapsed time, 0:10:20 cpu time, factor 3.00

15:58:50 Group doc: 0:00:00 elapsed time

15:58:50 Group timing: 0:13:38 elapsed time, 0:28:33 cpu time, factor 2.09

15:58:50 Group large: 0:00:00 elapsed time

15:58:50 Group no_doc: 0:00:00 elapsed time

15:58:50 Overall: 0:13:48 elapsed time, 0:38:56 cpu time, factor 2.82

15:58:50

15:58:50 === FAILED SESSIONS ===