13:29:25 Started by upstream project "afp-repo" build number 1529

13:29:25 originally caused by:

13:29:25 Started by an SCM change

13:29:25 [EnvInject] - Loading node environment variables.

13:29:25 Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/afp-repo-afp

13:29:25 [afp-repo-afp] $ hg showconfig paths.default

13:29:25 [afp-repo-afp] $ hg pull --rev default

13:29:26 pulling from http://isabelle.in.tum.de/repos/isabelle/

13:29:26 searching for changes

13:29:26 adding changesets

13:29:26 adding manifests

13:29:26 adding file changes

13:29:26 added 3 changesets with 6 changes to 5 files

13:29:26 (run 'hg update' to get a working copy)

13:29:26 [afp-repo-afp] $ hg update --clean --rev default

13:29:26 5 files updated, 0 files merged, 0 files removed, 0 files unresolved

13:29:26 [afp-repo-afp] $ hg log --rev . --template {node}

13:29:26 [afp-repo-afp] $ hg log --rev . --template {rev}

13:29:26 [afp] $ hg showconfig paths.default

13:29:26 [afp] $ hg pull --rev 4f309629d8ce64fbd161387ed6f0669b031b9fb0

13:29:27 pulling from https://bitbucket.org/isa-afp/afp-devel/

13:29:27 searching for changes

13:29:27 adding changesets

13:29:27 adding manifests

13:29:27 adding file changes

13:29:27 added 2 changesets with 6 changes to 4 files

13:29:27 (run 'hg update' to get a working copy)

13:29:27 [afp] $ hg update --clean --rev 4f309629d8ce64fbd161387ed6f0669b031b9fb0

13:29:28 418 files updated, 0 files merged, 0 files removed, 0 files unresolved

13:29:28 [afp] $ hg --config extensions.purge= clean --all

13:29:28 [afp] $ hg log --rev . --template {node}

13:29:28 [afp] $ hg log --rev . --template {rev}

13:29:28 [afp] $ hg id --branch

13:29:28 No emails were triggered.

13:29:28 [afp-repo-afp] $ /bin/sh -xe /tmp/jenkins842386173948564001.sh

13:29:28 + Admin/jenkins/run_build afp

13:29:28 + set -e

13:29:28 + PROFILE=afp

13:29:28 + shift

13:29:28 + bin/isabelle components -a

13:29:29 + bin/isabelle jedit -bf

13:29:29 ### Building Isabelle/Scala ...

13:29:56 ### Building Isabelle/jEdit ...

13:30:14 + bin/isabelle ci_build_afp

13:30:21

13:30:21 === CONFIGURATION ===

13:30:21

13:30:21 ISABELLE_BUILD_OPTIONS=""

13:30:21

13:30:21 ML_PLATFORM="x86_64-linux"

13:30:21 ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.7.1-5/x86_64-linux"

13:30:21 ML_SYSTEM="polyml-5.7.1"

13:30:21 ML_OPTIONS="-H 4000 --maxheap 8G"

13:30:21

13:30:21 === BUILD ===

13:30:21

13:30:21 Build started at Thu, 19 Apr 2018 11:30:20 GMT

13:30:21 Isabelle id 0a2a1b6507c1

13:30:21 AFP id 4f309629d8ce

13:30:21

13:30:21 === LOG ===

13:30:21

13:30:22 Session Pure/Pure

13:30:22 Session FOL/FOL

13:30:22 Session HOL/HOL (main)

13:30:23 Session AFP/AVL-Trees (AFP)

13:30:23 Session AFP/AWN (AFP)

13:30:23 Session AFP/Abortable_Linearizable_Modules (AFP)

13:30:23 Session AFP/Abstract-Hoare-Logics (AFP)

13:30:23 Session AFP/AnselmGod (AFP)

13:30:23 Session AFP/BinarySearchTree (AFP)

13:30:23 Session AFP/Binomial-Queues (AFP)

13:30:23 Session AFP/Bondy (AFP)

13:30:23 Session AFP/Bounded_Deducibility_Security (AFP)

13:30:23 Session AFP/BytecodeLogicJmlTypes (AFP)

13:30:23 Session AFP/CISC-Kernel (AFP)

13:30:23 Session AFP/CYK (AFP)

13:30:23 Session AFP/Cauchy (AFP)

13:30:23 Session AFP/Sqrt_Babylonian (AFP)

13:30:23 Session AFP/ClockSynchInst (AFP)

13:30:23 Session AFP/Compiling-Exceptions-Correctly (AFP)

13:30:23 Session AFP/ComponentDependencies (AFP)

13:30:23 Session AFP/Constructor_Funs (AFP)

13:30:24 Session AFP/CryptoBasedCompositionalProperties (AFP)

13:30:24 Session AFP/DPT-SAT-Solver (AFP)

13:30:24 Session AFP/Depth-First-Search (AFP)

13:30:24 Session AFP/Diophantine_Eqns_Lin_Hom (AFP)

13:30:24 Session AFP/DiskPaxos (AFP)

13:30:24 Session AFP/Example-Submission (AFP)

13:30:24 Session AFP/FFT (AFP)

13:30:24 Session AFP/FLP (AFP)

13:30:24 Session AFP/FeatherweightJava (AFP)

13:30:24 Session AFP/Featherweight_OCL (AFP)

13:30:24 Session AFP/FileRefinement (AFP)

13:30:24 Session AFP/FocusStreamsCaseStudies (AFP)

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

13:30:24 Session AFP/FunWithFunctions (AFP)

13:30:24 Session AFP/FunWithTilings (AFP)

13:30:24 Session AFP/GPU_Kernel_PL (AFP)

13:30:24 Session AFP/Gauss-Jordan-Elim-Fun (AFP)

13:30:24 Session AFP/GenClock (AFP)

13:30:24 Session AFP/General-Triangle (AFP)

13:30:24 Session AFP/GoedelGod (AFP)

13:30:24 Session HOL/HOL-Eisbach

13:30:24 Session AFP/Allen_Calculus (AFP)

13:30:24 Session AFP/Dependent_SIFUM_Type_Systems (AFP)

13:30:24 Session AFP/Dependent_SIFUM_Refinement (AFP)

13:30:24 Session HOL/HOL-Hoare

13:30:24 Session AFP/Case_Labeling (AFP)

13:30:24 Session HOL/HOL-Lattice

13:30:24 Session HOL/HOL-Library (main timing)

13:30:25 Session AFP/ArrowImpossibilityGS (AFP)

13:30:25 Session AFP/BNF_Operations (AFP)

13:30:25 Session AFP/Binomial-Heaps (AFP)

13:30:25 Session AFP/Boolean_Expression_Checkers (AFP)

13:30:25 Session AFP/Buildings (AFP)

13:30:25 Session AFP/CRDT (AFP)

13:30:25 Session AFP/IMAP-CRDT (AFP)

13:30:25 Session AFP/Card_Multisets (AFP)

13:30:25 Session AFP/Card_Number_Partitions (AFP)

13:30:26 Session AFP/Category (AFP)

13:30:26 Session AFP/Category3 (AFP)

13:30:26 Session AFP/MonoidalCategory (AFP)

13:30:26 Session AFP/CofGroups (AFP)

13:30:26 Session AFP/Completeness (AFP)

13:30:26 Session AFP/ConcurrentIMP (AFP)

13:30:26 Session AFP/Concurrent_Ref_Alg (AFP)

13:30:26 Session AFP/CoreC++ (AFP)

13:30:26 Session AFP/Decl_Sem_Fun_PL (AFP)

13:30:26 Session AFP/Derangements (AFP)

13:30:27 Session AFP/Discrete_Summation (AFP)

13:30:27 Session AFP/Card_Partitions (AFP)

13:30:27 Session AFP/Bell_Numbers_Spivey (AFP)

13:30:27 Session AFP/Card_Equiv_Relations (AFP)

13:30:27 Session AFP/Efficient-Mergesort (AFP)

13:30:27 Session AFP/Encodability_Process_Calculi (AFP)

13:30:27 Session AFP/Euler_Partition (AFP)

13:30:27 Session AFP/FOL-Fitting (AFP)

13:30:27 Session AFP/FOL_Harrison (AFP)

13:30:27 Session AFP/Falling_Factorial_Sum (AFP)

13:30:27 Session AFP/FinFun (AFP)

13:30:27 Session AFP/Finger-Trees (AFP)

13:30:27 Session AFP/Graph_Theory (AFP)

13:30:27 Session AFP/ShortestPath (AFP)

13:30:28 Session AFP/Group-Ring-Module (AFP)

13:30:28 Session AFP/Valuation (AFP)

13:30:28 Session HOL/HOL-Cardinals (timing)

13:30:28 Session AFP/Ordinals_and_Cardinals (AFP)

13:30:28 Session AFP/Sort_Encodings (AFP)

13:30:28 Session HOL/HOL-Computational_Algebra (main timing)

13:30:28 Session AFP/Descartes_Sign_Rule (AFP)

13:30:28 Session HOL/HOL-Algebra (main timing)

13:30:28 Session HOL/HOL-Decision_Procs (timing)

13:30:29 Session AFP/JNF-HOL-Lib (AFP)

13:30:29 Session AFP/Orbit_Stabiliser (AFP)

13:30:29 Session AFP/Perfect-Number-Thm (AFP)

13:30:29 Session AFP/Secondary_Sylow (AFP)

13:30:29 Session AFP/Jordan_Hoelder (AFP)

13:30:29 Session AFP/VectorSpace (AFP)

13:30:29 Session HOL/HOL-Analysis (main timing)

13:30:29 Session AFP/Bernoulli (AFP)

13:30:29 Session AFP/Cartan_FP (AFP)

13:30:30 Session AFP/Cayley_Hamilton (AFP)

13:30:30 Session AFP/Coinductive (AFP)

13:30:30 Session AFP/DynamicArchitectures (AFP)

13:30:30 Session AFP/Architectural_Design_Patterns (AFP)

13:30:30 Session AFP/Lazy-Lists-II (AFP)

13:30:30 Session AFP/Stream_Fusion_Code (AFP)

13:30:30 Session AFP/Topology (AFP)

13:30:30 Session AFP/First_Welfare_Theorem (AFP)

13:30:30 Session AFP/Green (AFP)

13:30:30 Session AFP/Gromov_Hyperbolicity (AFP)

13:30:31 Session HOL/HOL-Probability (main timing)

13:30:31 Session AFP/Buffons_Needle (AFP)

13:30:31 Session AFP/Density_Compiler (AFP)

13:30:31 Session AFP/Ergodic_Theory (AFP)

13:30:31 Session AFP/Fisher_Yates (AFP)

13:30:31 Session AFP/Girth_Chromatic (AFP)

13:30:31 Session AFP/Random_Graph_Subgraph_Threshold (AFP)

13:30:31 Session AFP/Lp (AFP)

13:30:31 Session AFP/Markov_Models (AFP)

13:30:31 Session AFP/Monad_Normalisation (AFP)

13:30:32 Session AFP/Monomorphic_Monad (AFP)

13:30:32 Session AFP/Probabilistic_Noninterference (AFP)

13:30:32 Session AFP/Probabilistic_System_Zoo (AFP)

13:30:32 Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)

13:30:32 Session AFP/Source_Coding_Theorem (AFP)

13:30:32 Session AFP/Kuratowski_Closure_Complement (AFP)

13:30:32 Session AFP/Lower_Semicontinuous (AFP)

13:30:32 Session AFP/Minkowskis_Theorem (AFP)

13:30:32 Session AFP/Probabilistic_System_Zoo-BNFs (AFP)

13:30:32 Session AFP/Ptolemys_Theorem (AFP)

13:30:32 Session AFP/Rank_Nullity_Theorem (AFP)

13:30:32 Session AFP/Gauss_Jordan (AFP)

13:30:32 Session AFP/Echelon_Form (AFP)

13:30:33 Session AFP/Hermite (AFP)

13:30:33 Session AFP/Tarskis_Geometry (AFP)

13:30:33 Session AFP/Triangle (AFP)

13:30:33 Session AFP/Chord_Segments (AFP)

13:30:33 Session AFP/Stewart_Apollonius (AFP)

13:30:33 Session AFP/pGCL (AFP)

13:30:33 Session HOL/HOL-Nonstandard_Analysis (timing)

13:30:33 Session HOL/HOL-Number_Theory (main timing)

13:30:33 Session AFP/E_Transcendental (AFP)

13:30:33 Session AFP/Elliptic_Curves_Group_Law (AFP)

13:30:34 Session AFP/Fermat3_4 (AFP)

13:30:34 Session HOL/HOL-Data_Structures (timing)

13:30:34 Session HOL/HOL-ex (timing)

13:30:34 Session AFP/Automatic_Refinement (AFP)

13:30:34 Session AFP/Lehmer (AFP)

13:30:34 Session AFP/Pratt_Certificate (AFP)

13:30:35 Session AFP/Prime_Harmonic_Series (AFP)

13:30:35 Session AFP/RSAPSS (AFP)

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

13:30:35 Session AFP/Liouville_Numbers (AFP)

13:30:35 Session AFP/Mason_Stothers (AFP)

13:30:35 Session AFP/Polynomial_Interpolation (AFP)

13:30:35 Session AFP/Rep_Fin_Groups (AFP)

13:30:35 Session AFP/Sturm_Sequences (AFP)

13:30:35 Session AFP/Special_Function_Bounds (AFP)

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

13:30:35 Session AFP/Winding_Number_Eval (AFP)

13:30:35 Session AFP/Count_Complex_Roots (AFP)

13:30:35 Session HOL/HOL-IMP (timing)

13:30:35 Session AFP/Abs_Int_ITP2012 (AFP)

13:30:36 Session HOL/HOL-Imperative_HOL (timing)

13:30:36 Session AFP/Imperative_Insertion_Sort (AFP)

13:30:36 Session HOL/HOL-Nominal

13:30:36 Session AFP/CCS (AFP)

13:30:36 Session AFP/Lam-ml-Normalization (AFP)

13:30:36 Session AFP/Pi_Calculus (AFP)

