Started by an SCM change Running as SYSTEM [EnvInject] - Loading node environment variables. Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-all [isabelle-all] $ hg showconfig paths.default [isabelle-all] $ hg pull --rev default pulling from http://isabelle.in.tum.de/repos/isabelle/ no changes found [isabelle-all] $ hg update --clean --rev default 1 files updated, 0 files merged, 0 files removed, 0 files unresolved [isabelle-all] $ hg log --rev . --template {node} [isabelle-all] $ hg log --rev . --template {rev} [isabelle-all] $ hg log --rev 65371451fde8afb008925d55f5f3c5260c40c14e --template exists\n exists [isabelle-all] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(65371451fde8afb008925d55f5f3c5260c40c14e)" --encoding UTF-8 --encodingmode replace [afp] $ hg showconfig paths.default [afp] $ hg pull --rev default pulling from https://bitbucket.org/isa-afp/afp-devel/ no changes found [afp] $ hg update --clean --rev default 490 files updated, 0 files merged, 0 files removed, 0 files unresolved [afp] $ hg --config extensions.purge= clean --all [afp] $ hg log --rev . --template {node} [afp] $ hg log --rev . --template {rev} [afp] $ hg log --rev 35d7fb94ba43cf8fa0126477df776980b8362608 --template exists\n exists [afp] $ hg log --template "{desc|xmlescape}{file_adds % '{file|xmlescape}'}{file_dels % '{file|xmlescape}'}{files % '{file|xmlescape}'}{parents}\n" --rev "ancestors('default') and not ancestors(35d7fb94ba43cf8fa0126477df776980b8362608)" --encoding UTF-8 --encodingmode replace No emails were triggered. [isabelle-all] $ /bin/sh -xe /tmp/jenkins5114492638357539121.sh + Admin/jenkins/run_build all + set -e + PROFILE=all + shift + bin/isabelle components -a + bin/isabelle jedit -bf ### Building Isabelle/Scala ... ### Building Isabelle/jEdit ... + bin/isabelle ocaml_setup # Run eval $(opam env) to update the current shell environment [NOTE] It seems you have not updated your repositories for a while. Consider updating them with: opam update [NOTE] Package zarith is already installed (current version is 1.7). + bin/isabelle ghc_setup stack will use a sandboxed GHC it installed For more information on paths, see 'stack path' and 'stack exec env' To use this GHC and packages outside of a project, consider using: stack ghc, stack ghci, stack runghc, or stack exec The Glorious Glasgow Haskell Compilation System, version 8.4.4 + bin/isabelle ci_build_all === CONFIGURATION === ISABELLE_BUILD_OPTIONS="" ML_PLATFORM="x86_64_32-linux" ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64_32-linux" ML_SYSTEM="polyml-5.8" ML_OPTIONS="-H 4000 --maxheap 8G" jobs = 10, threads = 4, numa = false === BUILD === Build started at Thu, 19 Sep 2019 13:25:00 GMT Isabelle id e19c18b4a0dd AFP id f807a036febc === LOG === Session Pure/Pure Session CTT/CTT Session Cube/Cube Session FOL/FOL Session CCL/CCL Session FOL/FOL-ex Session FOLP/FOLP Session FOLP/FOLP-ex Session HOL/HOL (main) Session AFP/AVL-Trees (AFP) Session AFP/AWN (AFP) Session AFP/Abortable_Linearizable_Modules (AFP) Session AFP/Abstract-Hoare-Logics (AFP) Session AFP/AnselmGod (AFP) Session AFP/AxiomaticCategoryTheory (AFP) Session AFP/BinarySearchTree (AFP) Session AFP/Binomial-Queues (AFP) Session AFP/Bondy (AFP) Session AFP/Bounded_Deducibility_Security (AFP) Session AFP/BytecodeLogicJmlTypes (AFP) Session AFP/CISC-Kernel (AFP) Session AFP/CYK (AFP) Session AFP/Cauchy (AFP) Session AFP/Sqrt_Babylonian (AFP) Session Doc/Classes (doc) Session AFP/ClockSynchInst (AFP) Session AFP/Compiling-Exceptions-Correctly (AFP) Session AFP/Complete_Non_Orders (AFP) Session AFP/ComponentDependencies (AFP) Session AFP/Concurrent_Revisions (AFP) Session AFP/Constructor_Funs (AFP) Session AFP/CryptoBasedCompositionalProperties (AFP) Session AFP/DPT-SAT-Solver (AFP) Session AFP/Depth-First-Search (AFP) Session AFP/Diophantine_Eqns_Lin_Hom (AFP) Session AFP/DiskPaxos (AFP) Session AFP/Example-Submission (AFP) Session AFP/FFT (AFP) Session AFP/FLP (AFP) Session AFP/FeatherweightJava (AFP) Session AFP/Featherweight_OCL (AFP) Session AFP/FileRefinement (AFP) Session AFP/FocusStreamsCaseStudies (AFP) Session AFP/Free-Boolean-Algebra (AFP) Session AFP/FunWithFunctions (AFP) Session AFP/FunWithTilings (AFP) Session Doc/Functions (doc) Session AFP/GPU_Kernel_PL (AFP) Session AFP/Gauss-Jordan-Elim-Fun (AFP) Session AFP/GenClock (AFP) Session AFP/General-Triangle (AFP) Session AFP/Generic_Deriving (AFP) Session AFP/GewirthPGCProof (AFP) Session AFP/GoedelGod (AFP) Session HOL/HOL-Cardinals (timing) Session AFP/Binding_Syntax_Theory (AFP) Session AFP/Ordinals_and_Cardinals (AFP) Session HOL/HOL-Eisbach Session AFP/Allen_Calculus (AFP) Session AFP/Dependent_SIFUM_Type_Systems (AFP) Session AFP/Dependent_SIFUM_Refinement (AFP) Session Doc/Eisbach (doc) Session HOL/HOL-Hoare Session AFP/Case_Labeling (AFP) Session HOL/HOL-Hoare_Parallel (timing) Session HOL/HOL-IMPP Session HOL/HOL-IOA Session HOL/HOL-Import Session HOL/HOL-Lattice Session HOL/HOL-Library (main timing) Session AFP/ArrowImpossibilityGS (AFP) Session AFP/Auto2_HOL (AFP) Session AFP/BNF_CC (AFP) Session AFP/BNF_Operations (AFP) Session AFP/Binomial-Heaps (AFP) Session AFP/Boolean_Expression_Checkers (AFP) Session AFP/Buildings (AFP) Session AFP/CRDT (AFP) Session AFP/IMAP-CRDT (AFP) Session AFP/Card_Multisets (AFP) Session AFP/Card_Number_Partitions (AFP) Session AFP/Category (AFP) Session AFP/Category3 (AFP) Session AFP/MonoidalCategory (AFP) Session Doc/Codegen (doc) Session AFP/CofGroups (AFP) Session AFP/Completeness (AFP) Session AFP/ConcurrentIMP (AFP) Session AFP/Concurrent_Ref_Alg (AFP) Session AFP/CoreC++ (AFP) Session AFP/Core_DOM (AFP) Session Doc/Datatypes (doc) Session Doc/Corec (doc) Session AFP/Decl_Sem_Fun_PL (AFP) Session AFP/Derangements (AFP) Session AFP/Discrete_Summation (AFP) Session AFP/Card_Partitions (AFP) Session AFP/Bell_Numbers_Spivey (AFP) Session AFP/Card_Equiv_Relations (AFP) Session AFP/Efficient-Mergesort (AFP) Session AFP/Encodability_Process_Calculi (AFP) Session AFP/Epistemic_Logic (AFP) Session AFP/Euler_Partition (AFP) Session AFP/FOL-Fitting (AFP) Session AFP/FOL_Harrison (AFP) Session AFP/Factored_Transition_System_Bounding (AFP) Session AFP/Falling_Factorial_Sum (AFP) Session AFP/FinFun (AFP) Session AFP/Finger-Trees (AFP) Session AFP/Graph_Saturation (AFP) Session AFP/Graph_Theory (AFP) Session AFP/ShortestPath (AFP) Session AFP/Group-Ring-Module (AFP) Session AFP/Valuation (AFP) Session HOL/HOL-Auth (timing) Session HOL/HOL-UNITY (timing) Session HOL/HOL-Bali (timing) Session HOL/HOL-Computational_Algebra (main timing) Session AFP/Descartes_Sign_Rule (AFP) Session HOL/HOL-Algebra (main timing) Session HOL/HOL-Decision_Procs (timing) Session HOL/HOL-Quotient_Examples (timing) Session AFP/Localization_Ring (AFP) Session AFP/Orbit_Stabiliser (AFP) Session AFP/Perfect-Number-Thm (AFP) Session AFP/Secondary_Sylow (AFP) Session AFP/Jordan_Hoelder (AFP) Session AFP/VectorSpace (AFP) Session HOL/HOL-Analysis (main timing) Session AFP/Bernoulli (AFP) Session AFP/Cartan_FP (AFP) Session AFP/Cayley_Hamilton (AFP) Session AFP/Coinductive (AFP) Session AFP/DynamicArchitectures (AFP) Session AFP/Architectural_Design_Patterns (AFP) Session AFP/Lazy-Lists-II (AFP) Session AFP/Stream_Fusion_Code (AFP) Session AFP/Topology (AFP) Session AFP/Differential_Game_Logic (AFP) Session AFP/First_Welfare_Theorem (AFP) Session AFP/Green (AFP) Session HOL/HOL-Analysis-ex Session HOL/HOL-Homology (timing) Session HOL/HOL-Probability (main timing) Session AFP/Buffons_Needle (AFP) Session AFP/Density_Compiler (AFP) Session AFP/DiscretePricing (AFP) Session AFP/Ergodic_Theory (AFP) Session AFP/Gromov_Hyperbolicity (AFP) Session AFP/Fisher_Yates (AFP) Session AFP/Girth_Chromatic (AFP) Session AFP/Random_Graph_Subgraph_Threshold (AFP) Session HOL/HOL-Probability-ex (timing) Session AFP/Lp (AFP) Session AFP/Markov_Models (AFP) Session AFP/Monad_Normalisation (AFP) Session AFP/Monomorphic_Monad (AFP) Session AFP/Neumann_Morgenstern_Utility (AFP) Session AFP/Probabilistic_Noninterference (AFP) Session AFP/Probabilistic_System_Zoo (AFP) Session AFP/Source_Coding_Theorem (AFP) Session AFP/Irrationality_J_Hancl (AFP) Session AFP/Kuratowski_Closure_Complement (AFP) Session AFP/Lower_Semicontinuous (AFP) Session AFP/Minkowskis_Theorem (AFP) Session AFP/Octonions (AFP) Session AFP/Ptolemys_Theorem (AFP) Session AFP/Quaternions (AFP) Session AFP/Rank_Nullity_Theorem (AFP) Session AFP/Gauss_Jordan (AFP) Session AFP/Echelon_Form (AFP) Session AFP/Hermite (AFP) Session AFP/Tarskis_Geometry (AFP) Session AFP/Triangle (AFP) Session AFP/Chord_Segments (AFP) Session AFP/Stewart_Apollonius (AFP) Session AFP/pGCL (AFP) Session HOL/HOL-Isar_Examples Session HOL/HOL-Nonstandard_Analysis (timing) Session HOL/HOL-Nonstandard_Analysis-Examples (timing) Session HOL/HOL-Number_Theory (main timing) Session AFP/E_Transcendental (AFP) Session AFP/Elliptic_Curves_Group_Law (AFP) Session AFP/Fermat3_4 (AFP) Session HOL/HOL-Data_Structures (timing) Session HOL/HOL-ex (timing) Session AFP/Automatic_Refinement (AFP) Session HOL/HOL-Codegenerator_Test Session AFP/Lehmer (AFP) Session AFP/Pratt_Certificate (AFP) Session AFP/Bertrands_Postulate (AFP) Session AFP/Prime_Harmonic_Series (AFP) Session AFP/RSAPSS (AFP) Session AFP/SumSquares (AFP) Session AFP/Liouville_Numbers (AFP) Session AFP/Mason_Stothers (AFP) Session AFP/Polynomial_Interpolation (AFP) Session AFP/Probabilistic_Prime_Tests (AFP) Session AFP/Rep_Fin_Groups (AFP) Session AFP/Sturm_Sequences (AFP) Session AFP/Special_Function_Bounds (AFP) Session AFP/Sturm_Tarski (AFP) Session AFP/Budan_Fourier (AFP) Session AFP/Winding_Number_Eval (AFP) Session AFP/Count_Complex_Roots (AFP) Session HOL/HOL-Corec_Examples (timing) Session HOL/HOL-Datatype_Examples (timing) Session HOL/HOL-Hahn_Banach Session HOL/HOL-IMP (timing) Session AFP/Abs_Int_ITP2012 (AFP) Session HOL/HOL-Imperative_HOL (timing) Session AFP/Auto2_Imperative_HOL (AFP) Session AFP/Imperative_Insertion_Sort (AFP) Session HOL/HOL-Induct Session HOL/HOL-Matrix_LP Session HOL/HOL-Metis_Examples (timing) Session HOL/HOL-MicroJava (timing) Session HOL/HOL-Mutabelle Session HOL/HOL-Nitpick_Examples Session HOL/HOL-Nominal Session AFP/CCS (AFP) Session HOL/HOL-Nominal-Examples (timing) Session AFP/Lam-ml-Normalization (AFP) Session AFP/Pi_Calculus (AFP) Session AFP/Psi_Calculi (AFP) Session AFP/SequentInvertibility (AFP) Session HOL/HOL-Predicate_Compile_Examples (timing) Session HOL/HOL-Quickcheck_Examples (timing) Session HOL/HOL-SET_Protocol (timing) Session HOL/HOL-TPTP Session HOL/HOL-Unix Session HOL/HOL-ZF Session AFP/Category2 (AFP) Session AFP/HereditarilyFinite (AFP) Session AFP/HyperCTL (AFP) Session AFP/Integration (AFP) Session AFP/Isabelle_Meta_Model (AFP) Session AFP/LTL (AFP) Session AFP/Stuttering_Equivalence (AFP) Session AFP/Lambda_Free_RPOs (AFP) Session AFP/Lambda_Free_EPO (AFP) Session AFP/Landau_Symbols (AFP) Session AFP/Akra_Bazzi (AFP) Session AFP/Catalan_Numbers (AFP) Session AFP/Error_Function (AFP) Session AFP/Euler_MacLaurin (AFP) Session AFP/Stirling_Formula (AFP) Session AFP/LightweightJava (AFP) Session AFP/LinearQuantifierElim (AFP) Session AFP/List-Infinite (AFP) Session AFP/Nat-Interval-Logic (AFP) Session AFP/AutoFocus-Stream (AFP) Session AFP/MuchAdoAboutTwo (AFP) Session AFP/Optics (AFP) Session AFP/UTP-Toolkit (AFP) Session AFP/UTP (AFP) Session AFP/Order_Lattice_Props (AFP) Session AFP/POPLmark-deBruijn (AFP) Session AFP/Pairing_Heap (AFP) Session AFP/Password_Authentication_Protocol (AFP) Session AFP/Pell (AFP) Session AFP/Presburger-Automata (AFP) Session AFP/Priority_Queue_Braun (AFP) Session AFP/Program-Conflict-Analysis (AFP) Session AFP/Regular-Sets (AFP) Session AFP/Abstract-Rewriting (AFP) Session AFP/Decreasing-Diagrams (AFP) Session AFP/First_Order_Terms (AFP) Session AFP/Matrix (AFP) Session AFP/Matrix_Tensor (AFP) Session AFP/Knot_Theory (AFP) Session AFP/Coinductive_Languages (AFP) Session AFP/Finite_Automata_HF (AFP) Session AFP/Functional-Automata (AFP) Session AFP/Posix-Lexing (AFP) Session AFP/Ribbon_Proofs (AFP) Session AFP/SATSolverVerification (AFP) Session AFP/Safe_OCL (AFP) Session AFP/Selection_Heap_Sort (AFP) Session AFP/Simplex (AFP) Session AFP/Skew_Heap (AFP) Session AFP/Sort_Encodings (AFP) Session AFP/Splay_Tree (AFP) Session AFP/Amortized_Complexity (AFP) Session AFP/Dynamic_Tables (AFP) Session AFP/Root_Balanced_Tree (AFP) Session AFP/Stable_Matching (AFP) Session AFP/SuperCalc (AFP) Session AFP/Tail_Recursive_Functions (AFP) Session AFP/TortoiseHare (AFP) Session AFP/Trie (AFP) Session AFP/Flyspeck-Tame (AFP) Session AFP/Twelvefold_Way (AFP) Session AFP/Vickrey_Clarke_Groves (AFP) Session HOL/HOL-Mirabelle Session HOL/HOL-Mirabelle-ex Session HOL/HOL-NanoJava Session HOL/HOL-Prolog Session HOL/HOL-Real_Asymp Session HOL/HOL-Real_Asymp-Manual Session HOL/HOL-Statespace Session HOL/HOL-TLA Session HOL/HOL-TLA-Buffer Session HOL/HOL-TLA-Inc Session HOL/HOL-TLA-Memory Session HOL/HOL-Types_To_Sets Session AFP/Smooth_Manifolds (AFP) Session HOL/HOL-Word (main timing) Session HOL/HOL-SPARK Session HOL/HOL-SPARK-Examples Session AFP/RIPEMD-160-SPARK (AFP) Session HOL/HOL-SPARK-Manual Session HOL/HOL-Word-SMT_Examples (timing) Session AFP/Kleene_Algebra (AFP) Session AFP/KAT_and_DRA (AFP) Session AFP/Multirelations (AFP) Session AFP/Quantales (AFP) Session AFP/Transformer_Semantics (AFP) Session AFP/Regular_Algebras (AFP) Session AFP/Relation_Algebra (AFP) Session AFP/Residuated_Lattices (AFP) Session AFP/LEM (AFP) Session AFP/Native_Word (AFP) Session AFP/WebAssembly (AFP) Session AFP/Refine_Monadic (AFP) Session AFP/Collections (AFP) Session AFP/Abstract_Completeness (AFP) Session AFP/Abstract_Soundness (AFP) Session AFP/Incredible_Proof_Machine (AFP) Session AFP/Deriving (AFP) Session AFP/CAVA_Base (AFP) Session AFP/CAVA_Automata (AFP) Session AFP/DFS_Framework (AFP) Session AFP/Gabow_SCC (AFP) Session AFP/LTL_to_GBA (AFP) Session AFP/Promela (AFP) Session AFP/Containers (AFP) Session AFP/Collections_Examples (AFP) Session AFP/Containers-Benchmarks (AFP) Session AFP/MFOTL_Monitor (AFP) Session AFP/Datatype_Order_Generator (AFP) Session AFP/Old_Datatype_Show (AFP) Session AFP/Show (AFP) Session AFP/JNF-AFP-Lib (AFP) Session AFP/Real_Impl (AFP) Session AFP/QR_Decomposition (AFP) Session AFP/Dijkstra_Shortest_Path (AFP) Session AFP/Koenigsberg_Friendship (AFP) Session AFP/Transition_Systems_and_Automata (AFP) Session AFP/Buchi_Complementation (AFP) Session AFP/LTL_Master_Theorem (AFP) Session AFP/Partial_Order_Reduction (AFP) Session AFP/SM_Base (AFP) Session AFP/SM (AFP) Session AFP/CAVA_Setup (AFP) Session AFP/CAVA_LTL_Modelchecker (AFP) Session AFP/Transitive-Closure (AFP) Session AFP/KBPs (AFP) Session AFP/Tree-Automata (AFP) Session AFP/SPARCv8 (AFP) Session AFP/Separation_Algebra (AFP) Session AFP/Separata (AFP) Session AFP/Separation_Logic_Imperative_HOL (AFP) Session AFP/Sepref_Prereq (AFP) Session AFP/ROBDD (AFP) Session AFP/UpDown_Scheme (AFP) Session AFP/Word_Lib (AFP) Session AFP/Complx (AFP) Session AFP/IEEE_Floating_Point (AFP) Session AFP/CakeML (AFP) Session AFP/IP_Addresses (AFP) Session AFP/Simple_Firewall (AFP) Session AFP/Routing (AFP) Session AFP/Iptables_Semantics (AFP) Session AFP/Iptables_Semantics_Examples (AFP) Session AFP/LOFT (AFP) Session HOL/HOLCF (main timing) Session AFP/Circus (AFP) Session AFP/HOL-CSP (AFP) Session HOL/HOLCF-IMP Session HOL/HOLCF-Library Session HOL/HOLCF-FOCUS Session HOL/HOLCF-ex Session AFP/PCF (AFP) Session AFP/HOLCF-Prelude (AFP) Session HOL/HOLCF-Tutorial Session HOL/IOA (timing) Session HOL/IOA-ABP Session HOL/IOA-NTP Session HOL/IOA-Storage Session HOL/IOA-ex Session AFP/Shivers-CFA (AFP) Session AFP/Stream-Fusion (AFP) Session AFP/Tycon (AFP) Session AFP/WorkerWrapper (AFP) Session AFP/Heard_Of (AFP) Session AFP/Consensus_Refined (AFP) Session AFP/Hoare_Time (AFP) Session AFP/HotelKeyCards (AFP) Session Doc/How_to_Prove_it (no_doc) Session AFP/Huffman (AFP) Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP) Session AFP/IMP2 (AFP) Session AFP/IMP2_Binary_Heap (AFP) Session Doc/Implementation (doc) Session AFP/Impossible_Geometry (AFP) Session AFP/Inductive_Confidentiality (AFP) Session AFP/InfPathElimination (AFP) Session Doc/Isar_Ref (doc) Session Doc/JEdit (doc) Session AFP/JiveDataStoreModel (AFP) Session AFP/KAD (AFP) Session AFP/Algebraic_VCs (AFP) Session AFP/Key_Agreement_Strong_Adversaries (AFP) Session AFP/LambdaMu (AFP) Session AFP/LatticeProperties (AFP) Session AFP/DataRefinementIBP (AFP) Session AFP/GraphMarkingIBP (AFP) Session AFP/Lazy_Case (AFP) Session AFP/Dict_Construction (AFP) Session AFP/Lifting_Definition_Option (AFP) Session AFP/List-Index (AFP) Session AFP/Affine_Arithmetic (AFP) Session AFP/Taylor_Models (AFP) Session AFP/Comparison_Sort_Lower_Bound (AFP) Session AFP/Formula_Derivatives (AFP) Session AFP/Formula_Derivatives-Examples (AFP) Session AFP/Higher_Order_Terms (AFP) Session AFP/CakeML_Codegen (AFP) Session AFP/Jinja (AFP) Session AFP/HRB-Slicing (AFP) Session AFP/InformationFlowSlicing_Inter (AFP) Session AFP/Slicing (AFP) Session AFP/Formal_SSA (AFP) Session AFP/Minimal_SSA (AFP) Session AFP/InformationFlowSlicing (AFP) Session AFP/LTL_to_DRA (AFP) Session AFP/List_Update (AFP) Session AFP/Ordinary_Differential_Equations (AFP) Session AFP/Differential_Dynamic_Logic (AFP) Session AFP/HOL-ODE-Numerics (AFP) Session AFP/HOL-ODE-ARCH-COMP (AFP) Session AFP/HOL-ODE-Examples (AFP large) Session AFP/Lorenz_Approximation (AFP) Session AFP/Lorenz_C0 (AFP large) Session AFP/Lorenz_C1 (AFP large) Session AFP/Quick_Sort_Cost (AFP) Session AFP/Random_BSTs (AFP) Session AFP/Randomised_BSTs (AFP) Session AFP/Treaps (AFP) Session AFP/Randomised_Social_Choice (AFP) Session AFP/Fishburn_Impossibility (AFP) Session AFP/SDS_Impossibility (AFP) Session AFP/Refine_Imperative_HOL (AFP) Session AFP/Floyd_Warshall (AFP) Session AFP/Sepref_Basic (AFP) Session AFP/Sepref_IICF (AFP) Session AFP/Flow_Networks (AFP) Session AFP/EdmondsKarp_Maxflow (AFP) Session AFP/MFMC_Countable (AFP) Session AFP/Prpu_Maxflow (AFP) Session AFP/Knuth_Morris_Pratt (AFP) Session AFP/VerifyThis2018 (AFP) Session AFP/List_Interleaving (AFP) Session AFP/List_Inversions (AFP) Session AFP/LocalLexing (AFP) Session Doc/Locales (doc) Session AFP/Lowe_Ontological_Argument (AFP) Session AFP/MSO_Regex_Equivalence (AFP) Session Doc/Main (doc) Session AFP/Marriage (AFP) Session AFP/Latin_Square (AFP) Session AFP/Matroids (AFP) Session AFP/Kruskal (AFP) Session AFP/Max-Card-Matching (AFP) Session AFP/Median_Of_Medians_Selection (AFP) Session AFP/KD_Tree (AFP) Session AFP/Menger (AFP) Session AFP/MiniML (AFP) Session AFP/Modular_Assembly_Kit_Security (AFP) Session AFP/Monad_Memo_DP (AFP) Session AFP/Hidden_Markov_Models (AFP) Session AFP/Optimal_BST (AFP) Session AFP/MonoBoolTranAlgebra (AFP) Session AFP/Name_Carrying_Type_Inference (AFP) Session AFP/Network_Security_Policy_Verification (AFP) Session AFP/No_FTL_observers (AFP) Session AFP/Nominal2 (AFP) Session AFP/Incompleteness (AFP) Session AFP/Surprise_Paradox (AFP) Session AFP/LambdaAuth (AFP) Session AFP/Launchbury (AFP) Session AFP/Call_Arity (AFP) Session AFP/Modal_Logics_for_NTS (AFP) Session AFP/Rewriting_Z (AFP) Session AFP/Noninterference_CSP (AFP) Session AFP/Noninterference_Ipurge_Unwinding (AFP) Session AFP/Noninterference_Generic_Unwinding (AFP) Session AFP/Noninterference_Inductive_Unwinding (AFP) Session AFP/Noninterference_Sequential_Composition (AFP) Session AFP/Noninterference_Concurrent_Composition (AFP) Session AFP/NormByEval (AFP) Session AFP/OpSets (AFP) Session AFP/Open_Induction (AFP) Session AFP/Well_Quasi_Orders (AFP) Session AFP/Decreasing-Diagrams-II (AFP) Session AFP/Myhill-Nerode (AFP) Session AFP/Polynomials (AFP) Session AFP/Symmetric_Polynomials (AFP) Session AFP/Pi_Transcendental (AFP) Session AFP/Ordinal (AFP) Session AFP/Nested_Multisets_Ordinals (AFP) Session AFP/Lambda_Free_KBOs (AFP) Session AFP/Ordered_Resolution_Prover (AFP) Session AFP/PLM (AFP) Session AFP/PSemigroupsConvolution (AFP) Session AFP/Paraconsistency (AFP) Session AFP/Parity_Game (AFP) Session AFP/Partial_Function_MR (AFP) Session AFP/Certification_Monads (AFP) Session AFP/XML (AFP) Session AFP/Polynomial_Factorization (AFP) Session AFP/Dirichlet_Series (AFP) Session AFP/Zeta_Function (AFP) Session AFP/Dirichlet_L (AFP) Session AFP/Prime_Number_Theorem (AFP) Session AFP/Prime_Distribution_Elementary (AFP) Session AFP/Transcendence_Series_Hancl_Rucki (AFP) Session AFP/Functional_Ordered_Resolution_Prover (AFP) Session AFP/Jordan_Normal_Form (AFP) Session AFP/Deep_Learning (AFP) Session AFP/Farkas (AFP) Session AFP/Groebner_Bases (AFP) Session AFP/Groebner_Macaulay (AFP) Session AFP/Nullstellensatz (AFP) Session AFP/Signature_Groebner (AFP) Session AFP/QHLProver (AFP) Session AFP/Linear_Recurrences (AFP) Session AFP/Perron_Frobenius (AFP) Session AFP/Stochastic_Matrices (AFP) Session AFP/Subresultants (AFP) Session AFP/Pre_BZ (AFP) Session AFP/Berlekamp_Zassenhaus (AFP) Session AFP/Algebraic_Numbers (AFP) Session AFP/LLL_Basis_Reduction (AFP) Session AFP/LLL_Factorization (AFP) Session AFP/Linear_Inequalities (AFP) Session AFP/Linear_Recurrences_Solver (AFP) Session AFP/Probabilistic_While (AFP) Session AFP/Pop_Refinement (AFP) Session AFP/Possibilistic_Noninterference (AFP) Session AFP/Priority_Search_Trees (AFP) Session AFP/Prim_Dijkstra_Simple (AFP) Session Doc/Prog_Prove (doc) Session AFP/Projective_Geometry (AFP) Session AFP/Proof_Strategy_Language (AFP) Session AFP/PropResPI (AFP) Session AFP/Propositional_Proof_Systems (AFP) Session AFP/PseudoHoops (AFP) Session AFP/Ramsey-Infinite (AFP) Session AFP/Recursion-Theory-I (AFP) Session AFP/Minsky_Machines (AFP) Session AFP/RefinementReactive (AFP) Session AFP/Resolution_FOL (AFP) Session AFP/Robbins-Conjecture (AFP) Session AFP/Roy_Floyd_Warshall (AFP) Session AFP/SIFPL (AFP) Session AFP/SIFUM_Type_Systems (AFP) Session AFP/Security_Protocol_Refinement (AFP) Session AFP/SenSocialChoice (AFP) Session AFP/Simpl (AFP) Session AFP/BDD (AFP) Session AFP/Planarity_Certificates (AFP) Session AFP/Statecharts (AFP) Session AFP/Stone_Algebras (AFP) Session AFP/Stone_Relation_Algebras (AFP) Session AFP/Stone_Kleene_Relation_Algebras (AFP) Session AFP/Aggregation_Algebras (AFP) Session AFP/Store_Buffer_Reduction (AFP) Session AFP/Strong_Security (AFP) Session Doc/Sugar (doc) Session AFP/TLA (AFP) Session AFP/Timed_Automata (AFP) Session AFP/Probabilistic_Timed_Automata (AFP) Session AFP/Transitive-Closure-II (AFP) Session AFP/Tree_Decomposition (AFP) Session Doc/Tutorial (doc) Session Doc/Typeclass_Hierarchy (doc) Session AFP/Types_Tableaus_and_Goedels_God (AFP) Session AFP/UPF (AFP) Session AFP/UPF_Firewall (AFP) Session AFP/Universal_Turing_Machine (AFP) Session AFP/Verified-Prover (AFP) Session AFP/VolpanoSmith (AFP) Session AFP/WHATandWHERE_Security (AFP) Session AFP/Weight_Balanced_Trees (AFP) Session HOL/HOL-Proofs (timing) Session HOL/HOL-Proofs-Extraction (timing) Session HOL/HOL-Proofs-Lambda (timing) Session AFP/Applicative_Lifting (AFP) Session AFP/CryptHOL (AFP) Session AFP/Constructive_Cryptography (AFP) Session AFP/Game_Based_Crypto (AFP) Session AFP/Multi_Party_Computation (AFP) Session AFP/Free-Groups (AFP) Session AFP/Locally-Nameless-Sigma (AFP) Session AFP/Stern_Brocot (AFP) Session HOL/HOL-Proofs-ex Session Tools/Haskell Session Doc/Intro (doc) Session LCF/LCF Session Doc/Logics (doc) Session Doc/Nitpick (doc) Session Tools/SML Session Sequents/Sequents Session Doc/Sledgehammer (doc) Session Tools/Spec_Check Session AFP/Regex_Equivalence (AFP) Session Doc/System (doc) Session ZF/ZF (main timing) Session Doc/Logics_ZF (doc) Session ZF/ZF-AC Session ZF/ZF-Coind Session ZF/ZF-Constructible Session ZF/ZF-IMP Session ZF/ZF-Induct Session ZF/ZF-UNITY (timing) Session ZF/ZF-Resid Session ZF/ZF-ex Building HOL-Analysis ... Running Perron_Frobenius ... HOL-Analysis: theory HOL-Library.Cancellation HOL-Analysis: theory HOL-Library.Disjoint_Sets HOL-Analysis: theory HOL-Library.FuncSet HOL-Analysis: theory HOL-Library.Infinite_Set HOL-Analysis: theory HOL-Library.Nat_Bijection HOL-Analysis: theory HOL-Library.Old_Datatype HOL-Analysis: theory HOL-Library.Phantom_Type HOL-Analysis: theory HOL-Library.Multiset HOL-Analysis: theory HOL-Library.Product_Plus HOL-Analysis: theory HOL-Library.Product_Order HOL-Analysis: theory HOL-Library.Set_Algebras HOL-Analysis: theory HOL-Library.Countable Perron_Frobenius: theory HOL-Eisbach.Eisbach Perron_Frobenius: theory HOL-Types_To_Sets.Types_To_Sets Perron_Frobenius: theory HOL-Analysis.Abstract_Topology Perron_Frobenius: theory HOL-Analysis.Continuum_Not_Denumerable HOL-Analysis: theory HOL-Analysis.Inner_Product HOL-Analysis: theory HOL-Library.Cardinality Perron_Frobenius: theory HOL-Analysis.Inner_Product Perron_Frobenius: theory HOL-Analysis.L2_Norm Perron_Frobenius: theory HOL-Analysis.Operator_Norm Perron_Frobenius: theory HOL-Analysis.Product_Vector Perron_Frobenius: theory Polynomial_Factorization.Polynomial_Divisibility Perron_Frobenius: theory Sturm_Sequences.Misc_Polynomial HOL-Analysis: theory HOL-Analysis.L2_Norm HOL-Analysis: theory HOL-Library.Numeral_Type HOL-Analysis: theory HOL-Library.Countable_Set Perron_Frobenius: theory Sturm_Sequences.Sturm_Library HOL-Analysis: theory HOL-Analysis.Operator_Norm Perron_Frobenius: theory Sturm_Sequences.Sturm_Theorem HOL-Analysis: theory HOL-Analysis.Poly_Roots HOL-Analysis: theory HOL-Analysis.Product_Vector Perron_Frobenius: theory HOL-Analysis.Elementary_Topology Perron_Frobenius: theory HOL-Analysis.Euclidean_Space HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices HOL-Analysis: theory HOL-Library.Set_Idioms Perron_Frobenius: theory Sturm_Sequences.Sturm_Method HOL-Analysis: theory HOL-Analysis.Abstract_Topology HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable HOL-Analysis: theory HOL-Analysis.Elementary_Topology Perron_Frobenius: theory HOL-Analysis.Norm_Arith Perron_Frobenius: theory HOL-Analysis.Abstract_Limits Perron_Frobenius: theory Polynomial_Factorization.Square_Free_Factorization Perron_Frobenius: theory Rank_Nullity_Theorem.Dual_Order Perron_Frobenius: theory HOL-Analysis.Finite_Cartesian_Product Perron_Frobenius: theory HOL-Analysis.Linear_Algebra Perron_Frobenius: theory HOL-Analysis.Abstract_Topology_2 HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring HOL-Analysis: theory HOL-Library.Permutations HOL-Analysis: theory HOL-Analysis.Euclidean_Space HOL-Analysis: theory HOL-Library.Discrete Perron_Frobenius: theory HOL-Analysis.Convex HOL-Analysis: theory HOL-Library.Indicator_Function HOL-Analysis: theory HOL-Analysis.Abstract_Limits Perron_Frobenius: theory HOL-Analysis.Connected HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2 Perron_Frobenius: theory HOL-Analysis.Cartesian_Space HOL-Analysis: theory HOL-Library.Liminf_Limsup Perron_Frobenius: theory HOL-Analysis.Elementary_Metric_Spaces HOL-Analysis: theory HOL-Library.Nonpos_Ints HOL-Analysis: theory HOL-Library.Order_Continuity Perron_Frobenius: theory HOL-Analysis.Determinants HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product HOL-Analysis: theory HOL-Analysis.Linear_Algebra HOL-Analysis: theory HOL-Analysis.Connected HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces Perron_Frobenius: theory HOL-Analysis.Elementary_Normed_Spaces Perron_Frobenius: theory HOL-Analysis.Topology_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Convex HOL-Analysis: theory HOL-Analysis.Cartesian_Space HOL-Analysis: theory HOL-Library.Extended_Nat HOL-Analysis: theory HOL-Library.Periodic_Fun HOL-Analysis: theory HOL-Library.Sum_of_Squares HOL-Analysis: theory HOL-Analysis.Determinants HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces HOL-Analysis: theory HOL-Library.Extended_Real HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm Perron_Frobenius: theory HOL-Analysis.Convex_Euclidean_Space Perron_Frobenius: theory HOL-Analysis.Extended_Real_Limits Perron_Frobenius: theory HOL-Analysis.Function_Topology HOL-Analysis: theory HOL-Analysis.Norm_Arith Perron_Frobenius: theory HOL-Analysis.Summation_Tests Perron_Frobenius: theory HOL-Analysis.Starlike Perron_Frobenius: theory HOL-Analysis.Product_Topology HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space Perron_Frobenius: theory HOL-Analysis.T1_Spaces Perron_Frobenius: theory HOL-Analysis.Uniform_Limit HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real Perron_Frobenius: theory HOL-Analysis.Bounded_Linear_Function HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space Perron_Frobenius: theory HOL-Analysis.Path_Connected HOL-Analysis: theory HOL-Analysis.Function_Topology HOL-Analysis: theory HOL-Analysis.Sigma_Algebra Perron_Frobenius: theory HOL-Analysis.Derivative Perron_Frobenius: theory HOL-Analysis.Homotopy HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits HOL-Analysis: theory HOL-Analysis.Starlike Perron_Frobenius: theory HOL-Analysis.Cartesian_Euclidean_Space Perron_Frobenius: theory Rank_Nullity_Theorem.Mod_Type HOL-Analysis: theory HOL-Computational_Algebra.Primes HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series Perron_Frobenius: theory HOL-Analysis.Homeomorphism HOL-Analysis: theory HOL-Analysis.Summation_Tests HOL-Analysis: theory HOL-Analysis.Measurable Perron_Frobenius: theory HOL-Analysis.Brouwer_Fixpoint HOL-Analysis: theory HOL-Analysis.Uniform_Limit HOL-Analysis: theory HOL-Analysis.Measure_Space Perron_Frobenius: theory Rank_Nullity_Theorem.Miscellaneous HOL-Analysis: theory HOL-Analysis.Continuous_Extension HOL-Analysis: theory HOL-Analysis.Product_Topology HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function HOL-Analysis: theory HOL-Analysis.T1_Spaces HOL-Analysis: theory HOL-Analysis.Lindelof_Spaces HOL-Analysis: theory HOL-Analysis.Path_Connected HOL-Analysis: theory HOL-Analysis.Caratheodory HOL-Analysis: theory HOL-Analysis.Tagged_Division HOL-Analysis: theory HOL-Analysis.Derivative HOL-Analysis: theory HOL-Analysis.Homotopy HOL-Analysis: theory HOL-Analysis.Locally HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Lipschitz HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems HOL-Analysis: theory HOL-Analysis.Cross3 HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Polytope HOL-Analysis: theory HOL-Analysis.Homeomorphism HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint HOL-Analysis: theory HOL-Analysis.Abstract_Euclidean_Space HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem HOL-Analysis: theory HOL-Analysis.Complex_Transcendental HOL-Analysis: theory HOL-Analysis.Arcwise_Connected HOL-Analysis: theory HOL-Analysis.Borel_Space HOL-Analysis: theory HOL-Analysis.Multivariate_Analysis HOL-Analysis: theory HOL-Analysis.Retracts HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem HOL-Analysis: theory HOL-Analysis.Infinite_Products HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration HOL-Analysis: theory HOL-Analysis.Regularity HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure HOL-Analysis: theory HOL-Analysis.Embed_Measure HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure HOL-Analysis: theory HOL-Analysis.Bochner_Integration HOL-Analysis: theory HOL-Analysis.Complete_Measure HOL-Analysis: theory HOL-Analysis.Radon_Nikodym HOL-Analysis: theory HOL-Analysis.Set_Integral HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration HOL-Analysis: theory HOL-Analysis.Integral_Test HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers HOL-Analysis: theory HOL-Analysis.Further_Topology HOL-Analysis: theory HOL-Analysis.Improper_Integral HOL-Analysis: theory HOL-Analysis.Equivalence_Measurable_On_Borel HOL-Analysis: theory HOL-Analysis.Interval_Integral HOL-Analysis: theory HOL-Analysis.Conformal_Mappings HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution HOL-Analysis: theory HOL-Analysis.Jordan_Curve HOL-Analysis: theory HOL-Analysis.FPS_Convergence HOL-Analysis: theory HOL-Analysis.Great_Picard HOL-Analysis: theory HOL-Analysis.Gamma_Function HOL-Analysis: theory HOL-Analysis.Riemann_Mapping HOL-Analysis: theory HOL-Analysis.Winding_Numbers HOL-Analysis: theory HOL-Analysis.Ball_Volume HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem HOL-Analysis: theory HOL-Analysis.Change_Of_Vars HOL-Analysis: theory HOL-Analysis.Simplex_Content HOL-Analysis: theory HOL-Analysis.Analysis Perron_Frobenius: theory Perron_Frobenius.Bij_Nat Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint Perron_Frobenius: theory HOL-Real_Asymp.Inst_Existentials Perron_Frobenius: theory HOL-Real_Asymp.Eventuallize Perron_Frobenius: theory HOL-Real_Asymp.Lazy_Eval Perron_Frobenius: theory Perron_Frobenius.Roots_Unity Perron_Frobenius: theory Perron_Frobenius.Hom_Gauss_Jordan Perron_Frobenius: theory Perron_Frobenius.HMA_Connect Perron_Frobenius: theory HOL-Real_Asymp.Multiseries_Expansion Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Aux Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_Irreducible Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory Perron_Frobenius: theory Perron_Frobenius.Perron_Frobenius_General Perron_Frobenius: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Perron_Frobenius: theory HOL-Real_Asymp.Real_Asymp Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block Perron_Frobenius: theory Perron_Frobenius.Spectral_Radius_Theory_2 Perron_Frobenius: theory Perron_Frobenius.Check_Matrix_Growth Timing Perron_Frobenius (4 threads, 208.738s elapsed time, 722.084s cpu time, 38.696s GC time, factor 3.46) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Perron_Frobenius Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Perron_Frobenius/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Perron_Frobenius/outline.pdf Timing Perron_Frobenius (4 threads, 208.738s elapsed time, 722.084s cpu time, 38.696s GC time, factor 3.46) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Perron_Frobenius Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Perron_Frobenius/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Perron_Frobenius/outline.pdf Finished Perron_Frobenius (0:03:36 elapsed time, 0:12:15 cpu time, factor 3.40) Timing HOL-Analysis (4 threads, 594.179s elapsed time, 1831.860s cpu time, 116.084s GC time, factor 3.08) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis/manual.pdf Timing HOL-Analysis (4 threads, 594.179s elapsed time, 1831.860s cpu time, 116.084s GC time, factor 3.08) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis/manual.pdf Finished HOL-Analysis (0:12:08 elapsed time, 0:34:11 cpu time, factor 2.82) Building Ordinary_Differential_Equations ... Building HOL-Probability ... Building Echelon_Form ... Building Affine_Arithmetic ... Building Dirichlet_Series ... Running Transcendence_Series_Hancl_Rucki ... Running QR_Decomposition ... Building Count_Complex_Roots ... Building E_Transcendental ... Running Gromov_Hyperbolicity ... Ordinary_Differential_Equations: theory HOL-Decision_Procs.Dense_Linear_Order Ordinary_Differential_Equations: theory HOL-Library.Code_Abstract_Nat Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Int Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence HOL-Probability: theory HOL-Library.Conditional_Parametricity HOL-Probability: theory HOL-Library.Adhoc_Overloading HOL-Probability: theory HOL-Library.AList HOL-Probability: theory HOL-Library.Lattice_Syntax Echelon_Form: theory HOL-Computational_Algebra.Fraction_Field Echelon_Form: theory HOL-Library.Code_Abstract_Nat Echelon_Form: theory HOL-Library.Code_Target_Int Echelon_Form: theory HOL-Library.Function_Algebras Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Nat HOL-Probability: theory HOL-Library.Complete_Partial_Order2 Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras Affine_Arithmetic: theory Deriving.Comparator Affine_Arithmetic: theory Deriving.Derive_Manager Affine_Arithmetic: theory Deriving.Generator_Aux Affine_Arithmetic: theory HOL-Decision_Procs.Dense_Linear_Order Echelon_Form: theory HOL-Library.Code_Target_Nat Echelon_Form: theory HOL-Library.IArray HOL-Probability: theory HOL-Library.Monad_Syntax Ordinary_Differential_Equations: theory HOL-Library.Log_Nat Affine_Arithmetic: theory HOL-Library.Adhoc_Overloading HOL-Probability: theory HOL-Library.Mapping Echelon_Form: theory HOL-Library.More_List Count_Complex_Roots: theory HOL-Eisbach.Eisbach Count_Complex_Roots: theory HOL-Computational_Algebra.Fraction_Field Count_Complex_Roots: theory HOL-Library.More_List Count_Complex_Roots: theory HOL-Computational_Algebra.Field_as_Ring Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral Echelon_Form: theory HOL-Library.Code_Target_Numeral Gromov_Hyperbolicity: theory HOL-Cardinals.Order_Relation_More Gromov_Hyperbolicity: theory HOL-Cardinals.Fun_More Gromov_Hyperbolicity: theory HOL-Cardinals.Order_Union Gromov_Hyperbolicity: theory HOL-Decision_Procs.Dense_Linear_Order Affine_Arithmetic: theory HOL-Library.Monad_Syntax Affine_Arithmetic: theory HOL-Library.Boolean_Algebra Ordinary_Differential_Equations: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities Ordinary_Differential_Equations: theory Triangle.Angles Affine_Arithmetic: theory Deriving.Equality_Generator Dirichlet_Series: theory HOL-Computational_Algebra.Fraction_Field Dirichlet_Series: theory HOL-Computational_Algebra.Group_Closure Dirichlet_Series: theory HOL-Library.Adhoc_Overloading Dirichlet_Series: theory HOL-Library.BNF_Corec Gromov_Hyperbolicity: theory HOL-Library.Code_Abstract_Nat E_Transcendental: theory HOL-Number_Theory.Cong E_Transcendental: theory HOL-Algebra.Congruence E_Transcendental: theory HOL-Library.More_List E_Transcendental: theory HOL-Library.Power_By_Squaring Transcendence_Series_Hancl_Rucki: theory HOL-Eisbach.Eisbach Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Fraction_Field Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Group_Closure Transcendence_Series_Hancl_Rucki: theory HOL-Library.BNF_Corec Echelon_Form: theory Gauss_Jordan.Code_Set Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Int Echelon_Form: theory HOL-Library.Z2 Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Nat Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial Echelon_Form: theory HOL-Computational_Algebra.Field_as_Ring HOL-Probability: theory HOL-Library.Stream Dirichlet_Series: theory HOL-Library.Monad_Syntax Ordinary_Differential_Equations: theory Triangle.Triangle Dirichlet_Series: theory HOL-Computational_Algebra.Nth_Powers Affine_Arithmetic: theory HOL-Library.Permutation Gromov_Hyperbolicity: theory HOL-Cardinals.Wellfounded_More QR_Decomposition: theory Deriving.Generator_Aux QR_Decomposition: theory HOL-Library.Code_Abstract_Nat QR_Decomposition: theory Real_Impl.Real_Impl_Auxiliary QR_Decomposition: theory Deriving.Derive_Manager Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Relation E_Transcendental: theory HOL-Number_Theory.Eratosthenes Gromov_Hyperbolicity: theory HOL-Library.Lattice_Algebras QR_Decomposition: theory HOL-Library.Code_Target_Int Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Numeral E_Transcendental: theory HOL-Computational_Algebra.Polynomial QR_Decomposition: theory HOL-Library.Function_Algebras QR_Decomposition: theory HOL-Library.Code_Target_Nat Affine_Arithmetic: theory HOL-Library.Char_ord Gromov_Hyperbolicity: theory HOL-Library.Log_Nat Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Vector_Derivative_On QR_Decomposition: theory HOL-Library.IArray Affine_Arithmetic: theory Deriving.Equality_Instances QR_Decomposition: theory Gauss_Jordan.Code_Set Affine_Arithmetic: theory HOL-Library.Code_Abstract_Nat Dirichlet_Series: theory HOL-Computational_Algebra.Squarefree QR_Decomposition: theory HOL-Library.Z2 Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Embedding QR_Decomposition: theory Cauchy.CauchysMeanTheorem QR_Decomposition: theory HOL-Library.Code_Target_Numeral Count_Complex_Roots: theory HOL-Eisbach.Eisbach_Tools Affine_Arithmetic: theory HOL-Library.Code_Target_Nat Echelon_Form: theory Gauss_Jordan.Code_Z2 Gromov_Hyperbolicity: theory Ergodic_Theory.Fekete Affine_Arithmetic: theory HOL-Library.Code_Target_Int Echelon_Form: theory HOL-Computational_Algebra.Polynomial Affine_Arithmetic: theory Deriving.Compare Count_Complex_Roots: theory Winding_Number_Eval.Missing_Topology E_Transcendental: theory HOL-Number_Theory.Fib Echelon_Form: theory Gauss_Jordan.IArray_Addenda Dirichlet_Series: theory HOL-Number_Theory.Cong QR_Decomposition: theory HOL-Library.Code_Real_Approx_By_Float Echelon_Form: theory Cayley_Hamilton.Square_Matrix Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Constructions Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Gronwall Transcendence_Series_Hancl_Rucki: theory HOL-Eisbach.Eisbach_Tools QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary Affine_Arithmetic: theory Deriving.Comparator_Generator Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Interval_Integral_HK Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Nth_Powers Dirichlet_Series: theory HOL-Library.Code_Abstract_Nat Affine_Arithmetic: theory HOL-Library.Mapping Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Squarefree HOL-Probability: theory HOL-Library.Rewrite QR_Decomposition: theory Gauss_Jordan.Code_Z2 Dirichlet_Series: theory HOL-Library.Code_Target_Nat Echelon_Form: theory HOL-Computational_Algebra.Normalized_Fraction Ordinary_Differential_Equations: theory List-Index.List_Index E_Transcendental: theory HOL-Number_Theory.Prime_Powers Count_Complex_Roots: theory Winding_Number_Eval.Missing_Analysis QR_Decomposition: theory Rank_Nullity_Theorem.Dual_Order E_Transcendental: theory HOL-Algebra.Order Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Cong Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Congruence Dirichlet_Series: theory HOL-Library.Code_Target_Int QR_Decomposition: theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell QR_Decomposition: theory Show.Show HOL-Probability: theory HOL-Library.Sublist Dirichlet_Series: theory HOL-Library.Code_Target_Numeral Count_Complex_Roots: theory HOL-Computational_Algebra.Normalized_Fraction Dirichlet_Series: theory HOL-Computational_Algebra.Normalized_Fraction Affine_Arithmetic: theory HOL-Library.Type_Length QR_Decomposition: theory Rank_Nullity_Theorem.Mod_Type QR_Decomposition: theory QR_Decomposition.IArray_Addenda_QR HOL-Probability: theory HOL-Library.AList_Mapping Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Normalized_Fraction HOL-Probability: theory HOL-Library.Tree Dirichlet_Series: theory HOL-Algebra.Congruence Gromov_Hyperbolicity: theory HOL-Cardinals.Cardinal_Order_Relation E_Transcendental: theory HOL-Number_Theory.Mod_Exp Affine_Arithmetic: theory HOL-Library.RBT_Impl Echelon_Form: theory Rank_Nullity_Theorem.Dual_Order QR_Decomposition: theory Sqrt_Babylonian.Log_Impl Affine_Arithmetic: theory Deriving.Compare_Generator HOL-Probability: theory HOL-Library.FSet Echelon_Form: theory Rank_Nullity_Theorem.Mod_Type QR_Decomposition: theory Sqrt_Babylonian.NthRoot_Impl Dirichlet_Series: theory HOL-Library.Function_Algebras E_Transcendental: theory HOL-Number_Theory.Totient Affine_Arithmetic: theory HOL-Library.Z2 Affine_Arithmetic: theory Deriving.Compare_Instances Transcendence_Series_Hancl_Rucki: theory HOL-Library.More_List Dirichlet_Series: theory HOL-Library.More_List Dirichlet_Series: theory HOL-Library.Power_By_Squaring QR_Decomposition: theory Show.Show_Instances QR_Decomposition: theory Show.Show_Real Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Order Transcendence_Series_Hancl_Rucki: theory HOL-Library.Power_By_Squaring E_Transcendental: theory HOL-Algebra.Lattice Dirichlet_Series: theory HOL-Library.Stirling Affine_Arithmetic: theory HOL-Word.Bits Dirichlet_Series: theory HOL-Number_Theory.Mod_Exp Affine_Arithmetic: theory HOL-Word.Misc_Auxiliary Affine_Arithmetic: theory HOL-Word.Bits_Z2 Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Library_Complements Dirichlet_Series: theory HOL-Algebra.Order QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian Affine_Arithmetic: theory HOL-Word.Bits_Int Transcendence_Series_Hancl_Rucki: theory HOL-Library.Stirling Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Mod_Exp Affine_Arithmetic: theory HOL-Word.Misc_Arithmetic HOL-Probability: theory HOL-Library.Diagonal_Subsequence Dirichlet_Series: theory HOL-Number_Theory.Eratosthenes Affine_Arithmetic: theory HOL-Word.Misc_Typedef QR_Decomposition: theory Real_Impl.Prime_Product QR_Decomposition: theory Real_Impl.Real_Impl HOL-Probability: theory HOL-Library.Multiset_Permutations HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams Affine_Arithmetic: theory Deriving.Countable_Generator Dirichlet_Series: theory HOL-Real_Asymp.Inst_Existentials Dirichlet_Series: theory Bernoulli.Bernoulli Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Integer Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Eratosthenes Affine_Arithmetic: theory HOL-Library.Lattice_Algebras Dirichlet_Series: theory Bernoulli.Bernoulli_FPS Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Inst_Existentials Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli Affine_Arithmetic: theory HOL-Library.Log_Nat Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Field_as_Ring Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Lattice E_Transcendental: theory HOL-Algebra.Complete_Lattice Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli_FPS Dirichlet_Series: theory HOL-Algebra.Lattice QR_Decomposition: theory Real_Impl.Real_Unique_Impl QR_Decomposition: theory Rank_Nullity_Theorem.Miscellaneous HOL-Probability: theory HOL-Probability.Discrete_Topology HOL-Probability: theory HOL-Probability.Essential_Supremum Echelon_Form: theory Rank_Nullity_Theorem.Miscellaneous Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector HOL-Probability: theory HOL-Probability.Probability_Measure HOL-Probability: theory HOL-Probability.Stopping_Time HOL-Probability: theory HOL-Probability.Tree_Space Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict E_Transcendental: theory HOL-Algebra.Group Dirichlet_Series: theory HOL-Library.Going_To_Filter Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Eexp_Eln Ordinary_Differential_Equations: theory HOL-Library.Float Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Hausdorff_Distance Dirichlet_Series: theory HOL-Library.Landau_Symbols Dirichlet_Series: theory HOL-Algebra.Complete_Lattice Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Complete_Lattice Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Isometries Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Polynomial Transcendence_Series_Hancl_Rucki: theory HOL-Library.Going_To_Filter Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary Transcendence_Series_Hancl_Rucki: theory HOL-Library.Landau_Symbols QR_Decomposition: theory Gauss_Jordan.Code_Matrix Affine_Arithmetic: theory HOL-Word.Bit_Comprehension Affine_Arithmetic: theory Native_Word.More_Bits_Int QR_Decomposition: theory Gauss_Jordan.Rref QR_Decomposition: theory Rank_Nullity_Theorem.Fundamental_Subspaces Echelon_Form: theory Gauss_Jordan.Code_Matrix QR_Decomposition: theory QR_Decomposition.Generalizations2 Echelon_Form: theory Gauss_Jordan.Rref Gromov_Hyperbolicity: theory HOL-Library.Float Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Group Dirichlet_Series: theory HOL-Algebra.Group QR_Decomposition: theory Rank_Nullity_Theorem.Dim_Formula Affine_Arithmetic: theory HOL-Word.Word QR_Decomposition: theory Gauss_Jordan.Elementary_Operations HOL-Probability: theory HOL-Library.Finite_Map HOL-Probability: theory HOL-Probability.Conditional_Expectation Echelon_Form: theory Rank_Nullity_Theorem.Fundamental_Subspaces QR_Decomposition: theory Gauss_Jordan.Rank HOL-Probability: theory HOL-Probability.Distribution_Functions Echelon_Form: theory Gauss_Jordan.Elementary_Operations Echelon_Form: theory Rank_Nullity_Theorem.Dim_Formula HOL-Probability: theory HOL-Probability.Weak_Convergence Echelon_Form: theory Gauss_Jordan.Rank QR_Decomposition: theory QR_Decomposition.Matrix_To_IArray_QR HOL-Probability: theory HOL-Probability.Giry_Monad QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan HOL-Probability: theory HOL-Probability.Helly_Selection E_Transcendental: theory HOL-Algebra.Coset Affine_Arithmetic: theory Native_Word.Code_Symbolic_Bits_Int E_Transcendental: theory HOL-Algebra.FiniteProduct Echelon_Form: theory Gauss_Jordan.Matrix_To_IArray Echelon_Form: theory Gauss_Jordan.Gauss_Jordan Affine_Arithmetic: theory Native_Word.Bits_Integer Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation_Bounds Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Metric_Completion Dirichlet_Series: theory Bernoulli.Periodic_Bernpoly Ordinary_Differential_Equations: theory Affine_Arithmetic.Executable_Euclidean_Space Dirichlet_Series: theory HOL-Number_Theory.Fib E_Transcendental: theory HOL-Algebra.Ring Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin Transcendence_Series_Hancl_Rucki: theory Bernoulli.Periodic_Bernpoly Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Gromov_Hyperbolicity Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Topology Dirichlet_Series: theory HOL-Number_Theory.Prime_Powers Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial_Factorial Count_Complex_Roots: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli_Zeta Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Coset HOL-Probability: theory HOL-Probability.Probability_Mass_Function Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.FiniteProduct HOL-Probability: theory HOL-Probability.Projective_Family Dirichlet_Series: theory HOL-Algebra.Coset QR_Decomposition: theory Gauss_Jordan.Linear_Maps Gromov_Hyperbolicity: theory HOL-Decision_Procs.Approximation_Bounds Transcendence_Series_Hancl_Rucki: theory Euler_MacLaurin.Euler_MacLaurin E_Transcendental: theory HOL-Algebra.Generated_Groups Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_IArrays Echelon_Form: theory Gauss_Jordan.Linear_Maps Affine_Arithmetic: theory HOL-Library.Float Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Ring Echelon_Form: theory HOL-Computational_Algebra.Polynomial_Factorial Echelon_Form: theory Cayley_Hamilton.Cayley_Hamilton Dirichlet_Series: theory HOL-Algebra.FiniteProduct HOL-Probability: theory HOL-Probability.Infinite_Product_Measure QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan_PA Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA Dirichlet_Series: theory HOL-Algebra.Ring Dirichlet_Series: theory HOL-Number_Theory.Totient HOL-Probability: theory HOL-Probability.Independent_Family HOL-Probability: theory HOL-Probability.Stream_Space QR_Decomposition: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces QR_Decomposition: theory Gauss_Jordan.Determinants2 Dirichlet_Series: theory HOL-Algebra.Generated_Groups QR_Decomposition: theory Gauss_Jordan.Inverse QR_Decomposition: theory Gauss_Jordan.System_Of_Equations Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Generated_Groups Echelon_Form: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces Echelon_Form: theory Gauss_Jordan.Determinants2 Dirichlet_Series: theory HOL-Real_Asymp.Eventuallize HOL-Probability: theory HOL-Probability.PMF_Impl Dirichlet_Series: theory HOL-Real_Asymp.Lazy_Eval Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Analysis Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Fib Echelon_Form: theory Gauss_Jordan.Inverse QR_Decomposition: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract Echelon_Form: theory Gauss_Jordan.System_Of_Equations HOL-Probability: theory HOL-Probability.Random_Permutations Echelon_Form: theory Gauss_Jordan.Inverse_IArrays Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Prime_Powers HOL-Probability: theory HOL-Probability.SPMF Affine_Arithmetic: theory Affine_Arithmetic.Polygon Dirichlet_Series: theory Landau_Symbols.Group_Sort Dirichlet_Series: theory HOL-Real_Asymp.Multiseries_Expansion Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Float Echelon_Form: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Totient Affine_Arithmetic: theory Affine_Arithmetic.Float_Real Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Gromov_Boundary Dirichlet_Series: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra E_Transcendental: theory HOL-Algebra.AbelCoset E_Transcendental: theory HOL-Algebra.Module Affine_Arithmetic: theory HOL-Decision_Procs.Approximation_Bounds Affine_Arithmetic: theory List-Index.List_Index QR_Decomposition: theory QR_Decomposition.Miscellaneous_QR Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Eventuallize Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Lazy_Eval HOL-Probability: theory HOL-Probability.Convolution Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_FPS Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities QR_Decomposition: theory QR_Decomposition.Projections HOL-Probability: theory HOL-Probability.Information QR_Decomposition: theory QR_Decomposition.Gram_Schmidt Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space Gromov_Hyperbolicity: theory HOL-Decision_Procs.Approximation Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_Factorial QR_Decomposition: theory QR_Decomposition.QR_Decomposition Dirichlet_Series: theory HOL-Computational_Algebra.Formal_Laurent_Series Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Cones Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Float Dirichlet_Series: theory HOL-Algebra.AbelCoset Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Multiseries_Expansion Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor HOL-Probability: theory HOL-Probability.Distributions Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.AbelCoset Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Module Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Polynomial_FPS Affine_Arithmetic: theory HOL-Decision_Procs.Approximation E_Transcendental: theory HOL-Algebra.Ideal QR_Decomposition: theory QR_Decomposition.Gram_Schmidt_IArrays Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative QR_Decomposition: theory QR_Decomposition.Least_Squares_Approximation Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Formal_Laurent_Series QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Symbolic HOL-Probability: theory HOL-Probability.Characteristic_Functions HOL-Probability: theory HOL-Probability.Sinc_Integral QR_Decomposition: theory QR_Decomposition.QR_Decomposition_IArrays QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Float QR_Decomposition: theory QR_Decomposition.QR_Efficient Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form HOL-Probability: theory HOL-Probability.Levy Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Polynomial_Factorial HOL-Probability: theory HOL-Probability.Central_Limit_Theorem Dirichlet_Series: theory HOL-Algebra.Module E_Transcendental: theory HOL-Algebra.RingHom HOL-Probability: theory HOL-Probability.Fin_Map Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Ideal Affine_Arithmetic: theory Native_Word.Code_Target_Word_Base Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Poincare_Map Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution E_Transcendental: theory HOL-Algebra.UnivPoly Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE Dirichlet_Series: theory HOL-Algebra.Ideal Affine_Arithmetic: theory Affine_Arithmetic.Intersection Dirichlet_Series: theory Landau_Symbols.Landau_Real_Products HOL-Probability: theory HOL-Probability.Projective_Limit Affine_Arithmetic: theory Native_Word.Uint32 Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis HOL-Probability: theory HOL-Probability.Probability Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.RingHom Affine_Arithmetic: theory Collections.HashCode Affine_Arithmetic: theory Deriving.Hash_Generator Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.UnivPoly Dirichlet_Series: theory HOL-Algebra.RingHom Affine_Arithmetic: theory Deriving.Hash_Instances Affine_Arithmetic: theory Deriving.Derive Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow_Congs Affine_Arithmetic: theory Show.Show QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Symbolic Dirichlet_Series: theory Landau_Symbols.Landau_Simprocs Dirichlet_Series: theory HOL-Algebra.UnivPoly Dirichlet_Series: theory Landau_Symbols.Landau_More Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin_Landau Affine_Arithmetic: theory Show.Show_Instances Dirichlet_Series: theory Matrix.Utility Dirichlet_Series: theory Polynomial_Factorization.Missing_List Echelon_Form: theory Echelon_Form.Rings2 Count_Complex_Roots: theory Sturm_Tarski.PolyMisc Count_Complex_Roots: theory Sturm_Tarski.Sturm_Tarski Count_Complex_Roots: theory Budan_Fourier.BF_Misc Dirichlet_Series: theory Polynomial_Factorization.Missing_Multiset Dirichlet_Series: theory Polynomial_Factorization.Prime_Factorization E_Transcendental: theory HOL-Algebra.Multiplicative_Group Count_Complex_Roots: theory Budan_Fourier.Sturm_Multiple_Roots Count_Complex_Roots: theory Winding_Number_Eval.Missing_Algebraic Count_Complex_Roots: theory Winding_Number_Eval.Missing_Transcendental Count_Complex_Roots: theory Count_Complex_Roots.More_Polynomials Count_Complex_Roots: theory Winding_Number_Eval.Cauchy_Index_Theorem E_Transcendental: theory HOL-Number_Theory.Residues Affine_Arithmetic: theory HOL-Library.RBT Count_Complex_Roots: theory Count_Complex_Roots.Extended_Sturm Affine_Arithmetic: theory HOL-Library.RBT_Mapping Count_Complex_Roots: theory Winding_Number_Eval.Winding_Number_Eval E_Transcendental: theory HOL-Number_Theory.Euler_Criterion E_Transcendental: theory HOL-Number_Theory.Pocklington E_Transcendental: theory HOL-Number_Theory.Gauss Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots E_Transcendental: theory HOL-Number_Theory.Residue_Primitive_Roots E_Transcendental: theory HOL-Number_Theory.Quadratic_Reciprocity Dirichlet_Series: theory HOL-Computational_Algebra.Computational_Algebra Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Multiplicative_Group E_Transcendental: theory HOL-Number_Theory.Number_Theory Dirichlet_Series: theory HOL-Algebra.Multiplicative_Group E_Transcendental: theory E_Transcendental.E_Transcendental Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots_Examples Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Computational_Algebra Transcendence_Series_Hancl_Rucki: theory Sturm_Tarski.PolyMisc Transcendence_Series_Hancl_Rucki: theory Sturm_Tarski.Sturm_Tarski Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Residues Transcendence_Series_Hancl_Rucki: theory Budan_Fourier.BF_Misc Dirichlet_Series: theory HOL-Number_Theory.Residues Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Algebraic Dirichlet_Series: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Euler_Criterion Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Gauss Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Quadratic_Reciprocity Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Pocklington Dirichlet_Series: theory HOL-Number_Theory.Euler_Criterion Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Transcendental Dirichlet_Series: theory HOL-Number_Theory.Pocklington Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Residue_Primitive_Roots Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Dirichlet_Series: theory HOL-Number_Theory.Gauss Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Cauchy_Index_Theorem Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Number_Theory Dirichlet_Series: theory HOL-Number_Theory.Quadratic_Reciprocity Dirichlet_Series: theory HOL-Number_Theory.Residue_Primitive_Roots Dirichlet_Series: theory HOL-Number_Theory.Number_Theory Dirichlet_Series: theory HOL-Real_Asymp.Real_Asymp Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Misc Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Multiplicative_Function Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Real_Asymp Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Product Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Euler_Products Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Misc Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Winding_Number_Eval Dirichlet_Series: theory Dirichlet_Series.Multiplicative_Function Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Series Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Product Dirichlet_Series: theory Dirichlet_Series.Euler_Products Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Moebius_Mu Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.More_Totient Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Divisor_Count Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Liouville_Lambda Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Arithmetic_Summatory Dirichlet_Series: theory Dirichlet_Series.Moebius_Mu Dirichlet_Series: theory Dirichlet_Series.More_Totient Dirichlet_Series: theory Dirichlet_Series.Liouville_Lambda Dirichlet_Series: theory Dirichlet_Series.Divisor_Count Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Partial_Summation Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Efficient_Code Dirichlet_Series: theory Dirichlet_Series.Partial_Summation Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Series_Analysis Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series_Analysis Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Morse_Gromov_Theorem Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis Echelon_Form: theory Echelon_Form.Cayley_Hamilton_Compatible Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Bonk_Schramm_Extension Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Boundary_Extension Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton Echelon_Form: theory Echelon_Form.Echelon_Form Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Busemann_Function Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Isometries_Classification Echelon_Form: theory Echelon_Form.Echelon_Form_Det Echelon_Form: theory Echelon_Form.Echelon_Form_IArrays Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression Echelon_Form: theory Echelon_Form.Echelon_Form_Det_IArrays Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton_IArrays Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_Abstract Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse_IArrays Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_IArrays Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics Transcendence_Series_Hancl_Rucki: theory Zeta_Function.Zeta_Function Transcendence_Series_Hancl_Rucki: theory Prime_Number_Theorem.Prime_Number_Theorem_Library Timing E_Transcendental (4 threads, 106.303s elapsed time, 375.944s cpu time, 16.120s GC time, factor 3.54) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/E_Transcendental Transcendence_Series_Hancl_Rucki: theory Transcendence_Series_Hancl_Rucki.Transcendence_Series Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/E_Transcendental/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/E_Transcendental/outline.pdf Affine_Arithmetic: theory Affine_Arithmetic.Straight_Line_Program Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation Timing HOL-Probability (4 threads, 132.107s elapsed time, 434.180s cpu time, 13.244s GC time, factor 3.29) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code Timing Count_Complex_Roots (4 threads, 139.999s elapsed time, 379.036s cpu time, 9.428s GC time, factor 2.71) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Count_Complex_Roots Affine_Arithmetic: theory Affine_Arithmetic.Print Timing Gromov_Hyperbolicity (4 threads, 142.258s elapsed time, 471.048s cpu time, 15.328s GC time, factor 3.31) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gromov_Hyperbolicity Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Count_Complex_Roots/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Count_Complex_Roots/outline.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability/outline.pdf Timing E_Transcendental (4 threads, 106.303s elapsed time, 375.944s cpu time, 16.120s GC time, factor 3.54) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/E_Transcendental Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/E_Transcendental/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/E_Transcendental/outline.pdf Finished E_Transcendental (0:02:33 elapsed time, 0:07:39 cpu time, factor 2.99) Running HOL-Homology ... Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gromov_Hyperbolicity/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gromov_Hyperbolicity/outline.pdf Timing Gromov_Hyperbolicity (4 threads, 142.258s elapsed time, 471.048s cpu time, 15.328s GC time, factor 3.31) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gromov_Hyperbolicity Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gromov_Hyperbolicity/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gromov_Hyperbolicity/outline.pdf Finished Gromov_Hyperbolicity (0:02:35 elapsed time, 0:08:12 cpu time, factor 3.17) Running Winding_Number_Eval ... HOL-Homology: theory HOL-Cardinals.Fun_More HOL-Homology: theory HOL-Cardinals.Order_Relation_More HOL-Homology: theory HOL-Cardinals.Order_Union HOL-Homology: theory HOL-Library.Fun_Lexorder HOL-Homology: theory HOL-Algebra.Congruence HOL-Homology: theory HOL-Library.Equipollence HOL-Homology: theory HOL-Library.Groups_Big_Fun HOL-Homology: theory HOL-Cardinals.Wellfounded_More HOL-Homology: theory HOL-Library.More_List HOL-Homology: theory HOL-Cardinals.Wellorder_Relation HOL-Homology: theory HOL-Cardinals.Wellorder_Embedding HOL-Homology: theory HOL-Library.Poly_Mapping Winding_Number_Eval: theory HOL-Eisbach.Eisbach Winding_Number_Eval: theory HOL-Computational_Algebra.Fraction_Field Winding_Number_Eval: theory HOL-Library.More_List Winding_Number_Eval: theory HOL-Computational_Algebra.Field_as_Ring HOL-Homology: theory HOL-Cardinals.Wellorder_Constructions Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial HOL-Homology: theory HOL-Algebra.Order Winding_Number_Eval: theory HOL-Eisbach.Eisbach_Tools Winding_Number_Eval: theory Winding_Number_Eval.Missing_Topology HOL-Homology: theory HOL-Cardinals.Cardinal_Order_Relation Winding_Number_Eval: theory Winding_Number_Eval.Missing_Analysis Winding_Number_Eval: theory HOL-Computational_Algebra.Normalized_Fraction HOL-Homology: theory HOL-Algebra.Lattice HOL-Homology: theory HOL-Cardinals.Cardinal_Arithmetic HOL-Homology: theory HOL-Algebra.Complete_Lattice HOL-Homology: theory HOL-Algebra.Group HOL-Homology: theory HOL-Algebra.Coset HOL-Homology: theory HOL-Algebra.FiniteProduct HOL-Homology: theory HOL-Algebra.Ring HOL-Homology: theory HOL-Algebra.Generated_Groups Winding_Number_Eval: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra HOL-Homology: theory HOL-Algebra.Solvable_Groups Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial_Factorial HOL-Homology: theory HOL-Algebra.AbelCoset HOL-Homology: theory HOL-Algebra.Module Timing Ordinary_Differential_Equations (4 threads, 174.211s elapsed time, 548.996s cpu time, 15.340s GC time, factor 3.15) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ordinary_Differential_Equations HOL-Homology: theory HOL-Algebra.Ideal HOL-Homology: theory HOL-Algebra.RingHom HOL-Homology: theory HOL-Algebra.UnivPoly Timing Count_Complex_Roots (4 threads, 139.999s elapsed time, 379.036s cpu time, 9.428s GC time, factor 2.71) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Count_Complex_Roots Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Count_Complex_Roots/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Count_Complex_Roots/outline.pdf Finished Count_Complex_Roots (0:03:03 elapsed time, 0:07:32 cpu time, factor 2.47) Running Gauss_Jordan ... Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ordinary_Differential_Equations/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ordinary_Differential_Equations/outline.pdf Gauss_Jordan: theory HOL-Library.Code_Abstract_Nat Gauss_Jordan: theory HOL-Library.Code_Target_Int Gauss_Jordan: theory HOL-Library.Function_Algebras Gauss_Jordan: theory HOL-Library.IArray Gauss_Jordan: theory HOL-Library.Code_Target_Nat Gauss_Jordan: theory Gauss_Jordan.Code_Set Gauss_Jordan: theory HOL-Library.Z2 Gauss_Jordan: theory HOL-Library.Code_Real_Approx_By_Float Gauss_Jordan: theory HOL-Library.Code_Target_Numeral Gauss_Jordan: theory Rank_Nullity_Theorem.Dual_Order Gauss_Jordan: theory Rank_Nullity_Theorem.Mod_Type Gauss_Jordan: theory Gauss_Jordan.Code_Z2 Gauss_Jordan: theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell Gauss_Jordan: theory Gauss_Jordan.IArray_Addenda Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic Gauss_Jordan: theory Rank_Nullity_Theorem.Miscellaneous Timing HOL-Probability (4 threads, 132.107s elapsed time, 434.180s cpu time, 13.244s GC time, factor 3.29) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability/outline.pdf Finished HOL-Probability (0:03:09 elapsed time, 0:09:44 cpu time, factor 3.08) Building Markov_Models ... Gauss_Jordan: theory Gauss_Jordan.Code_Matrix Gauss_Jordan: theory Gauss_Jordan.Rref Gauss_Jordan: theory Rank_Nullity_Theorem.Fundamental_Subspaces Gauss_Jordan: theory Rank_Nullity_Theorem.Dim_Formula Markov_Models: theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun Markov_Models: theory HOL-Computational_Algebra.Group_Closure Markov_Models: theory HOL-Library.Case_Converter Markov_Models: theory HOL-Library.Code_Abstract_Nat Winding_Number_Eval: theory Sturm_Tarski.PolyMisc Markov_Models: theory HOL-Library.Code_Target_Nat Winding_Number_Eval: theory Sturm_Tarski.Sturm_Tarski Gauss_Jordan: theory Gauss_Jordan.Elementary_Operations Markov_Models: theory HOL-Library.Simps_Case_Conv Gauss_Jordan: theory Gauss_Jordan.Rank Markov_Models: theory HOL-Library.Code_Target_Int Markov_Models: theory HOL-Library.IArray Markov_Models: theory HOL-Library.While_Combinator Markov_Models: theory HOL-Library.Code_Target_Numeral Markov_Models: theory Coinductive.Coinductive_Nat Gauss_Jordan: theory Gauss_Jordan.Matrix_To_IArray Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan Winding_Number_Eval: theory Budan_Fourier.BF_Misc Markov_Models: theory Coinductive.Coinductive_List Winding_Number_Eval: theory Winding_Number_Eval.Missing_Algebraic Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_IArrays Gauss_Jordan: theory Gauss_Jordan.Linear_Maps HOL-Homology: theory HOL-Algebra.Multiplicative_Group Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_PA Winding_Number_Eval: theory Winding_Number_Eval.Missing_Transcendental Winding_Number_Eval: theory Winding_Number_Eval.Cauchy_Index_Theorem Gauss_Jordan: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces Gauss_Jordan: theory Gauss_Jordan.Determinants2 Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays Gauss_Jordan: theory Gauss_Jordan.Inverse Gauss_Jordan: theory Gauss_Jordan.System_Of_Equations Gauss_Jordan: theory Gauss_Jordan.Determinants_IArrays Gauss_Jordan: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces_IArrays Gauss_Jordan: theory Gauss_Jordan.Inverse_IArrays Gauss_Jordan: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract Gauss_Jordan: theory Gauss_Jordan.System_Of_Equations_IArrays Gauss_Jordan: theory Gauss_Jordan.Examples_Gauss_Jordan_IArrays Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval HOL-Homology: theory HOL-Algebra.Elementary_Groups Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval_Examples Timing QR_Decomposition (4 threads, 200.869s elapsed time, 722.788s cpu time, 18.024s GC time, factor 3.60) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/QR_Decomposition HOL-Homology: theory HOL-Algebra.Exact_Sequence HOL-Homology: theory HOL-Algebra.Product_Groups Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays HOL-Homology: theory HOL-Algebra.Free_Abelian_Groups Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays_SML Gauss_Jordan: theory Gauss_Jordan.Code_Rational Markov_Models: theory Coinductive.Coinductive_Stream HOL-Homology: theory HOL-Homology.Simplices Markov_Models: theory Markov_Models.Markov_Models_Auxiliary Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays_Haskell Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/QR_Decomposition/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/QR_Decomposition/outline.pdf HOL-Homology: theory HOL-Homology.Homology_Groups Timing QR_Decomposition (4 threads, 200.869s elapsed time, 722.788s cpu time, 18.024s GC time, factor 3.60) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/QR_Decomposition Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/QR_Decomposition/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/QR_Decomposition/outline.pdf Finished QR_Decomposition (0:03:28 elapsed time, 0:12:17 cpu time, factor 3.53) Building Probabilistic_While ... Markov_Models: theory Markov_Models.Discrete_Time_Markov_Process Markov_Models: theory Markov_Models.Discrete_Time_Markov_Chain HOL-Homology: theory HOL-Homology.Brouwer_Degree Probabilistic_While: theory Flow_Networks.Graph Probabilistic_While: theory HOL-Library.Transitive_Closure_Table Probabilistic_While: theory HOL-Library.While_Combinator Probabilistic_While: theory HOL-Types_To_Sets.Types_To_Sets Markov_Models: theory Markov_Models.Classifying_Markov_Chain_States Markov_Models: theory Markov_Models.Crowds_Protocol Markov_Models: theory Markov_Models.Gossip_Broadcast Markov_Models: theory Markov_Models.Markov_Decision_Process HOL-Homology: theory HOL-Homology.Invariance_of_Domain Probabilistic_While: theory Probabilistic_While.Bernoulli Probabilistic_While: theory HOL-Library.Bourbaki_Witt_Fixpoint Markov_Models: theory Markov_Models.PCTL Probabilistic_While: theory MFMC_Countable.MFMC_Misc HOL-Homology: theory HOL-Homology.Homology Probabilistic_While: theory Flow_Networks.Network Markov_Models: theory Markov_Models.Trace_Space_Equals_Markov_Processes Markov_Models: theory Markov_Models.Zeroconf_Analysis Markov_Models: theory Markov_Models.MDP_Reachability_Problem Probabilistic_While: theory Flow_Networks.Residual_Graph Markov_Models: theory Markov_Models.Example_A Markov_Models: theory Markov_Models.Example_B Markov_Models: theory Markov_Models.MDP_RP_Certification Markov_Models: theory Markov_Models.PGCL Probabilistic_While: theory Flow_Networks.Augmenting_Flow Probabilistic_While: theory Flow_Networks.Augmenting_Path Markov_Models: theory Markov_Models.Continuous_Time_Markov_Chain Probabilistic_While: theory Flow_Networks.Ford_Fulkerson Probabilistic_While: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract Probabilistic_While: theory MFMC_Countable.MFMC_Finite Markov_Models: theory Markov_Models.Markov_Models Probabilistic_While: theory MFMC_Countable.Matrix_For_Marginals Probabilistic_While: theory MFMC_Countable.Rel_PMF_Characterisation Probabilistic_While: theory Probabilistic_While.While_SPMF Probabilistic_While: theory Probabilistic_While.Resampling Probabilistic_While: theory Probabilistic_While.Fast_Dice_Roll Probabilistic_While: theory Probabilistic_While.Geometric Timing Dirichlet_Series (4 threads, 236.549s elapsed time, 788.268s cpu time, 66.496s GC time, factor 3.33) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_Series Timing Ordinary_Differential_Equations (4 threads, 174.211s elapsed time, 548.996s cpu time, 15.340s GC time, factor 3.15) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ordinary_Differential_Equations Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ordinary_Differential_Equations/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ordinary_Differential_Equations/outline.pdf Finished Ordinary_Differential_Equations (0:03:58 elapsed time, 0:11:00 cpu time, factor 2.77) Building HOL-ODE-Numerics ... HOL-ODE-Numerics: theory HOL-Eisbach.Eisbach HOL-ODE-Numerics: theory Automatic_Refinement.Foldi HOL-ODE-Numerics: theory Automatic_Refinement.Prio_List HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util_Bootstrap1 HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot HOL-ODE-Numerics: theory Deriving.Comparator HOL-ODE-Numerics: theory Deriving.Derive_Manager HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util HOL-ODE-Numerics: theory Deriving.Generator_Aux HOL-ODE-Numerics: theory Deriving.Equality_Generator HOL-ODE-Numerics: theory HOL-Library.AList HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve HOL-ODE-Numerics: theory Deriving.Equality_Instances HOL-ODE-Numerics: theory Deriving.Compare HOL-ODE-Numerics: theory Deriving.Comparator_Generator HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax HOL-ODE-Numerics: theory HOL-Library.Boolean_Algebra HOL-ODE-Numerics: theory HOL-Library.Permutation HOL-ODE-Numerics: theory HOL-ex.Quicksort HOL-ODE-Numerics: theory HOL-Library.Char_ord HOL-ODE-Numerics: theory Deriving.Compare_Generator HOL-ODE-Numerics: theory HOL-Library.Mapping HOL-ODE-Numerics: theory HOL-Library.Option_ord HOL-ODE-Numerics: theory Deriving.Compare_Instances HOL-ODE-Numerics: theory HOL-Library.Parallel Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_Series/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_Series/outline.pdf HOL-ODE-Numerics: theory Automatic_Refinement.Misc HOL-ODE-Numerics: theory HOL-Library.Type_Length HOL-ODE-Numerics: theory HOL-Library.RBT_Impl HOL-ODE-Numerics: theory HOL-Library.While_Combinator HOL-ODE-Numerics: theory HOL-Library.Z2 HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets HOL-ODE-Numerics: theory HOL-Word.Bits HOL-ODE-Numerics: theory HOL-Word.Bits_Z2 HOL-ODE-Numerics: theory HOL-Word.Misc_Auxiliary HOL-ODE-Numerics: theory HOL-Word.Misc_Typedef HOL-ODE-Numerics: theory HOL-Word.Bits_Int HOL-ODE-Numerics: theory HOL-Word.Misc_Arithmetic HOL-ODE-Numerics: theory Deriving.Countable_Generator HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer Timing Winding_Number_Eval (4 threads, 91.186s elapsed time, 234.724s cpu time, 6.532s GC time, factor 2.57) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Winding_Number_Eval HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict Timing Probabilistic_While (4 threads, 40.237s elapsed time, 109.680s cpu time, 2.708s GC time, factor 2.73) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_While HOL-ODE-Numerics: theory HOL-Word.Bit_Comprehension HOL-ODE-Numerics: theory Native_Word.More_Bits_Int HOL-ODE-Numerics: theory HOL-Word.Word HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib HOL-ODE-Numerics: theory Collections.SetIterator HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Phases HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tagging HOL-ODE-Numerics: theory Automatic_Refinement.Relators HOL-ODE-Numerics: theory Collections.SetIteratorOperations Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_While/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_While/outline.pdf HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Winding_Number_Eval/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Winding_Number_Eval/outline.pdf HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL Timing Winding_Number_Eval (4 threads, 91.186s elapsed time, 234.724s cpu time, 6.532s GC time, factor 2.57) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Winding_Number_Eval Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Winding_Number_Eval/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Winding_Number_Eval/outline.pdf Finished Winding_Number_Eval (0:01:40 elapsed time, 0:04:10 cpu time, factor 2.50) Running Differential_Dynamic_Logic ... HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops HOL-ODE-Numerics: theory Collections.Assoc_List HOL-ODE-Numerics: theory Collections.Diff_Array Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Ids Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Lib HOL-ODE-Numerics: theory Collections.Proper_Iterator Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Syntax HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel HOL-ODE-Numerics: theory Collections.It_to_It HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface HOL-ODE-Numerics: theory Collections.SetIteratorGA HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool HOL-ODE-Numerics: theory Native_Word.Code_Symbolic_Bits_Int HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL HOL-ODE-Numerics: theory Native_Word.Bits_Integer HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement HOL-ODE-Numerics: theory Collections.Intf_Comp HOL-ODE-Numerics: theory Collections.Idx_Iterator HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis Timing Transcendence_Series_Hancl_Rucki (4 threads, 268.695s elapsed time, 904.872s cpu time, 61.488s GC time, factor 3.37) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Transcendence_Series_Hancl_Rucki HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form HOL-ODE-Numerics: theory Collections.Impl_Array_Stack HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression Markov_Models: theory Markov_Models.MDP_RP Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Transcendence_Series_Hancl_Rucki/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Transcendence_Series_Hancl_Rucki/outline.pdf Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Denotational_Semantics Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Pretty_Printer HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection Timing Transcendence_Series_Hancl_Rucki (4 threads, 268.695s elapsed time, 904.872s cpu time, 61.488s GC time, factor 3.37) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Transcendence_Series_Hancl_Rucki Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Transcendence_Series_Hancl_Rucki/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Transcendence_Series_Hancl_Rucki/outline.pdf Finished Transcendence_Series_Hancl_Rucki (0:04:34 elapsed time, 0:15:16 cpu time, factor 3.33) Running Probabilistic_Prime_Tests ... Timing Markov_Models (4 threads, 83.495s elapsed time, 288.172s cpu time, 11.188s GC time, factor 3.45) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Markov_Models HOL-ODE-Numerics: theory Native_Word.Code_Target_Bits_Int HOL-ODE-Numerics: theory Collections.Code_Target_ICF HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base Probabilistic_Prime_Tests: theory HOL-Cardinals.Order_Relation_More Probabilistic_Prime_Tests: theory HOL-Cardinals.Fun_More Probabilistic_Prime_Tests: theory HOL-Cardinals.Order_Union Probabilistic_Prime_Tests: theory HOL-Algebra.Exponent Probabilistic_Prime_Tests: theory HOL-Computational_Algebra.Squarefree Probabilistic_Prime_Tests: theory HOL-Number_Theory.Cong Probabilistic_Prime_Tests: theory HOL-Library.Permutation Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellfounded_More Probabilistic_Prime_Tests: theory HOL-Library.Fun_Lexorder Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellorder_Relation Timing Gauss_Jordan (4 threads, 92.238s elapsed time, 335.636s cpu time, 7.008s GC time, factor 3.64) Probabilistic_Prime_Tests: theory HOL-Algebra.Congruence Probabilistic_Prime_Tests: theory HOL-Algebra.Cycles Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gauss_Jordan HOL-ODE-Numerics: theory Native_Word.Uint Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellorder_Embedding Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellorder_Constructions Probabilistic_Prime_Tests: theory HOL-Library.Equipollence Probabilistic_Prime_Tests: theory HOL-Library.Groups_Big_Fun Probabilistic_Prime_Tests: theory HOL-Algebra.Order Probabilistic_Prime_Tests: theory HOL-Library.More_List Probabilistic_Prime_Tests: theory HOL-Library.Power_By_Squaring Probabilistic_Prime_Tests: theory HOL-Cardinals.Cardinal_Order_Relation HOL-ODE-Numerics: theory Native_Word.Uint32 Probabilistic_Prime_Tests: theory HOL-Library.Poly_Mapping Probabilistic_Prime_Tests: theory HOL-Number_Theory.Mod_Exp HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method Probabilistic_Prime_Tests: theory HOL-Number_Theory.Eratosthenes Probabilistic_Prime_Tests: theory HOL-Algebra.Lattice Probabilistic_Prime_Tests: theory HOL-Cardinals.Cardinal_Arithmetic Probabilistic_Prime_Tests: theory HOL-Number_Theory.Fib HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta HOL-ODE-Numerics: theory Collections.HashCode Probabilistic_Prime_Tests: theory HOL-Number_Theory.Prime_Powers Probabilistic_Prime_Tests: theory HOL-Number_Theory.Totient HOL-ODE-Numerics: theory Collections.Intf_Hash Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Axioms Probabilistic_Prime_Tests: theory HOL-Algebra.Complete_Lattice Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Frechet_Correctness HOL-ODE-Numerics: theory Collections.Gen_Hash HOL-ODE-Numerics: theory Deriving.Hash_Generator Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Static_Semantics Probabilistic_Prime_Tests: theory HOL-Algebra.Galois_Connection Probabilistic_Prime_Tests: theory HOL-Algebra.Group HOL-ODE-Numerics: theory Deriving.Hash_Instances HOL-ODE-Numerics: theory Deriving.Derive HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE Timing Probabilistic_While (4 threads, 40.237s elapsed time, 109.680s cpu time, 2.708s GC time, factor 2.73) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_While Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_While/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_While/outline.pdf Finished Probabilistic_While (0:01:15 elapsed time, 0:02:47 cpu time, factor 2.23) Building CryptHOL ... Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Markov_Models/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Markov_Models/outline.pdf HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover HOL-ODE-Numerics: theory Show.Show HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc Probabilistic_Prime_Tests: theory HOL-Algebra.Bij Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gauss_Jordan/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gauss_Jordan/outline.pdf Probabilistic_Prime_Tests: theory HOL-Algebra.Coset Probabilistic_Prime_Tests: theory HOL-Algebra.FiniteProduct Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Coincidence Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst Probabilistic_Prime_Tests: theory HOL-Algebra.Ring CryptHOL: theory HOL-Eisbach.Eisbach CryptHOL: theory Applicative_Lifting.Applicative CryptHOL: theory CryptHOL.Partial_Function_Set CryptHOL: theory HOL-Library.Case_Converter Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Bound_Effect HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Axioms Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Uniform_Renaming CryptHOL: theory HOL-Library.Simps_Case_Conv Timing HOL-Homology (4 threads, 131.259s elapsed time, 448.892s cpu time, 18.576s GC time, factor 3.42) Timing Gauss_Jordan (4 threads, 92.238s elapsed time, 335.636s cpu time, 7.008s GC time, factor 3.64) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gauss_Jordan Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gauss_Jordan/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gauss_Jordan/outline.pdf Finished Gauss_Jordan (0:01:43 elapsed time, 0:05:55 cpu time, factor 3.44) Running Deep_Learning ... HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer CryptHOL: theory HOL-Algebra.Congruence Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Homology HOL-ODE-Numerics: theory Show.Show_Instances CryptHOL: theory HOL-Library.Function_Algebras HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert CryptHOL: theory HOL-Library.Type_Length HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion CryptHOL: theory HOL-Library.Countable_Set_Type CryptHOL: theory HOL-Library.Landau_Symbols Probabilistic_Prime_Tests: theory HOL-Algebra.Sylow Probabilistic_Prime_Tests: theory HOL-Algebra.Group_Action HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While CryptHOL: theory Applicative_Lifting.Applicative_Environment HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det CryptHOL: theory Applicative_Lifting.Applicative_Set Probabilistic_Prime_Tests: theory HOL-Algebra.Divisibility CryptHOL: theory CryptHOL.Environment_Functor CryptHOL: theory CryptHOL.Set_Applicative CryptHOL: theory HOL-Algebra.Order Probabilistic_Prime_Tests: theory HOL-Algebra.Zassenhaus CryptHOL: theory Coinductive.Coinductive_Nat HOL-ODE-Numerics: theory HOL-Library.RBT Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Groups Deep_Learning: theory HOL-Computational_Algebra.Fraction_Field Deep_Learning: theory Deep_Learning.Tensor Deep_Learning: theory HOL-Library.Fun_Lexorder Deep_Learning: theory Deep_Learning.DL_Missing_Finite_Set HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic Deep_Learning: theory HOL-Algebra.Congruence Deep_Learning: theory HOL-Library.Groups_Big_Fun HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping Deep_Learning: theory HOL-Library.More_List Probabilistic_Prime_Tests: theory HOL-Algebra.Solvable_Groups CryptHOL: theory Coinductive.Coinductive_List Deep_Learning: theory Deep_Learning.Tensor_Subtensor HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program Deep_Learning: theory HOL-Library.Poly_Mapping Probabilistic_Prime_Tests: theory HOL-Algebra.Sym_Groups Deep_Learning: theory Deep_Learning.Tensor_Plus CryptHOL: theory Applicative_Lifting.Applicative_PMF CryptHOL: theory HOL-Algebra.Lattice Deep_Learning: theory Deep_Learning.Tensor_Scalar_Mult Deep_Learning: theory Deep_Learning.Tensor_Product Deep_Learning: theory HOL-Algebra.Order Deep_Learning: theory Deep_Learning.Tensor_Unit_Vec Deep_Learning: theory Deep_Learning.Tensor_Rank Deep_Learning: theory HOL-Computational_Algebra.Normalized_Fraction Deep_Learning: theory Jordan_Normal_Form.Conjugate CryptHOL: theory Monad_Normalisation.Monad_Normalisation CryptHOL: theory Monomorphic_Monad.Monomorphic_Monad Probabilistic_Prime_Tests: theory HOL-Algebra.AbelCoset Probabilistic_Prime_Tests: theory HOL-Algebra.Module Deep_Learning: theory Polynomial_Interpolation.Missing_Unsorted CryptHOL: theory HOL-Algebra.Complete_Lattice Deep_Learning: theory Polynomials.MPoly_Type Deep_Learning: theory HOL-Algebra.Lattice HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof CryptHOL: theory HOL-Algebra.Group HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun CryptHOL: theory CryptHOL.SPMF_Applicative HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb HOL-ODE-Numerics: theory Refine_Monadic.Refine_While Deep_Learning: theory Polynomials.More_MPoly_Type Deep_Learning: theory HOL-Computational_Algebra.Polynomial CryptHOL: theory Landau_Symbols.Group_Sort Deep_Learning: theory HOL-Algebra.Complete_Lattice Deep_Learning: theory Deep_Learning.Lebesgue_Functional Deep_Learning: theory Jordan_Normal_Form.DL_Missing_List Deep_Learning: theory Jordan_Normal_Form.DL_Missing_Sublist Deep_Learning: theory Polynomial_Interpolation.Ring_Hom HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Homology/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Homology/manual.pdf Deep_Learning: theory HOL-Algebra.Group HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach CryptHOL: theory Landau_Symbols.Landau_Real_Products Timing HOL-Homology (4 threads, 131.259s elapsed time, 448.892s cpu time, 18.576s GC time, factor 3.42) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Homology Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Homology/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Homology/manual.pdf Finished HOL-Homology (0:02:21 elapsed time, 0:07:46 cpu time, factor 3.28) Running Density_Compiler ... CryptHOL: theory HOL-Algebra.Coset Deep_Learning: theory VectorSpace.FunctionLemmas Density_Compiler: theory Density_Compiler.Density_Predicates Deep_Learning: theory HOL-Algebra.Coset Deep_Learning: theory HOL-Algebra.FiniteProduct HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic Density_Compiler: theory Density_Compiler.PDF_Transformations Density_Compiler: theory Density_Compiler.PDF_Values CryptHOL: theory CryptHOL.Cyclic_Group Deep_Learning: theory HOL-Algebra.Ring Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst_Lemma Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal CryptHOL: theory Coinductive.TLList HOL-ODE-Numerics: theory Collections.Gen_Iterator CryptHOL: theory CryptHOL.Cyclic_Group_SPMF HOL-ODE-Numerics: theory Collections.Intf_Map HOL-ODE-Numerics: theory Collections.Intf_Set HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set HOL-ODE-Numerics: theory Collections.Iterator CryptHOL: theory Landau_Symbols.Landau_Simprocs HOL-ODE-Numerics: theory Collections.Array_Iterator HOL-ODE-Numerics: theory Collections.RBT_add HOL-ODE-Numerics: theory Collections.Gen_Map HOL-ODE-Numerics: theory Collections.Gen_Map2Set HOL-ODE-Numerics: theory Collections.Impl_Array_Map HOL-ODE-Numerics: theory Collections.Impl_List_Map Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal_Product Probabilistic_Prime_Tests: theory HOL-Algebra.RingHom HOL-ODE-Numerics: theory Collections.Impl_RBT_Map Density_Compiler: theory Density_Compiler.PDF_Semantics Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Proof_Checker HOL-ODE-Numerics: theory Collections.Gen_Set Deep_Learning: theory Polynomials.MPoly_Type_Univariate Deep_Learning: theory HOL-Computational_Algebra.Polynomial_Factorial CryptHOL: theory Landau_Symbols.Landau_More Deep_Learning: theory HOL-Algebra.Module HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map CryptHOL: theory CryptHOL.Negligible Deep_Learning: theory Jordan_Normal_Form.Missing_Ring Probabilistic_Prime_Tests: theory HOL-Algebra.QuotRing Probabilistic_Prime_Tests: theory HOL-Algebra.UnivPoly Deep_Learning: theory Deep_Learning.Lebesgue_Zero_Set HOL-ODE-Numerics: theory Collections.Impl_Bit_Set HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation Deep_Learning: theory VectorSpace.RingModuleFacts HOL-ODE-Numerics: theory Collections.Impl_List_Set HOL-ODE-Numerics: theory Collections.Impl_Uv_Set Deep_Learning: theory VectorSpace.MonoidSums Timing Affine_Arithmetic (4 threads, 308.630s elapsed time, 1084.416s cpu time, 71.188s GC time, factor 3.51) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic Probabilistic_Prime_Tests: theory HOL-Algebra.IntRing Probabilistic_Prime_Tests: theory HOL-Algebra.Weak_Morphisms Deep_Learning: theory VectorSpace.LinearCombinations Deep_Learning: theory Jordan_Normal_Form.Missing_Permutations Deep_Learning: theory Jordan_Normal_Form.Matrix Probabilistic_Prime_Tests: theory HOL-Algebra.Chinese_Remainder Density_Compiler: theory Density_Compiler.PDF_Density_Contexts Density_Compiler: theory Density_Compiler.PDF_Target_Semantics Density_Compiler: theory Density_Compiler.PDF_Compiler_Pred Deep_Learning: theory VectorSpace.SumSpaces Deep_Learning: theory Deep_Learning.DL_Concrete_Matrices Deep_Learning: theory Deep_Learning.DL_Flatten_Matrix Deep_Learning: theory Deep_Learning.DL_Network Deep_Learning: theory Deep_Learning.Tensor_Matricization Deep_Learning: theory Jordan_Normal_Form.DL_Submatrix CryptHOL: theory CryptHOL.Misc_CryptHOL Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic/outline.pdf Deep_Learning: theory Jordan_Normal_Form.Gauss_Jordan_Elimination HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code Deep_Learning: theory VectorSpace.VectorSpace Density_Compiler: theory Density_Compiler.PDF_Target_Density_Contexts Density_Compiler: theory Density_Compiler.PDF_Compiler Deep_Learning: theory Jordan_Normal_Form.Column_Operations Deep_Learning: theory Deep_Learning.DL_Shallow_Model HOL-ODE-Numerics: theory Affine_Arithmetic.Print Probabilistic_Prime_Tests: theory HOL-Algebra.Multiplicative_Group Timing Dirichlet_Series (4 threads, 236.549s elapsed time, 788.268s cpu time, 66.496s GC time, factor 3.33) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_Series Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_Series/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_Series/outline.pdf Finished Dirichlet_Series (0:05:25 elapsed time, 0:15:49 cpu time, factor 2.92) Building Zeta_Function ... HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Affine_Approximation HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Ineqs HOL-ODE-Numerics: theory Affine_Arithmetic.Ex_Inter HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp Deep_Learning: theory Jordan_Normal_Form.Missing_VectorSpace CryptHOL: theory CryptHOL.Generat CryptHOL: theory CryptHOL.List_Bits CryptHOL: theory CryptHOL.Resumption Zeta_Function: theory Bernoulli.Bernoulli_Zeta Probabilistic_Prime_Tests: theory HOL-Algebra.Elementary_Groups Probabilistic_Prime_Tests: theory HOL-Algebra.Ring_Divisibility Probabilistic_Prime_Tests: theory HOL-Algebra.Subrings Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residues Probabilistic_Prime_Tests: theory HOL-Algebra.Exact_Sequence Deep_Learning: theory Jordan_Normal_Form.Determinant Probabilistic_Prime_Tests: theory HOL-Algebra.Product_Groups Probabilistic_Prime_Tests: theory HOL-Number_Theory.Euler_Criterion Probabilistic_Prime_Tests: theory HOL-Number_Theory.Gauss CryptHOL: theory CryptHOL.Generative_Probabilistic_Value Probabilistic_Prime_Tests: theory HOL-Algebra.Free_Abelian_Groups Probabilistic_Prime_Tests: theory HOL-Number_Theory.Quadratic_Reciprocity Probabilistic_Prime_Tests: theory HOL-Algebra.Embedded_Algebras Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Rings Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Fields Probabilistic_Prime_Tests: theory HOL-Number_Theory.Pocklington Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residue_Primitive_Roots Deep_Learning: theory Deep_Learning.DL_Deep_Model HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc Probabilistic_Prime_Tests: theory HOL-Number_Theory.Number_Theory Deep_Learning: theory Jordan_Normal_Form.VS_Connect Zeta_Function: theory HOL-Eisbach.Eisbach Zeta_Function: theory HOL-Computational_Algebra.Field_as_Ring Zeta_Function: theory Sturm_Tarski.PolyMisc Zeta_Function: theory Winding_Number_Eval.Missing_Topology Zeta_Function: theory Winding_Number_Eval.Missing_Analysis Timing Markov_Models (4 threads, 83.495s elapsed time, 288.172s cpu time, 11.188s GC time, factor 3.45) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Markov_Models Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Markov_Models/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Markov_Models/outline.pdf Finished Markov_Models (0:02:24 elapsed time, 0:06:39 cpu time, factor 2.77) Running Stochastic_Matrices ... Zeta_Function: theory HOL-Eisbach.Eisbach_Tools Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Legendre_Symbol Zeta_Function: theory Sturm_Tarski.Sturm_Tarski Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Dynamic_Logic Stochastic_Matrices: theory HOL-Eisbach.Eisbach Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field Stochastic_Matrices: theory HOL-Algebra.Congruence Stochastic_Matrices: theory HOL-Library.Function_Algebras Deep_Learning: theory Deep_Learning.DL_Deep_Model_Poly Stochastic_Matrices: theory HOL-Library.More_List Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomials Timing Echelon_Form (4 threads, 337.040s elapsed time, 1067.324s cpu time, 115.508s GC time, factor 3.17) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Echelon_Form Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate Zeta_Function: theory Budan_Fourier.BF_Misc Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint Stochastic_Matrices: theory HOL-Algebra.Order Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial Zeta_Function: theory Winding_Number_Eval.Missing_Algebraic Stochastic_Matrices: theory HOL-Algebra.Lattice Zeta_Function: theory Winding_Number_Eval.Missing_Transcendental Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom Zeta_Function: theory Winding_Number_Eval.Cauchy_Index_Theorem Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice Stochastic_Matrices: theory HOL-Algebra.Group Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Echelon_Form/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Echelon_Form/outline.pdf Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type Zeta_Function: theory Winding_Number_Eval.Winding_Number_Eval Stochastic_Matrices: theory VectorSpace.FunctionLemmas Zeta_Function: theory Zeta_Function.Zeta_Function Stochastic_Matrices: theory HOL-Algebra.Coset Stochastic_Matrices: theory HOL-Algebra.FiniteProduct Deep_Learning: theory Jordan_Normal_Form.DL_Rank Stochastic_Matrices: theory HOL-Algebra.Ring Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous CryptHOL: theory CryptHOL.Computational_Model CryptHOL: theory CryptHOL.GPV_Applicative CryptHOL: theory CryptHOL.GPV_Expectation CryptHOL: theory CryptHOL.GPV_Bisim Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial CryptHOL: theory CryptHOL.CryptHOL Stochastic_Matrices: theory HOL-Algebra.Module Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String Stochastic_Matrices: theory VectorSpace.RingModuleFacts HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set Stochastic_Matrices: theory VectorSpace.MonoidSums Stochastic_Matrices: theory VectorSpace.LinearCombinations Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomial_Divisibility Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank Deep_Learning: theory Jordan_Normal_Form.DL_Rank_Submatrix Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Permutations Stochastic_Matrices: theory Jordan_Normal_Form.Matrix Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations Stochastic_Matrices: theory VectorSpace.SumSpaces Stochastic_Matrices: theory VectorSpace.VectorSpace Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace Stochastic_Matrices: theory Jordan_Normal_Form.Determinant Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form Timing Echelon_Form (4 threads, 337.040s elapsed time, 1067.324s cpu time, 115.508s GC time, factor 3.17) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Echelon_Form Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Echelon_Form/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Echelon_Form/outline.pdf Finished Echelon_Form (0:06:23 elapsed time, 0:19:07 cpu time, factor 2.99) Running Probabilistic_Timed_Automata ... Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.MDP_Aux Probabilistic_Timed_Automata: theory Timed_Automata.Misc Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Basic Probabilistic_Prime_Tests: theory HOL-Algebra.Finite_Extensions Probabilistic_Prime_Tests: theory HOL-Algebra.Indexed_Polynomials Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Instantiate_Existentials Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.More_List Probabilistic_Timed_Automata: theory Timed_Automata.Floyd_Warshall Probabilistic_Timed_Automata: theory Timed_Automata.Timed_Automata Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach_Tools Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Finiteness Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence_LTL Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Stream_More Timing CryptHOL (4 threads, 101.324s elapsed time, 366.800s cpu time, 24.320s GC time, factor 3.62) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CryptHOL Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Graphs Timing Zeta_Function (4 threads, 61.726s elapsed time, 189.160s cpu time, 4.740s GC time, factor 3.06) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Zeta_Function HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom Probabilistic_Timed_Automata: theory Timed_Automata.DBM Probabilistic_Timed_Automata: theory Timed_Automata.Paths_Cycles Probabilistic_Timed_Automata: theory Timed_Automata.Regions Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Basics Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Zeta_Function/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Zeta_Function/outline.pdf Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Normalization Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Operations Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CryptHOL/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CryptHOL/outline.pdf Probabilistic_Timed_Automata: theory Timed_Automata.Closure HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics Probabilistic_Timed_Automata: theory Timed_Automata.Regions_Beta Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector Probabilistic_Prime_Tests: theory HOL-Algebra.Algebraic_Closure Probabilistic_Timed_Automata: theory Timed_Automata.Approx_Beta Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius Timing Affine_Arithmetic (4 threads, 308.630s elapsed time, 1084.416s cpu time, 71.188s GC time, factor 3.51) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic/outline.pdf Finished Affine_Arithmetic (0:06:44 elapsed time, 0:21:59 cpu time, factor 3.26) Running Taylor_Models ... Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Lib Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible Taylor_Models: theory HOL-Decision_Procs.Rat_Pair Taylor_Models: theory HOL-Decision_Procs.Polynomial_List Probabilistic_Prime_Tests: theory HOL-Algebra.Algebra HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Generalized_Primality_Test Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Residues_Nat Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Jacobi_Symbol Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Carmichael_Numbers Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.QuadRes Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Euler_Witness Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Witness Timing Density_Compiler (4 threads, 120.452s elapsed time, 265.708s cpu time, 4.776s GC time, factor 2.21) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Density_Compiler Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Test Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Miller_Rabin_Test Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Solovay_Strassen_Test Taylor_Models: theory Taylor_Models.Polynomial_Expression Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Density_Compiler/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Density_Compiler/outline.pdf Timing Density_Compiler (4 threads, 120.452s elapsed time, 265.708s cpu time, 4.776s GC time, factor 2.21) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Density_Compiler Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Density_Compiler/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Density_Compiler/outline.pdf Finished Density_Compiler (0:02:10 elapsed time, 0:04:42 cpu time, factor 2.17) Running Hermite ... Hermite: theory Hermite.Hermite Timing Zeta_Function (4 threads, 61.726s elapsed time, 189.160s cpu time, 4.740s GC time, factor 3.06) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Zeta_Function Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Zeta_Function/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Zeta_Function/outline.pdf Finished Zeta_Function (0:01:44 elapsed time, 0:04:20 cpu time, factor 2.49) Running List_Update ... List_Update: theory HOL-Library.While_Combinator List_Update: theory List_Update.Prob_Theory List_Update: theory List_Update.Bit_Strings List_Update: theory List_Update.On_Off List_Update: theory List-Index.List_Index Hermite: theory Hermite.Hermite_IArrays List_Update: theory Regular-Sets.Regular_Set List_Update: theory List_Update.Inversion List_Update: theory List_Update.Swaps List_Update: theory List_Update.Competitive_Analysis List_Update: theory List_Update.Move_to_Front List_Update: theory Regular-Sets.Regular_Exp List_Update: theory Regular-Sets.NDerivative List_Update: theory List_Update.MTF2_Effects List_Update: theory List_Update.Partial_Cost_Model List_Update: theory List_Update.BIT List_Update: theory List_Update.List_Factoring List_Update: theory Regular-Sets.Equivalence_Checking List_Update: theory List_Update.RExp_Var List_Update: theory List_Update.BIT_pairwise List_Update: theory List_Update.OPT2 List_Update: theory List_Update.Phase_Partitioning List_Update: theory List_Update.BIT_2comp_on2 List_Update: theory List_Update.TS Timing CryptHOL (4 threads, 101.324s elapsed time, 366.800s cpu time, 24.320s GC time, factor 3.62) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CryptHOL Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CryptHOL/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CryptHOL/outline.pdf Finished CryptHOL (0:02:46 elapsed time, 0:08:12 cpu time, factor 2.97) Building Game_Based_Crypto ... Taylor_Models: theory HOL-Library.Function_Algebras Taylor_Models: theory Taylor_Models.Float_Topology Taylor_Models: theory Taylor_Models.Interval Taylor_Models: theory Taylor_Models.Taylor_Models_Misc Game_Based_Crypto: theory HOL-Library.LaTeXsugar Game_Based_Crypto: theory Game_Based_Crypto.Diffie_Hellman Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2_sym Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK_Single Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Function Game_Based_Crypto: theory Game_Based_Crypto.Pseudo_Random_Permutation Game_Based_Crypto: theory Game_Based_Crypto.Guessing_Many_One Game_Based_Crypto: theory Game_Based_Crypto.CryptHOL_Tutorial List_Update: theory List_Update.Comb Game_Based_Crypto: theory Game_Based_Crypto.PRF_UHF Game_Based_Crypto: theory Game_Based_Crypto.Unpredictable_Function Game_Based_Crypto: theory Game_Based_Crypto.RP_RF Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2 Taylor_Models: theory Taylor_Models.Horner_Eval Taylor_Models: theory Taylor_Models.Interval_Approximation Game_Based_Crypto: theory Game_Based_Crypto.Elgamal Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions Taylor_Models: theory Taylor_Models.Taylor_Models Timing Deep_Learning (4 threads, 180.304s elapsed time, 608.900s cpu time, 26.140s GC time, factor 3.38) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Deep_Learning Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Deep_Learning/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Deep_Learning/outline.pdf Timing Deep_Learning (4 threads, 180.304s elapsed time, 608.900s cpu time, 26.140s GC time, factor 3.38) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Deep_Learning Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Deep_Learning/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Deep_Learning/outline.pdf Finished Deep_Learning (0:03:08 elapsed time, 0:10:23 cpu time, factor 3.30) Running Constructive_Cryptography ... Constructive_Cryptography: theory Constructive_Cryptography.More_CryptHOL Timing Game_Based_Crypto (4 threads, 29.265s elapsed time, 107.244s cpu time, 2.812s GC time, factor 3.66) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Game_Based_Crypto Constructive_Cryptography: theory Constructive_Cryptography.Resource Constructive_Cryptography: theory Constructive_Cryptography.Converter Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Game_Based_Crypto/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Game_Based_Crypto/outline.pdf HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2 Taylor_Models: theory Taylor_Models.Experiments Constructive_Cryptography: theory Constructive_Cryptography.Converter_Rewrite Timing Differential_Dynamic_Logic (4 threads, 241.765s elapsed time, 522.736s cpu time, 15.788s GC time, factor 2.16) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Dynamic_Logic Constructive_Cryptography: theory Constructive_Cryptography.Random_System Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher Constructive_Cryptography: theory Constructive_Cryptography.Wiring Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography Constructive_Cryptography: theory Constructive_Cryptography.System_Construction Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Dynamic_Logic/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Dynamic_Logic/outline.pdf Timing Differential_Dynamic_Logic (4 threads, 241.765s elapsed time, 522.736s cpu time, 15.788s GC time, factor 2.16) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Dynamic_Logic Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Dynamic_Logic/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Dynamic_Logic/outline.pdf Finished Differential_Dynamic_Logic (0:04:14 elapsed time, 0:09:03 cpu time, factor 2.14) Running Prime_Harmonic_Series ... Timing Probabilistic_Prime_Tests (4 threads, 235.929s elapsed time, 888.872s cpu time, 78.296s GC time, factor 3.77) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Prime_Tests Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad Prime_Harmonic_Series: theory HOL-Number_Theory.Cong Prime_Harmonic_Series: theory HOL-Algebra.Congruence Prime_Harmonic_Series: theory HOL-Library.Power_By_Squaring Prime_Harmonic_Series: theory HOL-Number_Theory.Eratosthenes Prime_Harmonic_Series: theory HOL-Number_Theory.Fib Prime_Harmonic_Series: theory HOL-Number_Theory.Prime_Powers Prime_Harmonic_Series: theory HOL-Algebra.Order Prime_Harmonic_Series: theory HOL-Number_Theory.Mod_Exp Prime_Harmonic_Series: theory HOL-Number_Theory.Totient Prime_Harmonic_Series: theory HOL-Algebra.Lattice HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Prime_Tests/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Prime_Tests/outline.pdf Prime_Harmonic_Series: theory HOL-Algebra.Complete_Lattice Timing Probabilistic_Prime_Tests (4 threads, 235.929s elapsed time, 888.872s cpu time, 78.296s GC time, factor 3.77) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Prime_Tests Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Prime_Tests/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Prime_Tests/outline.pdf Finished Probabilistic_Prime_Tests (0:04:02 elapsed time, 0:15:01 cpu time, factor 3.71) Running Linear_Recurrences ... Prime_Harmonic_Series: theory HOL-Algebra.Group Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel Linear_Recurrences: theory HOL-Computational_Algebra.Group_Closure Linear_Recurrences: theory HOL-Library.BNF_Corec Linear_Recurrences: theory HOL-Computational_Algebra.Squarefree Linear_Recurrences: theory HOL-Computational_Algebra.Nth_Powers HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics Linear_Recurrences: theory HOL-Library.Code_Abstract_Nat Linear_Recurrences: theory HOL-Library.Code_Target_Int Linear_Recurrences: theory HOL-Library.Code_Target_Nat Linear_Recurrences: theory HOL-Library.Stirling Linear_Recurrences: theory HOL-Library.Code_Target_Numeral Constructive_Cryptography: theory Constructive_Cryptography.Examples Prime_Harmonic_Series: theory HOL-Algebra.Coset Linear_Recurrences: theory HOL-Library.Sublist Prime_Harmonic_Series: theory HOL-Algebra.FiniteProduct Linear_Recurrences: theory HOL-Real_Asymp.Inst_Existentials Linear_Recurrences: theory Polynomial_Interpolation.Missing_Unsorted Linear_Recurrences: theory HOL-Computational_Algebra.Polynomial_FPS HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics Prime_Harmonic_Series: theory HOL-Algebra.Ring Timing Taylor_Models (4 threads, 114.806s elapsed time, 322.508s cpu time, 11.680s GC time, factor 2.81) Linear_Recurrences: theory HOL-Computational_Algebra.Formal_Laurent_Series Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform Linear_Recurrences: theory HOL-Library.Landau_Symbols Prime_Harmonic_Series: theory HOL-Algebra.Generated_Groups Linear_Recurrences: theory Polynomial_Interpolation.Missing_Polynomial Linear_Recurrences: theory Polynomial_Factorization.Order_Polynomial Linear_Recurrences: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized Timing List_Update (4 threads, 92.066s elapsed time, 277.204s cpu time, 9.612s GC time, factor 3.01) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/List_Update Linear_Recurrences: theory Polynomial_Factorization.Polynomial_Divisibility Linear_Recurrences: theory HOL-Real_Asymp.Eventuallize Linear_Recurrences: theory HOL-Real_Asymp.Lazy_Eval Linear_Recurrences: theory Linear_Recurrences.Pochhammer_Polynomials Linear_Recurrences: theory HOL-Computational_Algebra.Computational_Algebra Timing Game_Based_Crypto (4 threads, 29.265s elapsed time, 107.244s cpu time, 2.812s GC time, factor 3.66) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Game_Based_Crypto Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Game_Based_Crypto/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Game_Based_Crypto/outline.pdf Finished Game_Based_Crypto (0:01:13 elapsed time, 0:03:01 cpu time, factor 2.48) Running Multi_Party_Computation ... Prime_Harmonic_Series: theory HOL-Algebra.AbelCoset Prime_Harmonic_Series: theory HOL-Algebra.Module Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models/outline.pdf Linear_Recurrences: theory Matrix.Utility Linear_Recurrences: theory Polynomial_Interpolation.Ring_Hom Timing Taylor_Models (4 threads, 114.806s elapsed time, 322.508s cpu time, 11.680s GC time, factor 2.81) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models/outline.pdf Finished Taylor_Models (0:02:01 elapsed time, 0:05:35 cpu time, factor 2.76) Running Ergodic_Theory ... HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis Linear_Recurrences: theory Linear_Recurrences.Eulerian_Polynomials Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Common Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Misc Linear_Recurrences: theory Linear_Recurrences.RatFPS Linear_Recurrences: theory Linear_Recurrences.Factorizations Linear_Recurrences: theory HOL-Real_Asymp.Multiseries_Expansion Linear_Recurrences: theory Linear_Recurrences.Partial_Fraction_Decomposition Multi_Party_Computation: theory HOL-Number_Theory.Cong Multi_Party_Computation: theory HOL-Algebra.FiniteProduct Multi_Party_Computation: theory HOL-Algebra.Generated_Groups Multi_Party_Computation: theory Multi_Party_Computation.ETP Ergodic_Theory: theory Ergodic_Theory.Fekete Ergodic_Theory: theory Ergodic_Theory.SG_Library_Complement Multi_Party_Computation: theory Multi_Party_Computation.Malicious_Defs Ergodic_Theory: theory Ergodic_Theory.Kohlberg_Neyman_Karlsson Multi_Party_Computation: theory Multi_Party_Computation.OT_Functionalities Multi_Party_Computation: theory HOL-Algebra.Ring Multi_Party_Computation: theory Multi_Party_Computation.Semi_Honest_Def Ergodic_Theory: theory Ergodic_Theory.Asymptotic_Density Prime_Harmonic_Series: theory HOL-Algebra.Ideal Multi_Party_Computation: theory Multi_Party_Computation.Uniform_Sampling Ergodic_Theory: theory Ergodic_Theory.Measure_Preserving_Transformations Multi_Party_Computation: theory HOL-Number_Theory.Totient Linear_Recurrences: theory Polynomial_Interpolation.Ring_Hom_Poly Multi_Party_Computation: theory Multi_Party_Computation.Cyclic_Group_Ext Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Solver Multi_Party_Computation: theory Multi_Party_Computation.ETP_OT Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA Multi_Party_Computation: theory Multi_Party_Computation.DH_Ext Linear_Recurrences: theory Linear_Recurrences.Linear_Homogenous_Recurrences Ergodic_Theory: theory Ergodic_Theory.Recurrence Linear_Recurrences: theory Polynomial_Factorization.Square_Free_Factorization Multi_Party_Computation: theory Multi_Party_Computation.Noar_Pinkas_OT Prime_Harmonic_Series: theory HOL-Algebra.RingHom Multi_Party_Computation: theory Multi_Party_Computation.OT14 Linear_Recurrences: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences Timing Hermite (4 threads, 105.343s elapsed time, 236.076s cpu time, 12.772s GC time, factor 2.24) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hermite Ergodic_Theory: theory Ergodic_Theory.Invariants Ergodic_Theory: theory Ergodic_Theory.Transfer_Operator Multi_Party_Computation: theory HOL-Algebra.AbelCoset Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/List_Update/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/List_Update/outline.pdf Prime_Harmonic_Series: theory HOL-Algebra.UnivPoly Ergodic_Theory: theory Ergodic_Theory.Normalizing_Sequences Ergodic_Theory: theory Ergodic_Theory.Ergodicity Timing List_Update (4 threads, 92.066s elapsed time, 277.204s cpu time, 9.612s GC time, factor 3.01) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/List_Update Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/List_Update/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/List_Update/outline.pdf Finished List_Update (0:01:44 elapsed time, 0:05:06 cpu time, factor 2.92) Running Green ... Multi_Party_Computation: theory HOL-Algebra.Module Ergodic_Theory: theory Ergodic_Theory.Kingman Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hermite/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hermite/outline.pdf Multi_Party_Computation: theory Multi_Party_Computation.GMW Green: theory Green.General_Utils Multi_Party_Computation: theory Multi_Party_Computation.Secure_Multiplication Timing Hermite (4 threads, 105.343s elapsed time, 236.076s cpu time, 12.772s GC time, factor 2.24) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hermite Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hermite/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hermite/outline.pdf Finished Hermite (0:01:51 elapsed time, 0:04:07 cpu time, factor 2.23) Running Pi_Transcendental ... Green: theory Green.Derivs Green: theory Green.Integrals Green: theory Green.Paths Ergodic_Theory: theory Ergodic_Theory.Gouezel_Karlsson HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1 Multi_Party_Computation: theory HOL-Algebra.Ideal Pi_Transcendental: theory HOL-Computational_Algebra.Fraction_Field Pi_Transcendental: theory HOL-Library.BNF_Corec Pi_Transcendental: theory HOL-Computational_Algebra.Group_Closure Pi_Transcendental: theory HOL-Computational_Algebra.Nth_Powers Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree Pi_Transcendental: theory HOL-Library.Fun_Lexorder Pi_Transcendental: theory HOL-Library.Groups_Big_Fun Pi_Transcendental: theory HOL-Real_Asymp.Inst_Existentials Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra Green: theory Green.Green Pi_Transcendental: theory HOL-Library.Poly_Mapping Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_FPS Pi_Transcendental: theory HOL-Computational_Algebra.Normalized_Fraction Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_Factorial Pi_Transcendental: theory HOL-Computational_Algebra.Formal_Laurent_Series Multi_Party_Computation: theory HOL-Algebra.RingHom Green: theory Green.SymmetricR2Shapes Green: theory Green.CircExample Pi_Transcendental: theory Polynomials.MPoly_Type Green: theory Green.DiamExample Multi_Party_Computation: theory HOL-Algebra.UnivPoly Pi_Transcendental: theory Polynomials.More_MPoly_Type Pi_Transcendental: theory HOL-Library.Landau_Symbols Pi_Transcendental: theory HOL-Real_Asymp.Eventuallize Pi_Transcendental: theory HOL-Real_Asymp.Lazy_Eval Prime_Harmonic_Series: theory HOL-Algebra.Multiplicative_Group Pi_Transcendental: theory HOL-Real_Asymp.Multiseries_Expansion HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA_Reachability Prime_Harmonic_Series: theory HOL-Number_Theory.Residues Prime_Harmonic_Series: theory HOL-Number_Theory.Euler_Criterion Prime_Harmonic_Series: theory HOL-Number_Theory.Gauss Prime_Harmonic_Series: theory HOL-Number_Theory.Quadratic_Reciprocity Prime_Harmonic_Series: theory HOL-Number_Theory.Pocklington Prime_Harmonic_Series: theory HOL-Number_Theory.Residue_Primitive_Roots Prime_Harmonic_Series: theory HOL-Number_Theory.Number_Theory Prime_Harmonic_Series: theory Prime_Harmonic_Series.Prime_Harmonic_Misc Prime_Harmonic_Series: theory Prime_Harmonic_Series.Squarefree_Nat Prime_Harmonic_Series: theory Prime_Harmonic_Series.Prime_Harmonic Multi_Party_Computation: theory HOL-Algebra.Multiplicative_Group Linear_Recurrences: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Linear_Recurrences: theory HOL-Real_Asymp.Real_Asymp Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Asymptotics Multi_Party_Computation: theory HOL-Number_Theory.Residues Multi_Party_Computation: theory Multi_Party_Computation.Number_Theory_Aux Multi_Party_Computation: theory Multi_Party_Computation.Malicious_OT Multi_Party_Computation: theory Multi_Party_Computation.ETP_RSA_OT Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library Pi_Transcendental: theory Symmetric_Polynomials.Vieta Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials Timing Probabilistic_Timed_Automata (4 threads, 193.803s elapsed time, 571.492s cpu time, 16.588s GC time, factor 2.95) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Timed_Automata Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Timed_Automata/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Timed_Automata/outline.pdf Timing Probabilistic_Timed_Automata (4 threads, 193.803s elapsed time, 571.492s cpu time, 16.588s GC time, factor 2.95) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Timed_Automata Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Timed_Automata/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Timed_Automata/outline.pdf Finished Probabilistic_Timed_Automata (0:03:22 elapsed time, 0:09:47 cpu time, factor 2.90) Building Girth_Chromatic ... Girth_Chromatic: theory HOL-Decision_Procs.Dense_Linear_Order Girth_Chromatic: theory HOL-Library.Code_Abstract_Nat Girth_Chromatic: theory HOL-Library.Code_Target_Int Girth_Chromatic: theory HOL-Library.Lattice_Algebras Girth_Chromatic: theory HOL-Library.Code_Target_Nat Girth_Chromatic: theory HOL-Library.Log_Nat Girth_Chromatic: theory HOL-Library.Code_Target_Numeral Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic_Misc Girth_Chromatic: theory Girth_Chromatic.Ugraphs Pi_Transcendental: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds Timing Prime_Harmonic_Series (4 threads, 81.196s elapsed time, 296.068s cpu time, 12.448s GC time, factor 3.65) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Harmonic_Series Pi_Transcendental: theory HOL-Real_Asymp.Real_Asymp Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1 Girth_Chromatic: theory HOL-Library.Float Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Harmonic_Series/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Harmonic_Series/outline.pdf Timing Prime_Harmonic_Series (4 threads, 81.196s elapsed time, 296.068s cpu time, 12.448s GC time, factor 3.65) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Harmonic_Series Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Harmonic_Series/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Harmonic_Series/outline.pdf Finished Prime_Harmonic_Series (0:01:26 elapsed time, 0:05:07 cpu time, factor 3.55) Running Akra_Bazzi ... Akra_Bazzi: theory HOL-Decision_Procs.Dense_Linear_Order Akra_Bazzi: theory HOL-Library.Code_Abstract_Nat Akra_Bazzi: theory HOL-Library.Code_Target_Int Akra_Bazzi: theory HOL-Library.Function_Algebras Akra_Bazzi: theory HOL-Library.Code_Target_Nat Akra_Bazzi: theory Akra_Bazzi.Eval_Numeral Akra_Bazzi: theory HOL-Library.Landau_Symbols Akra_Bazzi: theory HOL-Library.Code_Target_Numeral Girth_Chromatic: theory HOL-Decision_Procs.Approximation_Bounds Akra_Bazzi: theory HOL-Library.Lattice_Algebras Akra_Bazzi: theory HOL-Library.Log_Nat Akra_Bazzi: theory Landau_Symbols.Group_Sort Timing Constructive_Cryptography (4 threads, 122.153s elapsed time, 389.500s cpu time, 5.712s GC time, factor 3.19) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography Akra_Bazzi: theory Landau_Symbols.Landau_Real_Products Timing Linear_Recurrences (4 threads, 84.528s elapsed time, 319.968s cpu time, 12.456s GC time, factor 3.79) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Recurrences Girth_Chromatic: theory HOL-Decision_Procs.Approximation Timing Ergodic_Theory (4 threads, 77.808s elapsed time, 267.776s cpu time, 5.624s GC time, factor 3.44) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ergodic_Theory Akra_Bazzi: theory HOL-Library.Float Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Recurrences/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Recurrences/outline.pdf Akra_Bazzi: theory Landau_Symbols.Landau_Simprocs Akra_Bazzi: theory Landau_Symbols.Landau_More Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography/outline.pdf Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Library Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Asymptotics Timing Linear_Recurrences (4 threads, 84.528s elapsed time, 319.968s cpu time, 12.456s GC time, factor 3.79) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Recurrences Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Recurrences/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Recurrences/outline.pdf Finished Linear_Recurrences (0:01:30 elapsed time, 0:05:31 cpu time, factor 3.66) Running Differential_Game_Logic ... Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Real Timing Constructive_Cryptography (4 threads, 122.153s elapsed time, 389.500s cpu time, 5.712s GC time, factor 3.19) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography/outline.pdf Finished Constructive_Cryptography (0:02:12 elapsed time, 0:06:47 cpu time, factor 3.08) Running Probabilistic_Noninterference ... Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi Akra_Bazzi: theory HOL-Decision_Procs.Approximation_Bounds Differential_Game_Logic: theory Differential_Game_Logic.Identifiers Differential_Game_Logic: theory Differential_Game_Logic.Lib Differential_Game_Logic: theory Differential_Game_Logic.Syntax Probabilistic_Noninterference: theory HOL-Library.Case_Converter Probabilistic_Noninterference: theory HOL-Library.Prefix_Order Probabilistic_Noninterference: theory Coinductive.Coinductive_Nat Probabilistic_Noninterference: theory HOL-Library.Simps_Case_Conv Akra_Bazzi: theory Akra_Bazzi.Master_Theorem Probabilistic_Noninterference: theory Coinductive.Coinductive_List Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Method Akra_Bazzi: theory HOL-Decision_Procs.Approximation Timing Green (4 threads, 77.287s elapsed time, 264.088s cpu time, 3.840s GC time, factor 3.42) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Green Differential_Game_Logic: theory Differential_Game_Logic.Denotational_Semantics Differential_Game_Logic: theory Differential_Game_Logic.Ids Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ergodic_Theory/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ergodic_Theory/outline.pdf Timing Ergodic_Theory (4 threads, 77.808s elapsed time, 267.776s cpu time, 5.624s GC time, factor 3.44) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ergodic_Theory Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ergodic_Theory/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ergodic_Theory/outline.pdf Finished Ergodic_Theory (0:01:30 elapsed time, 0:04:48 cpu time, factor 3.18) Building Applicative_Lifting ... Applicative_Lifting: theory Applicative_Lifting.Applicative Applicative_Lifting: theory Applicative_Lifting.Joinable Applicative_Lifting: theory HOL-Library.State_Monad Applicative_Lifting: theory HOL-Library.Dlist Applicative_Lifting: theory HOL-Library.Function_Algebras Applicative_Lifting: theory HOL-Library.Function_Division Applicative_Lifting: theory HOL-Nonstandard_Analysis.Free_Ultrafilter Applicative_Lifting: theory HOL-Nonstandard_Analysis.StarDef Differential_Game_Logic: theory Differential_Game_Logic.Axioms Differential_Game_Logic: theory Differential_Game_Logic.Static_Semantics Differential_Game_Logic: theory Differential_Game_Logic.Coincidence Timing Pi_Transcendental (4 threads, 80.052s elapsed time, 259.984s cpu time, 11.784s GC time, factor 3.25) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Pi_Transcendental Probabilistic_Noninterference: theory Coinductive.Coinductive_Stream Applicative_Lifting: theory HOL-Proofs-Lambda.Commutation Applicative_Lifting: theory HOL-Proofs-Lambda.Lambda Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment Applicative_Lifting: theory Applicative_Lifting.Applicative_List Applicative_Lifting: theory Applicative_Lifting.Applicative_Monoid Applicative_Lifting: theory Applicative_Lifting.Applicative_Open_State Applicative_Lifting: theory Applicative_Lifting.Applicative_Option Applicative_Lifting: theory Applicative_Lifting.Applicative_Set Probabilistic_Noninterference: theory Markov_Models.Markov_Models_Auxiliary Applicative_Lifting: theory Applicative_Lifting.Applicative_Sum Differential_Game_Logic: theory Differential_Game_Logic.USubst Applicative_Lifting: theory Applicative_Lifting.Applicative_State Applicative_Lifting: theory Applicative_Lifting.Applicative_DNEList Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment_Algebra Applicative_Lifting: theory Applicative_Lifting.Applicative_Star Applicative_Lifting: theory Applicative_Lifting.Applicative_Stream Applicative_Lifting: theory HOL-Proofs-Lambda.ParRed Applicative_Lifting: theory Applicative_Lifting.Applicative_Filter Applicative_Lifting: theory Applicative_Lifting.Applicative_Probability_List Applicative_Lifting: theory Applicative_Lifting.Stream_Algebra Applicative_Lifting: theory HOL-Proofs-Lambda.Eta Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Green/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Green/outline.pdf Applicative_Lifting: theory Applicative_Lifting.Applicative_Vector Applicative_Lifting: theory Applicative_Lifting.Beta_Eta Applicative_Lifting: theory Applicative_Lifting.Applicative_PMF Timing Green (4 threads, 77.287s elapsed time, 264.088s cpu time, 3.840s GC time, factor 3.42) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Green Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Green/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Green/outline.pdf Finished Green (0:01:27 elapsed time, 0:04:47 cpu time, factor 3.29) Running Hidden_Markov_Models ... Applicative_Lifting: theory Applicative_Lifting.Combinators Applicative_Lifting: theory Applicative_Lifting.Idiomatic_Terms Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Pi_Transcendental/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Pi_Transcendental/outline.pdf Probabilistic_Noninterference: theory Markov_Models.Discrete_Time_Markov_Chain Timing Pi_Transcendental (4 threads, 80.052s elapsed time, 259.984s cpu time, 11.784s GC time, factor 3.25) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Pi_Transcendental Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Pi_Transcendental/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Pi_Transcendental/outline.pdf Finished Pi_Transcendental (0:01:26 elapsed time, 0:04:31 cpu time, factor 3.14) Running DiscretePricing ... Hidden_Markov_Models: theory Hidden_Markov_Models.Auxiliary Hidden_Markov_Models: theory HOL-Library.State_Monad Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap Hidden_Markov_Models: theory Hidden_Markov_Models.Hidden_Markov_Model Hidden_Markov_Models: theory Monad_Memo_DP.Pure_Monad Applicative_Lifting: theory Applicative_Lifting.Applicative_Functor Applicative_Lifting: theory Applicative_Lifting.Tree_Relabelling Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc Probabilistic_Noninterference: theory Probabilistic_Noninterference.Interface DiscretePricing: theory DiscretePricing.Filtration DiscretePricing: theory DiscretePricing.Generated_Subalgebra Differential_Game_Logic: theory Differential_Game_Logic.Differential_Game_Logic DiscretePricing: theory DiscretePricing.Disc_Cond_Expect Hidden_Markov_Models: theory Monad_Memo_DP.State_Monad_Ext Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVS Hidden_Markov_Models: theory HOL-Imperative_HOL.Heap_Monad Hidden_Markov_Models: theory Monad_Memo_DP.Memory DiscretePricing: theory DiscretePricing.Martingale DiscretePricing: theory DiscretePricing.Infinite_Coin_Toss_Space Hidden_Markov_Models: theory HOL-Imperative_HOL.Array Hidden_Markov_Models: theory HOL-Imperative_HOL.Ref Hidden_Markov_Models: theory HOL-Imperative_HOL.Imperative_HOL Hidden_Markov_Models: theory Monad_Memo_DP.Heap_Monad_Ext Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap Applicative_Lifting: theory Applicative_Lifting.Applicative_Examples Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace Probabilistic_Noninterference: theory Probabilistic_Noninterference.Language_Semantics Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd Hidden_Markov_Models: theory Monad_Memo_DP.State_Main Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models DiscretePricing: theory DiscretePricing.Geometric_Random_Walk DiscretePricing: theory DiscretePricing.Fair_Price Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius Probabilistic_Noninterference: theory Probabilistic_Noninterference.Resumption_Based Timing Stochastic_Matrices (4 threads, 306.121s elapsed time, 809.988s cpu time, 32.140s GC time, factor 2.65) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stochastic_Matrices DiscretePricing: theory DiscretePricing.CRR_Model Applicative_Lifting: theory Applicative_Lifting.Abstract_AF Applicative_Lifting: theory Applicative_Lifting.Applicative_Test Probabilistic_Noninterference: theory Probabilistic_Noninterference.Compositionality Probabilistic_Noninterference: theory Probabilistic_Noninterference.Trace_Based Timing Applicative_Lifting (4 threads, 25.498s elapsed time, 74.604s cpu time, 4.452s GC time, factor 2.93) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Applicative_Lifting Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stochastic_Matrices/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stochastic_Matrices/outline.pdf Timing Stochastic_Matrices (4 threads, 306.121s elapsed time, 809.988s cpu time, 32.140s GC time, factor 2.65) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stochastic_Matrices Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stochastic_Matrices/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stochastic_Matrices/outline.pdf Finished Stochastic_Matrices (0:05:11 elapsed time, 0:13:40 cpu time, factor 2.63) Running Irrationality_J_Hancl ... Probabilistic_Noninterference: theory Probabilistic_Noninterference.Syntactic_Criteria Irrationality_J_Hancl: theory HOL-Library.Code_Abstract_Nat Irrationality_J_Hancl: theory HOL-Decision_Procs.Dense_Linear_Order Irrationality_J_Hancl: theory HOL-Library.Code_Target_Int Irrationality_J_Hancl: theory HOL-Library.Lattice_Algebras Irrationality_J_Hancl: theory HOL-Library.Code_Target_Nat Irrationality_J_Hancl: theory HOL-Library.Log_Nat Irrationality_J_Hancl: theory HOL-Library.Code_Target_Numeral Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Applicative_Lifting/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Applicative_Lifting/outline.pdf Probabilistic_Noninterference: theory Probabilistic_Noninterference.Concrete DiscretePricing: theory DiscretePricing.Option_Price_Examples Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic Irrationality_J_Hancl: theory HOL-Library.Float Irrationality_J_Hancl: theory HOL-Decision_Procs.Approximation_Bounds Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation Timing Girth_Chromatic (4 threads, 68.328s elapsed time, 147.268s cpu time, 5.728s GC time, factor 2.16) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic/outline.pdf Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Approximation Irrationality_J_Hancl: theory HOL-Decision_Procs.Approximation Akra_Bazzi: theory Akra_Bazzi.Master_Theorem_Examples Timing Akra_Bazzi (4 threads, 66.126s elapsed time, 210.256s cpu time, 8.204s GC time, factor 3.18) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Akra_Bazzi Timing Multi_Party_Computation (4 threads, 138.878s elapsed time, 516.096s cpu time, 13.956s GC time, factor 3.72) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Multi_Party_Computation Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Akra_Bazzi/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Akra_Bazzi/outline.pdf Timing Akra_Bazzi (4 threads, 66.126s elapsed time, 210.256s cpu time, 8.204s GC time, factor 3.18) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Akra_Bazzi Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Akra_Bazzi/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Akra_Bazzi/outline.pdf Finished Akra_Bazzi (0:01:12 elapsed time, 0:03:42 cpu time, factor 3.06) Running MFMC_Countable ... Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Multi_Party_Computation/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Multi_Party_Computation/outline.pdf MFMC_Countable: theory Flow_Networks.Graph MFMC_Countable: theory HOL-Library.Transitive_Closure_Table MFMC_Countable: theory HOL-Library.While_Combinator HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1 MFMC_Countable: theory HOL-Library.Bourbaki_Witt_Fixpoint Timing Multi_Party_Computation (4 threads, 138.878s elapsed time, 516.096s cpu time, 13.956s GC time, factor 3.72) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Multi_Party_Computation Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Multi_Party_Computation/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Multi_Party_Computation/outline.pdf Finished Multi_Party_Computation (0:02:27 elapsed time, 0:08:51 cpu time, factor 3.61) Running Dirichlet_L ... MFMC_Countable: theory MFMC_Countable.MFMC_Misc MFMC_Countable: theory Flow_Networks.Network MFMC_Countable: theory MFMC_Countable.Max_Flow_Min_Cut_Countable Dirichlet_L: theory HOL-Decision_Procs.Dense_Linear_Order Dirichlet_L: theory HOL-Library.Lattice_Algebras Dirichlet_L: theory HOL-Library.Log_Nat Dirichlet_L: theory Lehmer.Lehmer Dirichlet_L: theory Pratt_Certificate.Pratt_Certificate MFMC_Countable: theory Flow_Networks.Residual_Graph MFMC_Countable: theory Flow_Networks.Augmenting_Flow MFMC_Countable: theory Flow_Networks.Augmenting_Path MFMC_Countable: theory Flow_Networks.Ford_Fulkerson MFMC_Countable: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract MFMC_Countable: theory MFMC_Countable.MFMC_Finite Timing Applicative_Lifting (4 threads, 25.498s elapsed time, 74.604s cpu time, 4.452s GC time, factor 2.93) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Applicative_Lifting Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Applicative_Lifting/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Applicative_Lifting/outline.pdf Finished Applicative_Lifting (0:01:01 elapsed time, 0:02:18 cpu time, factor 2.24) Building Randomised_Social_Choice ... MFMC_Countable: theory MFMC_Countable.Matrix_For_Marginals MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation Randomised_Social_Choice: theory Randomised_Social_Choice.Lotteries Randomised_Social_Choice: theory Randomised_Social_Choice.QSOpt_Exact Randomised_Social_Choice: theory List-Index.List_Index Timing Probabilistic_Noninterference (4 threads, 71.050s elapsed time, 236.168s cpu time, 6.988s GC time, factor 3.32) Dirichlet_L: theory HOL-Library.Float Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Noninterference Randomised_Social_Choice: theory Randomised_Social_Choice.Order_Predicates Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profiles Randomised_Social_Choice: theory Randomised_Social_Choice.Elections Randomised_Social_Choice: theory Randomised_Social_Choice.Utility_Functions Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profile_Cmd Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds Timing Differential_Game_Logic (4 threads, 74.819s elapsed time, 131.748s cpu time, 3.868s GC time, factor 1.76) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Game_Logic Randomised_Social_Choice: theory Randomised_Social_Choice.Stochastic_Dominance Randomised_Social_Choice: theory Randomised_Social_Choice.SD_Efficiency Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example Randomised_Social_Choice: theory Randomised_Social_Choice.Social_Decision_Schemes Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Noninterference/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Noninterference/outline.pdf Timing DiscretePricing (4 threads, 60.734s elapsed time, 205.216s cpu time, 7.560s GC time, factor 3.38) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DiscretePricing Timing Probabilistic_Noninterference (4 threads, 71.050s elapsed time, 236.168s cpu time, 6.988s GC time, factor 3.32) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Noninterference Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Noninterference/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Noninterference/outline.pdf Finished Probabilistic_Noninterference (0:01:18 elapsed time, 0:04:15 cpu time, factor 3.25) Running Stern_Brocot ... Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Dictatorship Dirichlet_L: theory Bertrands_Postulate.Bertrand Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Automation Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Serial_Dictatorship Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Lowering Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Game_Logic/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Game_Logic/outline.pdf Stern_Brocot: theory HOL-Library.BNF_Corec Randomised_Social_Choice: theory Randomised_Social_Choice.Randomised_Social_Choice Timing Differential_Game_Logic (4 threads, 74.819s elapsed time, 131.748s cpu time, 3.868s GC time, factor 1.76) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Game_Logic Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Game_Logic/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Game_Logic/outline.pdf Finished Differential_Game_Logic (0:01:21 elapsed time, 0:02:24 cpu time, factor 1.77) Running Smooth_Manifolds ... Smooth_Manifolds: theory HOL-Library.Function_Algebras Smooth_Manifolds: theory HOL-Library.Quotient_Syntax Smooth_Manifolds: theory HOL-Types_To_Sets.Prerequisites Smooth_Manifolds: theory HOL-Types_To_Sets.Types_To_Sets Smooth_Manifolds: theory HOL-Library.Quotient_Set Smooth_Manifolds: theory HOL-Types_To_Sets.Group_On_With Timing Randomised_Social_Choice (4 threads, 12.322s elapsed time, 46.044s cpu time, 1.852s GC time, factor 3.74) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_Social_Choice Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On_With Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On Timing Girth_Chromatic (4 threads, 68.328s elapsed time, 147.268s cpu time, 5.728s GC time, factor 2.16) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic/outline.pdf Finished Girth_Chromatic (0:01:48 elapsed time, 0:03:36 cpu time, factor 2.00) Running Prime_Distribution_Elementary ... Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DiscretePricing/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DiscretePricing/outline.pdf Timing Hidden_Markov_Models (4 threads, 71.228s elapsed time, 127.548s cpu time, 7.904s GC time, factor 1.79) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hidden_Markov_Models Timing DiscretePricing (4 threads, 60.734s elapsed time, 205.216s cpu time, 7.560s GC time, factor 3.38) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DiscretePricing Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DiscretePricing/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DiscretePricing/outline.pdf Finished DiscretePricing (0:01:11 elapsed time, 0:03:43 cpu time, factor 3.11) Running Treaps ... Stern_Brocot: theory Stern_Brocot.Cotree Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primes_Omega Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Number_Theorem_Library Prime_Distribution_Elementary: theory Stirling_Formula.Stirling_Formula Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_Social_Choice/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_Social_Choice/outline.pdf Treaps: theory HOL-Data_Structures.Cmp Treaps: theory HOL-Data_Structures.Less_False Treaps: theory HOL-Library.Function_Algebras Treaps: theory HOL-Library.Landau_Symbols Treaps: theory HOL-Data_Structures.Sorted_Less Treaps: theory HOL-Data_Structures.List_Ins_Del Treaps: theory Landau_Symbols.Group_Sort Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions Treaps: theory HOL-Data_Structures.Set_Specs Treaps: theory List-Index.List_Index Treaps: theory HOL-Data_Structures.Tree_Set Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hidden_Markov_Models/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hidden_Markov_Models/outline.pdf Treaps: theory Comparison_Sort_Lower_Bound.Linorder_Relations Timing Hidden_Markov_Models (4 threads, 71.228s elapsed time, 127.548s cpu time, 7.904s GC time, factor 1.79) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hidden_Markov_Models Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hidden_Markov_Models/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hidden_Markov_Models/outline.pdf Finished Hidden_Markov_Models (0:01:17 elapsed time, 0:02:19 cpu time, factor 1.80) Running Monomorphic_Monad ... Treaps: theory Landau_Symbols.Landau_Real_Products Monomorphic_Monad: theory HOL-Library.Countable_Set_Type Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Lcm_Nat_Upto Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library Prime_Distribution_Elementary: theory Prime_Number_Theorem.Mertens_Theorems Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.More_Dirichlet_Misc Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Elementary_Prime_Bounds Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Primorial Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Shapiro_Tauberian Monomorphic_Monad: theory Monomorphic_Monad.Monomorphic_Monad Stern_Brocot: theory Stern_Brocot.Cotree_Algebra Irrationality_J_Hancl: theory Irrationality_J_Hancl.Irrationality_J_Hancl Treaps: theory Landau_Symbols.Landau_Simprocs Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula Treaps: theory Landau_Symbols.Landau_More Smooth_Manifolds: theory Smooth_Manifolds.Analysis_More Treaps: theory Quick_Sort_Cost.Randomised_Quick_Sort Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences Timing Irrationality_J_Hancl (4 threads, 61.897s elapsed time, 134.476s cpu time, 4.904s GC time, factor 2.17) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Irrationality_J_Hancl Smooth_Manifolds: theory Smooth_Manifolds.Chart Smooth_Manifolds: theory Smooth_Manifolds.Smooth Treaps: theory Quick_Sort_Cost.Quick_Sort_Average_Case Smooth_Manifolds: theory Smooth_Manifolds.Topological_Manifold Smooth_Manifolds: theory Smooth_Manifolds.Bump_Function Smooth_Manifolds: theory Smooth_Manifolds.Differentiable_Manifold Treaps: theory Random_BSTs.Random_BSTs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Irrationality_J_Hancl/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Irrationality_J_Hancl/outline.pdf Smooth_Manifolds: theory Smooth_Manifolds.Partition_Of_Unity Smooth_Manifolds: theory Smooth_Manifolds.Product_Manifold Smooth_Manifolds: theory Smooth_Manifolds.Projective_Space Smooth_Manifolds: theory Smooth_Manifolds.Sphere Smooth_Manifolds: theory Smooth_Manifolds.Tangent_Space Timing Irrationality_J_Hancl (4 threads, 61.897s elapsed time, 134.476s cpu time, 4.904s GC time, factor 2.17) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Irrationality_J_Hancl Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Irrationality_J_Hancl/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Irrationality_J_Hancl/outline.pdf Finished Irrationality_J_Hancl (0:01:08 elapsed time, 0:02:25 cpu time, factor 2.14) Running Prime_Number_Theorem ... Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem_Library Prime_Number_Theorem: theory Stirling_Formula.Stirling_Formula Treaps: theory Treaps.Treap Treaps: theory Treaps.Probability_Misc Treaps: theory Treaps.Random_List_Permutation Treaps: theory Treaps.Treap_Sort_and_BSTs Prime_Number_Theorem: theory Prime_Number_Theorem.Newman_Ingham_Tauberian Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Counting_Functions Smooth_Manifolds: theory Smooth_Manifolds.Cotangent_Space Treaps: theory Treaps.Random_Treap Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem Prime_Number_Theorem: theory Prime_Number_Theorem.Mertens_Theorems Dirichlet_L: theory Dirichlet_L.Group_Adjoin Timing Randomised_Social_Choice (4 threads, 12.322s elapsed time, 46.044s cpu time, 1.852s GC time, factor 3.74) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_Social_Choice Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_Social_Choice/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_Social_Choice/outline.pdf Finished Randomised_Social_Choice (0:00:43 elapsed time, 0:01:38 cpu time, factor 2.25) Running SDS_Impossibility ... Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions Monomorphic_Monad: theory Monomorphic_Monad.Interpreter Monomorphic_Monad: theory Monomorphic_Monad.Just_Do_It_Examples Monomorphic_Monad: theory Monomorphic_Monad.Monad_Overloading Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Smooth_Manifolds Timing MFMC_Countable (4 threads, 61.653s elapsed time, 190.184s cpu time, 5.568s GC time, factor 3.08) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MFMC_Countable Stern_Brocot: theory Stern_Brocot.Bird_Tree Timing Prime_Distribution_Elementary (4 threads, 37.479s elapsed time, 138.980s cpu time, 3.004s GC time, factor 3.71) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary Timing Stern_Brocot (4 threads, 45.497s elapsed time, 74.556s cpu time, 4.320s GC time, factor 1.64) Timing Treaps (4 threads, 36.446s elapsed time, 120.524s cpu time, 3.756s GC time, factor 3.31) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stern_Brocot Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Treaps Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Smooth_Manifolds/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Smooth_Manifolds/outline.pdf Timing Monomorphic_Monad (4 threads, 34.124s elapsed time, 60.764s cpu time, 2.984s GC time, factor 1.78) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monomorphic_Monad Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Smooth_Manifolds Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Smooth_Manifolds/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Smooth_Manifolds/outline.pdf Smooth_Manifolds FAILED (see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64_32-linux/log/Smooth_Manifolds) *** x \ Basis \ *** ?s6 x = *** (\j\Basis. *** frechet_derivative (\a. frechet_derivative f (at a) j) *** (at a) x * *** (v \ j)) *** At command "apply" (line 724 of "$AFP/Smooth_Manifolds/Smooth.thy") *** Failed to finish proof (line 472 of "$AFP/Smooth_Manifolds/Smooth.thy"): *** goal (1 subgoal): *** 1. \a b. *** higher_differentiable_on (S \ T) snd k \ *** higher_differentiable_on (S \ T) *** (\x. snd (frechet_derivative (\x. x) (at x) (a, b))) *** k *** At command "by" (line 471 of "$AFP/Smooth_Manifolds/Smooth.thy") *** Failed to finish proof (line 462 of "$AFP/Smooth_Manifolds/Smooth.thy"): *** goal (1 subgoal): *** 1. \a b. *** higher_differentiable_on (S \ T) fst k \ *** higher_differentiable_on (S \ T) *** (\x. fst (frechet_derivative (\x. x) (at x) (a, b))) *** k *** At command "by" (line 462 of "$AFP/Smooth_Manifolds/Smooth.thy") *** Failed to finish proof (line 160 of "$AFP/Smooth_Manifolds/Smooth.thy"): *** goal (1 subgoal): *** 1. \nat v. *** n = Suc nat \ *** higher_differentiable_on S *** (\x. frechet_derivative (\x. x) (at x) v) nat *** At command "by" (line 160 of "$AFP/Smooth_Manifolds/Smooth.thy") *** exception THM 0 raised (line 309 of "drule.ML"): *** OF: no unifiers *** \?f differentiable at ?x; open ?X; ?x \ ?X; *** \x. x \ ?X \ ?f x = ?g x\ *** \ frechet_derivative ?f (at ?x) = *** frechet_derivative ?g (at ?x) *** open S *** x \ S *** ?x \ S \ f ?x = g ?x *** At command "apply" (line 104 of "$AFP/Smooth_Manifolds/Smooth.thy") Running Probabilistic_System_Zoo ... Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Treaps/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Treaps/outline.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stern_Brocot/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stern_Brocot/outline.pdf Probabilistic_System_Zoo: theory HOL-Eisbach.Eisbach Probabilistic_System_Zoo: theory HOL-Cardinals.Fun_More Probabilistic_System_Zoo: theory HOL-Cardinals.Order_Relation_More Probabilistic_System_Zoo: theory HOL-Cardinals.Order_Union Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Extension Timing Treaps (4 threads, 36.446s elapsed time, 120.524s cpu time, 3.756s GC time, factor 3.31) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Treaps Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Treaps/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Treaps/outline.pdf Finished Treaps (0:00:42 elapsed time, 0:02:11 cpu time, factor 3.12) Running UpDown_Scheme ... Probabilistic_System_Zoo: theory HOL-Cardinals.Wellfounded_More Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Relation Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Embedding Timing Stern_Brocot (4 threads, 45.497s elapsed time, 74.556s cpu time, 4.320s GC time, factor 1.64) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stern_Brocot Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stern_Brocot/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stern_Brocot/outline.pdf Finished Stern_Brocot (0:00:51 elapsed time, 0:01:26 cpu time, factor 1.67) Building Quick_Sort_Cost ... Timing Dirichlet_L (4 threads, 65.103s elapsed time, 203.956s cpu time, 6.056s GC time, factor 3.13) Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Constructions Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_L Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary/outline.pdf Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Order_Relation Probabilistic_System_Zoo: theory HOL-Cardinals.Ordinal_Arithmetic UpDown_Scheme: theory HOL-Eisbach.Eisbach UpDown_Scheme: theory HOL-Library.Adhoc_Overloading UpDown_Scheme: theory HOL-ex.Quicksort UpDown_Scheme: theory HOL-Library.Option_ord Timing Prime_Distribution_Elementary (4 threads, 37.479s elapsed time, 138.980s cpu time, 3.004s GC time, factor 3.71) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary/outline.pdf Finished Prime_Distribution_Elementary (0:00:45 elapsed time, 0:02:32 cpu time, factor 3.36) Building Stirling_Formula ... UpDown_Scheme: theory HOL-Library.Monad_Syntax UpDown_Scheme: theory HOL-Imperative_HOL.Heap Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monomorphic_Monad/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monomorphic_Monad/outline.pdf UpDown_Scheme: theory UpDown_Scheme.Grid_Point Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MFMC_Countable/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MFMC_Countable/outline.pdf UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Syntax_Match Quick_Sort_Cost: theory HOL-Library.Function_Algebras Quick_Sort_Cost: theory HOL-Library.Landau_Symbols UpDown_Scheme: theory Automatic_Refinement.Misc Quick_Sort_Cost: theory Landau_Symbols.Group_Sort Quick_Sort_Cost: theory List-Index.List_Index Timing Monomorphic_Monad (4 threads, 34.124s elapsed time, 60.764s cpu time, 2.984s GC time, factor 1.78) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monomorphic_Monad Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monomorphic_Monad/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monomorphic_Monad/outline.pdf Finished Monomorphic_Monad (0:00:41 elapsed time, 0:01:14 cpu time, factor 1.81) Running Tarskis_Geometry ... Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Arithmetic Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinals Stirling_Formula: theory HOL-Library.Stirling Stirling_Formula: theory HOL-Library.Function_Algebras Stirling_Formula: theory Bernoulli.Bernoulli Stirling_Formula: theory HOL-Library.Landau_Symbols Timing MFMC_Countable (4 threads, 61.653s elapsed time, 190.184s cpu time, 5.568s GC time, factor 3.08) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MFMC_Countable Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MFMC_Countable/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MFMC_Countable/outline.pdf Finished MFMC_Countable (0:01:12 elapsed time, 0:03:27 cpu time, factor 2.87) Running Lp ... Quick_Sort_Cost: theory Comparison_Sort_Lower_Bound.Linorder_Relations Stirling_Formula: theory Landau_Symbols.Group_Sort UpDown_Scheme: theory UpDown_Scheme.Grid Stirling_Formula: theory Bernoulli.Periodic_Bernpoly Timing Prime_Number_Theorem (4 threads, 27.117s elapsed time, 93.272s cpu time, 1.984s GC time, factor 3.44) Probabilistic_System_Zoo: theory HOL-Cardinals.Bounded_Set Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Bool_Bounded_Set Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Finitely_Bounded_Set_Counterexample Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Number_Theorem Stirling_Formula: theory Bernoulli.Bernoulli_FPS UpDown_Scheme: theory HOL-Imperative_HOL.Heap_Monad Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Nonempty_Bounded_Set Tarskis_Geometry: theory HOL-Algebra.Congruence Tarskis_Geometry: theory HOL-Library.Quadratic_Discriminant Tarskis_Geometry: theory Tarskis_Geometry.Metric Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Probabilistic_Hierarchy Tarskis_Geometry: theory Tarskis_Geometry.Miscellany UpDown_Scheme: theory UpDown_Scheme.UpDown_Scheme Tarskis_Geometry: theory Tarskis_Geometry.Linear_Algebra2 Tarskis_Geometry: theory Tarskis_Geometry.Tarski Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_L/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_L/outline.pdf Lp: theory Ergodic_Theory.SG_Library_Complement Tarskis_Geometry: theory Tarskis_Geometry.Euclid_Tarski Timing Dirichlet_L (4 threads, 65.103s elapsed time, 203.956s cpu time, 6.056s GC time, factor 3.13) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_L Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_L/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_L/outline.pdf Finished Dirichlet_L (0:01:12 elapsed time, 0:03:36 cpu time, factor 2.99) Running Quaternions ... Tarskis_Geometry: theory HOL-Algebra.Order UpDown_Scheme: theory UpDown_Scheme.Triangular_Function Quick_Sort_Cost: theory Landau_Symbols.Landau_Real_Products Stirling_Formula: theory Landau_Symbols.Landau_Real_Products Lp: theory Lp.Functional_Spaces UpDown_Scheme: theory HOL-Imperative_HOL.Array UpDown_Scheme: theory UpDown_Scheme.Down UpDown_Scheme: theory UpDown_Scheme.Up UpDown_Scheme: theory HOL-Imperative_HOL.Ref Tarskis_Geometry: theory HOL-Algebra.Lattice UpDown_Scheme: theory HOL-Imperative_HOL.Imperative_HOL UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Run Quaternions: theory Quaternions.Quaternions UpDown_Scheme: theory UpDown_Scheme.Up_Down Lp: theory Lp.Lp Tarskis_Geometry: theory HOL-Algebra.Complete_Lattice Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Number_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Number_Theorem/outline.pdf UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Assertions Tarskis_Geometry: theory HOL-Algebra.Group Timing Prime_Number_Theorem (4 threads, 27.117s elapsed time, 93.272s cpu time, 1.984s GC time, factor 3.44) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Number_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Number_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Number_Theorem/outline.pdf Finished Prime_Number_Theorem (0:00:36 elapsed time, 0:01:48 cpu time, factor 3.00) Running pGCL ... Stirling_Formula: theory Landau_Symbols.Landau_Simprocs Quick_Sort_Cost: theory Landau_Symbols.Landau_Simprocs Stirling_Formula: theory Landau_Symbols.Landau_More UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Hoare_Triple Stirling_Formula: theory Stirling_Formula.Stirling_Formula Quick_Sort_Cost: theory Landau_Symbols.Landau_More pGCL: theory pGCL.Misc Quick_Sort_Cost: theory Quick_Sort_Cost.Randomised_Quick_Sort UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Automation pGCL: theory pGCL.Expectations Tarskis_Geometry: theory Tarskis_Geometry.Action Tarskis_Geometry: theory Tarskis_Geometry.Projective Stirling_Formula: theory Stirling_Formula.Ln_Gamma_Asymptotics pGCL: theory pGCL.Transformers UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Sep_Main UpDown_Scheme: theory UpDown_Scheme.Imperative pGCL: theory pGCL.Induction pGCL: theory pGCL.Embedding Quick_Sort_Cost: theory Quick_Sort_Cost.Quick_Sort_Average_Case pGCL: theory pGCL.Healthiness Tarskis_Geometry: theory Tarskis_Geometry.Hyperbolic_Tarski pGCL: theory pGCL.Continuity pGCL: theory pGCL.LoopInduction pGCL: theory pGCL.Sublinearity pGCL: theory pGCL.WellDefined Timing Quick_Sort_Cost (4 threads, 16.801s elapsed time, 62.400s cpu time, 2.284s GC time, factor 3.71) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quick_Sort_Cost pGCL: theory pGCL.Algebra pGCL: theory pGCL.Determinism pGCL: theory pGCL.Loops pGCL: theory pGCL.StructuredReasoning pGCL: theory pGCL.Automation pGCL: theory pGCL.Termination Timing SDS_Impossibility (4 threads, 36.758s elapsed time, 93.340s cpu time, 2.060s GC time, factor 2.54) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/SDS_Impossibility pGCL: theory pGCL.pGCL Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quick_Sort_Cost/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quick_Sort_Cost/outline.pdf pGCL: theory pGCL.LoopExamples pGCL: theory pGCL.Monty pGCL: theory pGCL.Primitives Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/SDS_Impossibility/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/SDS_Impossibility/outline.pdf Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi Timing SDS_Impossibility (4 threads, 36.758s elapsed time, 93.340s cpu time, 2.060s GC time, factor 2.54) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/SDS_Impossibility Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/SDS_Impossibility/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/SDS_Impossibility/outline.pdf Finished SDS_Impossibility (0:00:42 elapsed time, 0:01:44 cpu time, factor 2.45) Running Kuratowski_Closure_Complement ... Timing Stirling_Formula (4 threads, 24.300s elapsed time, 78.684s cpu time, 2.776s GC time, factor 3.24) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula Kuratowski_Closure_Complement: theory Kuratowski_Closure_Complement.KuratowskiClosureComplementTheorem Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi_Counterexample Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula/outline.pdf Timing UpDown_Scheme (4 threads, 31.259s elapsed time, 119.744s cpu time, 4.364s GC time, factor 3.83) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UpDown_Scheme Timing Probabilistic_System_Zoo (4 threads, 33.714s elapsed time, 119.452s cpu time, 5.608s GC time, factor 3.54) Timing Lp (4 threads, 27.757s elapsed time, 87.604s cpu time, 1.400s GC time, factor 3.16) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lp Timing Tarskis_Geometry (4 threads, 29.376s elapsed time, 107.236s cpu time, 3.836s GC time, factor 3.65) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tarskis_Geometry Timing Quaternions (4 threads, 26.046s elapsed time, 33.152s cpu time, 0.948s GC time, factor 1.27) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quaternions Timing pGCL (4 threads, 22.329s elapsed time, 85.800s cpu time, 1.940s GC time, factor 3.84) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/pGCL Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo/outline.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo/bnfs.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo/non_bnfs.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UpDown_Scheme/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UpDown_Scheme/outline.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quaternions/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quaternions/outline.pdf Timing Probabilistic_System_Zoo (4 threads, 33.714s elapsed time, 119.452s cpu time, 5.608s GC time, factor 3.54) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo/outline.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo/bnfs.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo/non_bnfs.pdf Finished Probabilistic_System_Zoo (0:00:39 elapsed time, 0:02:17 cpu time, factor 3.48) Running HOL-Analysis-ex ... Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lp/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lp/outline.pdf Timing Quaternions (4 threads, 26.046s elapsed time, 33.152s cpu time, 0.948s GC time, factor 1.27) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quaternions Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quaternions/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quaternions/outline.pdf Finished Quaternions (0:00:31 elapsed time, 0:00:43 cpu time, factor 1.38) Timing UpDown_Scheme (4 threads, 31.259s elapsed time, 119.744s cpu time, 4.364s GC time, factor 3.83) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UpDown_Scheme Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UpDown_Scheme/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UpDown_Scheme/outline.pdf Finished UpDown_Scheme (0:00:37 elapsed time, 0:02:11 cpu time, factor 3.49) Running Euler_MacLaurin ... Running Octonions ... Timing Lp (4 threads, 27.757s elapsed time, 87.604s cpu time, 1.400s GC time, factor 3.16) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lp Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lp/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lp/outline.pdf Finished Lp (0:00:34 elapsed time, 0:01:40 cpu time, factor 2.87) Running Cayley_Hamilton ... HOL-Analysis-ex: theory HOL-Analysis-ex.Approximations Octonions: theory Octonions.Cross_Product_7 Euler_MacLaurin: theory HOL-Library.Function_Algebras Euler_MacLaurin: theory HOL-Library.Stirling Euler_MacLaurin: theory Bernoulli.Bernoulli Euler_MacLaurin: theory HOL-Library.Landau_Symbols Euler_MacLaurin: theory Landau_Symbols.Group_Sort Euler_MacLaurin: theory Bernoulli.Periodic_Bernpoly Euler_MacLaurin: theory Bernoulli.Bernoulli_FPS Cayley_Hamilton: theory HOL-Library.More_List Cayley_Hamilton: theory Cayley_Hamilton.Square_Matrix Cayley_Hamilton: theory HOL-Computational_Algebra.Polynomial Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tarskis_Geometry/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tarskis_Geometry/outline.pdf Timing Tarskis_Geometry (4 threads, 29.376s elapsed time, 107.236s cpu time, 3.836s GC time, factor 3.65) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tarskis_Geometry Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tarskis_Geometry/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tarskis_Geometry/outline.pdf Finished Tarskis_Geometry (0:00:38 elapsed time, 0:02:02 cpu time, factor 3.20) Running Neumann_Morgenstern_Utility ... Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin Octonions: theory Octonions.Octonions Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/pGCL/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/pGCL/outline.pdf Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Syntax Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.PMF_Composition Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Preferences Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries Timing pGCL (4 threads, 22.329s elapsed time, 85.800s cpu time, 1.940s GC time, factor 3.84) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/pGCL Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/pGCL/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/pGCL/outline.pdf Finished pGCL (0:00:31 elapsed time, 0:01:42 cpu time, factor 3.22) Running Catalan_Numbers ... Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem Catalan_Numbers: theory HOL-Library.Function_Algebras Catalan_Numbers: theory HOL-Library.Landau_Symbols Catalan_Numbers: theory Catalan_Numbers.Catalan_Auxiliary_Integral Catalan_Numbers: theory Landau_Symbols.Group_Sort Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility Euler_MacLaurin: theory Landau_Symbols.Landau_More Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau Timing Quick_Sort_Cost (4 threads, 16.801s elapsed time, 62.400s cpu time, 2.284s GC time, factor 3.71) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quick_Sort_Cost Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quick_Sort_Cost/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quick_Sort_Cost/outline.pdf Finished Quick_Sort_Cost (0:00:47 elapsed time, 0:01:53 cpu time, factor 2.40) Building Random_BSTs ... Catalan_Numbers: theory Landau_Symbols.Landau_Real_Products Random_BSTs: theory HOL-Data_Structures.Cmp Random_BSTs: theory HOL-Data_Structures.Less_False Random_BSTs: theory HOL-Data_Structures.Sorted_Less Random_BSTs: theory HOL-Data_Structures.List_Ins_Del Cayley_Hamilton: theory Cayley_Hamilton.Cayley_Hamilton Timing Kuratowski_Closure_Complement (4 threads, 21.873s elapsed time, 64.556s cpu time, 1.436s GC time, factor 2.95) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement Random_BSTs: theory HOL-Data_Structures.Set_Specs Random_BSTs: theory HOL-Data_Structures.Tree_Set Random_BSTs: theory Random_BSTs.Random_BSTs Timing Cayley_Hamilton (4 threads, 12.843s elapsed time, 40.728s cpu time, 1.764s GC time, factor 3.17) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cayley_Hamilton Catalan_Numbers: theory Landau_Symbols.Landau_Simprocs Catalan_Numbers: theory Landau_Symbols.Landau_More Catalan_Numbers: theory Catalan_Numbers.Catalan_Numbers Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement/outline.pdf Timing Neumann_Morgenstern_Utility (4 threads, 11.915s elapsed time, 40.436s cpu time, 1.036s GC time, factor 3.39) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Neumann_Morgenstern_Utility Timing Kuratowski_Closure_Complement (4 threads, 21.873s elapsed time, 64.556s cpu time, 1.436s GC time, factor 2.95) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement/outline.pdf Finished Kuratowski_Closure_Complement (0:00:28 elapsed time, 0:01:17 cpu time, factor 2.74) Timing Stirling_Formula (4 threads, 24.300s elapsed time, 78.684s cpu time, 2.776s GC time, factor 3.24) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula/outline.pdf Finished Stirling_Formula (0:00:53 elapsed time, 0:02:07 cpu time, factor 2.39) Timing Octonions (4 threads, 15.834s elapsed time, 55.272s cpu time, 1.484s GC time, factor 3.49) Running Error_Function ... Running Bernoulli ... Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Octonions Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cayley_Hamilton/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cayley_Hamilton/outline.pdf Timing Random_BSTs (4 threads, 6.563s elapsed time, 12.492s cpu time, 0.512s GC time, factor 1.90) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_BSTs Timing Euler_MacLaurin (4 threads, 17.285s elapsed time, 64.664s cpu time, 2.296s GC time, factor 3.74) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Euler_MacLaurin Error_Function: theory HOL-Library.Function_Algebras Error_Function: theory HOL-Library.Landau_Symbols Error_Function: theory Landau_Symbols.Group_Sort Timing Cayley_Hamilton (4 threads, 12.843s elapsed time, 40.728s cpu time, 1.764s GC time, factor 3.17) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cayley_Hamilton Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cayley_Hamilton/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cayley_Hamilton/outline.pdf Finished Cayley_Hamilton (0:00:17 elapsed time, 0:00:50 cpu time, factor 2.83) Running HOL-Probability-ex ... Bernoulli: theory HOL-Library.Stirling Bernoulli: theory Bernoulli.Bernoulli Timing Catalan_Numbers (4 threads, 11.877s elapsed time, 40.412s cpu time, 1.752s GC time, factor 3.40) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Catalan_Numbers Timing HOL-Analysis-ex (4 threads, 18.389s elapsed time, 52.108s cpu time, 0.612s GC time, factor 2.83) Bernoulli: theory Bernoulli.Periodic_Bernpoly Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis-ex Bernoulli: theory Bernoulli.Bernoulli_FPS Timing HOL-Analysis-ex (4 threads, 18.389s elapsed time, 52.108s cpu time, 0.612s GC time, factor 2.83) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis-ex Finished HOL-Analysis-ex (0:00:20 elapsed time, 0:00:54 cpu time, factor 2.64) Running Lower_Semicontinuous ... Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Neumann_Morgenstern_Utility/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Neumann_Morgenstern_Utility/outline.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Octonions/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Octonions/outline.pdf HOL-Probability-ex: theory HOL-Library.Permutation HOL-Probability-ex: theory HOL-Probability-ex.Dining_Cryptographers HOL-Probability-ex: theory HOL-Probability-ex.Measure_Not_CCC HOL-Probability-ex: theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure Timing Neumann_Morgenstern_Utility (4 threads, 11.915s elapsed time, 40.436s cpu time, 1.036s GC time, factor 3.39) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Neumann_Morgenstern_Utility Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Neumann_Morgenstern_Utility/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Neumann_Morgenstern_Utility/outline.pdf Finished Neumann_Morgenstern_Utility (0:00:17 elapsed time, 0:00:51 cpu time, factor 2.92) Running Random_Graph_Subgraph_Threshold ... Timing Octonions (4 threads, 15.834s elapsed time, 55.272s cpu time, 1.484s GC time, factor 3.49) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Octonions Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Octonions/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Octonions/outline.pdf Finished Octonions (0:00:21 elapsed time, 0:01:05 cpu time, factor 3.12) Running Rank_Nullity_Theorem ... Bernoulli: theory Bernoulli.Bernoulli_Zeta Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_BSTs/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_BSTs/outline.pdf Lower_Semicontinuous: theory Lower_Semicontinuous.Lower_Semicontinuous Error_Function: theory Error_Function.Error_Function Error_Function: theory Landau_Symbols.Landau_Real_Products Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Catalan_Numbers/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Catalan_Numbers/outline.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Euler_MacLaurin/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Euler_MacLaurin/outline.pdf Rank_Nullity_Theorem: theory HOL-Library.Function_Algebras Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dual_Order Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Mod_Type Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc Timing Catalan_Numbers (4 threads, 11.877s elapsed time, 40.412s cpu time, 1.752s GC time, factor 3.40) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Catalan_Numbers Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Catalan_Numbers/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Catalan_Numbers/outline.pdf Finished Catalan_Numbers (0:00:16 elapsed time, 0:00:50 cpu time, factor 2.97) Timing Euler_MacLaurin (4 threads, 17.285s elapsed time, 64.664s cpu time, 2.296s GC time, factor 3.74) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Euler_MacLaurin Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Euler_MacLaurin/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Euler_MacLaurin/outline.pdf Finished Euler_MacLaurin (0:00:22 elapsed time, 0:01:15 cpu time, factor 3.28) Running First_Welfare_Theorem ... Running Comparison_Sort_Lower_Bound ... Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas First_Welfare_Theorem: theory First_Welfare_Theorem.Syntax First_Welfare_Theorem: theory First_Welfare_Theorem.Argmax Comparison_Sort_Lower_Bound: theory HOL-Library.Multiset_Permutations Comparison_Sort_Lower_Bound: theory List-Index.List_Index First_Welfare_Theorem: theory First_Welfare_Theorem.Consumers First_Welfare_Theorem: theory First_Welfare_Theorem.Preferences Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Miscellaneous Error_Function: theory Landau_Symbols.Landau_Simprocs Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties First_Welfare_Theorem: theory First_Welfare_Theorem.Utility_Functions Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold Error_Function: theory Landau_Symbols.Landau_More First_Welfare_Theorem: theory First_Welfare_Theorem.Common Error_Function: theory Error_Function.Error_Function_Asymptotics Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound First_Welfare_Theorem: theory First_Welfare_Theorem.Arrow_Debreu_Model First_Welfare_Theorem: theory First_Welfare_Theorem.Exchange_Economy First_Welfare_Theorem: theory First_Welfare_Theorem.Private_Ownership_Economy Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Fundamental_Subspaces Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dim_Formula Timing Bernoulli (4 threads, 9.841s elapsed time, 26.252s cpu time, 0.752s GC time, factor 2.67) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli Timing Error_Function (4 threads, 10.648s elapsed time, 38.556s cpu time, 1.508s GC time, factor 3.62) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Error_Function Timing HOL-Probability-ex (4 threads, 9.108s elapsed time, 25.700s cpu time, 0.692s GC time, factor 2.82) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability-ex Timing Lower_Semicontinuous (4 threads, 8.806s elapsed time, 20.924s cpu time, 0.408s GC time, factor 2.38) Timing Rank_Nullity_Theorem (4 threads, 7.791s elapsed time, 14.952s cpu time, 0.592s GC time, factor 1.92) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lower_Semicontinuous Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem Timing Random_Graph_Subgraph_Threshold (4 threads, 7.588s elapsed time, 21.804s cpu time, 0.460s GC time, factor 2.87) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_Graph_Subgraph_Threshold Timing HOL-Probability-ex (4 threads, 9.108s elapsed time, 25.700s cpu time, 0.692s GC time, factor 2.82) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability-ex Finished HOL-Probability-ex (0:00:11 elapsed time, 0:00:27 cpu time, factor 2.44) Running Triangle ... Timing Comparison_Sort_Lower_Bound (4 threads, 6.449s elapsed time, 18.612s cpu time, 0.800s GC time, factor 2.89) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Comparison_Sort_Lower_Bound Timing First_Welfare_Theorem (4 threads, 7.309s elapsed time, 24.784s cpu time, 0.528s GC time, factor 3.39) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/First_Welfare_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli/outline.pdf Triangle: theory Triangle.Angles Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Error_Function/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Error_Function/outline.pdf Triangle: theory Triangle.Triangle Timing Bernoulli (4 threads, 9.841s elapsed time, 26.252s cpu time, 0.752s GC time, factor 2.67) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli/outline.pdf Finished Bernoulli (0:00:15 elapsed time, 0:00:37 cpu time, factor 2.41) Timing Error_Function (4 threads, 10.648s elapsed time, 38.556s cpu time, 1.508s GC time, factor 3.62) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Error_Function Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Error_Function/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Error_Function/outline.pdf Finished Error_Function (0:00:15 elapsed time, 0:00:48 cpu time, factor 3.07) Running Source_Coding_Theorem ... Running Stewart_Apollonius ... Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem/outline.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lower_Semicontinuous/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lower_Semicontinuous/outline.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_Graph_Subgraph_Threshold/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_Graph_Subgraph_Threshold/outline.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Comparison_Sort_Lower_Bound/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Comparison_Sort_Lower_Bound/outline.pdf Timing Lower_Semicontinuous (4 threads, 8.806s elapsed time, 20.924s cpu time, 0.408s GC time, factor 2.38) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lower_Semicontinuous Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lower_Semicontinuous/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lower_Semicontinuous/outline.pdf Finished Lower_Semicontinuous (0:00:14 elapsed time, 0:00:31 cpu time, factor 2.18) Timing Rank_Nullity_Theorem (4 threads, 7.791s elapsed time, 14.952s cpu time, 0.592s GC time, factor 1.92) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem/outline.pdf Finished Rank_Nullity_Theorem (0:00:13 elapsed time, 0:00:25 cpu time, factor 1.96) Running Buffons_Needle ... Running Chord_Segments ... Stewart_Apollonius: theory Triangle.Angles Timing Comparison_Sort_Lower_Bound (4 threads, 6.449s elapsed time, 18.612s cpu time, 0.800s GC time, factor 2.89) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Comparison_Sort_Lower_Bound Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Comparison_Sort_Lower_Bound/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Comparison_Sort_Lower_Bound/outline.pdf Finished Comparison_Sort_Lower_Bound (0:00:11 elapsed time, 0:00:28 cpu time, factor 2.47) Timing Random_Graph_Subgraph_Threshold (4 threads, 7.588s elapsed time, 21.804s cpu time, 0.460s GC time, factor 2.87) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_Graph_Subgraph_Threshold Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_Graph_Subgraph_Threshold/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_Graph_Subgraph_Threshold/outline.pdf Finished Random_Graph_Subgraph_Threshold (0:00:13 elapsed time, 0:00:32 cpu time, factor 2.43) Running Fisher_Yates ... Running Cartan_FP ... Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem Stewart_Apollonius: theory Triangle.Triangle Stewart_Apollonius: theory Stewart_Apollonius.Stewart_Apollonius Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/First_Welfare_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/First_Welfare_Theorem/outline.pdf Chord_Segments: theory Triangle.Angles Timing First_Welfare_Theorem (4 threads, 7.309s elapsed time, 24.784s cpu time, 0.528s GC time, factor 3.39) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/First_Welfare_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/First_Welfare_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/First_Welfare_Theorem/outline.pdf Finished First_Welfare_Theorem (0:00:12 elapsed time, 0:00:35 cpu time, factor 2.75) Running Minkowskis_Theorem ... Timing Triangle (4 threads, 3.786s elapsed time, 6.436s cpu time, 0.184s GC time, factor 1.70) Buffons_Needle: theory Buffons_Needle.Buffons_Needle Chord_Segments: theory Triangle.Triangle Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Triangle Cartan_FP: theory Cartan_FP.Cartan Chord_Segments: theory Chord_Segments.Chord_Segments Fisher_Yates: theory Fisher_Yates.Fisher_Yates Minkowskis_Theorem: theory Minkowskis_Theorem.Minkowskis_Theorem Timing Cartan_FP (4 threads, 1.543s elapsed time, 4.924s cpu time, 0.000s GC time, factor 3.19) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cartan_FP Timing Source_Coding_Theorem (4 threads, 3.507s elapsed time, 9.412s cpu time, 0.128s GC time, factor 2.68) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Source_Coding_Theorem Timing Minkowskis_Theorem (4 threads, 1.099s elapsed time, 3.764s cpu time, 0.000s GC time, factor 3.42) Timing Stewart_Apollonius (4 threads, 3.902s elapsed time, 6.884s cpu time, 0.188s GC time, factor 1.76) Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Triangle/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Triangle/outline.pdf Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius Timing Triangle (4 threads, 3.786s elapsed time, 6.436s cpu time, 0.184s GC time, factor 1.70) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Triangle Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Triangle/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Triangle/outline.pdf Finished Triangle (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.88) Running Ptolemys_Theorem ... Timing Fisher_Yates (4 threads, 2.784s elapsed time, 8.288s cpu time, 0.136s GC time, factor 2.98) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fisher_Yates Timing Chord_Segments (4 threads, 3.868s elapsed time, 8.692s cpu time, 0.140s GC time, factor 2.25) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Chord_Segments Timing Buffons_Needle (4 threads, 4.085s elapsed time, 11.900s cpu time, 0.084s GC time, factor 2.91) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle Ptolemys_Theorem: theory Ptolemys_Theorem.Ptolemys_Theorem Timing Random_BSTs (4 threads, 6.563s elapsed time, 12.492s cpu time, 0.512s GC time, factor 1.90) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_BSTs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_BSTs/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_BSTs/outline.pdf Finished Random_BSTs (0:00:30 elapsed time, 0:00:52 cpu time, factor 1.72) Running Randomised_BSTs ... Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cartan_FP/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cartan_FP/outline.pdf Timing Cartan_FP (4 threads, 1.543s elapsed time, 4.924s cpu time, 0.000s GC time, factor 3.19) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cartan_FP Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cartan_FP/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cartan_FP/outline.pdf Finished Cartan_FP (0:00:06 elapsed time, 0:00:14 cpu time, factor 2.37) Running Monad_Normalisation ... Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius/outline.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Source_Coding_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Source_Coding_Theorem/outline.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem/outline.pdf Timing Stewart_Apollonius (4 threads, 3.902s elapsed time, 6.884s cpu time, 0.188s GC time, factor 1.76) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius/outline.pdf Finished Stewart_Apollonius (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.89) Timing Ptolemys_Theorem (4 threads, 1.390s elapsed time, 2.948s cpu time, 0.000s GC time, factor 2.12) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ptolemys_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fisher_Yates/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fisher_Yates/outline.pdf Timing Source_Coding_Theorem (4 threads, 3.507s elapsed time, 9.412s cpu time, 0.128s GC time, factor 2.68) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Source_Coding_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Source_Coding_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Source_Coding_Theorem/outline.pdf Finished Source_Coding_Theorem (0:00:08 elapsed time, 0:00:19 cpu time, factor 2.25) Timing Minkowskis_Theorem (4 threads, 1.099s elapsed time, 3.764s cpu time, 0.000s GC time, factor 3.42) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem/outline.pdf Finished Minkowskis_Theorem (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.24) Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Chord_Segments/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Chord_Segments/outline.pdf Timing Fisher_Yates (4 threads, 2.784s elapsed time, 8.288s cpu time, 0.136s GC time, factor 2.98) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fisher_Yates Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fisher_Yates/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fisher_Yates/outline.pdf Finished Fisher_Yates (0:00:07 elapsed time, 0:00:17 cpu time, factor 2.30) Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle/outline.pdf Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test Timing Chord_Segments (4 threads, 3.868s elapsed time, 8.692s cpu time, 0.140s GC time, factor 2.25) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Chord_Segments Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Chord_Segments/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Chord_Segments/outline.pdf Finished Chord_Segments (0:00:08 elapsed time, 0:00:18 cpu time, factor 2.12) Timing Buffons_Needle (4 threads, 4.085s elapsed time, 11.900s cpu time, 0.084s GC time, factor 2.91) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle/outline.pdf Finished Buffons_Needle (0:00:09 elapsed time, 0:00:21 cpu time, factor 2.36) Timing Monad_Normalisation (4 threads, 0.779s elapsed time, 1.232s cpu time, 0.000s GC time, factor 1.58) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monad_Normalisation Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ptolemys_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ptolemys_Theorem/outline.pdf Timing Ptolemys_Theorem (4 threads, 1.390s elapsed time, 2.948s cpu time, 0.000s GC time, factor 2.12) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ptolemys_Theorem Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ptolemys_Theorem/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ptolemys_Theorem/outline.pdf Finished Ptolemys_Theorem (0:00:05 elapsed time, 0:00:11 cpu time, factor 2.01) Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monad_Normalisation/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monad_Normalisation/outline.pdf Timing Monad_Normalisation (4 threads, 0.779s elapsed time, 1.232s cpu time, 0.000s GC time, factor 1.58) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monad_Normalisation Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monad_Normalisation/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monad_Normalisation/outline.pdf Finished Monad_Normalisation (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.88) Timing Randomised_BSTs (4 threads, 7.853s elapsed time, 26.480s cpu time, 0.720s GC time, factor 3.37) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_BSTs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_BSTs/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_BSTs/outline.pdf Timing Randomised_BSTs (4 threads, 7.853s elapsed time, 26.480s cpu time, 0.720s GC time, factor 3.37) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_BSTs Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_BSTs/document.pdf Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_BSTs/outline.pdf Finished Randomised_BSTs (0:00:13 elapsed time, 0:00:36 cpu time, factor 2.77) HOL-ODE-Numerics: theory HOL-ODE-Numerics.Init_ODE_Solver HOL-ODE-Numerics: theory HOL-ODE-Numerics.Example_Utilities HOL-ODE-Numerics: theory HOL-ODE-Numerics.ODE_Numerics Timing HOL-ODE-Numerics (4 threads, 1009.428s elapsed time, 3629.468s cpu time, 338.812s GC time, factor 3.60) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Numerics Timing HOL-ODE-Numerics (4 threads, 1009.428s elapsed time, 3629.468s cpu time, 338.812s GC time, factor 3.60) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Numerics Finished HOL-ODE-Numerics (0:18:47 elapsed time, 1:06:38 cpu time, factor 3.55) Building Lorenz_Approximation ... Running HOL-ODE-ARCH-COMP ... Running HOL-ODE-Examples ... Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples Timing Lorenz_Approximation (4 threads, 210.141s elapsed time, 464.672s cpu time, 20.492s GC time, factor 2.21) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_Approximation Timing Lorenz_Approximation (4 threads, 210.141s elapsed time, 464.672s cpu time, 20.492s GC time, factor 2.21) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_Approximation Finished Lorenz_Approximation (0:04:14 elapsed time, 0:09:02 cpu time, factor 2.13) Running Lorenz_C0 ... Running Lorenz_C1 ... Lorenz_C0: theory Lorenz_C0.Lorenz_C0 Lorenz_C1: theory Lorenz_C1.Lorenz_C1 Timing Lorenz_C1 (4 threads, 0.993s elapsed time, 1.684s cpu time, 0.000s GC time, factor 1.70) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_C1 Timing Lorenz_C1 (4 threads, 0.993s elapsed time, 1.684s cpu time, 0.000s GC time, factor 1.70) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_C1 Finished Lorenz_C1 (0:00:03 elapsed time, 0:00:04 cpu time, factor 1.16) Timing HOL-ODE-Examples (4 threads, 473.793s elapsed time, 1356.748s cpu time, 11.216s GC time, factor 2.86) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Examples Timing HOL-ODE-Examples (4 threads, 473.793s elapsed time, 1356.748s cpu time, 11.216s GC time, factor 2.86) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Examples Finished HOL-ODE-Examples (0:07:56 elapsed time, 0:22:39 cpu time, factor 2.85) Timing HOL-ODE-ARCH-COMP (4 threads, 527.027s elapsed time, 1191.592s cpu time, 18.896s GC time, factor 2.26) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-ARCH-COMP Timing HOL-ODE-ARCH-COMP (4 threads, 527.027s elapsed time, 1191.592s cpu time, 18.896s GC time, factor 2.26) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-ARCH-COMP Finished HOL-ODE-ARCH-COMP (0:08:49 elapsed time, 0:19:54 cpu time, factor 2.25) Timing Lorenz_C0 (4 threads, 1552.422s elapsed time, 6131.128s cpu time, 37.344s GC time, factor 3.95) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_C0 Timing Lorenz_C0 (4 threads, 1552.422s elapsed time, 6131.128s cpu time, 37.344s GC time, factor 3.95) Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_C0 Finished Lorenz_C0 (0:25:55 elapsed time, 1:42:14 cpu time, factor 3.94) Unfinished session(s): Smooth_Manifolds === TIMING === Group AFP: 3:10:16 elapsed time, 9:40:16 cpu time, factor 3.05 Group main: 0:15:17 elapsed time, 0:43:55 cpu time, factor 2.87 Group doc: 0:00:00 elapsed time Group timing: 0:17:51 elapsed time, 0:52:09 cpu time, factor 2.92 Group large: 0:33:55 elapsed time, 2:04:58 cpu time, factor 3.68 Group no_doc: 0:00:00 elapsed time Overall: 1:06:00 elapsed time, 10:33:20 cpu time, factor 9.59 === FAILED SESSIONS === Session Smooth_Manifolds: FAILED 2 === DEPENDENCIES === Generating dependencies file ... Writing dependencies file ... === REPORT === Writing report file ... === SITEGEN === Writing status file ... Running sitegen ... Success: Generated topics.html Success: Generated index.html Success: Generated html files for 485 entries Success: Generated statistics.html Success: Generated download.html Success: Generated about.html Success: Generated citing.html Success: Generated updating.html Success: Generated search.html Success: Generated submitting.html Success: Generated using.html Success: Generated rss.xml Success: Generated status.html Checked directory thys. Found 0 warnings. Packing tars ... === NOTIFICATIONS === === COMPLETED === Build step 'Execute shell' marked build as failure Archiving artifacts Started calculate disk usage of build Finished Calculation of disk usage of build in 0 seconds Started calculate disk usage of workspace Finished Calculation of disk usage of workspace in 0 seconds Email was triggered for: Failure - 1st Trigger Failure - Any was overridden by another trigger and will not send an email. Trigger Failure - Still was overridden by another trigger and will not send an email. Sending email for trigger: Failure - 1st Sending email to: isabelle-ci@mail46.informatik.tu-muenchen.de Finished: FAILURE