13:30:36 Session AFP/Psi_Calculi (AFP)

13:30:36 Session AFP/SequentInvertibility (AFP)

13:30:36 Session HOL/HOL-ZF

13:30:36 Session AFP/Category2 (AFP)

13:30:36 Session AFP/HereditarilyFinite (AFP)

13:30:36 Session AFP/HyperCTL (AFP)

13:30:36 Session AFP/Integration (AFP)

13:30:36 Session AFP/Isabelle_Meta_Model (AFP)

13:30:37 Session Doc/Isar_Ref (doc)

13:30:37 Session AFP/LTL (AFP)

13:30:37 Session AFP/Stuttering_Equivalence (AFP)

13:30:37 Session AFP/Lambda_Free_RPOs (AFP)

13:30:37 Session AFP/Landau_Symbols (AFP)

13:30:37 Session AFP/Error_Function (AFP)

13:30:37 Session AFP/Landau_Analysis (AFP)

13:30:37 Session AFP/Catalan_Numbers (AFP)

13:30:37 Session AFP/Euler_MacLaurin (AFP)

13:30:37 Session AFP/Stirling_Formula (AFP)

13:30:37 Session AFP/LightweightJava (AFP)

13:30:37 Session AFP/LinearQuantifierElim (AFP)

13:30:37 Session AFP/List-Infinite (AFP)

13:30:37 Session AFP/Nat-Interval-Logic (AFP)

13:30:38 Session AFP/AutoFocus-Stream (AFP)

13:30:38 Session AFP/MuchAdoAboutTwo (AFP)

13:30:38 Session AFP/Optics (AFP)

13:30:38 Session AFP/POPLmark-deBruijn (AFP)

13:30:38 Session AFP/Pairing_Heap (AFP)

13:30:38 Session AFP/Password_Authentication_Protocol (AFP)

13:30:38 Session AFP/Presburger-Automata (AFP)

13:30:38 Session AFP/Priority_Queue_Braun (AFP)

13:30:38 Session AFP/Program-Conflict-Analysis (AFP)

13:30:38 Session AFP/Regular-Sets (AFP)

13:30:38 Session AFP/Abstract-Rewriting (AFP)

13:30:38 Session AFP/Decreasing-Diagrams (AFP)

13:30:38 Session AFP/First_Order_Terms (AFP)

13:30:38 Session AFP/Matrix (AFP)

13:30:38 Session AFP/Matrix_Tensor (AFP)

13:30:38 Session AFP/Knot_Theory (AFP)

13:30:39 Session AFP/Coinductive_Languages (AFP)

13:30:39 Session AFP/Finite_Automata_HF (AFP)

13:30:39 Session AFP/Functional-Automata (AFP)

13:30:39 Session AFP/Posix-Lexing (AFP)

13:30:39 Session AFP/Ribbon_Proofs (AFP)

13:30:39 Session AFP/SATSolverVerification (AFP)

13:30:39 Session AFP/Selection_Heap_Sort (AFP)

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

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

13:30:39 Session AFP/Amortized_Complexity (AFP)

13:30:39 Session AFP/Dynamic_Tables (AFP)

13:30:39 Session AFP/Root_Balanced_Tree (AFP)

13:30:40 Session AFP/Stable_Matching (AFP)

13:30:40 Session AFP/SuperCalc (AFP)

13:30:40 Session AFP/Tail_Recursive_Functions (AFP)

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

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

13:30:40 Session AFP/Twelvefold_Way (AFP)

13:30:40 Session AFP/Vickrey_Clarke_Groves (AFP)

13:30:40 Session HOL/HOL-Statespace

13:30:40 Session HOL/HOL-Types_To_Sets

13:30:40 Session HOL/HOL-Word (main timing)

13:30:40 Session HOL/HOL-SPARK (main)

13:30:40 Session HOL/HOL-SPARK-Examples

13:30:41 Session AFP/RIPEMD-160-SPARK (AFP)

13:30:41 Session AFP/Kleene_Algebra (AFP)

13:30:41 Session AFP/KAT_and_DRA (AFP)

13:30:41 Session AFP/Multirelations (AFP)

13:30:41 Session AFP/Regular_Algebras (AFP)

13:30:41 Session AFP/Relation_Algebra (AFP)

13:30:41 Session AFP/Residuated_Lattices (AFP)

13:30:41 Session AFP/Native_Word (AFP)

13:30:41 Session AFP/Refine_Monadic (AFP)

13:30:41 Session AFP/Collections (AFP)

13:30:42 Session AFP/Abstract_Completeness (AFP)

13:30:42 Session AFP/Abstract_Soundness (AFP)

13:30:42 Session AFP/Incredible_Proof_Machine (AFP)

13:30:42 Session AFP/Deriving (AFP)

13:30:42 Session AFP/CAVA_Base (AFP)

13:30:43 Session AFP/CAVA_Automata (AFP)

13:30:43 Session AFP/DFS_Framework (AFP)

13:30:43 Session AFP/Gabow_SCC (AFP)

13:30:43 Session AFP/LTL_to_GBA (AFP)

13:30:43 Session AFP/CAVA_buildchain1 (AFP)

13:30:43 Session AFP/Promela (AFP)

13:30:43 Session AFP/CAVA_buildchain3 (AFP)

13:30:44 Session AFP/CAVA_LTL_Modelchecker (AFP)

13:30:44 Session AFP/Containers (AFP)

13:30:44 Session AFP/Collections_Examples (AFP)

13:30:44 Session AFP/Containers-Benchmarks (AFP)

13:30:45 Session AFP/Datatype_Order_Generator (AFP)

13:30:45 Session AFP/Old_Datatype_Show (AFP)

13:30:45 Session AFP/Show (AFP)

13:30:45 Session AFP/JNF-AFP-Lib (AFP)

13:30:46 Session AFP/Polynomials (AFP)

13:30:46 Session AFP/Groebner_Bases (AFP)

13:30:46 Session AFP/Real_Impl (AFP)

13:30:46 Session AFP/QR_Decomposition (AFP)

13:30:47 Session AFP/Dijkstra_Shortest_Path (AFP)

13:30:47 Session AFP/Koenigsberg_Friendship (AFP)

13:30:47 Session AFP/Transition_Systems_and_Automata (AFP)

13:30:47 Session AFP/Buchi_Complementation (AFP)

13:30:47 Session AFP/Transitive-Closure (AFP)

13:30:47 Session AFP/KBPs (AFP)

13:30:47 Session AFP/Tree-Automata (AFP)

13:30:47 Session AFP/SPARCv8 (AFP)

13:30:48 Session AFP/Separation_Algebra (AFP)

13:30:48 Session AFP/Separata (AFP)

13:30:48 Session AFP/Separation_Logic_Imperative_HOL (AFP)

13:30:48 Session AFP/Sepref_Prereq (AFP)

13:30:49 Session AFP/ROBDD (AFP)

13:30:49 Session AFP/UpDown_Scheme (AFP)

13:30:49 Session AFP/Word_Lib (AFP)

13:30:49 Session AFP/Complx (AFP)

13:30:49 Session AFP/IEEE_Floating_Point (AFP)

13:30:49 Session AFP/IP_Addresses (AFP)

13:30:50 Session AFP/Simple_Firewall (AFP)

13:30:50 Session AFP/Routing (AFP)

13:30:50 Session AFP/Iptables_Semantics (AFP)

13:30:50 Session AFP/Iptables_Semantics_Examples (AFP)

13:30:50 Session AFP/LOFT (AFP)

13:30:50 Session AFP/LEM (AFP)

13:30:50 Session AFP/CakeML_Prelim (AFP)

13:30:51 Session AFP/CakeML (AFP)

13:30:51 Session HOL/HOLCF (main timing)

13:30:51 Session AFP/Circus (AFP)

13:30:51 Session HOL/HOLCF-Library

13:30:51 Session AFP/PCF (AFP)

13:30:51 Session AFP/HOLCF-Prelude (AFP)

13:30:51 Session AFP/Shivers-CFA (AFP)

13:30:51 Session AFP/Stream-Fusion (AFP)

13:30:51 Session AFP/Tycon (AFP)

13:30:51 Session AFP/WorkerWrapper (AFP)

13:30:52 Session AFP/Heard_Of (AFP)

13:30:52 Session AFP/Consensus_Refined (AFP)

13:30:52 Session AFP/Hoare_Time (AFP)

13:30:52 Session AFP/HotelKeyCards (AFP)

13:30:52 Session AFP/Huffman (AFP)

13:30:52 Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)

13:30:52 Session AFP/Impossible_Geometry (AFP)

13:30:52 Session AFP/Inductive_Confidentiality (AFP)

13:30:52 Session AFP/InfPathElimination (AFP)

13:30:52 Session AFP/JiveDataStoreModel (AFP)

13:30:52 Session AFP/KAD (AFP)

13:30:52 Session AFP/Algebraic_VCs (AFP)

13:30:52 Session AFP/Key_Agreement_Strong_Adversaries (AFP)

13:30:52 Session AFP/LambdaMu (AFP)

13:30:52 Session AFP/LatticeProperties (AFP)

13:30:52 Session AFP/DataRefinementIBP (AFP)

13:30:52 Session AFP/GraphMarkingIBP (AFP)

13:30:52 Session AFP/Lazy_Case (AFP)

13:30:52 Session AFP/Dict_Construction (AFP)

13:30:53 Session AFP/Lifting_Definition_Option (AFP)

13:30:53 Session AFP/List-Index (AFP)

13:30:53 Session AFP/Affine_Arithmetic (AFP)

13:30:53 Session AFP/Taylor_Models (AFP)

13:30:53 Session AFP/Comparison_Sort_Lower_Bound (AFP)

13:30:53 Session AFP/Formula_Derivatives (AFP)

13:30:54 Session AFP/Formula_Derivatives-Examples (AFP)

13:30:54 Session AFP/Jinja (AFP)

13:30:54 Session AFP/HRB-Slicing (AFP)

13:30:54 Session AFP/InformationFlowSlicing_Inter (AFP)

13:30:54 Session AFP/Slicing (AFP)

13:30:54 Session AFP/Formal_SSA (AFP)

13:30:54 Session AFP/Minimal_SSA (AFP)

13:30:54 Session AFP/InformationFlowSlicing (AFP)

13:30:55 Session AFP/LTL_to_DRA (AFP)

13:30:55 Session AFP/List_Update (AFP)

13:30:55 Session AFP/Ordinary_Differential_Equations (AFP)

13:30:55 Session AFP/Akra_Bazzi (AFP)

13:30:55 Session AFP/Bertrands_Postulate (AFP)

13:30:56 Session AFP/HOL-ODE (AFP)

13:30:56 Session AFP/Differential_Dynamic_Logic (AFP)

13:30:56 Session AFP/HOL-ODE-Refinement (AFP)

13:30:57 Session AFP/HOL-ODE-Numerics (AFP)

13:30:57 Session AFP/HOL-ODE-Examples (AFP)

13:30:57 Session AFP/Lorenz_Approximation (AFP)

13:30:57 Session AFP/Lorenz_C1 (AFP)

13:30:57 Session AFP/Quick_Sort_Cost (AFP)

13:30:57 Session AFP/Random_BSTs (AFP)

13:30:58 Session AFP/Treaps (AFP)

13:30:58 Session AFP/Randomised_Social_Choice (AFP)

13:30:58 Session AFP/SDS_Impossibility (AFP)

13:30:58 Session AFP/Refine_Imperative_HOL (AFP)

13:30:58 Session AFP/Floyd_Warshall (AFP)

13:30:58 Session AFP/Sepref_Basic (AFP)

13:30:59 Session AFP/Sepref_IICF (AFP)

13:30:59 Session AFP/Knuth_Morris_Pratt (AFP)

13:30:59 Session AFP/Maxflow_Lib (AFP)

13:30:59 Session AFP/Flow_Networks (AFP)

13:30:59 Session AFP/EdmondsKarp_Maxflow (AFP)

13:31:00 Session AFP/MFMC_Countable (AFP)

13:31:00 Session AFP/Prpu_Maxflow (AFP)

13:31:00 Session AFP/List_Interleaving (AFP)

13:31:00 Session AFP/LocalLexing (AFP)

13:31:00 Session AFP/Lowe_Ontological_Argument (AFP)

13:31:00 Session AFP/MSO_Regex_Equivalence (AFP)

13:31:00 Session AFP/MSO_Examples (AFP)

13:31:00 Session AFP/Marriage (AFP)

13:31:00 Session AFP/Latin_Square (AFP)

13:31:00 Session AFP/Max-Card-Matching (AFP)

13:31:00 Session AFP/Median_Of_Medians_Selection (AFP)

13:31:01 Session AFP/Menger (AFP)

13:31:01 Session AFP/MiniML (AFP)

13:31:01 Session AFP/MonoBoolTranAlgebra (AFP)

13:31:01 Session AFP/Name_Carrying_Type_Inference (AFP)

13:31:01 Session AFP/Network_Security_Policy_Verification (AFP)

13:31:01 Session AFP/No_FTL_observers (AFP)

13:31:01 Session AFP/Nominal2 (AFP)

13:31:02 Session AFP/Incompleteness (AFP)

13:31:02 Session AFP/Surprise_Paradox (AFP)

13:31:02 Session AFP/Launchbury (AFP)

13:31:02 Session AFP/Call_Arity (AFP)

13:31:02 Session AFP/Modal_Logics_for_NTS (AFP)

13:31:02 Session AFP/Rewriting_Z (AFP)

13:31:02 Session AFP/Noninterference_CSP (AFP)

13:31:03 Session AFP/Noninterference_Ipurge_Unwinding (AFP)

13:31:03 Session AFP/Noninterference_Generic_Unwinding (AFP)

13:31:03 Session AFP/Noninterference_Inductive_Unwinding (AFP)

13:31:03 Session AFP/Noninterference_Sequential_Composition (AFP)

13:31:03 Session AFP/Noninterference_Concurrent_Composition (AFP)

13:31:03 Session AFP/NormByEval (AFP)

13:31:03 Session AFP/Open_Induction (AFP)

13:31:03 Session AFP/Well_Quasi_Orders (AFP)

13:31:03 Session AFP/Decreasing-Diagrams-II (AFP)

13:31:03 Session AFP/Myhill-Nerode (AFP)

13:31:03 Session AFP/Ordinal (AFP)

13:31:03 Session AFP/Nested_Multisets_Ordinals (AFP)

13:31:03 Session AFP/Lambda_Free_KBOs (AFP)

13:31:04 Session AFP/Ordered_Resolution_Prover (AFP)

13:31:04 Session AFP/PLM (AFP)

13:31:04 Session AFP/PSemigroupsConvolution (AFP)

13:31:04 Session AFP/Paraconsistency (AFP)

13:31:04 Session AFP/Parity_Game (AFP)

13:31:04 Session AFP/Partial_Function_MR (AFP)

13:31:04 Session AFP/Certification_Monads (AFP)

13:31:04 Session AFP/XML (AFP)

13:31:05 Session AFP/Pre_Polynomial_Factorization (AFP)

13:31:05 Session AFP/Polynomial_Factorization (AFP)

13:31:05 Session AFP/Dirichlet_Series (AFP)

13:31:05 Session AFP/Zeta_Function (AFP)

13:31:06 Session AFP/Dirichlet_L (AFP)

13:31:06 Session AFP/Jordan_Normal_Form (AFP)

13:31:06 Session AFP/Deep_Learning_Lib (AFP)

13:31:07 Session AFP/Deep_Learning (AFP)

13:31:07 Session AFP/Subresultants (AFP)

13:31:07 Session AFP/Pre_BZ (AFP)

13:31:07 Session AFP/Berlekamp_Zassenhaus (AFP)

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

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

13:31:08 Session AFP/Algebraic_Numbers_Lib (AFP)

13:31:08 Session AFP/Linear_Recurrences (AFP)

13:31:08 Session AFP/Linear_Recurrences_Test (AFP)

13:31:09 Session AFP/Pre_Perron_Frobenius (AFP)

13:31:09 Session AFP/Perron_Frobenius (AFP)

13:31:09 Session AFP/LLL_Basis_Reduction (AFP)

13:31:09 Session AFP/LLL_Factorization (AFP)

13:31:10 Session AFP/Stochastic_Matrices (AFP)

13:31:10 Session AFP/Probabilistic_While (AFP)

13:31:10 Session AFP/Pop_Refinement (AFP)

13:31:10 Session AFP/Possibilistic_Noninterference (AFP)

13:31:10 Session AFP/Proof_Strategy_Language (AFP)

13:31:10 Session AFP/PropResPI (AFP)

13:31:10 Session AFP/Propositional_Proof_Systems (AFP)

13:31:10 Session AFP/PseudoHoops (AFP)

13:31:11 Session AFP/Ramsey-Infinite (AFP)

13:31:11 Session AFP/Recursion-Theory-I (AFP)

13:31:11 Session AFP/RefinementReactive (AFP)

13:31:11 Session AFP/Regex_Equivalence (AFP)

13:31:11 Session AFP/Resolution_FOL (AFP)

13:31:11 Session AFP/Robbins-Conjecture (AFP)

13:31:11 Session AFP/Roy_Floyd_Warshall (AFP)

13:31:11 Session AFP/SIFPL (AFP)

13:31:11 Session AFP/SIFUM_Type_Systems (AFP)

13:31:11 Session AFP/Security_Protocol_Refinement (AFP)

13:31:11 Session AFP/SenSocialChoice (AFP)

13:31:11 Session AFP/Simpl (AFP)

13:31:12 Session AFP/BDD (AFP)

13:31:12 Session AFP/Planarity_Certificates (AFP)

13:31:12 Session AFP/Statecharts (AFP)

13:31:12 Session AFP/Stone_Algebras (AFP)

13:31:12 Session AFP/Stone_Relation_Algebras (AFP)

13:31:12 Session AFP/Stone_Kleene_Relation_Algebras (AFP)

13:31:12 Session AFP/Strong_Security (AFP)

13:31:12 Session AFP/TLA (AFP)

13:31:12 Session AFP/Timed_Automata (AFP)

13:31:12 Session AFP/Transitive-Closure-II (AFP)

13:31:12 Session AFP/Tree_Decomposition (AFP)

13:31:12 Session AFP/Types_Tableaus_and_Goedels_God (AFP)

13:31:12 Session AFP/UPF (AFP)

13:31:13 Session AFP/UPF_Firewall (AFP)

13:31:13 Session AFP/Verified-Prover (AFP)

13:31:13 Session AFP/VolpanoSmith (AFP)

13:31:13 Session AFP/WHATandWHERE_Security (AFP)

13:31:13 Session AFP/Weight_Balanced_Trees (AFP)

13:31:13 Session HOL/HOL-Proofs (timing)

13:31:13 Session HOL/HOL-Proofs-Lambda (timing)

13:31:13 Session AFP/Applicative_Lifting (AFP)

13:31:14 Session AFP/CryptHOL (AFP)

13:31:14 Session AFP/Game_Based_Crypto (AFP)

13:31:14 Session AFP/Free-Groups (AFP)

13:31:14 Session AFP/Locally-Nameless-Sigma (AFP)

13:31:14 Session AFP/Stern_Brocot (AFP)

13:31:14 Session Unsorted/Spec_Check

13:31:14 Session AFP/Regex_Equivalence_Examples (AFP)

13:31:25 Building HOL-Analysis ...

13:31:26 Building HOL-Number_Theory ...

13:31:26 Building HOL-Algebra ...

13:31:26 Building Matrix ...

13:31:26 Running Free-Groups ...

13:31:28 Free-Groups: theory HOL-Cardinals.Fun_More

13:31:28 Free-Groups: theory HOL-Cardinals.Order_Relation_More

13:31:28 HOL-Algebra: theory HOL-Algebra.Exponent

13:31:28 HOL-Algebra: theory HOL-Algebra.Congruence

13:31:28 Free-Groups: theory HOL-Cardinals.Order_Union

13:31:28 Free-Groups: theory HOL-Library.Cancellation

13:31:28 Free-Groups: theory HOL-Cardinals.Wellfounded_More

13:31:28 HOL-Number_Theory: theory HOL-Algebra.Congruence

13:31:28 HOL-Number_Theory: theory HOL-Number_Theory.Cong

13:31:28 Free-Groups: theory HOL-Cardinals.Wellorder_Relation

13:31:28 Free-Groups: theory HOL-Cardinals.Wellorder_Embedding

13:31:28 Free-Groups: theory HOL-Library.Cardinal_Notations

13:31:28 Free-Groups: theory HOL-Cardinals.Wellorder_Constructions

13:31:29 Matrix: theory HOL-Algebra.Congruence

13:31:29 Matrix: theory Matrix.Utility

13:31:29 Free-Groups: theory HOL-Library.Multiset

13:31:29 HOL-Algebra: theory HOL-Algebra.Order

13:31:29 HOL-Number_Theory: theory HOL-Algebra.Order

13:31:29 HOL-Number_Theory: theory HOL-Number_Theory.Eratosthenes

13:31:30 Matrix: theory HOL-Algebra.Order

13:31:30 HOL-Number_Theory: theory HOL-Number_Theory.Fib

13:31:30 Free-Groups: theory HOL-Cardinals.Cardinal_Order_Relation

13:31:30 HOL-Number_Theory: theory HOL-Number_Theory.Prime_Powers

13:31:30 HOL-Algebra: theory HOL-Algebra.Lattice

13:31:30 HOL-Number_Theory: theory HOL-Algebra.Lattice

13:31:31 Matrix: theory HOL-Algebra.Lattice

13:31:31 HOL-Number_Theory: theory HOL-Number_Theory.Totient

13:31:31 Free-Groups: theory HOL-Library.FuncSet

13:31:31 HOL-Algebra: theory HOL-Algebra.Complete_Lattice

13:31:31 HOL-Number_Theory: theory HOL-Algebra.Complete_Lattice

13:31:32 Free-Groups: theory HOL-Algebra.Congruence

13:31:32 Matrix: theory HOL-Algebra.Complete_Lattice

13:31:33 HOL-Algebra: theory HOL-Algebra.Galois_Connection

13:31:33 HOL-Number_Theory: theory HOL-Algebra.Group

13:31:33 Free-Groups: theory HOL-Algebra.Order

13:31:33 Matrix: theory HOL-Algebra.Group

13:31:34 HOL-Algebra: theory HOL-Algebra.Group

13:31:34 Free-Groups: theory HOL-Computational_Algebra.Factorial_Ring

13:31:34 HOL-Number_Theory: theory HOL-Algebra.Coset

13:31:34 HOL-Number_Theory: theory HOL-Algebra.FiniteProduct

13:31:34 Free-Groups: theory HOL-Algebra.Lattice

13:31:34 Matrix: theory HOL-Algebra.FiniteProduct

13:31:35 HOL-Number_Theory: theory HOL-Algebra.Ring

13:31:35 Matrix: theory HOL-Algebra.Ring

13:31:35 HOL-Algebra: theory HOL-Algebra.Bij

13:31:36 HOL-Algebra: theory HOL-Algebra.Coset

13:31:36 Free-Groups: theory HOL-Algebra.Complete_Lattice

13:31:36 HOL-Algebra: theory HOL-Algebra.FiniteProduct

13:31:37 HOL-Algebra: theory HOL-Algebra.Sylow

13:31:37 Free-Groups: theory HOL-Algebra.Group

13:31:37 HOL-Algebra: theory HOL-Algebra.Divisibility

13:31:37 HOL-Algebra: theory HOL-Algebra.Ring

13:31:38 HOL-Number_Theory: theory HOL-Algebra.AbelCoset

13:31:38 Matrix: theory Matrix.Ordered_Semiring

13:31:38 Free-Groups: theory Free-Groups.C2

13:31:38 Free-Groups: theory Free-Groups.Generators

13:31:39 Free-Groups: theory Free-Groups.UnitGroup

13:31:39 Free-Groups: theory HOL-Algebra.Bij

13:31:39 Free-Groups: theory HOL-Algebra.Coset

13:31:39 Matrix: theory Matrix.Matrix_Legacy

13:31:40 HOL-Number_Theory: theory HOL-Algebra.Module

13:31:40 HOL-Analysis: theory HOL-Library.Disjoint_Sets

13:31:40 HOL-Analysis: theory HOL-Library.Cancellation

13:31:40 Free-Groups: theory HOL-Algebra.FiniteProduct

13:31:40 HOL-Analysis: theory HOL-Library.FuncSet

13:31:40 HOL-Analysis: theory HOL-Library.Multiset

13:31:40 HOL-Analysis: theory HOL-Library.Infinite_Set

13:31:41 Free-Groups: theory HOL-Algebra.Ring

13:31:41 HOL-Analysis: theory HOL-Library.Nat_Bijection

13:31:41 HOL-Algebra: theory HOL-Algebra.AbelCoset

13:31:41 Free-Groups: theory HOL-Computational_Algebra.Euclidean_Algorithm

13:31:41 HOL-Algebra: theory HOL-Algebra.Module

13:31:41 HOL-Analysis: theory HOL-Library.Old_Datatype

13:31:41 HOL-Number_Theory: theory HOL-Algebra.More_Group

13:31:41 HOL-Number_Theory: theory HOL-Algebra.More_Finite_Product

13:31:42 HOL-Number_Theory: theory HOL-Algebra.Ideal

13:31:42 HOL-Analysis: theory HOL-Library.Phantom_Type

13:31:42 HOL-Number_Theory: theory HOL-Algebra.More_Ring

13:31:42 HOL-Analysis: theory HOL-Library.Cardinality

13:31:42 HOL-Algebra: theory HOL-Algebra.More_Group

13:31:43 HOL-Algebra: theory HOL-Algebra.More_Finite_Product

13:31:43 HOL-Algebra: theory HOL-Algebra.More_Ring

13:31:44 HOL-Analysis: theory HOL-Library.Numeral_Type

13:31:45 HOL-Analysis: theory HOL-Library.Product_Plus

13:31:45 HOL-Analysis: theory HOL-Library.Product_Order

13:31:45 HOL-Analysis: theory HOL-Library.Set_Algebras

13:31:45 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring

13:31:45 HOL-Analysis: theory HOL-Library.Permutations

13:31:46 Free-Groups: theory HOL-Algebra.AbelCoset

13:31:46 HOL-Number_Theory: theory HOL-Algebra.RingHom

13:31:46 HOL-Algebra: theory HOL-Algebra.Ideal

13:31:47 HOL-Analysis: theory HOL-Library.Countable

13:31:47 HOL-Number_Theory: theory HOL-Algebra.UnivPoly

13:31:48 HOL-Analysis: theory HOL-Library.Countable_Set

13:31:48 HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices

13:31:49 HOL-Algebra: theory HOL-Algebra.RingHom

13:31:49 Free-Groups: theory HOL-Algebra.Ideal

13:31:50 Free-Groups: theory HOL-Computational_Algebra.Primes

13:31:50 HOL-Algebra: theory HOL-Algebra.QuotRing

13:31:50 HOL-Algebra: theory HOL-Algebra.UnivPoly

13:31:50 Free-Groups: theory HOL-Proofs-Lambda.Commutation

13:31:51 Free-Groups: theory Free-Groups.Cancelation

13:31:51 Free-Groups: theory Free-Groups.FreeGroups

13:31:51 HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable

13:31:51 Free-Groups: theory Free-Groups.PingPongLemma

13:31:51 HOL-Analysis: theory HOL-Analysis.Infinite_Products

13:31:52 Free-Groups: theory HOL-Algebra.RingHom

13:31:52 HOL-Algebra: theory HOL-Algebra.IntRing

13:31:52 Free-Groups: theory HOL-Algebra.QuotRing

13:31:53 Free-Groups: theory HOL-Algebra.IntRing

13:31:53 HOL-Analysis: theory HOL-Analysis.Inner_Product

13:31:53 HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm

13:31:54 Free-Groups: theory Free-Groups.Isomorphisms

13:31:54 HOL-Analysis: theory HOL-Analysis.Product_Vector

13:31:55 HOL-Analysis: theory HOL-Analysis.L2_Norm

13:31:55 HOL-Analysis: theory HOL-Analysis.Euclidean_Space

13:31:56 HOL-Analysis: theory HOL-Analysis.Linear_Algebra

13:31:57 HOL-Number_Theory: theory HOL-Algebra.Multiplicative_Group

13:31:59 HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product

13:32:00 HOL-Number_Theory: theory HOL-Number_Theory.Residues

13:32:01 HOL-Analysis: theory HOL-Analysis.Operator_Norm

13:32:01 HOL-Analysis: theory HOL-Analysis.Poly_Roots

13:32:01 HOL-Analysis: theory HOL-Library.Discrete

13:32:01 HOL-Analysis: theory HOL-Computational_Algebra.Primes

13:32:01 HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series

13:32:01 HOL-Analysis: theory HOL-Library.Indicator_Function

13:32:02 HOL-Analysis: theory HOL-Library.Liminf_Limsup

13:32:02 HOL-Number_Theory: theory HOL-Number_Theory.Euler_Criterion

13:32:02 HOL-Number_Theory: theory HOL-Number_Theory.Gauss

13:32:02 HOL-Number_Theory: theory HOL-Number_Theory.Quadratic_Reciprocity

13:32:02 HOL-Analysis: theory HOL-Library.Nonpos_Ints

13:32:02 HOL-Algebra: theory HOL-Algebra.Multiplicative_Group

13:32:02 HOL-Analysis: theory HOL-Library.Order_Continuity

13:32:03 HOL-Number_Theory: theory HOL-Number_Theory.Pocklington

13:32:03 HOL-Number_Theory: theory HOL-Number_Theory.Number_Theory

13:32:03 HOL-Analysis: theory HOL-Library.Extended_Nat

13:32:04 HOL-Analysis: theory HOL-Library.Extended_Real

13:32:05 HOL-Analysis: theory HOL-Library.Periodic_Fun

13:32:05 HOL-Analysis: theory HOL-Library.Sum_of_Squares

13:32:08 HOL-Analysis: theory HOL-Analysis.Norm_Arith

13:32:08 HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real

13:32:11 HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space

13:32:13 HOL-Analysis: theory HOL-Analysis.Sigma_Algebra

13:32:17 HOL-Analysis: theory HOL-Analysis.Measurable

13:32:17 HOL-Analysis: theory HOL-Analysis.Measure_Space

13:32:18 HOL-Analysis: theory HOL-Analysis.Connected

13:32:20 HOL-Analysis: theory HOL-Analysis.Caratheodory

13:32:20 HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits

13:32:20 HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space

13:32:22 HOL-Analysis: theory HOL-Analysis.Tagged_Division

13:32:23 HOL-Analysis: theory HOL-Analysis.Summation_Tests

13:32:23 HOL-Analysis: theory HOL-Analysis.Starlike

13:32:24 HOL-Analysis: theory HOL-Analysis.Uniform_Limit

13:32:25 HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function

13:32:26 HOL-Analysis: theory HOL-Analysis.Continuous_Extension

13:32:27 HOL-Analysis: theory HOL-Analysis.Path_Connected

13:32:31 HOL-Analysis: theory HOL-Analysis.Homeomorphism

13:32:32 HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint

13:32:34 HOL-Analysis: theory HOL-Analysis.Derivative

13:32:36 HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space

13:32:36 HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems

13:32:37 Timing Matrix (2 threads, 44.420s elapsed time, 73.804s cpu time, 3.752s GC time, factor 1.66)

13:32:37 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Matrix

13:32:37 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Matrix/document.pdf

13:32:37 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Matrix/outline.pdf

13:32:37 Finished Matrix (0:01:09 elapsed time, 0:01:50 cpu time, factor 1.59)

13:32:37 Building Matrix_Tensor ...

13:32:38 Matrix_Tensor: theory Matrix_Tensor.Matrix_Tensor

13:32:38 HOL-Analysis: theory HOL-Analysis.Determinants

13:32:38 HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem

13:32:39 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space

13:32:39 HOL-Analysis: theory HOL-Analysis.Polytope

13:32:42 HOL-Analysis: theory HOL-Analysis.Arcwise_Connected

13:32:42 HOL-Analysis: theory HOL-Analysis.Borel_Space

13:32:45 HOL-Analysis: theory HOL-Analysis.Lipschitz

13:32:45 HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration

13:32:46 HOL-Analysis: theory HOL-Analysis.Regularity

13:32:47 HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure

13:32:49 HOL-Analysis: theory HOL-Analysis.Embed_Measure

13:32:49 HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure

13:32:50 HOL-Analysis: theory HOL-Analysis.Bochner_Integration

13:32:50 HOL-Analysis: theory HOL-Analysis.Function_Topology

13:32:52 HOL-Analysis: theory HOL-Analysis.Complete_Measure

13:32:52 HOL-Analysis: theory HOL-Analysis.Radon_Nikodym

13:32:52 HOL-Analysis: theory HOL-Analysis.Set_Integral

13:32:53 HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure

13:32:53 HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum

13:32:54 HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration

13:32:58 HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function

13:32:58 HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration

13:32:59 HOL-Analysis: theory HOL-Analysis.Integral_Test

13:33:00 HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics

13:33:00 HOL-Analysis: theory HOL-Analysis.Improper_Integral

13:33:01 HOL-Analysis: theory HOL-Analysis.Interval_Integral

13:33:02 HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution

13:33:02 Timing Free-Groups (2 threads, 89.902s elapsed time, 164.464s cpu time, 12.616s GC time, factor 1.83)

13:33:02 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Free-Groups

13:33:02 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Free-Groups/document.pdf

13:33:02 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Free-Groups/outline.pdf

13:33:02 Finished Free-Groups (0:01:35 elapsed time, 0:02:53 cpu time, factor 1.83)

13:33:02 HOL-Analysis: theory HOL-Analysis.Complex_Transcendental

13:33:04 HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem

13:33:04 HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers

13:33:04 HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem

13:33:04 HOL-Analysis: theory HOL-Analysis.Further_Topology

13:33:07 HOL-Analysis: theory HOL-Analysis.Jordan_Curve

13:33:08 HOL-Analysis: theory HOL-Analysis.Conformal_Mappings

13:33:09 HOL-Analysis: theory HOL-Analysis.FPS_Convergence

13:33:09 HOL-Analysis: theory HOL-Analysis.Gamma_Function

13:33:11 HOL-Analysis: theory HOL-Analysis.Great_Picard

13:33:12 HOL-Analysis: theory HOL-Analysis.Riemann_Mapping

13:33:13 HOL-Analysis: theory HOL-Analysis.Ball_Volume

13:33:13 HOL-Analysis: theory HOL-Analysis.Winding_Numbers

13:33:13 HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem

13:33:14 HOL-Analysis: theory HOL-Analysis.Change_Of_Vars

13:33:15 HOL-Analysis: theory HOL-Analysis.Analysis

13:33:33 Timing Matrix_Tensor (2 threads, 37.604s elapsed time, 55.796s cpu time, 2.740s GC time, factor 1.48)

13:33:33 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Matrix_Tensor

13:33:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Matrix_Tensor/document.pdf

13:33:33 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Matrix_Tensor/outline.pdf

13:33:33 Finished Matrix_Tensor (0:00:55 elapsed time, 0:01:23 cpu time, factor 1.50)

13:33:33 Running Knot_Theory ...

13:33:35 Knot_Theory: theory HOL-Computational_Algebra.Fraction_Field

13:33:35 Knot_Theory: theory HOL-Computational_Algebra.Factorial_Ring

13:33:36 Knot_Theory: theory Knot_Theory.Preliminaries

13:33:37 Knot_Theory: theory Knot_Theory.Tangles

13:33:37 Knot_Theory: theory Knot_Theory.Tangle_Algebra

13:33:39 Knot_Theory: theory Knot_Theory.Tangle_Relation

13:33:39 Knot_Theory: theory Knot_Theory.Tangle_Moves

13:33:39 Knot_Theory: theory Knot_Theory.Link_Algebra

13:33:40 Knot_Theory: theory Knot_Theory.Example

13:33:41 Knot_Theory: theory HOL-Computational_Algebra.Polynomial

13:33:45 Timing HOL-Algebra (2 threads, 84.202s elapsed time, 152.692s cpu time, 17.504s GC time, factor 1.81)

13:33:45 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Algebra

13:33:45 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Algebra/document.pdf

13:33:45 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Algebra/outline.pdf

13:33:45 Finished HOL-Algebra (0:02:17 elapsed time, 0:03:42 cpu time, factor 1.62)

13:33:45 Building JNF-HOL-Lib ...

13:33:45 Running VectorSpace ...

13:33:45 Running Jordan_Hoelder ...

13:33:45 Running Orbit_Stabiliser ...

13:33:45 Running Secondary_Sylow ...

13:33:47 VectorSpace: theory VectorSpace.RingModuleFacts

13:33:47 VectorSpace: theory VectorSpace.FunctionLemmas

13:33:47 Secondary_Sylow: theory Secondary_Sylow.GroupAction

13:33:47 Jordan_Hoelder: theory Secondary_Sylow.GroupAction

13:33:47 Jordan_Hoelder: theory Jordan_Hoelder.GroupIsoClasses

13:33:47 JNF-HOL-Lib: theory HOL-Cardinals.Order_Union

13:33:47 Orbit_Stabiliser: theory Orbit_Stabiliser.Left_Coset

13:33:47 JNF-HOL-Lib: theory HOL-Cardinals.Wellorder_Extension

13:33:47 Orbit_Stabiliser: theory Orbit_Stabiliser.Orbit_Stabiliser

13:33:48 Orbit_Stabiliser: theory Orbit_Stabiliser.Tetrahedron

13:33:48 Secondary_Sylow: theory Secondary_Sylow.SubgroupConjugation

13:33:48 Jordan_Hoelder: theory Secondary_Sylow.SubgroupConjugation

13:33:48 Secondary_Sylow: theory Secondary_Sylow.SndSylow

13:33:48 Jordan_Hoelder: theory Secondary_Sylow.SndSylow

13:33:48 VectorSpace: theory VectorSpace.MonoidSums

13:33:48 Jordan_Hoelder: theory Jordan_Hoelder.SndIsomorphismGrp

13:33:48 Jordan_Hoelder: theory Jordan_Hoelder.SubgroupsAndNormalSubgroups

13:33:48 Knot_Theory: theory Knot_Theory.Kauffman_Matrix

13:33:48 VectorSpace: theory VectorSpace.LinearCombinations

13:33:49 Jordan_Hoelder: theory Jordan_Hoelder.SimpleGroups

13:33:49 Jordan_Hoelder: theory Jordan_Hoelder.MaximalNormalSubgroups

13:33:49 Jordan_Hoelder: theory Jordan_Hoelder.CompositionSeries

13:33:50 Jordan_Hoelder: theory Jordan_Hoelder.JordanHolder

13:33:51 Knot_Theory: theory Knot_Theory.Computations

13:33:51 Knot_Theory: theory Knot_Theory.Linkrel_Kauffman

13:33:52 Knot_Theory: theory Knot_Theory.Kauffman_Invariance

13:33:52 Knot_Theory: theory Knot_Theory.Knot_Theory

13:33:54 VectorSpace: theory VectorSpace.SumSpaces

13:33:54 VectorSpace: theory VectorSpace.VectorSpace

13:33:57 Timing Secondary_Sylow (2 threads, 5.410s elapsed time, 9.576s cpu time, 0.516s GC time, factor 1.77)

13:33:57 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Secondary_Sylow

13:33:57 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Secondary_Sylow/document.pdf

13:33:57 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Secondary_Sylow/outline.pdf

13:33:57 Finished Secondary_Sylow (0:00:11 elapsed time, 0:00:18 cpu time, factor 1.69)

13:33:57 Timing HOL-Number_Theory (2 threads, 102.270s elapsed time, 184.820s cpu time, 12.580s GC time, factor 1.81)

13:33:57 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Number_Theory

13:33:57 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Number_Theory/document.pdf

13:33:57 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Number_Theory/outline.pdf

13:33:57 Finished HOL-Number_Theory (0:02:29 elapsed time, 0:04:07 cpu time, factor 1.65)

13:33:57 Running Bertrands_Postulate ...

13:33:57 Running Elliptic_Curves_Group_Law ...

13:33:59 Bertrands_Postulate: theory HOL-Decision_Procs.Dense_Linear_Order

13:33:59 Bertrands_Postulate: theory Lehmer.Lehmer

13:33:59 Elliptic_Curves_Group_Law: theory HOL-Decision_Procs.Conversions

13:33:59 Elliptic_Curves_Group_Law: theory HOL-Decision_Procs.Algebra_Aux

13:33:59 Bertrands_Postulate: theory Pratt_Certificate.Pratt_Certificate

13:34:00 Elliptic_Curves_Group_Law: theory HOL-Decision_Procs.Commutative_Ring

13:34:02 Bertrands_Postulate: theory HOL-Decision_Procs.Approximation_Bounds

13:34:03 Timing Orbit_Stabiliser (2 threads, 11.803s elapsed time, 15.984s cpu time, 0.696s GC time, factor 1.35)

13:34:03 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Orbit_Stabiliser

13:34:03 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Orbit_Stabiliser/document.pdf

13:34:03 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Orbit_Stabiliser/outline.pdf

13:34:03 Finished Orbit_Stabiliser (0:00:17 elapsed time, 0:00:25 cpu time, factor 1.40)

13:34:03 Running Koenigsberg_Friendship ...

13:34:05 Koenigsberg_Friendship: theory Dijkstra_Shortest_Path.Graph

13:34:06 Koenigsberg_Friendship: theory Koenigsberg_Friendship.MoreGraph

13:34:06 Timing JNF-HOL-Lib (2 threads, 1.580s elapsed time, 2.644s cpu time, 0.000s GC time, factor 1.67)

13:34:06 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/JNF-HOL-Lib

13:34:06 Finished JNF-HOL-Lib (0:00:21 elapsed time, 0:00:27 cpu time, factor 1.29)

13:34:06 Building JNF-AFP-Lib ...

13:34:07 Bertrands_Postulate: theory Bertrands_Postulate.Bertrand

13:34:10 Timing Jordan_Hoelder (2 threads, 17.491s elapsed time, 31.824s cpu time, 1.416s GC time, factor 1.82)

13:34:10 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Hoelder

13:34:10 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Hoelder/document.pdf

13:34:10 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Hoelder/outline.pdf

13:34:10 Finished Jordan_Hoelder (0:00:24 elapsed time, 0:00:42 cpu time, factor 1.75)

13:34:10 Running RSAPSS ...

13:34:10 Koenigsberg_Friendship: theory Koenigsberg_Friendship.FriendshipTheory

13:34:11 Koenigsberg_Friendship: theory Koenigsberg_Friendship.KoenigsbergBridge

13:34:11 Elliptic_Curves_Group_Law: theory HOL-Decision_Procs.Reflective_Field

13:34:12 RSAPSS: theory RSAPSS.Word

13:34:14 JNF-AFP-Lib: theory Containers.Equal

13:34:14 JNF-AFP-Lib: theory Containers.Extend_Partial_Order

13:34:14 JNF-AFP-Lib: theory Containers.Closure_Set

13:34:14 JNF-AFP-Lib: theory Containers.List_Fusion

13:34:14 JNF-AFP-Lib: theory Deriving.Comparator

13:34:14 JNF-AFP-Lib: theory Deriving.Compare

13:34:15 JNF-AFP-Lib: theory Deriving.Derive_Manager

13:34:15 JNF-AFP-Lib: theory Deriving.Generator_Aux

13:34:15 JNF-AFP-Lib: theory Deriving.Comparator_Generator

13:34:15 JNF-AFP-Lib: theory Deriving.Equality_Generator

13:34:15 JNF-AFP-Lib: theory Deriving.Equality_Instances

13:34:16 JNF-AFP-Lib: theory Containers.Lexicographic_Order

13:34:16 JNF-AFP-Lib: theory Deriving.Compare_Generator

13:34:16 JNF-AFP-Lib: theory Gauss_Jordan.IArray_Addenda

13:34:16 JNF-AFP-Lib: theory Gauss_Jordan.IArray_Haskell

13:34:16 JNF-AFP-Lib: theory Abstract-Rewriting.Seq

13:34:16 JNF-AFP-Lib: theory Deriving.Compare_Instances

13:34:16 RSAPSS: theory RSAPSS.Mod

13:34:16 RSAPSS: theory RSAPSS.WordOperations

13:34:17 RSAPSS: theory RSAPSS.Crypt

13:34:17 RSAPSS: theory RSAPSS.Pdifference

13:34:17 JNF-AFP-Lib: theory Containers.Containers_Auxiliary

13:34:17 RSAPSS: theory RSAPSS.Productdivides

13:34:17 JNF-AFP-Lib: theory Containers.Containers_Generator

13:34:17 JNF-AFP-Lib: theory Containers.Set_Linorder

13:34:17 RSAPSS: theory RSAPSS.Cryptinverts

13:34:18 JNF-AFP-Lib: theory Containers.Collection_Enum

13:34:18 JNF-AFP-Lib: theory Containers.Collection_Eq

13:34:19 RSAPSS: theory RSAPSS.SHA1Padding

13:34:19 RSAPSS: theory RSAPSS.SHA1

13:34:19 RSAPSS: theory RSAPSS.Wordarith

13:34:19 JNF-AFP-Lib: theory Containers.DList_Set

13:34:20 JNF-AFP-Lib: theory Containers.RBT_ext

13:34:20 RSAPSS: theory RSAPSS.EMSAPSS

13:34:21 RSAPSS: theory RSAPSS.RSAPSS

13:34:22 JNF-AFP-Lib: theory Deriving.RBT_Comparator_Impl

13:34:23 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Axclass

13:34:23 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Locale

13:34:27 JNF-AFP-Lib: theory Polynomial_Interpolation.Missing_Unsorted

13:34:27 Elliptic_Curves_Group_Law: theory Elliptic_Curves_Group_Law.Elliptic_Test

13:34:28 JNF-AFP-Lib: theory Containers.Collection_Order

13:34:29 JNF-AFP-Lib: theory Polynomial_Interpolation.Missing_Polynomial

13:34:30 JNF-AFP-Lib: theory Matrix.Utility

13:34:31 JNF-AFP-Lib: theory Polynomial_Interpolation.Ring_Hom

13:34:31 JNF-AFP-Lib: theory Containers.RBT_Mapping2

13:34:33 JNF-AFP-Lib: theory Containers.RBT_Set2

13:34:34 JNF-AFP-Lib: theory Polynomial_Interpolation.Ring_Hom_Poly

13:34:34 JNF-AFP-Lib: theory Containers.Set_Impl

13:34:34 Timing VectorSpace (2 threads, 42.626s elapsed time, 73.452s cpu time, 6.116s GC time, factor 1.72)

13:34:34 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/VectorSpace

13:34:34 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/VectorSpace/document.pdf

13:34:34 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/VectorSpace/outline.pdf

13:34:34 Finished VectorSpace (0:00:49 elapsed time, 0:01:23 cpu time, factor 1.69)

13:34:34 Running Pratt_Certificate ...

13:34:36 JNF-AFP-Lib: theory Regular-Sets.Regular_Set

13:34:36 Pratt_Certificate: theory Lehmer.Lehmer

13:34:36 Pratt_Certificate: theory Pratt_Certificate.Pratt_Certificate

13:34:38 Timing RSAPSS (2 threads, 21.728s elapsed time, 41.532s cpu time, 1.724s GC time, factor 1.91)

13:34:38 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/RSAPSS

13:34:38 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/RSAPSS/document.pdf

13:34:38 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/RSAPSS/outline.pdf

13:34:38 Finished RSAPSS (0:00:27 elapsed time, 0:00:51 cpu time, factor 1.83)

13:34:38 Running Fermat3_4 ...

13:34:40 Fermat3_4: theory Fermat3_4.Fermat4

13:34:40 Fermat3_4: theory Fermat3_4.Quad_Form

13:34:40 JNF-AFP-Lib: theory Regular-Sets.Regular_Exp

13:34:40 Fermat3_4: theory Fermat3_4.Fermat3

13:34:44 JNF-AFP-Lib: theory Regular-Sets.NDerivative

13:34:48 JNF-AFP-Lib: theory Regular-Sets.Equivalence_Checking

13:34:49 JNF-AFP-Lib: theory Regular-Sets.Relation_Interpretation

13:34:49 JNF-AFP-Lib: theory Regular-Sets.Regexp_Method

13:34:49 Timing Knot_Theory (2 threads, 69.292s elapsed time, 133.400s cpu time, 6.196s GC time, factor 1.93)

13:34:49 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Knot_Theory

13:34:49 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Knot_Theory/document.pdf

13:34:49 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Knot_Theory/outline.pdf

13:34:49 Finished Knot_Theory (0:01:16 elapsed time, 0:02:23 cpu time, factor 1.88)

13:34:49 Running SumSquares ...

13:34:49 JNF-AFP-Lib: theory Abstract-Rewriting.Abstract_Rewriting

13:34:51 JNF-AFP-Lib: theory Abstract-Rewriting.Relative_Rewriting

13:34:52 SumSquares: theory SumSquares.TwoSquares

13:34:52 SumSquares: theory SumSquares.FourSquares

13:34:56 JNF-AFP-Lib: theory Abstract-Rewriting.SN_Orders

13:34:58 JNF-AFP-Lib: theory Show.Show

13:34:58 JNF-AFP-Lib: theory Abstract-Rewriting.SN_Order_Carrier

13:34:59 JNF-AFP-Lib: theory Matrix.Ordered_Semiring

13:35:00 JNF-AFP-Lib: theory Show.Show_Instances

13:35:01 Timing Pratt_Certificate (2 threads, 20.578s elapsed time, 39.804s cpu time, 0.756s GC time, factor 1.93)

13:35:01 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pratt_Certificate

13:35:01 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pratt_Certificate/document.pdf

13:35:01 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pratt_Certificate/outline.pdf

13:35:01 Finished Pratt_Certificate (0:00:26 elapsed time, 0:00:48 cpu time, factor 1.82)

13:35:01 Running Perfect-Number-Thm ...

13:35:02 JNF-AFP-Lib: theory VectorSpace.FunctionLemmas

13:35:02 JNF-AFP-Lib: theory VectorSpace.RingModuleFacts

13:35:02 Timing Fermat3_4 (2 threads, 17.769s elapsed time, 31.956s cpu time, 0.756s GC time, factor 1.80)

13:35:02 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Fermat3_4

13:35:02 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Fermat3_4/document.pdf

13:35:02 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Fermat3_4/outline.pdf

13:35:02 Finished Fermat3_4 (0:00:24 elapsed time, 0:00:41 cpu time, factor 1.70)

13:35:02 Running Lehmer ...

13:35:03 Perfect-Number-Thm: theory Perfect-Number-Thm.PerfectBasics

13:35:03 JNF-AFP-Lib: theory VectorSpace.MonoidSums

13:35:03 Timing SumSquares (2 threads, 7.317s elapsed time, 13.688s cpu time, 0.348s GC time, factor 1.87)

13:35:03 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/SumSquares

13:35:03 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/SumSquares/document.pdf

13:35:03 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/SumSquares/outline.pdf

13:35:03 Finished SumSquares (0:00:13 elapsed time, 0:00:22 cpu time, factor 1.69)

13:35:03 Perfect-Number-Thm: theory Perfect-Number-Thm.Sigma

13:35:03 JNF-AFP-Lib: theory VectorSpace.LinearCombinations

13:35:03 Perfect-Number-Thm: theory Perfect-Number-Thm.Perfect

13:35:05 Lehmer: theory Lehmer.Lehmer

13:35:08 JNF-AFP-Lib: theory VectorSpace.SumSpaces

13:35:08 JNF-AFP-Lib: theory VectorSpace.VectorSpace

13:35:09 Timing Perfect-Number-Thm (2 threads, 1.697s elapsed time, 3.340s cpu time, 0.000s GC time, factor 1.97)

13:35:09 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Perfect-Number-Thm

13:35:09 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Perfect-Number-Thm/document.pdf

13:35:09 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Perfect-Number-Thm/outline.pdf

13:35:09 Finished Perfect-Number-Thm (0:00:07 elapsed time, 0:00:11 cpu time, factor 1.58)

13:35:10 Timing Lehmer (2 threads, 1.332s elapsed time, 2.340s cpu time, 0.000s GC time, factor 1.76)

13:35:10 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lehmer

13:35:10 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lehmer/document.pdf

13:35:10 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Lehmer/outline.pdf

13:35:10 Finished Lehmer (0:00:06 elapsed time, 0:00:10 cpu time, factor 1.54)

13:35:10 Timing Elliptic_Curves_Group_Law (2 threads, 65.145s elapsed time, 122.500s cpu time, 6.472s GC time, factor 1.88)

13:35:10 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Elliptic_Curves_Group_Law

13:35:10 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Elliptic_Curves_Group_Law/document.pdf

13:35:10 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Elliptic_Curves_Group_Law/outline.pdf

13:35:10 Finished Elliptic_Curves_Group_Law (0:01:12 elapsed time, 0:02:12 cpu time, factor 1.84)

13:35:11 Timing Koenigsberg_Friendship (2 threads, 59.915s elapsed time, 109.124s cpu time, 4.872s GC time, factor 1.82)

13:35:11 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Koenigsberg_Friendship

13:35:11 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Koenigsberg_Friendship/document.pdf

13:35:11 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Koenigsberg_Friendship/outline.pdf

13:35:11 Finished Koenigsberg_Friendship (0:01:07 elapsed time, 0:01:59 cpu time, factor 1.78)

13:35:23 Timing Bertrands_Postulate (2 threads, 79.613s elapsed time, 153.304s cpu time, 3.484s GC time, factor 1.93)

13:35:23 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Bertrands_Postulate

13:35:23 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Bertrands_Postulate/document.pdf

13:35:23 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Bertrands_Postulate/outline.pdf

13:35:23 Finished Bertrands_Postulate (0:01:25 elapsed time, 0:02:44 cpu time, factor 1.91)

13:37:00 Timing JNF-AFP-Lib (2 threads, 135.048s elapsed time, 252.680s cpu time, 23.620s GC time, factor 1.87)

13:37:00 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/JNF-AFP-Lib

13:37:00 Finished JNF-AFP-Lib (0:02:52 elapsed time, 0:05:09 cpu time, factor 1.80)

13:37:00 Building Jordan_Normal_Form ...

13:37:00 Building Pre_Polynomial_Factorization ...

13:37:02 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Ring

13:37:03 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Neville_Aitken_Interpolation

13:37:03 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Improved_Code_Equations

13:37:03 Pre_Polynomial_Factorization: theory Cauchy.CauchysMeanTheorem

13:37:03 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Lagrange_Interpolation

13:37:03 Pre_Polynomial_Factorization: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary

13:37:04 Pre_Polynomial_Factorization: theory Partial_Function_MR.Partial_Function_MR

13:37:04 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Divmod_Int

13:37:04 Pre_Polynomial_Factorization: theory Show.Show_Poly

13:37:04 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Is_Rat_To_Rat

13:37:05 Pre_Polynomial_Factorization: theory Sqrt_Babylonian.Log_Impl

13:37:05 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Newton_Interpolation

13:37:05 Pre_Polynomial_Factorization: theory Sqrt_Babylonian.NthRoot_Impl

13:37:06 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_Permutations

13:37:06 Pre_Polynomial_Factorization: theory Sqrt_Babylonian.Sqrt_Babylonian

13:37:07 Jordan_Normal_Form: theory Jordan_Normal_Form.Conjugate

13:37:07 Jordan_Normal_Form: theory Polynomial_Factorization.Order_Polynomial

13:37:07 Jordan_Normal_Form: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized

13:37:08 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix

13:37:08 Pre_Polynomial_Factorization: theory Polynomial_Interpolation.Polynomial_Interpolation

13:37:10 Jordan_Normal_Form: theory Jordan_Normal_Form.Derivation_Bound

13:37:10 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Arctic

13:37:10 Jordan_Normal_Form: theory Jordan_Normal_Form.Missing_VectorSpace

13:37:13 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_Elimination

13:37:13 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_IArray_Impl

13:37:15 Jordan_Normal_Form: theory Jordan_Normal_Form.Column_Operations

13:37:15 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant

13:37:16 Jordan_Normal_Form: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl

13:37:18 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm

13:37:18 Jordan_Normal_Form: theory Jordan_Normal_Form.Determinant_Impl

13:37:20 Jordan_Normal_Form: theory Jordan_Normal_Form.Strassen_Algorithm_Code

13:37:20 Jordan_Normal_Form: theory Jordan_Normal_Form.Ring_Hom_Matrix

13:37:20 Jordan_Normal_Form: theory Jordan_Normal_Form.Char_Poly

13:37:21 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form

13:37:22 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Comparison

13:37:22 Jordan_Normal_Form: theory Jordan_Normal_Form.Complexity_Carrier

13:37:23 Jordan_Normal_Form: theory Jordan_Normal_Form.Show_Matrix

13:37:25 Jordan_Normal_Form: theory Jordan_Normal_Form.VS_Connect

13:37:26 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Complexity

13:37:30 Jordan_Normal_Form: theory Jordan_Normal_Form.Gram_Schmidt

13:37:30 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Kernel

13:37:31 Jordan_Normal_Form: theory Jordan_Normal_Form.Schur_Decomposition

13:37:32 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness

13:37:35 Jordan_Normal_Form: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence

13:37:39 Jordan_Normal_Form: theory Jordan_Normal_Form.Matrix_Impl

13:37:39 Jordan_Normal_Form: theory Jordan_Normal_Form.Spectral_Radius

13:37:47 Timing Pre_Polynomial_Factorization (2 threads, 22.425s elapsed time, 43.144s cpu time, 2.444s GC time, factor 1.92)

13:37:47 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pre_Polynomial_Factorization

13:37:47 Finished Pre_Polynomial_Factorization (0:00:46 elapsed time, 0:01:15 cpu time, factor 1.62)

13:37:47 Running Polynomial_Factorization ...

13:37:50 Polynomial_Factorization: theory Polynomial_Factorization.Precomputation

13:37:50 Polynomial_Factorization: theory Polynomial_Factorization.Missing_Polynomial_Factorial

13:37:50 Polynomial_Factorization: theory Polynomial_Factorization.Order_Polynomial

13:37:50 Polynomial_Factorization: theory Polynomial_Factorization.Polynomial_Divisibility

13:37:50 Polynomial_Factorization: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized

13:37:50 Polynomial_Factorization: theory Polynomial_Factorization.Explicit_Roots

13:37:50 Polynomial_Factorization: theory Polynomial_Factorization.Missing_List

13:37:51 Polynomial_Factorization: theory Polynomial_Factorization.Dvd_Int_Poly

13:37:51 Polynomial_Factorization: theory Polynomial_Factorization.Gauss_Lemma

13:37:53 Polynomial_Factorization: theory Polynomial_Factorization.Gcd_Rat_Poly

13:37:53 Polynomial_Factorization: theory Polynomial_Factorization.Missing_Multiset

13:37:53 Polynomial_Factorization: theory Polynomial_Factorization.Square_Free_Factorization

13:37:53 Polynomial_Factorization: theory Polynomial_Factorization.Prime_Factorization

13:37:54 Polynomial_Factorization: theory Polynomial_Factorization.Rational_Root_Test

13:37:55 Polynomial_Factorization: theory Polynomial_Factorization.Kronecker_Factorization

13:37:57 Polynomial_Factorization: theory Polynomial_Factorization.Rational_Factorization

13:38:41 Timing Polynomial_Factorization (2 threads, 45.743s elapsed time, 75.100s cpu time, 3.404s GC time, factor 1.64)

13:38:41 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Polynomial_Factorization

13:38:41 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Polynomial_Factorization/document.pdf

13:38:41 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Polynomial_Factorization/outline.pdf

13:38:41 Finished Polynomial_Factorization (0:00:54 elapsed time, 0:01:28 cpu time, factor 1.64)

13:41:46 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_List

13:41:46 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Missing_Sublist

13:41:46 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank

13:41:46 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Submatrix

13:41:52 Jordan_Normal_Form: theory Jordan_Normal_Form.DL_Rank_Submatrix

13:42:55 Timing Jordan_Normal_Form (2 threads, 296.390s elapsed time, 476.448s cpu time, 19.060s GC time, factor 1.61)

13:42:55 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Normal_Form

13:42:55 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Normal_Form/document.pdf

13:42:55 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Jordan_Normal_Form/outline.pdf

13:42:55 Finished Jordan_Normal_Form (0:05:54 elapsed time, 0:09:15 cpu time, factor 1.57)

13:42:55 Building Subresultants ...

13:42:59 Subresultants: theory Polynomial_Factorization.Missing_Polynomial_Factorial

13:42:59 Subresultants: theory Subresultants.Coeff_Int

13:42:59 Subresultants: theory Subresultants.Dichotomous_Lazard

13:42:59 Subresultants: theory Subresultants.More_Homomorphisms

13:42:59 Subresultants: theory Subresultants.Resultant_Prelim

13:43:00 Subresultants: theory Subresultants.Binary_Exponentiation

13:43:00 Subresultants: theory Subresultants.Subresultant

13:43:04 Subresultants: theory Subresultants.Subresultant_Gcd

13:44:27 Timing Subresultants (2 threads, 63.394s elapsed time, 95.060s cpu time, 3.384s GC time, factor 1.50)

13:44:27 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Subresultants

13:44:27 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Subresultants/document.pdf

13:44:27 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Subresultants/outline.pdf

13:44:27 Finished Subresultants (0:01:31 elapsed time, 0:02:16 cpu time, factor 1.50)

13:44:27 Building Pre_BZ ...

13:44:31 Pre_BZ: theory Efficient-Mergesort.Efficient_Sort

13:44:31 Pre_BZ: theory HOL-Number_Theory.Cong

13:44:33 Pre_BZ: theory Polynomial_Factorization.Precomputation

13:44:33 Pre_BZ: theory HOL-Types_To_Sets.Types_To_Sets

13:44:33 Pre_BZ: theory HOL-Word.Bits

13:44:33 Pre_BZ: theory HOL-Word.Bits_Bit

13:44:33 Pre_BZ: theory HOL-Word.Misc_Numeric

13:44:33 Pre_BZ: theory HOL-Word.Bit_Representation

13:44:34 Pre_BZ: theory HOL-Word.Bits_Int

13:44:36 Pre_BZ: theory HOL-Word.Bool_List_Representation

13:44:36 Pre_BZ: theory Native_Word.More_Bits_Int

13:44:37 Pre_BZ: theory HOL-Word.Word_Miscellaneous

13:44:38 Pre_BZ: theory HOL-Word.Misc_Typedef

13:44:38 Pre_BZ: theory HOL-Word.Word

13:44:38 Pre_BZ: theory Native_Word.Bits_Integer

13:44:42 Pre_BZ: theory Native_Word.Word_Misc

13:44:43 Pre_BZ: theory Polynomial_Interpolation.Improved_Code_Equations

13:44:43 Pre_BZ: theory Polynomial_Interpolation.Neville_Aitken_Interpolation

13:44:44 Pre_BZ: theory Cauchy.CauchysMeanTheorem

13:44:44 Pre_BZ: theory Polynomial_Factorization.Polynomial_Divisibility

13:44:44 Pre_BZ: theory Polynomial_Interpolation.Lagrange_Interpolation

13:44:45 Pre_BZ: theory HOL-Number_Theory.Totient

13:44:45 Pre_BZ: theory HOL-Number_Theory.Residues

13:44:47 Pre_BZ: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary

13:44:49 Pre_BZ: theory Native_Word.Code_Target_Bits_Int

13:44:50 Pre_BZ: theory Native_Word.Uint32

13:44:50 Pre_BZ: theory Native_Word.Uint64

13:44:51 Pre_BZ: theory Polynomial_Interpolation.Is_Rat_To_Rat

13:44:52 Pre_BZ: theory Sqrt_Babylonian.Log_Impl

13:44:52 Pre_BZ: theory Sqrt_Babylonian.NthRoot_Impl

13:44:52 Pre_BZ: theory Polynomial_Factorization.Missing_List

13:44:52 Pre_BZ: theory Sqrt_Babylonian.Sqrt_Babylonian

13:44:53 Timing HOL-Analysis (2 threads, 720.782s elapsed time, 1295.160s cpu time, 56.096s GC time, factor 1.80)

13:44:53 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Analysis

13:44:53 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Analysis/document.pdf

13:44:53 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Analysis/manual.pdf

13:44:53 Finished HOL-Analysis (0:13:24 elapsed time, 0:23:28 cpu time, factor 1.75)

13:44:53 Building HOL-Probability ...

13:44:53 Building Landau_Analysis ...

13:44:53 Building Dirichlet_Series ...

13:44:53 Building Affine_Arithmetic ...

13:44:53 Building Echelon_Form ...

13:44:53 Building Ordinary_Differential_Equations ...

13:44:53 Running QR_Decomposition ...

13:44:53 Pre_BZ: theory Polynomial_Factorization.Explicit_Roots

13:44:54 Pre_BZ: theory Polynomial_Interpolation.Divmod_Int

13:44:54 Pre_BZ: theory Polynomial_Factorization.Dvd_Int_Poly

13:44:54 HOL-Probability: theory HOL-Library.Adhoc_Overloading

13:44:54 HOL-Probability: theory HOL-Library.Lattice_Syntax

13:44:54 Landau_Analysis: theory HOL-Library.Function_Algebras

13:44:54 Landau_Analysis: theory Landau_Symbols.Landau_Library

13:44:54 HOL-Probability: theory HOL-Library.AList

13:44:54 Echelon_Form: theory HOL-Library.Bit

13:44:54 Echelon_Form: theory HOL-Computational_Algebra.Fraction_Field

13:44:54 HOL-Probability: theory HOL-Library.Complete_Partial_Order2

13:44:54 Affine_Arithmetic: theory HOL-Library.Adhoc_Overloading

13:44:54 Affine_Arithmetic: theory Deriving.Comparator

13:44:54 Landau_Analysis: theory Landau_Symbols.Group_Sort

13:44:54 Landau_Analysis: theory Landau_Symbols.Landau_Symbols_Definition

13:44:54 Affine_Arithmetic: theory Deriving.Derive_Manager

13:44:54 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Dense_Linear_Order

13:44:54 Ordinary_Differential_Equations: theory HOL-Library.Code_Abstract_Nat

13:44:54 Affine_Arithmetic: theory Deriving.Generator_Aux

13:44:54 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Nat

13:44:54 QR_Decomposition: theory Deriving.Generator_Aux

13:44:54 QR_Decomposition: theory Deriving.Derive_Manager

13:44:54 Dirichlet_Series: theory HOL-Library.Adhoc_Overloading

13:44:54 Dirichlet_Series: theory HOL-Computational_Algebra.Fraction_Field

13:44:55 QR_Decomposition: theory HOL-Library.Bit

13:44:55 Affine_Arithmetic: theory Deriving.Equality_Generator

13:44:55 Dirichlet_Series: theory HOL-Computational_Algebra.Group_Closure

13:44:55 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Int

13:44:55 Echelon_Form: theory Gauss_Jordan.Code_Bit

13:44:55 Echelon_Form: theory HOL-Library.Code_Abstract_Nat

13:44:55 QR_Decomposition: theory Real_Impl.Real_Impl_Auxiliary

13:44:55 Pre_BZ: theory Polynomial_Factorization.Gauss_Lemma

13:44:55 QR_Decomposition: theory HOL-Library.Code_Abstract_Nat

13:44:55 Echelon_Form: theory HOL-Library.Code_Target_Nat

13:44:55 QR_Decomposition: theory HOL-Library.Code_Target_Nat

13:44:55 Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral

13:44:55 Echelon_Form: theory HOL-Library.Code_Target_Int

13:44:55 QR_Decomposition: theory HOL-Library.Code_Target_Int

13:44:55 Ordinary_Differential_Equations: theory HOL-Word.Bits

13:44:55 Affine_Arithmetic: theory Deriving.Equality_Instances

13:44:55 QR_Decomposition: theory Gauss_Jordan.Code_Bit

13:44:55 Pre_BZ: theory Polynomial_Factorization.Missing_Multiset

13:44:55 QR_Decomposition: theory HOL-Library.Function_Algebras

13:44:55 Echelon_Form: theory HOL-Library.Code_Target_Numeral

13:44:55 Ordinary_Differential_Equations: theory HOL-Word.Misc_Numeric

13:44:55 Affine_Arithmetic: theory HOL-Decision_Procs.Dense_Linear_Order

13:44:55 QR_Decomposition: theory HOL-Library.Code_Target_Numeral

13:44:55 Affine_Arithmetic: theory Deriving.Compare

13:44:55 Ordinary_Differential_Equations: theory HOL-Word.Bit_Representation

13:44:55 Dirichlet_Series: theory HOL-Computational_Algebra.Nth_Powers

13:44:55 QR_Decomposition: theory HOL-Library.IArray

13:44:55 Echelon_Form: theory HOL-Library.Function_Algebras

13:44:55 QR_Decomposition: theory Gauss_Jordan.Code_Set

13:44:55 Echelon_Form: theory HOL-Computational_Algebra.Normalized_Fraction

13:44:55 QR_Decomposition: theory Cauchy.CauchysMeanTheorem

13:44:55 Pre_BZ: theory Polynomial_Factorization.Prime_Factorization

13:44:55 Echelon_Form: theory HOL-Library.IArray

13:44:56 Dirichlet_Series: theory HOL-Computational_Algebra.Squarefree

13:44:56 QR_Decomposition: theory HOL-Library.Code_Real_Approx_By_Float

13:44:56 Dirichlet_Series: theory HOL-Computational_Algebra.Normalized_Fraction

13:44:56 Pre_BZ: theory Polynomial_Factorization.Gcd_Rat_Poly

13:44:56 Dirichlet_Series: theory HOL-Number_Theory.Cong

13:44:56 HOL-Probability: theory HOL-Library.Mapping

13:44:56 Affine_Arithmetic: theory Deriving.Comparator_Generator

13:44:56 Ordinary_Differential_Equations: theory HOL-Word.Bits_Int

13:44:56 Echelon_Form: theory HOL-Library.More_List

13:44:56 Pre_BZ: theory Polynomial_Factorization.Rational_Root_Test

13:44:56 Pre_BZ: theory Polynomial_Factorization.Square_Free_Factorization

13:44:56 Dirichlet_Series: theory HOL-Library.Code_Abstract_Nat

13:44:56 Echelon_Form: theory Gauss_Jordan.Code_Set

13:44:56 Dirichlet_Series: theory HOL-Library.Code_Target_Nat

13:44:56 QR_Decomposition: theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell

13:44:56 Echelon_Form: theory HOL-Computational_Algebra.Polynomial

13:44:56 QR_Decomposition: theory Rank_Nullity_Theorem.Generalizations

13:44:56 QR_Decomposition: theory QR_Decomposition.IArray_Addenda_QR

13:44:57 Dirichlet_Series: theory HOL-Library.Code_Target_Int

13:44:57 Echelon_Form: theory Gauss_Jordan.IArray_Addenda

13:44:57 Dirichlet_Series: theory HOL-Library.Code_Target_Numeral

13:44:57 QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary

13:44:57 Echelon_Form: theory HOL-Computational_Algebra.Field_as_Ring

13:44:57 Affine_Arithmetic: theory Deriving.Compare_Generator

13:44:57 Pre_BZ: theory Polynomial_Interpolation.Newton_Interpolation

13:44:57 Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence

13:44:57 Dirichlet_Series: theory HOL-Algebra.Congruence

13:44:57 Dirichlet_Series: theory HOL-Library.Function_Algebras

13:44:57 Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras

13:44:57 HOL-Probability: theory HOL-Library.AList_Mapping

13:44:57 Dirichlet_Series: theory HOL-Library.Monad_Syntax

13:44:57 QR_Decomposition: theory Sqrt_Babylonian.Log_Impl

13:44:57 Affine_Arithmetic: theory HOL-Library.Bit

13:44:57 Dirichlet_Series: theory HOL-Library.More_List

13:44:57 HOL-Probability: theory HOL-Library.Monad_Syntax

13:44:57 QR_Decomposition: theory Sqrt_Babylonian.NthRoot_Impl

13:44:57 Ordinary_Differential_Equations: theory HOL-Word.Bool_List_Representation

13:44:58 HOL-Probability: theory HOL-Library.Stream

13:44:58 HOL-Probability: theory HOL-Library.Rewrite

13:44:58 Dirichlet_Series: theory HOL-Library.Stirling

13:44:58 Landau_Analysis: theory Landau_Symbols.Asymptotic_Equivalence

13:44:58 Affine_Arithmetic: theory HOL-Library.Boolean_Algebra

13:44:58 Affine_Arithmetic: theory HOL-Library.Permutation

13:44:58 HOL-Probability: theory HOL-Library.Sublist

13:44:58 Affine_Arithmetic: theory HOL-Library.Char_ord

13:44:58 Dirichlet_Series: theory HOL-Algebra.Order

13:44:58 Affine_Arithmetic: theory HOL-Library.Code_Abstract_Nat

13:44:58 Affine_Arithmetic: theory HOL-Library.Code_Target_Nat

13:44:58 Dirichlet_Series: theory HOL-Number_Theory.Eratosthenes

13:44:58 Affine_Arithmetic: theory Deriving.Compare_Instances

13:44:58 Echelon_Form: theory Cayley_Hamilton.Square_Matrix

13:44:58 Landau_Analysis: theory Landau_Symbols.Landau_Real_Products

13:44:58 Affine_Arithmetic: theory HOL-Library.Code_Char

13:44:58 QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian

13:44:58 Affine_Arithmetic: theory HOL-Library.Code_Target_Int

13:44:58 Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial

13:44:58 Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral

13:44:58 Ordinary_Differential_Equations: theory HOL-Library.Log_Nat

13:44:58 QR_Decomposition: theory Rank_Nullity_Theorem.Dual_Order

13:44:59 Affine_Arithmetic: theory HOL-Library.Mapping

13:44:59 Ordinary_Differential_Equations: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities

13:44:59 QR_Decomposition: theory Rank_Nullity_Theorem.Mod_Type

13:44:59 Affine_Arithmetic: theory HOL-Library.Monad_Syntax

13:44:59 QR_Decomposition: theory Real_Impl.Prime_Product

13:44:59 Affine_Arithmetic: theory HOL-Library.Type_Length

13:44:59 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator

13:44:59 Pre_BZ: theory Show.Show_Poly

13:44:59 HOL-Probability: theory HOL-Library.Tree

13:44:59 Affine_Arithmetic: theory HOL-Library.RBT_Impl

13:44:59 Dirichlet_Series: theory HOL-Algebra.Lattice

13:45:00 HOL-Probability: theory HOL-Library.FSet

13:45:00 Affine_Arithmetic: theory HOL-Word.Bits

13:45:00 QR_Decomposition: theory Real_Impl.Real_Impl

13:45:00 Affine_Arithmetic: theory HOL-Word.Bits_Bit

13:45:00 Pre_BZ: theory Polynomial_Interpolation.Polynomial_Interpolation

13:45:00 Echelon_Form: theory Rank_Nullity_Theorem.Generalizations

13:45:00 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Vector_Derivative_On

13:45:00 Affine_Arithmetic: theory HOL-Word.Misc_Numeric

13:45:00 Affine_Arithmetic: theory HOL-Word.Bit_Representation

13:45:00 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Gronwall

13:45:01 Dirichlet_Series: theory HOL-Algebra.Complete_Lattice

13:45:01 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Interval_Integral_HK

13:45:01 QR_Decomposition: theory Show.Show

13:45:01 Affine_Arithmetic: theory HOL-Word.Bits_Int

13:45:01 Ordinary_Differential_Equations: theory Triangle.Angles

13:45:01 Ordinary_Differential_Equations: theory HOL-Library.Float

13:45:01 Ordinary_Differential_Equations: theory Triangle.Triangle

13:45:01 Landau_Analysis: theory Landau_Symbols.Landau_Simprocs

13:45:01 QR_Decomposition: theory Rank_Nullity_Theorem.Miscellaneous

13:45:01 Dirichlet_Series: theory HOL-Algebra.Group

13:45:02 Ordinary_Differential_Equations: theory List-Index.List_Index

13:45:02 QR_Decomposition: theory Show.Show_Instances

13:45:02 HOL-Probability: theory HOL-Library.Diagonal_Subsequence

13:45:02 HOL-Probability: theory HOL-Library.Multiset_Permutations

13:45:02 Landau_Analysis: theory Landau_Symbols.Landau_More

13:45:02 Echelon_Form: theory Rank_Nullity_Theorem.Dual_Order

13:45:03 Landau_Analysis: theory Landau_Symbols.Landau_Symbols

13:45:03 Pre_BZ: theory Polynomial_Factorization.Kronecker_Factorization

13:45:03 Echelon_Form: theory Rank_Nullity_Theorem.Mod_Type

13:45:03 Affine_Arithmetic: theory HOL-Word.Bool_List_Representation

13:45:03 QR_Decomposition: theory Gauss_Jordan.Code_Matrix

13:45:03 Dirichlet_Series: theory HOL-Algebra.Coset

13:45:03 QR_Decomposition: theory Gauss_Jordan.Rref

13:45:03 HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams

13:45:03 QR_Decomposition: theory Rank_Nullity_Theorem.Fundamental_Subspaces

13:45:04 Affine_Arithmetic: theory Native_Word.More_Bits_Int

13:45:04 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation_Bounds

13:45:04 Ordinary_Differential_Equations: theory Affine_Arithmetic.Executable_Euclidean_Space

13:45:04 QR_Decomposition: theory Gauss_Jordan.Elementary_Operations

13:45:04 HOL-Probability: theory HOL-Library.Finite_Map

13:45:04 QR_Decomposition: theory QR_Decomposition.Generalizations2

13:45:04 Dirichlet_Series: theory HOL-Algebra.FiniteProduct

13:45:04 Echelon_Form: theory HOL-Computational_Algebra.Polynomial_Factorial

13:45:05 QR_Decomposition: theory QR_Decomposition.Matrix_To_IArray_QR

13:45:05 Pre_BZ: theory Polynomial_Factorization.Rational_Factorization

13:45:05 Echelon_Form: theory Cayley_Hamilton.Cayley_Hamilton

13:45:05 Dirichlet_Series: theory HOL-Algebra.Ring

13:45:05 HOL-Probability: theory HOL-Probability.Discrete_Topology

13:45:05 HOL-Probability: theory HOL-Probability.Essential_Supremum

13:45:06 Affine_Arithmetic: theory Native_Word.Bits_Integer

13:45:06 HOL-Probability: theory HOL-Probability.Probability_Measure

13:45:06 QR_Decomposition: theory Rank_Nullity_Theorem.Dim_Formula

13:45:06 Echelon_Form: theory Rank_Nullity_Theorem.Miscellaneous

13:45:06 QR_Decomposition: theory Gauss_Jordan.Rank

13:45:06 QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan

13:45:06 HOL-Probability: theory HOL-Probability.Fin_Map

13:45:06 Dirichlet_Series: theory Bernoulli.Bernoulli

13:45:07 QR_Decomposition: theory Show.Show_Real

13:45:07 Dirichlet_Series: theory Bernoulli.Bernoulli_FPS

13:45:07 QR_Decomposition: theory Real_Impl.Real_Unique_Impl

13:45:07 Echelon_Form: theory Gauss_Jordan.Code_Matrix

13:45:08 HOL-Probability: theory HOL-Probability.Conditional_Expectation

13:45:08 Echelon_Form: theory Gauss_Jordan.Rref

13:45:08 QR_Decomposition: theory Gauss_Jordan.Linear_Maps

13:45:08 HOL-Probability: theory HOL-Probability.Distribution_Functions

13:45:08 Dirichlet_Series: theory HOL-Algebra.AbelCoset

13:45:08 Echelon_Form: theory Rank_Nullity_Theorem.Fundamental_Subspaces

13:45:08 HOL-Probability: theory HOL-Probability.Giry_Monad

13:45:08 HOL-Probability: theory HOL-Probability.Weak_Convergence

13:45:08 Echelon_Form: theory Gauss_Jordan.Elementary_Operations

13:45:08 Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation

13:45:08 Dirichlet_Series: theory HOL-Algebra.Module

13:45:09 HOL-Probability: theory HOL-Probability.Helly_Selection

13:45:09 QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan_PA

13:45:10 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities

13:45:10 Echelon_Form: theory Gauss_Jordan.Matrix_To_IArray

13:45:10 QR_Decomposition: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces

13:45:10 QR_Decomposition: theory Gauss_Jordan.Determinants2

13:45:10 QR_Decomposition: theory Gauss_Jordan.Inverse

13:45:10 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Cones

13:45:10 QR_Decomposition: theory Gauss_Jordan.System_Of_Equations

13:45:11 Echelon_Form: theory Rank_Nullity_Theorem.Dim_Formula

13:45:11 Echelon_Form: theory Gauss_Jordan.Rank

13:45:11 QR_Decomposition: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract

13:45:11 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan

13:45:11 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem

13:45:12 HOL-Probability: theory HOL-Probability.Stopping_Time

13:45:12 HOL-Probability: theory HOL-Probability.Probability_Mass_Function

13:45:12 Dirichlet_Series: theory HOL-Algebra.More_Group

13:45:12 HOL-Probability: theory HOL-Probability.Projective_Family

13:45:12 Dirichlet_Series: theory HOL-Algebra.More_Finite_Product

13:45:12 QR_Decomposition: theory QR_Decomposition.Miscellaneous_QR

13:45:13 QR_Decomposition: theory QR_Decomposition.Projections

13:45:13 Dirichlet_Series: theory HOL-Algebra.More_Ring

13:45:13 QR_Decomposition: theory QR_Decomposition.Gram_Schmidt

13:45:13 Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_FPS

13:45:13 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_IArrays

13:45:13 HOL-Probability: theory HOL-Probability.Infinite_Product_Measure

13:45:13 QR_Decomposition: theory QR_Decomposition.QR_Decomposition

13:45:14 Echelon_Form: theory Gauss_Jordan.Linear_Maps

13:45:14 QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Float

13:45:14 Dirichlet_Series: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra

13:45:14 HOL-Probability: theory HOL-Probability.Independent_Family

13:45:14 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative

13:45:14 Dirichlet_Series: theory HOL-Algebra.Ideal

13:45:14 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA

13:45:15 HOL-Probability: theory HOL-Probability.PMF_Impl

13:45:15 Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_Factorial

13:45:15 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor

13:45:15 Echelon_Form: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces

13:45:15 HOL-Probability: theory HOL-Probability.Random_Permutations

13:45:16 Echelon_Form: theory Gauss_Jordan.Determinants2

13:45:16 QR_Decomposition: theory QR_Decomposition.Gram_Schmidt_IArrays

13:45:16 Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays

13:45:16 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow

13:45:16 QR_Decomposition: theory QR_Decomposition.Least_Squares_Approximation

13:45:16 QR_Decomposition: theory QR_Decomposition.QR_Decomposition_IArrays

13:45:16 QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Float

13:45:16 QR_Decomposition: theory QR_Decomposition.QR_Efficient

13:45:17 Echelon_Form: theory Gauss_Jordan.Inverse

13:45:17 QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Symbolic

13:45:17 HOL-Probability: theory HOL-Probability.SPMF

13:45:17 Echelon_Form: theory Gauss_Jordan.Inverse_IArrays

13:45:17 HOL-Probability: theory HOL-Probability.Convolution

13:45:18 Dirichlet_Series: theory HOL-Algebra.RingHom

13:45:18 Echelon_Form: theory Gauss_Jordan.System_Of_Equations

13:45:18 HOL-Probability: theory HOL-Probability.Information

13:45:18 Echelon_Form: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract

13:45:18 Dirichlet_Series: theory HOL-Algebra.UnivPoly

13:45:19 Echelon_Form: theory Echelon_Form.Rings2

13:45:20 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Poincare_Map

13:45:20 Affine_Arithmetic: theory HOL-Word.Word_Miscellaneous

13:45:20 Affine_Arithmetic: theory HOL-Word.Misc_Typedef

13:45:21 Affine_Arithmetic: theory HOL-Word.Word

13:45:21 HOL-Probability: theory HOL-Probability.Distributions

13:45:21 HOL-Probability: theory HOL-Probability.Projective_Limit

13:45:22 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis

13:45:23 HOL-Probability: theory HOL-Probability.Characteristic_Functions

13:45:23 HOL-Probability: theory HOL-Probability.Sinc_Integral

13:45:23 HOL-Probability: theory HOL-Probability.Stream_Space

13:45:23 HOL-Probability: theory HOL-Probability.Levy

13:45:24 QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Symbolic

13:45:24 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution

13:45:24 HOL-Probability: theory HOL-Probability.Tree_Space

13:45:24 HOL-Probability: theory HOL-Probability.Central_Limit_Theorem

13:45:24 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE

13:45:25 HOL-Probability: theory HOL-Probability.Probability

13:45:25 Timing Landau_Analysis (2 threads, 14.394s elapsed time, 27.184s cpu time, 1.332s GC time, factor 1.89)

13:45:25 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Landau_Analysis

13:45:25 Finished Landau_Analysis (0:00:32 elapsed time, 0:00:48 cpu time, factor 1.51)

13:45:25 Building Stirling_Formula ...

13:45:26 Affine_Arithmetic: theory Native_Word.Word_Misc

13:45:27 Stirling_Formula: theory Bernoulli.Bernoulli

13:45:27 Stirling_Formula: theory HOL-Library.Stirling

13:45:27 Affine_Arithmetic: theory Native_Word.Uint32

13:45:27 Stirling_Formula: theory Bernoulli.Periodic_Bernpoly

13:45:27 Stirling_Formula: theory Bernoulli.Bernoulli_FPS

13:45:27 Stirling_Formula: theory Stirling_Formula.Stirling_Formula

13:45:29 Affine_Arithmetic: theory Collections.HashCode

13:45:29 Stirling_Formula: theory Stirling_Formula.Ln_Gamma_Asymptotics

13:45:29 Affine_Arithmetic: theory Deriving.Hash_Generator

13:45:30 Affine_Arithmetic: theory Deriving.Hash_Instances

13:45:30 Affine_Arithmetic: theory Deriving.Countable_Generator

13:45:30 Affine_Arithmetic: theory Deriving.Derive

13:45:31 Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Integer

13:45:31 Dirichlet_Series: theory HOL-Algebra.Multiplicative_Group

13:45:31 Affine_Arithmetic: theory HOL-Library.Lattice_Algebras

13:45:32 Dirichlet_Series: theory HOL-Computational_Algebra.Computational_Algebra

13:45:33 Affine_Arithmetic: theory HOL-Library.RBT

13:45:33 Affine_Arithmetic: theory HOL-Library.RBT_Mapping

13:45:34 Affine_Arithmetic: theory HOL-Library.Log_Nat

13:45:34 Dirichlet_Series: theory HOL-Library.Going_To_Filter

13:45:34 Dirichlet_Series: theory Bernoulli.Periodic_Bernpoly

13:45:34 Dirichlet_Series: theory HOL-Number_Theory.Fib

13:45:34 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities

13:45:34 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise

13:45:34 Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin

13:45:34 Dirichlet_Series: theory HOL-Number_Theory.Prime_Powers

13:45:35 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector

13:45:35 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict

13:45:35 Dirichlet_Series: theory HOL-Number_Theory.Totient

13:45:36 Affine_Arithmetic: theory HOL-Library.Float

13:45:36 Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary

13:45:36 Dirichlet_Series: theory HOL-Number_Theory.Residues

13:45:36 Dirichlet_Series: theory Landau_Symbols.Landau_Library

13:45:37 Dirichlet_Series: theory Landau_Symbols.Landau_Symbols_Definition

13:45:37 Affine_Arithmetic: theory Affine_Arithmetic.Polygon

13:45:37 Affine_Arithmetic: theory List-Index.List_Index

13:45:38 Affine_Arithmetic: theory Show.Show

13:45:38 Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Float

13:45:38 Dirichlet_Series: theory HOL-Number_Theory.Euler_Criterion

13:45:39 Dirichlet_Series: theory HOL-Number_Theory.Gauss

13:45:39 Affine_Arithmetic: theory Affine_Arithmetic.Float_Real

13:45:39 Dirichlet_Series: theory HOL-Number_Theory.Quadratic_Reciprocity

13:45:39 Affine_Arithmetic: theory HOL-Decision_Procs.Approximation_Bounds

13:45:39 Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space

13:45:39 Echelon_Form: theory Echelon_Form.Cayley_Hamilton_Compatible

13:45:40 Dirichlet_Series: theory HOL-Number_Theory.Pocklington

13:45:40 Dirichlet_Series: theory Landau_Symbols.Asymptotic_Equivalence

13:45:40 Dirichlet_Series: theory HOL-Number_Theory.Number_Theory

13:45:40 Dirichlet_Series: theory Landau_Symbols.Group_Sort

13:45:41 Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton

13:45:41 Echelon_Form: theory Echelon_Form.Echelon_Form

13:45:41 Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Misc

13:45:41 Dirichlet_Series: theory Dirichlet_Series.Multiplicative_Function

13:45:42 Dirichlet_Series: theory Landau_Symbols.Landau_Real_Products

13:45:42 Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Product

13:45:42 Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series

13:45:43 Echelon_Form: theory Echelon_Form.Echelon_Form_Det

13:45:43 Echelon_Form: theory Echelon_Form.Echelon_Form_IArrays

13:45:43 Affine_Arithmetic: theory HOL-Decision_Procs.Approximation

13:45:44 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form

13:45:44 Echelon_Form: theory Echelon_Form.Echelon_Form_Det_IArrays

13:45:45 Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse

13:45:45 Dirichlet_Series: theory Dirichlet_Series.Euler_Products

13:45:45 Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton_IArrays

13:45:45 Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_Abstract

13:45:45 Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse_IArrays

13:45:46 Dirichlet_Series: theory Landau_Symbols.Landau_Simprocs

13:45:46 Dirichlet_Series: theory Dirichlet_Series.Moebius_Mu

13:45:47 Dirichlet_Series: theory Dirichlet_Series.More_Totient

13:45:47 Dirichlet_Series: theory Dirichlet_Series.Divisor_Count

13:45:47 Dirichlet_Series: theory Dirichlet_Series.Liouville_Lambda

13:45:47 Dirichlet_Series: theory Landau_Symbols.Landau_More

13:45:47 Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory

13:45:47 Dirichlet_Series: theory Landau_Symbols.Landau_Symbols

13:45:47 Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin_Landau

13:45:47 Dirichlet_Series: theory Dirichlet_Series.Partial_Summation

13:45:48 Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_IArrays

13:45:48 Dirichlet_Series: theory Matrix.Utility

13:45:48 Dirichlet_Series: theory Polynomial_Factorization.Missing_List

13:45:49 Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series_Analysis

13:45:49 Affine_Arithmetic: theory Affine_Arithmetic.Intersection

13:45:51 Dirichlet_Series: theory Polynomial_Factorization.Missing_Multiset

13:45:51 Dirichlet_Series: theory Polynomial_Factorization.Prime_Factorization

13:45:52 Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Efficient_Code

13:45:55 Affine_Arithmetic: theory Show.Show_Instances

13:45:55 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex

13:45:56 Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics

13:45:56 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis

13:46:02 Timing Stirling_Formula (2 threads, 16.063s elapsed time, 29.908s cpu time, 0.872s GC time, factor 1.86)

13:46:02 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stirling_Formula

13:46:02 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stirling_Formula/document.pdf

13:46:02 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Stirling_Formula/outline.pdf

13:46:02 Finished Stirling_Formula (0:00:36 elapsed time, 0:00:58 cpu time, factor 1.60)

13:46:02 Running Gromov_Hyperbolicity ...

13:46:03 Gromov_Hyperbolicity: theory HOL-Cardinals.Order_Relation_More

13:46:03 Gromov_Hyperbolicity: theory HOL-Cardinals.Fun_More

13:46:03 Gromov_Hyperbolicity: theory HOL-Cardinals.Order_Union

13:46:04 Gromov_Hyperbolicity: theory HOL-Decision_Procs.Dense_Linear_Order

13:46:04 Gromov_Hyperbolicity: theory HOL-Cardinals.Wellfounded_More

13:46:04 Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Relation

13:46:04 Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Embedding

13:46:04 Gromov_Hyperbolicity: theory HOL-Library.Cardinal_Notations

13:46:04 Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Constructions

13:46:06 Gromov_Hyperbolicity: theory HOL-Cardinals.Cardinal_Order_Relation

13:46:06 Gromov_Hyperbolicity: theory HOL-Library.Code_Abstract_Nat

13:46:06 Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Nat

13:46:06 Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Int

13:46:06 Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Numeral

13:46:07 Gromov_Hyperbolicity: theory HOL-Library.Lattice_Algebras

13:46:07 Gromov_Hyperbolicity: theory HOL-Library.Log_Nat

13:46:07 Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Library_Complements

13:46:09 Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Eexp_Eln

13:46:09 Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Hausdorff_Distance

13:46:10 Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Isometries

13:46:11 Gromov_Hyperbolicity: theory HOL-Library.Float

13:46:12 Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Metric_Completion

13:46:14 Gromov_Hyperbolicity: theory HOL-Decision_Procs.Approximation_Bounds

13:46:18 Gromov_Hyperbolicity: theory HOL-Decision_Procs.Approximation

13:46:29 Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression

13:46:38 Affine_Arithmetic: theory Affine_Arithmetic.Straight_Line_Program

13:46:45 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation

13:46:55 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code

13:46:58 Affine_Arithmetic: theory Affine_Arithmetic.Print

13:47:01 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation

13:47:02 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs

13:47:02 Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter

13:47:04 Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Gromov_Hyperbolicity

13:47:09 Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Bonk_Schramm_Extension

13:47:10 Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Gromov_Boundary

13:47:12 Timing Pre_BZ (2 threads, 121.931s elapsed time, 207.376s cpu time, 11.332s GC time, factor 1.70)

13:47:12 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Pre_BZ

13:47:12 Finished Pre_BZ (0:02:43 elapsed time, 0:05:02 cpu time, factor 1.84)

13:47:12 Building Berlekamp_Zassenhaus ...

13:47:17 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Arithmetic_Record_Based

13:47:17 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Missing_Multiset2

13:47:18 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Code_Abort_Gcd

13:47:18 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Degree_Bound

13:47:19 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Karatsuba_Multiplication

13:47:20 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly

13:47:21 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Sublist_Iteration

13:47:23 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Polynomial_Record_Based

13:47:28 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Matrix_Record_Based

13:47:29 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization

13:47:30 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field

13:47:34 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Record_Based

13:47:38 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Unique_Factorization_Poly

13:47:39 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp

13:47:40 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod

13:47:42 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field

13:47:45 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based

13:47:45 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Type_Based

13:47:48 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting

13:47:50 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Mahler_Measure

13:47:53 Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic

13:47:54 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based

13:47:55 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factor_Bound

13:47:56 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Suitable_Prime

13:47:56 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization

13:47:58 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization

13:47:58 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl

13:47:58 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based

13:47:59 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int

13:48:02 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Hensel

13:48:03 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Reconstruction

13:48:08 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus

13:48:09 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Int_Poly

13:48:11 Berlekamp_Zassenhaus: theory Berlekamp_Zassenhaus.Factorize_Rat_Poly

13:48:19 Timing HOL-Probability (2 threads, 163.586s elapsed time, 299.976s cpu time, 19.980s GC time, factor 1.83)

13:48:19 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Probability

13:48:19 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Probability/document.pdf

13:48:19 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/HOL/HOL-Probability/outline.pdf

13:48:19 Finished HOL-Probability (0:03:25 elapsed time, 0:06:01 cpu time, factor 1.76)

13:48:19 Building Deep_Learning_Lib ...

13:48:21 Deep_Learning_Lib: theory HOL-Computational_Algebra.Fraction_Field

13:48:21 Deep_Learning_Lib: theory HOL-Library.Fun_Lexorder

13:48:21 Deep_Learning_Lib: theory HOL-Algebra.Congruence

13:48:22 Deep_Learning_Lib: theory HOL-Computational_Algebra.Normalized_Fraction

13:48:22 Deep_Learning_Lib: theory HOL-Algebra.Order

13:48:23 Timing Gromov_Hyperbolicity (2 threads, 131.515s elapsed time, 243.780s cpu time, 12.004s GC time, factor 1.85)

13:48:23 Browser info at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Gromov_Hyperbolicity

13:48:23 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Gromov_Hyperbolicity/document.pdf

13:48:23 Document at /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Gromov_Hyperbolicity/outline.pdf

13:48:23 Finished Gromov_Hyperbolicity (0:02:20 elapsed time, 0:04:17 cpu time, factor 1.84)

13:48:23 Building Markov_Models ...