[EnvInject] - Loading node environment variables.
workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-all Building remotely on
[isabelle-all] $ hg showconfig paths.default
[isabelle-all] $ hg pull --rev default
http://isabelle.in.tum.de/repos/isabelle/ pulling from
[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 781b15f53098f6c538b8d018def40659c80c0c93 --template exists\n
[isabelle-all] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(781b15f53098f6c538b8d018def40659c80c0c93)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
https://bitbucket.org/isa-afp/afp-devel/ pulling from
[afp] $ hg update --clean --rev default
504 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 5580004cc07480924076ebffb4a22b9bc866daff --template exists\n
[afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(5580004cc07480924076ebffb4a22b9bc866daff)" --encoding UTF-8 --encodingmode replace
[isabelle-all] $ /bin/sh -xe /tmp/jenkins2443813226096371947.sh
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
# 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:
[NOTE] Package zarith is already installed (current version is 1.7).
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
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8.1-20191114/x86_64_32-linux"
Session Doc/Sledgehammer (doc)
Session AFP/Abortable_Linearizable_Modules (AFP)
Session AFP/Abstract-Hoare-Logics (AFP)
Session AFP/Aristotles_Assertoric_Syllogistic (AFP)
Session AFP/AxiomaticCategoryTheory (AFP)
Session AFP/BinarySearchTree (AFP)
Session AFP/Binomial-Queues (AFP)
Session AFP/Bounded_Deducibility_Security (AFP)
Session AFP/BytecodeLogicJmlTypes (AFP)
Session AFP/C2KA_DistributedSystems (AFP)
Session AFP/Sqrt_Babylonian (AFP)
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/Example-Submission (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 AFP/GPU_Kernel_PL (AFP)
Session AFP/Gauss-Jordan-Elim-Fun (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/Generic_Deriving (AFP)
Session AFP/GewirthPGCProof (AFP)
Session HOL/HOL-Cardinals (timing)
Session AFP/Binding_Syntax_Theory (AFP)
Session AFP/Ordinals_and_Cardinals (AFP)
Session HOL/HOL-Hoare_Parallel (timing)
Session HOL/HOL-Library (main timing)
Session AFP/ArrowImpossibilityGS (AFP)
Session AFP/BNF_Operations (AFP)
Session AFP/Binomial-Heaps (AFP)
Session AFP/Boolean_Expression_Checkers (AFP)
Session AFP/Card_Multisets (AFP)
Session AFP/Card_Number_Partitions (AFP)
Session AFP/MonoidalCategory (AFP)
Session AFP/Completeness (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/Concurrent_Ref_Alg (AFP)
Session AFP/Decl_Sem_Fun_PL (AFP)
Session AFP/Derangements (AFP)
Session AFP/Discrete_Summation (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_Seq_Calc1 (AFP)
Session AFP/FOL_Harrison (AFP)
Session AFP/Factored_Transition_System_Bounding (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 HOL/HOL-UNITY (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 HOL/HOL-Analysis (main timing)
Session AFP/Cayley_Hamilton (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/Differential_Game_Logic (AFP)
Session AFP/First_Welfare_Theorem (AFP)
Session AFP/Allen_Calculus (AFP)
Session AFP/Card_Partitions (AFP)
Session AFP/Bell_Numbers_Spivey (AFP)
Session AFP/Card_Equiv_Relations (AFP)
Session AFP/Falling_Factorial_Sum (AFP)
Session AFP/Case_Labeling (AFP)
Session AFP/Dependent_SIFUM_Type_Systems (AFP)
Session AFP/Dependent_SIFUM_Refinement (AFP)
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/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/Laplace_Transform (AFP)
Session AFP/Lower_Semicontinuous (AFP)
Session AFP/Minkowskis_Theorem (AFP)
Session AFP/Ptolemys_Theorem (AFP)
Session AFP/Rank_Nullity_Theorem (AFP)
Session AFP/Gauss_Jordan (AFP)
Session AFP/Echelon_Form (AFP)
Session AFP/Tarskis_Geometry (AFP)
Session AFP/Chord_Segments (AFP)
Session AFP/Stewart_Apollonius (AFP)
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 HOL/HOL-Data_Structures (timing)
Session AFP/Automatic_Refinement (AFP)
Session HOL/HOL-Codegenerator_Test
Session AFP/Pratt_Certificate (AFP)
Session AFP/Bertrands_Postulate (AFP)
Session AFP/Prime_Harmonic_Series (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 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-Metis_Examples (timing)
Session HOL/HOL-MicroJava (timing)
Session HOL/HOL-Nitpick_Examples
Session HOL/HOL-Nominal-Examples (timing)
Session AFP/Lam-ml-Normalization (AFP)
Session AFP/SequentInvertibility (AFP)
Session HOL/HOL-Predicate_Compile_Examples (timing)
Session HOL/HOL-Proofs (timing)
Session HOL/HOL-Proofs-Extraction (timing)
Session HOL/HOL-Proofs-Lambda (timing)
Session AFP/Applicative_Lifting (AFP)
Session AFP/Stern_Brocot (AFP)
Session HOL/HOL-Quickcheck_Examples (timing)
Session HOL/HOL-SET_Protocol (timing)
Session AFP/HereditarilyFinite (AFP)
Session AFP/Isabelle_Meta_Model (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/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/Order_Lattice_Props (AFP)
Session AFP/POPLmark-deBruijn (AFP)
Session AFP/Pairing_Heap (AFP)
Session AFP/Password_Authentication_Protocol (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_Tensor (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/Selection_Heap_Sort (AFP)
Session AFP/Sort_Encodings (AFP)
Session AFP/Amortized_Complexity (AFP)
Session AFP/Dynamic_Tables (AFP)
Session AFP/Root_Balanced_Tree (AFP)
Session AFP/Stable_Matching (AFP)
Session AFP/Tail_Recursive_Functions (AFP)
Session AFP/TortoiseHare (AFP)
Session AFP/Flyspeck-Tame (AFP)
Session AFP/Twelvefold_Way (AFP)
Session AFP/Vickrey_Clarke_Groves (AFP)
Session HOL/HOL-Real_Asymp-Manual
Session AFP/Smooth_Manifolds (AFP)
Session HOL/HOL-Word (main timing)
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session HOL/HOL-Word-SMT_Examples (timing)
Session AFP/Kleene_Algebra (AFP)
Session AFP/Multirelations (AFP)
Session AFP/Transformer_Semantics (AFP)
Session AFP/Regular_Algebras (AFP)
Session AFP/Relation_Algebra (AFP)
Session AFP/Residuated_Lattices (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Abstract_Completeness (AFP)
Session AFP/Abstract_Soundness (AFP)
Session AFP/Incredible_Proof_Machine (AFP)
Session AFP/CAVA_Automata (AFP)
Session AFP/DFS_Framework (AFP)
Session AFP/Collections_Examples (AFP)
Session AFP/Containers-Benchmarks (AFP)
Session AFP/MFOTL_Monitor (AFP)
Session AFP/Generic_Join (AFP)
Session AFP/Datatype_Order_Generator (AFP)
Session AFP/Old_Datatype_Show (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/Adaptive_State_Counting (AFP)
Session AFP/Buchi_Complementation (AFP)
Session AFP/LTL_Master_Theorem (AFP)
Session AFP/Partial_Order_Reduction (AFP)
Session AFP/CAVA_LTL_Modelchecker (AFP)
Session AFP/Transitive-Closure (AFP)
Session AFP/Tree-Automata (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/Separation_Logic_Imperative_HOL (AFP)
Session AFP/Sepref_Prereq (AFP)
Session AFP/UpDown_Scheme (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session HOL/HOLCF (main timing)
Session AFP/HOLCF-Prelude (AFP)
Session AFP/Stream-Fusion (AFP)
Session AFP/WorkerWrapper (AFP)
Session AFP/Consensus_Refined (AFP)
Session AFP/HotelKeyCards (AFP)
Session Doc/How_to_Prove_it (no_doc)
Session AFP/Hybrid_Multi_Lane_Spatial_Logic (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 AFP/Jacobson_Basic_Algebra (AFP)
Session AFP/JiveDataStoreModel (AFP)
Session AFP/Algebraic_VCs (AFP)
Session AFP/Key_Agreement_Strong_Adversaries (AFP)
Session AFP/LatticeProperties (AFP)
Session AFP/DataRefinementIBP (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Dict_Construction (AFP)
Session AFP/Lifting_Definition_Option (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/InformationFlowSlicing_Inter (AFP)
Session AFP/InformationFlowSlicing (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/Hybrid_Systems_VCs (AFP)
Session AFP/Quick_Sort_Cost (AFP)
Session AFP/Randomised_BSTs (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/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/Locally-Nameless-Sigma (AFP)
Session AFP/Lowe_Ontological_Argument (AFP)
Session AFP/MSO_Regex_Equivalence (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/Median_Of_Medians_Selection (AFP)
Session AFP/Modular_Assembly_Kit_Security (AFP)
Session AFP/Monad_Memo_DP (AFP)
Session AFP/Hidden_Markov_Models (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/Incompleteness (AFP)
Session AFP/Surprise_Paradox (AFP)
Session AFP/Modal_Logics_for_NTS (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/Open_Induction (AFP)
Session AFP/Well_Quasi_Orders (AFP)
Session AFP/Decreasing-Diagrams-II (AFP)
Session AFP/Myhill-Nerode (AFP)
Session AFP/Symmetric_Polynomials (AFP)
Session AFP/Pi_Transcendental (AFP)
Session AFP/Nested_Multisets_Ordinals (AFP)
Session AFP/Lambda_Free_KBOs (AFP)
Session AFP/Ordered_Resolution_Prover (AFP)
Session AFP/PSemigroupsConvolution (AFP)
Session AFP/Paraconsistency (AFP)
Session AFP/Partial_Function_MR (AFP)
Session AFP/Certification_Monads (AFP)
Session AFP/Polynomial_Factorization (AFP)
Session AFP/Dirichlet_Series (AFP)
Session AFP/Zeta_Function (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/Groebner_Bases (AFP)
Session AFP/Groebner_Macaulay (AFP)
Session AFP/Nullstellensatz (AFP)
Session AFP/Signature_Groebner (AFP)
Session AFP/Linear_Recurrences (AFP)
Session AFP/Perron_Frobenius (AFP)
Session AFP/Stochastic_Matrices (AFP)
Session AFP/Subresultants (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_Programming (AFP)
Session AFP/Linear_Recurrences_Solver (AFP)
Session AFP/Probabilistic_While (AFP)
Session AFP/Constructive_Cryptography (AFP)
Session AFP/Game_Based_Crypto (AFP)
Session AFP/Multi_Party_Computation (AFP)
Session AFP/Sigma_Commit_Crypto (AFP)
Session AFP/Pop_Refinement (AFP)
Session AFP/Possibilistic_Noninterference (AFP)
Session AFP/Priority_Search_Trees (AFP)
Session AFP/Prim_Dijkstra_Simple (AFP)
Session AFP/Projective_Geometry (AFP)
Session AFP/Proof_Strategy_Language (AFP)
Session AFP/Propositional_Proof_Systems (AFP)
Session AFP/Ramsey-Infinite (AFP)
Session AFP/Recursion-Theory-I (AFP)
Session AFP/Minsky_Machines (AFP)
Session AFP/RefinementReactive (AFP)
Session AFP/Regex_Equivalence (AFP)
Session AFP/Resolution_FOL (AFP)
Session AFP/Robbins-Conjecture (AFP)
Session AFP/Roy_Floyd_Warshall (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/Security_Protocol_Refinement (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Planarity_Certificates (AFP)
Session AFP/Stellar_Quorums (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 AFP/TESL_Language (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/Typeclass_Hierarchy (doc)
Session AFP/Types_Tableaus_and_Goedels_God (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)
HOL-Analysis: theory HOL-Library.Cancellation
HOL-Analysis: theory HOL-Library.Infinite_Set
HOL-Analysis: theory HOL-Library.FuncSet
HOL-Analysis: theory HOL-Library.Disjoint_Sets
HOL-Analysis: theory HOL-Library.Nat_Bijection
HOL-Analysis: theory HOL-Library.Old_Datatype
HOL-Analysis: theory HOL-Library.Multiset
HOL-Analysis: theory HOL-Library.Phantom_Type
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
HOL-Analysis: theory HOL-Analysis.Metric_Arith
Perron_Frobenius: theory HOL-Eisbach.Eisbach
Perron_Frobenius: theory HOL-Types_To_Sets.Types_To_Sets
Perron_Frobenius: theory HOL-Analysis.Metric_Arith
Perron_Frobenius: theory HOL-Analysis.Abstract_Topology
HOL-Analysis: theory HOL-Library.Cardinality
Perron_Frobenius: theory HOL-Analysis.Continuum_Not_Denumerable
HOL-Analysis: theory HOL-Analysis.Inner_Product
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-Library.Numeral_Type
HOL-Analysis: theory HOL-Library.Countable_Set
Perron_Frobenius: theory Sturm_Sequences.Sturm_Library
Perron_Frobenius: theory Sturm_Sequences.Sturm_Theorem
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
HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable
HOL-Analysis: theory HOL-Analysis.Abstract_Topology
Perron_Frobenius: theory Sturm_Sequences.Sturm_Method
HOL-Analysis: theory HOL-Analysis.L2_Norm
HOL-Analysis: theory HOL-Analysis.Operator_Norm
HOL-Analysis: theory HOL-Analysis.Poly_Roots
HOL-Analysis: theory HOL-Analysis.Product_Vector
Perron_Frobenius: theory HOL-Analysis.Norm_Arith
Perron_Frobenius: theory Polynomial_Factorization.Square_Free_Factorization
Perron_Frobenius: theory HOL-Analysis.Abstract_Limits
HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring
HOL-Analysis: theory HOL-Library.Permutations
Perron_Frobenius: theory Rank_Nullity_Theorem.Dual_Order
Perron_Frobenius: theory HOL-Analysis.Finite_Cartesian_Product
HOL-Analysis: theory HOL-Analysis.Elementary_Topology
Perron_Frobenius: theory HOL-Analysis.Linear_Algebra
Perron_Frobenius: theory HOL-Analysis.Abstract_Topology_2
HOL-Analysis: theory HOL-Analysis.Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Abstract_Limits
Perron_Frobenius: theory HOL-Analysis.Convex
HOL-Analysis: theory HOL-Library.Discrete
HOL-Analysis: theory HOL-Library.Indicator_Function
Perron_Frobenius: theory HOL-Analysis.Connected
Perron_Frobenius: theory HOL-Analysis.Cartesian_Space
Perron_Frobenius: theory HOL-Analysis.Elementary_Metric_Spaces
HOL-Analysis: theory HOL-Library.Liminf_Limsup
HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2
HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product
HOL-Analysis: theory HOL-Analysis.Linear_Algebra
Perron_Frobenius: theory HOL-Analysis.Determinants
HOL-Analysis: theory HOL-Analysis.Connected
HOL-Analysis: theory HOL-Analysis.Convex
Perron_Frobenius: theory HOL-Analysis.Elementary_Normed_Spaces
HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces
Perron_Frobenius: theory HOL-Analysis.Topology_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Cartesian_Space
HOL-Analysis: theory HOL-Analysis.Determinants
HOL-Analysis: theory HOL-Library.Nonpos_Ints
HOL-Analysis: theory HOL-Library.Order_Continuity
HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm
HOL-Analysis: theory HOL-Library.Periodic_Fun
HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces
Perron_Frobenius: theory HOL-Analysis.Convex_Euclidean_Space
Perron_Frobenius: theory HOL-Analysis.Extended_Real_Limits
HOL-Analysis: theory HOL-Library.Extended_Nat
HOL-Analysis: theory HOL-Library.Sum_of_Squares
Perron_Frobenius: theory HOL-Analysis.Function_Topology
HOL-Analysis: theory HOL-Library.Extended_Real
Perron_Frobenius: theory HOL-Analysis.Line_Segment
Perron_Frobenius: theory HOL-Analysis.Summation_Tests
Perron_Frobenius: theory HOL-Analysis.Product_Topology
Perron_Frobenius: theory HOL-Analysis.T1_Spaces
Perron_Frobenius: theory HOL-Analysis.Starlike
Perron_Frobenius: theory HOL-Analysis.Uniform_Limit
HOL-Analysis: theory HOL-Analysis.Norm_Arith
Perron_Frobenius: theory HOL-Analysis.Bounded_Linear_Function
HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space
HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real
HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Function_Topology
HOL-Analysis: theory HOL-Analysis.Sigma_Algebra
Perron_Frobenius: theory HOL-Analysis.Path_Connected
HOL-Analysis: theory HOL-Computational_Algebra.Primes
HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series
HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits
Perron_Frobenius: theory HOL-Analysis.Derivative
HOL-Analysis: theory HOL-Analysis.Summation_Tests
Perron_Frobenius: theory HOL-Analysis.Homotopy
HOL-Analysis: theory HOL-Analysis.Measurable
HOL-Analysis: theory HOL-Analysis.Uniform_Limit
HOL-Analysis: theory HOL-Analysis.Measure_Space
Perron_Frobenius: theory HOL-Analysis.Cartesian_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function
Perron_Frobenius: theory Rank_Nullity_Theorem.Mod_Type
Perron_Frobenius: theory HOL-Analysis.Homeomorphism
Perron_Frobenius: theory HOL-Analysis.Brouwer_Fixpoint
HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function
Perron_Frobenius: theory Rank_Nullity_Theorem.Miscellaneous
HOL-Analysis: theory HOL-Analysis.Product_Topology
HOL-Analysis: theory HOL-Analysis.T1_Spaces
HOL-Analysis: theory HOL-Analysis.Line_Segment
HOL-Analysis: theory HOL-Analysis.Lindelof_Spaces
HOL-Analysis: theory HOL-Analysis.Tagged_Division
HOL-Analysis: theory HOL-Analysis.Caratheodory
HOL-Analysis: theory HOL-Analysis.Starlike
HOL-Analysis: theory HOL-Analysis.Derivative
HOL-Analysis: theory HOL-Analysis.Borel_Space
HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics
HOL-Analysis: theory HOL-Analysis.Lipschitz
HOL-Analysis: theory HOL-Analysis.Cross3
HOL-Analysis: theory HOL-Analysis.Continuous_Extension
HOL-Analysis: theory HOL-Analysis.Path_Connected
HOL-Analysis: theory HOL-Analysis.Complex_Transcendental
HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
HOL-Analysis: theory HOL-Analysis.Regularity
HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem
HOL-Analysis: theory HOL-Analysis.Infinite_Products
HOL-Analysis: theory HOL-Analysis.Multivariate_Analysis
HOL-Analysis: theory HOL-Analysis.Arcwise_Connected
HOL-Analysis: theory HOL-Analysis.Homotopy
HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure
HOL-Analysis: theory HOL-Analysis.Locally
HOL-Analysis: theory HOL-Analysis.Embed_Measure
HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure
HOL-Analysis: theory HOL-Analysis.Polytope
HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems
HOL-Analysis: theory HOL-Analysis.Bochner_Integration
HOL-Analysis: theory HOL-Analysis.Homeomorphism
HOL-Analysis: theory HOL-Analysis.Abstract_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint
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.Fashoda_Theorem
HOL-Analysis: theory HOL-Analysis.Retracts
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.FPS_Convergence
HOL-Analysis: theory HOL-Analysis.Gamma_Function
HOL-Analysis: theory HOL-Analysis.Great_Picard
HOL-Analysis: theory HOL-Analysis.Jordan_Curve
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 HOL-Real_Asymp.Inst_Existentials
Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint
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, 217.772s elapsed time, 749.644s cpu time, 63.988s GC time, factor 3.44)
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, 217.772s elapsed time, 749.644s cpu time, 63.988s GC time, factor 3.44)
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:45 elapsed time, 0:12:43 cpu time, factor 3.38)
Timing HOL-Analysis (4 threads, 486.882s elapsed time, 1717.652s cpu time, 103.196s GC time, factor 3.53)
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, 486.882s elapsed time, 1717.652s cpu time, 103.196s GC time, factor 3.53)
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:10:22 elapsed time, 0:32:17 cpu time, factor 3.11)
Building Ordinary_Differential_Equations ...
Building Affine_Arithmetic ...
Running Hybrid_Systems_VCs ...
Building Count_Complex_Roots ...
Running Transcendence_Series_Hancl_Rucki ...
Ordinary_Differential_Equations: theory HOL-Library.Code_Abstract_Nat
Ordinary_Differential_Equations: theory HOL-Decision_Procs.Dense_Linear_Order
Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Int
Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence
HOL-Probability: theory HOL-Library.Adhoc_Overloading
HOL-Probability: theory HOL-Library.Conditional_Parametricity
HOL-Probability: theory HOL-Library.AList
HOL-Probability: theory HOL-Library.Lattice_Syntax
Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Nat
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
HOL-Probability: theory HOL-Library.Complete_Partial_Order2
Echelon_Form: theory HOL-Library.Code_Target_Nat
Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras
HOL-Probability: theory HOL-Library.Monad_Syntax
Ordinary_Differential_Equations: theory HOL-Library.Log_Nat
Count_Complex_Roots: theory HOL-Eisbach.Eisbach
Count_Complex_Roots: theory HOL-Computational_Algebra.Fraction_Field
Count_Complex_Roots: theory HOL-Library.More_List
HOL-Probability: theory HOL-Library.Mapping
Count_Complex_Roots: theory HOL-Computational_Algebra.Field_as_Ring
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
Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral
Echelon_Form: theory HOL-Library.IArray
Echelon_Form: theory HOL-Library.More_List
Hybrid_Systems_VCs: theory HOL-Library.Lattice_Syntax
Hybrid_Systems_VCs: theory HOL-Library.Log_Nat
Hybrid_Systems_VCs: theory HOL-Library.Lattice_Algebras
Hybrid_Systems_VCs: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
Affine_Arithmetic: theory HOL-Library.Adhoc_Overloading
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
Hybrid_Systems_VCs: theory Ordinary_Differential_Equations.Vector_Derivative_On
Ordinary_Differential_Equations: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
Ordinary_Differential_Equations: theory Triangle.Angles
Echelon_Form: theory HOL-Library.Code_Target_Numeral
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
Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial
Affine_Arithmetic: theory HOL-Library.Monad_Syntax
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
Affine_Arithmetic: theory Deriving.Equality_Generator
Hybrid_Systems_VCs: theory Kleene_Algebra.Signatures
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator
Dirichlet_Series: theory HOL-Library.Monad_Syntax
Affine_Arithmetic: theory HOL-Library.Boolean_Algebra
Hybrid_Systems_VCs: theory List-Index.List_Index
Dirichlet_Series: theory HOL-Computational_Algebra.Nth_Powers
Echelon_Form: theory Gauss_Jordan.Code_Set
Echelon_Form: theory HOL-Library.Z2
Echelon_Form: theory HOL-Computational_Algebra.Field_as_Ring
HOL-Probability: theory HOL-Library.Stream
Ordinary_Differential_Equations: theory Triangle.Triangle
QR_Decomposition: theory Deriving.Derive_Manager
QR_Decomposition: theory Real_Impl.Real_Impl_Auxiliary
QR_Decomposition: theory HOL-Library.Code_Abstract_Nat
QR_Decomposition: theory Deriving.Generator_Aux
E_Transcendental: theory HOL-Number_Theory.Eratosthenes
Hybrid_Systems_VCs: theory Ordinary_Differential_Equations.Gronwall
QR_Decomposition: theory HOL-Library.Code_Target_Int
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.Permutation
Hybrid_Systems_VCs: theory Ordinary_Differential_Equations.Interval_Integral_HK
QR_Decomposition: theory HOL-Library.IArray
Dirichlet_Series: theory HOL-Computational_Algebra.Squarefree
Hybrid_Systems_VCs: theory Kleene_Algebra.Dioid
QR_Decomposition: theory Gauss_Jordan.Code_Set
QR_Decomposition: theory HOL-Library.Z2
QR_Decomposition: theory Cauchy.CauchysMeanTheorem
Affine_Arithmetic: theory HOL-Library.Char_ord
QR_Decomposition: theory HOL-Library.Code_Target_Numeral
Affine_Arithmetic: theory Deriving.Equality_Instances
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Vector_Derivative_On
E_Transcendental: theory HOL-Number_Theory.Fib
Count_Complex_Roots: theory HOL-Eisbach.Eisbach_Tools
Affine_Arithmetic: theory HOL-Library.Code_Abstract_Nat
Echelon_Form: theory Gauss_Jordan.Code_Z2
QR_Decomposition: theory HOL-Library.Code_Real_Approx_By_Float
Hybrid_Systems_VCs: theory Order_Lattice_Props.Sup_Lattice
Affine_Arithmetic: theory HOL-Library.Code_Target_Int
Count_Complex_Roots: theory Winding_Number_Eval.Missing_Topology
Dirichlet_Series: theory HOL-Number_Theory.Cong
Echelon_Form: theory HOL-Computational_Algebra.Polynomial
Affine_Arithmetic: theory HOL-Library.Code_Target_Nat
Echelon_Form: theory Gauss_Jordan.IArray_Addenda
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Gronwall
Echelon_Form: theory Cayley_Hamilton.Square_Matrix
Affine_Arithmetic: theory Deriving.Compare
QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
Transcendence_Series_Hancl_Rucki: theory HOL-Eisbach.Eisbach_Tools
Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Nth_Powers
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Interval_Integral_HK
Dirichlet_Series: theory HOL-Library.Code_Abstract_Nat
QR_Decomposition: theory Gauss_Jordan.Code_Z2
E_Transcendental: theory HOL-Number_Theory.Prime_Powers
Affine_Arithmetic: theory Deriving.Comparator_Generator
Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral
Dirichlet_Series: theory HOL-Library.Code_Target_Nat
HOL-Probability: theory HOL-Library.Rewrite
QR_Decomposition: theory Rank_Nullity_Theorem.Dual_Order
Affine_Arithmetic: theory HOL-Library.Mapping
Ordinary_Differential_Equations: theory List-Index.List_Index
Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Squarefree
QR_Decomposition: theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell
Dirichlet_Series: theory HOL-Library.Code_Target_Int
Count_Complex_Roots: theory Winding_Number_Eval.Missing_Analysis
Echelon_Form: theory HOL-Computational_Algebra.Normalized_Fraction
QR_Decomposition: theory Show.Show
Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Cong
Count_Complex_Roots: theory HOL-Computational_Algebra.Normalized_Fraction
E_Transcendental: theory HOL-Algebra.Order
QR_Decomposition: theory QR_Decomposition.IArray_Addenda_QR
HOL-Probability: theory HOL-Library.AList_Mapping
QR_Decomposition: theory Rank_Nullity_Theorem.Mod_Type
HOL-Probability: theory HOL-Library.Sublist
Dirichlet_Series: theory HOL-Library.Code_Target_Numeral
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Congruence
Dirichlet_Series: theory HOL-Computational_Algebra.Normalized_Fraction
HOL-Probability: theory HOL-Library.Tree
Dirichlet_Series: theory HOL-Algebra.Congruence
Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Normalized_Fraction
E_Transcendental: theory HOL-Number_Theory.Mod_Exp
HOL-Probability: theory HOL-Library.FSet
QR_Decomposition: theory Sqrt_Babylonian.Log_Impl
Affine_Arithmetic: theory HOL-Library.Type_Length
Affine_Arithmetic: theory Deriving.Compare_Generator
Echelon_Form: theory Rank_Nullity_Theorem.Dual_Order
Dirichlet_Series: theory HOL-Library.Function_Algebras
Affine_Arithmetic: theory HOL-Library.RBT_Impl
QR_Decomposition: theory Sqrt_Babylonian.NthRoot_Impl
E_Transcendental: theory HOL-Number_Theory.Totient
Echelon_Form: theory Rank_Nullity_Theorem.Mod_Type
Dirichlet_Series: theory HOL-Library.More_List
Affine_Arithmetic: theory HOL-Library.Z2
Dirichlet_Series: theory HOL-Library.Power_By_Squaring
Transcendence_Series_Hancl_Rucki: theory HOL-Library.More_List
Affine_Arithmetic: theory Deriving.Compare_Instances
QR_Decomposition: theory Show.Show_Instances
QR_Decomposition: theory Show.Show_Real
Dirichlet_Series: theory HOL-Library.Stirling
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Order
Dirichlet_Series: theory HOL-Number_Theory.Mod_Exp
Transcendence_Series_Hancl_Rucki: theory HOL-Library.Power_By_Squaring
E_Transcendental: theory HOL-Algebra.Lattice
Affine_Arithmetic: theory HOL-Word.Bits
Dirichlet_Series: theory HOL-Algebra.Order
Affine_Arithmetic: theory HOL-Word.Misc_Auxiliary
QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian
Affine_Arithmetic: theory HOL-Word.Bits_Z2
HOL-Probability: theory HOL-Library.Diagonal_Subsequence
Transcendence_Series_Hancl_Rucki: theory HOL-Library.Stirling
Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Mod_Exp
Dirichlet_Series: theory HOL-Number_Theory.Eratosthenes
Affine_Arithmetic: theory HOL-Word.Bits_Int
Affine_Arithmetic: theory HOL-Word.Misc_Arithmetic
Affine_Arithmetic: theory HOL-Word.Misc_Typedef
HOL-Probability: theory HOL-Library.Multiset_Permutations
HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams
Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Eratosthenes
QR_Decomposition: theory Real_Impl.Prime_Product
QR_Decomposition: theory Real_Impl.Real_Impl
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
Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Inst_Existentials
Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli
Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Field_as_Ring
Dirichlet_Series: theory HOL-Library.Going_To_Filter
Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Integer
Affine_Arithmetic: theory HOL-Library.Lattice_Algebras
Dirichlet_Series: theory HOL-Library.Landau_Symbols
Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Polynomial
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Lattice
E_Transcendental: theory HOL-Algebra.Complete_Lattice
Affine_Arithmetic: theory HOL-Library.Log_Nat
Dirichlet_Series: theory HOL-Algebra.Lattice
QR_Decomposition: theory Rank_Nullity_Theorem.Miscellaneous
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
HOL-Probability: theory HOL-Probability.Discrete_Topology
QR_Decomposition: theory Real_Impl.Real_Unique_Impl
Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise
HOL-Probability: theory HOL-Probability.Essential_Supremum
HOL-Probability: theory HOL-Probability.Probability_Measure
HOL-Probability: theory HOL-Probability.Stopping_Time
HOL-Probability: theory HOL-Probability.Tree_Space
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Complete_Lattice
Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector
E_Transcendental: theory HOL-Algebra.Group
Ordinary_Differential_Equations: theory HOL-Library.Interval
Ordinary_Differential_Equations: theory HOL-Library.Float
Echelon_Form: theory Rank_Nullity_Theorem.Miscellaneous
Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict
Transcendence_Series_Hancl_Rucki: theory HOL-Library.Going_To_Filter
Dirichlet_Series: theory HOL-Algebra.Complete_Lattice
Transcendence_Series_Hancl_Rucki: theory HOL-Library.Landau_Symbols
QR_Decomposition: theory Gauss_Jordan.Code_Matrix
QR_Decomposition: theory Gauss_Jordan.Rref
Hybrid_Systems_VCs: theory HOL-Library.Float
QR_Decomposition: theory Rank_Nullity_Theorem.Fundamental_Subspaces
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Group
Affine_Arithmetic: theory HOL-Word.Bit_Comprehension
QR_Decomposition: theory QR_Decomposition.Generalizations2
Hybrid_Systems_VCs: theory Order_Lattice_Props.Order_Duality
QR_Decomposition: theory Rank_Nullity_Theorem.Dim_Formula
Affine_Arithmetic: theory Native_Word.More_Bits_Int
Affine_Arithmetic: theory HOL-Word.Word
QR_Decomposition: theory Gauss_Jordan.Elementary_Operations
HOL-Probability: theory HOL-Probability.Conditional_Expectation
QR_Decomposition: theory Gauss_Jordan.Rank
HOL-Probability: theory HOL-Library.Finite_Map
Dirichlet_Series: theory HOL-Algebra.Group
HOL-Probability: theory HOL-Probability.Distribution_Functions
Dirichlet_Series: theory Bernoulli.Periodic_Bernpoly
Echelon_Form: theory Gauss_Jordan.Code_Matrix
Echelon_Form: theory Gauss_Jordan.Rref
HOL-Probability: theory HOL-Probability.Weak_Convergence
Dirichlet_Series: theory HOL-Number_Theory.Fib
QR_Decomposition: theory QR_Decomposition.Matrix_To_IArray_QR
QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan
HOL-Probability: theory HOL-Probability.Giry_Monad
Echelon_Form: theory Rank_Nullity_Theorem.Fundamental_Subspaces
HOL-Probability: theory HOL-Probability.Helly_Selection
Echelon_Form: theory Rank_Nullity_Theorem.Dim_Formula
Echelon_Form: theory Gauss_Jordan.Elementary_Operations
Dirichlet_Series: theory HOL-Number_Theory.Prime_Powers
E_Transcendental: theory HOL-Algebra.Coset
E_Transcendental: theory HOL-Algebra.FiniteProduct
Echelon_Form: theory Gauss_Jordan.Rank
Affine_Arithmetic: theory Native_Word.Code_Symbolic_Bits_Int
Affine_Arithmetic: theory Native_Word.Bits_Integer
Ordinary_Differential_Equations: theory Affine_Arithmetic.Executable_Euclidean_Space
Ordinary_Differential_Equations: theory HOL-Library.Interval_Float
Transcendence_Series_Hancl_Rucki: theory Bernoulli.Periodic_Bernpoly
Echelon_Form: theory Gauss_Jordan.Matrix_To_IArray
Dirichlet_Series: theory HOL-Number_Theory.Totient
Echelon_Form: theory Gauss_Jordan.Gauss_Jordan
E_Transcendental: theory HOL-Algebra.Ring
Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Topology
Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Analysis
Hybrid_Systems_VCs: theory Affine_Arithmetic.Executable_Euclidean_Space
Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Fib
Dirichlet_Series: theory HOL-Real_Asymp.Eventuallize
Dirichlet_Series: theory HOL-Real_Asymp.Lazy_Eval
Count_Complex_Roots: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial_Factorial
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Coset
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.FiniteProduct
Dirichlet_Series: theory Landau_Symbols.Group_Sort
Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Prime_Powers
QR_Decomposition: theory Gauss_Jordan.Linear_Maps
HOL-Probability: theory HOL-Probability.Probability_Mass_Function
HOL-Probability: theory HOL-Probability.Projective_Family
Dirichlet_Series: theory HOL-Algebra.Coset
Dirichlet_Series: theory HOL-Algebra.FiniteProduct
E_Transcendental: theory HOL-Algebra.Generated_Groups
Echelon_Form: theory HOL-Computational_Algebra.Polynomial_Factorial
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Ring
Echelon_Form: theory Cayley_Hamilton.Cayley_Hamilton
Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation_Bounds
Affine_Arithmetic: theory HOL-Library.Interval
QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan_PA
Dirichlet_Series: theory HOL-Algebra.Ring
Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Totient
Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_IArrays
Echelon_Form: theory Gauss_Jordan.Linear_Maps
HOL-Probability: theory HOL-Probability.Infinite_Product_Measure
Dirichlet_Series: theory HOL-Real_Asymp.Multiseries_Expansion
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Generated_Groups
Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Eventuallize
Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Lazy_Eval
QR_Decomposition: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
QR_Decomposition: theory Gauss_Jordan.Determinants2
HOL-Probability: theory HOL-Probability.Independent_Family
HOL-Probability: theory HOL-Probability.Stream_Space
Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA
QR_Decomposition: theory Gauss_Jordan.Inverse
Dirichlet_Series: theory HOL-Algebra.Generated_Groups
QR_Decomposition: theory Gauss_Jordan.System_Of_Equations
HOL-Probability: theory HOL-Probability.PMF_Impl
QR_Decomposition: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
Echelon_Form: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
Echelon_Form: theory Gauss_Jordan.Determinants2
Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays
Affine_Arithmetic: theory HOL-Library.Float
HOL-Probability: theory HOL-Probability.Random_Permutations
Echelon_Form: theory Gauss_Jordan.Inverse
Echelon_Form: theory Gauss_Jordan.System_Of_Equations
HOL-Probability: theory HOL-Probability.SPMF
Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
Echelon_Form: theory Gauss_Jordan.Inverse_IArrays
Echelon_Form: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
QR_Decomposition: theory QR_Decomposition.Miscellaneous_QR
Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Multiseries_Expansion
Affine_Arithmetic: theory Affine_Arithmetic.Polygon
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities
Hybrid_Systems_VCs: theory Ordinary_Differential_Equations.ODE_Auxiliarities
QR_Decomposition: theory QR_Decomposition.Projections
HOL-Probability: theory HOL-Probability.Convolution
QR_Decomposition: theory QR_Decomposition.Gram_Schmidt
Affine_Arithmetic: theory List-Index.List_Index
HOL-Probability: theory HOL-Probability.Information
Dirichlet_Series: theory Landau_Symbols.Landau_Real_Products
Hybrid_Systems_VCs: theory Kleene_Algebra.Conway
QR_Decomposition: theory QR_Decomposition.QR_Decomposition
E_Transcendental: theory HOL-Algebra.AbelCoset
E_Transcendental: theory HOL-Algebra.Module
Affine_Arithmetic: theory Show.Show
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Cones
Hybrid_Systems_VCs: theory Ordinary_Differential_Equations.Initial_Value_Problem
Dirichlet_Series: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Hybrid_Systems_VCs: theory Order_Lattice_Props.Order_Lattice_Props
Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Polynomial_FPS
QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Float
Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_FPS
Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Polynomial_Factorial
Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Float
Affine_Arithmetic: theory Affine_Arithmetic.Float_Real
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem
Transcendence_Series_Hancl_Rucki: theory HOL-Computational_Algebra.Formal_Laurent_Series
Affine_Arithmetic: theory HOL-Library.Interval_Float
Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space
Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation
Dirichlet_Series: theory HOL-Computational_Algebra.Formal_Laurent_Series
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.AbelCoset
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor
Dirichlet_Series: theory HOL-Algebra.AbelCoset
Affine_Arithmetic: theory HOL-Decision_Procs.Approximation_Bounds
QR_Decomposition: theory QR_Decomposition.Gram_Schmidt_IArrays
QR_Decomposition: theory QR_Decomposition.Least_Squares_Approximation
Hybrid_Systems_VCs: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Symbolic
QR_Decomposition: theory QR_Decomposition.QR_Decomposition_IArrays
QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Float
QR_Decomposition: theory QR_Decomposition.QR_Efficient
HOL-Probability: theory HOL-Probability.Distributions
Hybrid_Systems_VCs: theory Hybrid_Systems_VCs.HS_Preliminaries
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
Hybrid_Systems_VCs: theory Hybrid_Systems_VCs.HS_ODEs
Dirichlet_Series: theory HOL-Algebra.Module
E_Transcendental: theory HOL-Algebra.Ideal
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Module
Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_Factorial
Hybrid_Systems_VCs: theory Hybrid_Systems_VCs.HS_VC_Spartan
HOL-Probability: theory HOL-Probability.Characteristic_Functions
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Ideal
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form
HOL-Probability: theory HOL-Probability.Sinc_Integral
HOL-Probability: theory HOL-Probability.Fin_Map
Hybrid_Systems_VCs: theory Hybrid_Systems_VCs.HS_VC_Examples
HOL-Probability: theory HOL-Probability.Levy
Affine_Arithmetic: theory Native_Word.Code_Target_Word_Base
Dirichlet_Series: theory HOL-Algebra.Ideal
Dirichlet_Series: theory Landau_Symbols.Landau_Simprocs
HOL-Probability: theory HOL-Probability.Central_Limit_Theorem
Affine_Arithmetic: theory HOL-Decision_Procs.Approximation
Affine_Arithmetic: theory Native_Word.Uint32
E_Transcendental: theory HOL-Algebra.RingHom
Dirichlet_Series: theory Landau_Symbols.Landau_More
HOL-Probability: theory HOL-Probability.Projective_Limit
Dirichlet_Series: theory Matrix.Utility
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Poincare_Map
Dirichlet_Series: theory Polynomial_Factorization.Missing_List
Hybrid_Systems_VCs: theory Kleene_Algebra.Kleene_Algebra
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.RingHom
E_Transcendental: theory HOL-Algebra.UnivPoly
Affine_Arithmetic: theory Collections.HashCode
HOL-Probability: theory HOL-Probability.Probability
Affine_Arithmetic: theory Affine_Arithmetic.Intersection
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis
Dirichlet_Series: theory HOL-Algebra.RingHom
Affine_Arithmetic: theory Deriving.Hash_Generator
Dirichlet_Series: theory Polynomial_Factorization.Missing_Multiset
Hybrid_Systems_VCs: theory Order_Lattice_Props.Galois_Connections
Hybrid_Systems_VCs: theory Transformer_Semantics.Powerset_Monad
Hybrid_Systems_VCs: theory Order_Lattice_Props.Closure_Operators
Affine_Arithmetic: theory Deriving.Hash_Instances
Affine_Arithmetic: theory Deriving.Derive
QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Symbolic
Hybrid_Systems_VCs: theory Order_Lattice_Props.Fixpoint_Fusion
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow_Congs
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.UnivPoly
Hybrid_Systems_VCs: theory Quantales.Quantales
Dirichlet_Series: theory Polynomial_Factorization.Prime_Factorization
Dirichlet_Series: theory HOL-Algebra.UnivPoly
Affine_Arithmetic: theory Show.Show_Instances
Hybrid_Systems_VCs: theory KAD.Domain_Semiring
Count_Complex_Roots: theory Sturm_Tarski.PolyMisc
Echelon_Form: theory Echelon_Form.Rings2
Count_Complex_Roots: theory Sturm_Tarski.Sturm_Tarski
Count_Complex_Roots: theory Budan_Fourier.BF_Misc
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-Algebra.Multiplicative_Group
Count_Complex_Roots: theory Count_Complex_Roots.Extended_Sturm
Count_Complex_Roots: theory Winding_Number_Eval.Winding_Number_Eval
Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots
E_Transcendental: theory HOL-Number_Theory.Residues
Transcendence_Series_Hancl_Rucki: theory HOL-Algebra.Multiplicative_Group
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
Affine_Arithmetic: theory HOL-Library.RBT
Dirichlet_Series: theory HOL-Algebra.Multiplicative_Group
Affine_Arithmetic: theory HOL-Library.RBT_Mapping
Transcendence_Series_Hancl_Rucki: theory Budan_Fourier.BF_Misc
E_Transcendental: theory HOL-Number_Theory.Euler_Criterion
E_Transcendental: theory HOL-Number_Theory.Pocklington
Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots_Examples
E_Transcendental: theory HOL-Number_Theory.Gauss
E_Transcendental: theory HOL-Number_Theory.Residue_Primitive_Roots
E_Transcendental: theory HOL-Number_Theory.Quadratic_Reciprocity
Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Algebraic
E_Transcendental: theory HOL-Number_Theory.Number_Theory
Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Residues
Dirichlet_Series: theory HOL-Computational_Algebra.Computational_Algebra
Dirichlet_Series: theory HOL-Number_Theory.Residues
Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Missing_Transcendental
Dirichlet_Series: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
E_Transcendental: theory E_Transcendental.E_Transcendental
Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Cauchy_Index_Theorem
Transcendence_Series_Hancl_Rucki: 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
Dirichlet_Series: theory HOL-Number_Theory.Euler_Criterion
Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Pocklington
Dirichlet_Series: theory HOL-Number_Theory.Gauss
Dirichlet_Series: theory HOL-Number_Theory.Pocklington
Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Quadratic_Reciprocity
Dirichlet_Series: theory HOL-Number_Theory.Quadratic_Reciprocity
Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Residue_Primitive_Roots
Dirichlet_Series: theory HOL-Real_Asymp.Real_Asymp
Transcendence_Series_Hancl_Rucki: theory HOL-Number_Theory.Number_Theory
Transcendence_Series_Hancl_Rucki: theory Winding_Number_Eval.Winding_Number_Eval
Dirichlet_Series: theory HOL-Number_Theory.Residue_Primitive_Roots
Dirichlet_Series: theory HOL-Number_Theory.Number_Theory
Transcendence_Series_Hancl_Rucki: theory HOL-Real_Asymp.Real_Asymp
Hybrid_Systems_VCs: theory KAD.Antidomain_Semiring
Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli_FPS
Dirichlet_Series: theory Bernoulli.Bernoulli_FPS
Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Misc
Dirichlet_Series: theory Dirichlet_Series.Multiplicative_Function
Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Product
Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Misc
Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Multiplicative_Function
Dirichlet_Series: theory Dirichlet_Series.Euler_Products
Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series
Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Product
Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Euler_Products
Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Series
Transcendence_Series_Hancl_Rucki: theory Bernoulli.Bernoulli_Zeta
Transcendence_Series_Hancl_Rucki: theory Euler_MacLaurin.Euler_MacLaurin
Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin
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
Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory
Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Efficient_Code
Dirichlet_Series: theory Dirichlet_Series.Partial_Summation
Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin_Landau
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.Liouville_Lambda
Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Divisor_Count
Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Arithmetic_Summatory
Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Partial_Summation
Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series_Analysis
Transcendence_Series_Hancl_Rucki: theory Dirichlet_Series.Dirichlet_Series_Analysis
Echelon_Form: theory Echelon_Form.Cayley_Hamilton_Compatible
Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton
Echelon_Form: theory Echelon_Form.Echelon_Form
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex
Echelon_Form: theory Echelon_Form.Echelon_Form_Det
Echelon_Form: theory Echelon_Form.Echelon_Form_IArrays
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis
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.Echelon_Form_Inverse_IArrays
Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_Abstract
Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics
Transcendence_Series_Hancl_Rucki: theory Zeta_Function.Zeta_Function
Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_IArrays
Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression
Transcendence_Series_Hancl_Rucki: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
Transcendence_Series_Hancl_Rucki: theory Transcendence_Series_Hancl_Rucki.Transcendence_Series
Timing E_Transcendental (4 threads, 108.362s elapsed time, 386.832s cpu time, 23.116s GC time, factor 3.57)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/E_Transcendental
Hybrid_Systems_VCs: theory Quantales.Quantale_Star
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
Hybrid_Systems_VCs: theory Transformer_Semantics.Isotone_Transformers
Hybrid_Systems_VCs: theory KAD.Range_Semiring
Hybrid_Systems_VCs: theory Transformer_Semantics.Sup_Inf_Preserving_Transformers
Hybrid_Systems_VCs: theory Transformer_Semantics.Kleisli_Transformers
Hybrid_Systems_VCs: theory Transformer_Semantics.Kleisli_Quantaloid
Hybrid_Systems_VCs: theory Transformer_Semantics.Kleisli_Quantale
Hybrid_Systems_VCs: theory Hybrid_Systems_VCs.HS_VC_PT
Hybrid_Systems_VCs: theory Hybrid_Systems_VCs.HS_VC_PT_Examples
Timing HOL-Probability (4 threads, 135.231s elapsed time, 446.616s cpu time, 21.760s GC time, factor 3.30)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation
Timing Count_Complex_Roots (4 threads, 145.597s elapsed time, 402.964s cpu time, 16.748s GC time, factor 2.77)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Count_Complex_Roots
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code
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
Affine_Arithmetic: theory Affine_Arithmetic.Print
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
Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation
Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs
Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter
Timing E_Transcendental (4 threads, 108.362s elapsed time, 386.832s cpu time, 23.116s GC time, factor 3.57)
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:36 elapsed time, 0:07:53 cpu time, factor 3.01)
Running Gromov_Hyperbolicity ...
Gromov_Hyperbolicity: theory HOL-Cardinals.Fun_More
Gromov_Hyperbolicity: theory HOL-Cardinals.Order_Relation_More
Gromov_Hyperbolicity: theory HOL-Cardinals.Order_Union
Gromov_Hyperbolicity: theory HOL-Decision_Procs.Dense_Linear_Order
Gromov_Hyperbolicity: theory HOL-Library.Code_Abstract_Nat
Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Int
Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Nat
Gromov_Hyperbolicity: theory HOL-Cardinals.Wellfounded_More
Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Relation
Gromov_Hyperbolicity: theory HOL-Library.Lattice_Algebras
Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Numeral
Gromov_Hyperbolicity: theory HOL-Library.Log_Nat
Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Embedding
Gromov_Hyperbolicity: theory Ergodic_Theory.Fekete
Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Constructions
Gromov_Hyperbolicity: theory HOL-Cardinals.Cardinal_Order_Relation
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Library_Complements
Hybrid_Systems_VCs: theory KAD.Modal_Kleene_Algebra
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Eexp_Eln
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Hausdorff_Distance
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Isometries
Gromov_Hyperbolicity: theory HOL-Library.Interval
Gromov_Hyperbolicity: theory HOL-Library.Float
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Metric_Completion
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Gromov_Hyperbolicity
Gromov_Hyperbolicity: theory HOL-Library.Interval_Float
Gromov_Hyperbolicity: theory HOL-Decision_Procs.Approximation_Bounds
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Gromov_Boundary
Gromov_Hyperbolicity: theory HOL-Decision_Procs.Approximation
Timing Count_Complex_Roots (4 threads, 145.597s elapsed time, 402.964s cpu time, 16.748s GC time, factor 2.77)
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:09 elapsed time, 0:07:56 cpu time, factor 2.52)
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-Cardinals.Wellorder_Relation
HOL-Homology: theory HOL-Library.More_List
HOL-Homology: theory HOL-Cardinals.Wellorder_Embedding
HOL-Homology: theory HOL-Library.Poly_Mapping
HOL-Homology: theory HOL-Cardinals.Wellorder_Constructions
Timing Ordinary_Differential_Equations (4 threads, 191.969s elapsed time, 591.756s cpu time, 26.444s GC time, factor 3.08)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ordinary_Differential_Equations
HOL-Homology: theory HOL-Algebra.Order
HOL-Homology: theory HOL-Cardinals.Cardinal_Order_Relation
Timing HOL-Probability (4 threads, 135.231s elapsed time, 446.616s cpu time, 21.760s GC time, factor 3.30)
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:13 elapsed time, 0:10:00 cpu time, factor 3.10)
HOL-Homology: theory HOL-Algebra.Lattice
HOL-Homology: theory HOL-Cardinals.Cardinal_Arithmetic
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic
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
Markov_Models: theory HOL-Library.Code_Target_Nat
HOL-Homology: theory HOL-Algebra.Complete_Lattice
Markov_Models: theory HOL-Library.Simps_Case_Conv
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
HOL-Homology: theory HOL-Algebra.Group
Markov_Models: theory Coinductive.Coinductive_List
Hybrid_Systems_VCs: theory Hybrid_Systems_VCs.HS_VC_MKA_rel
Hybrid_Systems_VCs: theory Hybrid_Systems_VCs.HS_VC_MKA_ndfun
HOL-Homology: theory HOL-Algebra.Coset
HOL-Homology: theory HOL-Algebra.FiniteProduct
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
HOL-Homology: theory HOL-Algebra.Ring
Timing QR_Decomposition (4 threads, 201.453s elapsed time, 728.008s cpu time, 15.872s GC time, factor 3.61)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/QR_Decomposition
HOL-Homology: theory HOL-Algebra.Generated_Groups
HOL-Homology: theory HOL-Algebra.Solvable_Groups
Markov_Models: theory Coinductive.Coinductive_Stream
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
Timing QR_Decomposition (4 threads, 201.453s elapsed time, 728.008s cpu time, 15.872s GC time, factor 3.61)
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:29 elapsed time, 0:12:23 cpu time, factor 3.55)
Building Probabilistic_While ...
Markov_Models: theory Markov_Models.Markov_Models_Auxiliary
HOL-Homology: theory HOL-Algebra.AbelCoset
HOL-Homology: theory HOL-Algebra.Module
Probabilistic_While: theory Flow_Networks.Graph
Probabilistic_While: theory HOL-Library.Transitive_Closure_Table
Probabilistic_While: theory HOL-Types_To_Sets.Types_To_Sets
Probabilistic_While: theory HOL-Library.While_Combinator
Probabilistic_While: theory Probabilistic_While.Bernoulli
Probabilistic_While: theory HOL-Library.Bourbaki_Witt_Fixpoint
Markov_Models: theory Markov_Models.Discrete_Time_Markov_Chain
Probabilistic_While: theory MFMC_Countable.MFMC_Misc
Markov_Models: theory Markov_Models.Discrete_Time_Markov_Process
Probabilistic_While: theory Flow_Networks.Network
Markov_Models: theory Markov_Models.Classifying_Markov_Chain_States
Markov_Models: theory Markov_Models.Crowds_Protocol
Markov_Models: theory Markov_Models.Gossip_Broadcast
HOL-Homology: theory HOL-Algebra.Ideal
Probabilistic_While: theory Flow_Networks.Residual_Graph
Markov_Models: theory Markov_Models.Markov_Decision_Process
Markov_Models: theory Markov_Models.PCTL
Probabilistic_While: theory Flow_Networks.Augmenting_Flow
Markov_Models: theory Markov_Models.Trace_Space_Equals_Markov_Processes
Probabilistic_While: theory Flow_Networks.Augmenting_Path
Markov_Models: theory Markov_Models.Zeroconf_Analysis
Probabilistic_While: theory Flow_Networks.Ford_Fulkerson
Probabilistic_While: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
HOL-Homology: theory HOL-Algebra.RingHom
Markov_Models: theory Markov_Models.MDP_Reachability_Problem
Markov_Models: theory Markov_Models.Example_A
Probabilistic_While: theory MFMC_Countable.MFMC_Finite
Markov_Models: theory Markov_Models.Example_B
Markov_Models: theory Markov_Models.PGCL
Probabilistic_While: theory MFMC_Countable.Matrix_For_Marginals
Markov_Models: theory Markov_Models.MDP_RP_Certification
HOL-Homology: theory HOL-Algebra.UnivPoly
Markov_Models: theory Markov_Models.Continuous_Time_Markov_Chain
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
Markov_Models: theory Markov_Models.Markov_Models
Hybrid_Systems_VCs: theory Hybrid_Systems_VCs.HS_VC_MKA_Examples_ndfun
Hybrid_Systems_VCs: theory Hybrid_Systems_VCs.HS_VC_MKA_Examples_rel
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Morse_Gromov_Theorem
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Bonk_Schramm_Extension
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Boundary_Extension
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Busemann_Function
HOL-Homology: theory HOL-Algebra.Multiplicative_Group
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Isometries_Classification
Timing Hybrid_Systems_VCs (4 threads, 238.198s elapsed time, 748.084s cpu time, 24.336s GC time, factor 3.14)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hybrid_Systems_VCs
Timing Dirichlet_Series (4 threads, 239.722s elapsed time, 798.180s cpu time, 60.904s GC time, factor 3.33)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_Series
HOL-Homology: theory HOL-Algebra.Elementary_Groups
HOL-Homology: theory HOL-Algebra.Exact_Sequence
HOL-Homology: theory HOL-Algebra.Product_Groups
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hybrid_Systems_VCs/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hybrid_Systems_VCs/outline.pdf
HOL-Homology: theory HOL-Algebra.Free_Abelian_Groups
Timing Hybrid_Systems_VCs (4 threads, 238.198s elapsed time, 748.084s cpu time, 24.336s GC time, factor 3.14)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hybrid_Systems_VCs
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hybrid_Systems_VCs/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hybrid_Systems_VCs/outline.pdf
Finished Hybrid_Systems_VCs (0:04:04 elapsed time, 0:12:42 cpu time, factor 3.12)
Running Probabilistic_Prime_Tests ...
HOL-Homology: theory HOL-Homology.Simplices
Probabilistic_Prime_Tests: theory HOL-Cardinals.Fun_More
Probabilistic_Prime_Tests: theory HOL-Cardinals.Order_Union
Probabilistic_Prime_Tests: theory HOL-Cardinals.Order_Relation_More
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
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
Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellfounded_More
Probabilistic_Prime_Tests: theory HOL-Library.Fun_Lexorder
Probabilistic_Prime_Tests: theory HOL-Cardinals.Wellorder_Relation
Probabilistic_Prime_Tests: theory HOL-Algebra.Congruence
Probabilistic_Prime_Tests: theory HOL-Algebra.Cycles
HOL-Homology: theory HOL-Homology.Homology_Groups
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-Cardinals.Cardinal_Order_Relation
Probabilistic_Prime_Tests: theory HOL-Library.More_List
Probabilistic_Prime_Tests: theory HOL-Library.Power_By_Squaring
Probabilistic_Prime_Tests: theory HOL-Library.Poly_Mapping
Timing Probabilistic_While (4 threads, 38.638s elapsed time, 107.828s cpu time, 2.464s GC time, factor 2.79)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_While
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Mod_Exp
HOL-Homology: theory HOL-Homology.Brouwer_Degree
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Eratosthenes
Probabilistic_Prime_Tests: theory HOL-Cardinals.Cardinal_Arithmetic
Probabilistic_Prime_Tests: theory HOL-Algebra.Lattice
HOL-Homology: theory HOL-Homology.Invariance_of_Domain
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Fib
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Prime_Powers
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Totient
Probabilistic_Prime_Tests: theory HOL-Algebra.Complete_Lattice
HOL-Homology: theory HOL-Homology.Homology
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
Probabilistic_Prime_Tests: theory HOL-Algebra.Galois_Connection
Probabilistic_Prime_Tests: theory HOL-Algebra.Group
Timing Ordinary_Differential_Equations (4 threads, 191.969s elapsed time, 591.756s cpu time, 26.444s GC time, factor 3.08)
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:04:15 elapsed time, 0:11:44 cpu time, factor 2.76)
Probabilistic_Prime_Tests: theory HOL-Algebra.Bij
Probabilistic_Prime_Tests: theory HOL-Algebra.Coset
Probabilistic_Prime_Tests: theory HOL-Algebra.FiniteProduct
Probabilistic_Prime_Tests: theory HOL-Algebra.Ring
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 Deriving.Generator_Aux
HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util
Probabilistic_Prime_Tests: theory HOL-Algebra.Group_Action
HOL-ODE-Numerics: theory Deriving.Equality_Generator
Probabilistic_Prime_Tests: theory HOL-Algebra.Sylow
HOL-ODE-Numerics: theory HOL-Library.AList
Probabilistic_Prime_Tests: theory HOL-Algebra.Zassenhaus
HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification
HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data
Probabilistic_Prime_Tests: theory HOL-Algebra.Divisibility
HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars
HOL-ODE-Numerics: theory Automatic_Refinement.Named_Sorted_Thms
HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Record_Simp
HOL-ODE-Numerics: theory Automatic_Refinement.Tagged_Solver
HOL-ODE-Numerics: theory Automatic_Refinement.Select_Solve
HOL-ODE-Numerics: theory Deriving.Equality_Instances
Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Groups
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 HOL-Library.Mapping
HOL-ODE-Numerics: theory Deriving.Compare_Generator
HOL-ODE-Numerics: theory HOL-Library.Option_ord
HOL-ODE-Numerics: theory HOL-Library.Parallel
HOL-ODE-Numerics: theory Deriving.Compare_Instances
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
Probabilistic_Prime_Tests: theory HOL-Algebra.Solvable_Groups
HOL-ODE-Numerics: theory HOL-Types_To_Sets.Types_To_Sets
HOL-ODE-Numerics: theory HOL-Word.Bits
Probabilistic_Prime_Tests: theory HOL-Algebra.Sym_Groups
HOL-ODE-Numerics: theory HOL-Word.Bits_Z2
HOL-ODE-Numerics: theory HOL-Word.Misc_Auxiliary
HOL-ODE-Numerics: theory HOL-Word.Bits_Int
HOL-ODE-Numerics: theory HOL-Word.Misc_Arithmetic
Probabilistic_Prime_Tests: theory HOL-Algebra.AbelCoset
Probabilistic_Prime_Tests: theory HOL-Algebra.Module
HOL-ODE-Numerics: theory HOL-Word.Misc_Typedef
HOL-ODE-Numerics: theory Deriving.Countable_Generator
HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer
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 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
Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal
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
Timing Transcendence_Series_Hancl_Rucki (4 threads, 269.675s elapsed time, 913.960s cpu time, 62.716s GC time, factor 3.39)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Transcendence_Series_Hancl_Rucki
HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
HOL-ODE-Numerics: theory Collections.Assoc_List
Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal_Product
Probabilistic_Prime_Tests: theory HOL-Algebra.RingHom
HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
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
HOL-ODE-Numerics: theory Collections.Proper_Iterator
HOL-ODE-Numerics: theory Collections.Diff_Array
Markov_Models: theory Markov_Models.MDP_RP
Timing Transcendence_Series_Hancl_Rucki (4 threads, 269.675s elapsed time, 913.960s cpu time, 62.716s GC time, factor 3.39)
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:35 elapsed time, 0:15:25 cpu time, factor 3.36)
Running Differential_Dynamic_Logic ...
HOL-ODE-Numerics: theory Collections.It_to_It
HOL-ODE-Numerics: theory Collections.SetIteratorGA
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
Probabilistic_Prime_Tests: theory HOL-Algebra.QuotRing
Probabilistic_Prime_Tests: theory HOL-Algebra.UnivPoly
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
HOL-ODE-Numerics: theory Native_Word.Code_Symbolic_Bits_Int
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Ids
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Lib
HOL-ODE-Numerics: theory Native_Word.Bits_Integer
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Syntax
Timing Markov_Models (4 threads, 82.423s elapsed time, 291.000s cpu time, 18.068s GC time, factor 3.53)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Markov_Models
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
Probabilistic_Prime_Tests: theory HOL-Algebra.IntRing
Probabilistic_Prime_Tests: theory HOL-Algebra.Weak_Morphisms
Timing Probabilistic_While (4 threads, 38.638s elapsed time, 107.828s cpu time, 2.464s GC time, factor 2.79)
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:12 elapsed time, 0:02:44 cpu time, factor 2.26)
Probabilistic_Prime_Tests: theory HOL-Algebra.Chinese_Remainder
HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
HOL-ODE-Numerics: theory Collections.Intf_Comp
CryptHOL: theory HOL-Eisbach.Eisbach
CryptHOL: theory Applicative_Lifting.Applicative
CryptHOL: theory CryptHOL.Partial_Function_Set
CryptHOL: theory HOL-Library.Case_Converter
CryptHOL: theory HOL-Library.Simps_Case_Conv
CryptHOL: theory HOL-Algebra.Congruence
CryptHOL: theory HOL-Library.Function_Algebras
CryptHOL: theory HOL-Library.Type_Length
CryptHOL: theory HOL-Library.Countable_Set_Type
CryptHOL: theory HOL-Library.Landau_Symbols
HOL-ODE-Numerics: theory Collections.Idx_Iterator
CryptHOL: theory Applicative_Lifting.Applicative_Environment
CryptHOL: theory Applicative_Lifting.Applicative_Set
CryptHOL: theory CryptHOL.Environment_Functor
HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict
CryptHOL: theory CryptHOL.Set_Applicative
CryptHOL: theory HOL-Algebra.Order
CryptHOL: theory Coinductive.Coinductive_Nat
HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
CryptHOL: theory Coinductive.Coinductive_List
CryptHOL: theory HOL-Algebra.Lattice
HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
CryptHOL: theory Applicative_Lifting.Applicative_PMF
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis
HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form
CryptHOL: theory Monad_Normalisation.Monad_Normalisation
HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression
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
CryptHOL: theory Monomorphic_Monad.Monomorphic_Monad
CryptHOL: theory HOL-Algebra.Complete_Lattice
CryptHOL: theory HOL-Algebra.Group
CryptHOL: theory CryptHOL.SPMF_Applicative
CryptHOL: theory Landau_Symbols.Group_Sort
Probabilistic_Prime_Tests: theory HOL-Algebra.Multiplicative_Group
HOL-ODE-Numerics: theory Native_Word.Code_Target_Bits_Int
HOL-ODE-Numerics: theory Collections.Code_Target_ICF
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Denotational_Semantics
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Pretty_Printer
HOL-ODE-Numerics: theory Native_Word.Code_Target_Word_Base
HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
CryptHOL: theory Landau_Symbols.Landau_Real_Products
CryptHOL: theory HOL-Algebra.Coset
HOL-ODE-Numerics: theory Native_Word.Uint
HOL-ODE-Numerics: theory Native_Word.Uint32
CryptHOL: theory CryptHOL.Cyclic_Group
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
CryptHOL: theory CryptHOL.Cyclic_Group_SPMF
CryptHOL: theory Coinductive.TLList
Timing Gromov_Hyperbolicity (4 threads, 140.698s elapsed time, 459.108s cpu time, 22.604s GC time, factor 3.26)
Probabilistic_Prime_Tests: theory HOL-Algebra.Exact_Sequence
CryptHOL: theory Landau_Symbols.Landau_Simprocs
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gromov_Hyperbolicity
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
Probabilistic_Prime_Tests: theory HOL-Algebra.Embedded_Algebras
Probabilistic_Prime_Tests: theory HOL-Algebra.Free_Abelian_Groups
Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Rings
HOL-ODE-Numerics: theory Collections.HashCode
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Axioms
CryptHOL: theory Landau_Symbols.Landau_More
Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Fields
HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Frechet_Correctness
CryptHOL: theory CryptHOL.Negligible
HOL-ODE-Numerics: theory Collections.Intf_Hash
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Quadratic_Reciprocity
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Static_Semantics
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Pocklington
HOL-ODE-Numerics: theory Deriving.Hash_Generator
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residue_Primitive_Roots
HOL-ODE-Numerics: theory Collections.Gen_Hash
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Number_Theory
HOL-ODE-Numerics: theory Deriving.Hash_Instances
HOL-ODE-Numerics: theory Deriving.Derive
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Legendre_Symbol
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Coincidence
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Bound_Effect
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Axioms
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Uniform_Renaming
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Assert
HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Recursion
HOL-ODE-Numerics: theory Show.Show
HOL-ODE-Numerics: theory Refine_Monadic.RefineG_While
HOL-ODE-Numerics: theory HOL-Library.RBT
Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomials
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
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
HOL-ODE-Numerics: theory Show.Show_Instances
Timing Gromov_Hyperbolicity (4 threads, 140.698s elapsed time, 459.108s cpu time, 22.604s GC time, factor 3.26)
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:34 elapsed time, 0:08:01 cpu time, factor 3.11)
HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
Deep_Learning: theory Deep_Learning.Tensor
Deep_Learning: theory Deep_Learning.DL_Missing_Finite_Set
Deep_Learning: theory HOL-Computational_Algebra.Fraction_Field
Deep_Learning: theory HOL-Library.Fun_Lexorder
Deep_Learning: theory HOL-Algebra.Congruence
Deep_Learning: theory HOL-Library.Groups_Big_Fun
Deep_Learning: theory HOL-Library.More_List
Deep_Learning: theory Deep_Learning.Tensor_Subtensor
Deep_Learning: theory Deep_Learning.Tensor_Plus
Deep_Learning: theory HOL-Library.Poly_Mapping
Deep_Learning: theory Deep_Learning.Tensor_Scalar_Mult
Deep_Learning: theory Deep_Learning.Tensor_Product
Deep_Learning: theory Deep_Learning.Tensor_Unit_Vec
Deep_Learning: theory HOL-Algebra.Order
Deep_Learning: theory Deep_Learning.Tensor_Rank
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
Deep_Learning: theory Jordan_Normal_Form.Conjugate
Deep_Learning: theory HOL-Computational_Algebra.Normalized_Fraction
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Pfun
HOL-ODE-Numerics: theory Refine_Monadic.Refine_More_Comb
HOL-ODE-Numerics: theory Refine_Monadic.Refine_While
Deep_Learning: theory Polynomial_Interpolation.Missing_Unsorted
Deep_Learning: theory HOL-Algebra.Lattice
CryptHOL: theory CryptHOL.Misc_CryptHOL
Deep_Learning: theory Polynomials.MPoly_Type
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
Deep_Learning: theory Polynomials.More_MPoly_Type
Deep_Learning: theory HOL-Algebra.Complete_Lattice
Deep_Learning: theory HOL-Computational_Algebra.Polynomial
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
Deep_Learning: theory HOL-Algebra.Group
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst_Lemma
Deep_Learning: theory VectorSpace.FunctionLemmas
HOL-ODE-Numerics: theory Collections.Gen_Iterator
HOL-ODE-Numerics: theory Collections.Intf_Map
Deep_Learning: theory HOL-Algebra.Coset
Deep_Learning: theory HOL-Algebra.FiniteProduct
HOL-ODE-Numerics: theory Collections.Intf_Set
HOL-ODE-Numerics: theory Collections.Iterator
HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
Deep_Learning: theory HOL-Algebra.Ring
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
CryptHOL: theory CryptHOL.Generat
CryptHOL: theory CryptHOL.List_Bits
HOL-ODE-Numerics: theory Collections.Impl_List_Map
CryptHOL: theory CryptHOL.Resumption
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Proof_Checker
HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
HOL-ODE-Numerics: theory Collections.Gen_Set
HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
Timing Dirichlet_Series (4 threads, 239.722s elapsed time, 798.180s cpu time, 60.904s 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:26 elapsed time, 0:15:57 cpu time, factor 2.93)
HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
Timing HOL-Homology (4 threads, 137.923s elapsed time, 469.428s cpu time, 34.724s GC time, factor 3.40)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Homology
Density_Compiler: theory Density_Compiler.Density_Predicates
CryptHOL: theory CryptHOL.Generative_Probabilistic_Value
HOL-ODE-Numerics: theory Collections.Impl_List_Set
Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomial_Divisibility
Density_Compiler: theory Density_Compiler.PDF_Transformations
Density_Compiler: theory Density_Compiler.PDF_Values
HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
Deep_Learning: theory HOL-Algebra.Module
Deep_Learning: theory Jordan_Normal_Form.Missing_Ring
Timing Affine_Arithmetic (4 threads, 330.483s elapsed time, 1146.092s cpu time, 97.836s GC time, factor 3.47)
Deep_Learning: theory Polynomials.MPoly_Type_Univariate
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Affine_Arithmetic
Deep_Learning: theory HOL-Computational_Algebra.Polynomial_Factorial
Deep_Learning: theory Deep_Learning.Lebesgue_Zero_Set
Timing Echelon_Form (4 threads, 332.162s elapsed time, 1090.492s cpu time, 118.776s GC time, factor 3.28)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Echelon_Form
Deep_Learning: theory VectorSpace.RingModuleFacts
Density_Compiler: theory Density_Compiler.PDF_Semantics
Deep_Learning: theory VectorSpace.MonoidSums
Deep_Learning: theory VectorSpace.LinearCombinations
Deep_Learning: theory Jordan_Normal_Form.Missing_Permutations
Deep_Learning: theory Jordan_Normal_Form.Matrix
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
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
Timing Markov_Models (4 threads, 82.423s elapsed time, 291.000s cpu time, 18.068s GC time, factor 3.53)
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:23 elapsed time, 0:06:43 cpu time, factor 2.81)
Timing HOL-Homology (4 threads, 137.923s elapsed time, 469.428s cpu time, 34.724s GC time, factor 3.40)
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:28 elapsed time, 0:08:06 cpu time, factor 3.27)
Running Stochastic_Matrices ...
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_Timed_Automata: theory Probabilistic_Timed_Automata.Instantiate_Existentials
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence
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
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.More_List
Stochastic_Matrices: theory HOL-Library.More_List
Probabilistic_Timed_Automata: theory Timed_Automata.Floyd_Warshall
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
Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat
HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets
Probabilistic_Timed_Automata: theory Timed_Automata.Timed_Automata
Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach_Tools
Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Finiteness
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence_LTL
Deep_Learning: theory VectorSpace.SumSpaces
Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint
Stochastic_Matrices: theory HOL-Algebra.Order
Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted
Deep_Learning: theory Deep_Learning.DL_Concrete_Matrices
Deep_Learning: theory Deep_Learning.DL_Flatten_Matrix
Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction
Deep_Learning: theory Deep_Learning.DL_Network
Deep_Learning: theory Deep_Learning.Tensor_Matricization
Deep_Learning: theory Jordan_Normal_Form.DL_Submatrix
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Stream_More
Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial
Stochastic_Matrices: theory HOL-Algebra.Lattice
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Graphs
HOL-ODE-Numerics: theory Affine_Arithmetic.Print
Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom
Density_Compiler: theory Density_Compiler.PDF_Density_Contexts
Density_Compiler: theory Density_Compiler.PDF_Target_Semantics
CryptHOL: theory CryptHOL.Computational_Model
CryptHOL: theory CryptHOL.GPV_Applicative
CryptHOL: theory CryptHOL.GPV_Expectation
Deep_Learning: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice
CryptHOL: theory CryptHOL.GPV_Bisim
Density_Compiler: theory Density_Compiler.PDF_Compiler_Pred
Probabilistic_Timed_Automata: theory Timed_Automata.DBM
Stochastic_Matrices: theory HOL-Algebra.Group
Probabilistic_Timed_Automata: theory Timed_Automata.Paths_Cycles
Deep_Learning: theory VectorSpace.VectorSpace
CryptHOL: theory CryptHOL.CryptHOL
Deep_Learning: theory Jordan_Normal_Form.Column_Operations
Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order
Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type
Probabilistic_Timed_Automata: theory Timed_Automata.Regions
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
Density_Compiler: theory Density_Compiler.PDF_Target_Density_Contexts
Stochastic_Matrices: theory VectorSpace.FunctionLemmas
Stochastic_Matrices: theory HOL-Algebra.Coset
Stochastic_Matrices: theory HOL-Algebra.FiniteProduct
Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Basics
Deep_Learning: theory Deep_Learning.DL_Shallow_Model
Density_Compiler: theory Density_Compiler.PDF_Compiler
Stochastic_Matrices: theory HOL-Algebra.Ring
Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Normalization
Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous
Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Operations
HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
Probabilistic_Timed_Automata: theory Timed_Automata.Closure
Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics
Probabilistic_Timed_Automata: theory Timed_Automata.Regions_Beta
Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Deep_Learning: theory Jordan_Normal_Form.Missing_VectorSpace
Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial
Stochastic_Matrices: theory HOL-Algebra.Module
Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring
Probabilistic_Timed_Automata: theory Timed_Automata.Approx_Beta
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-Algebra.Finite_Extensions
Deep_Learning: theory Jordan_Normal_Form.Determinant
Probabilistic_Prime_Tests: theory HOL-Algebra.Indexed_Polynomials
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Dynamic_Logic
Stochastic_Matrices: theory VectorSpace.RingModuleFacts
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Lib
Stochastic_Matrices: theory VectorSpace.MonoidSums
Stochastic_Matrices: theory VectorSpace.LinearCombinations
Deep_Learning: theory Deep_Learning.DL_Deep_Model
Deep_Learning: theory Jordan_Normal_Form.VS_Connect
Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Permutations
Stochastic_Matrices: theory Jordan_Normal_Form.Matrix
Deep_Learning: theory Deep_Learning.DL_Deep_Model_Poly
Stochastic_Matrices: theory VectorSpace.SumSpaces
Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
Stochastic_Matrices: theory VectorSpace.VectorSpace
Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations
Probabilistic_Prime_Tests: theory HOL-Algebra.Algebraic_Closure
Deep_Learning: theory Jordan_Normal_Form.DL_Rank
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
Timing Echelon_Form (4 threads, 332.162s elapsed time, 1090.492s cpu time, 118.776s GC time, factor 3.28)
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:22 elapsed time, 0:19:37 cpu time, factor 3.08)
Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace
Stirling_Formula: theory HOL-Computational_Algebra.Squarefree
Stirling_Formula: theory HOL-Computational_Algebra.Group_Closure
Stirling_Formula: theory HOL-Computational_Algebra.Nth_Powers
Stirling_Formula: theory HOL-Computational_Algebra.Fraction_Field
Stirling_Formula: theory HOL-Number_Theory.Cong
Stirling_Formula: theory HOL-Algebra.Congruence
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
Stirling_Formula: theory HOL-Library.Function_Algebras
Stirling_Formula: theory HOL-Library.More_List
Stirling_Formula: theory HOL-Library.Power_By_Squaring
Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank
Stirling_Formula: theory HOL-Algebra.Order
Stirling_Formula: theory HOL-Computational_Algebra.Normalized_Fraction
Deep_Learning: theory Jordan_Normal_Form.DL_Rank_Submatrix
Stirling_Formula: theory HOL-Library.Stirling
Stirling_Formula: theory HOL-Number_Theory.Mod_Exp
Probabilistic_Prime_Tests: theory HOL-Algebra.Algebra
Stirling_Formula: theory HOL-Number_Theory.Eratosthenes
Timing CryptHOL (4 threads, 103.178s elapsed time, 370.364s cpu time, 24.548s GC time, factor 3.59)
Stirling_Formula: theory Bernoulli.Bernoulli
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/CryptHOL
Stirling_Formula: theory HOL-Computational_Algebra.Polynomial
Stirling_Formula: theory HOL-Library.Landau_Symbols
Stirling_Formula: theory Bernoulli.Periodic_Bernpoly
Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial
Stochastic_Matrices: theory Jordan_Normal_Form.Determinant
Stirling_Formula: theory HOL-Algebra.Lattice
Stirling_Formula: theory HOL-Number_Theory.Fib
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
Stirling_Formula: theory HOL-Number_Theory.Prime_Powers
Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity
Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial
Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly
Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
Stirling_Formula: theory HOL-Algebra.Complete_Lattice
Stirling_Formula: theory HOL-Number_Theory.Totient
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
Stirling_Formula: theory HOL-Algebra.Group
Stirling_Formula: theory Landau_Symbols.Group_Sort
Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Generalized_Primality_Test
Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly
Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity
Stirling_Formula: theory Landau_Symbols.Landau_Real_Products
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Residues_Nat
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Jacobi_Symbol
Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form
Stirling_Formula: theory HOL-Algebra.Coset
Stirling_Formula: theory HOL-Algebra.FiniteProduct
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Carmichael_Numbers
HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
Stirling_Formula: theory HOL-Algebra.Ring
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
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Solovay_Strassen_Test
Stirling_Formula: theory HOL-Algebra.Generated_Groups
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Test
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Miller_Rabin_Test
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
Stirling_Formula: theory Landau_Symbols.Landau_Simprocs
Stirling_Formula: theory Landau_Symbols.Landau_More
Stirling_Formula: theory Stirling_Formula.Stirling_Formula
Stirling_Formula: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Stirling_Formula: theory HOL-Computational_Algebra.Polynomial_FPS
Stirling_Formula: theory HOL-Computational_Algebra.Polynomial_Factorial
Stirling_Formula: theory HOL-Algebra.AbelCoset
Stirling_Formula: theory HOL-Algebra.Module
Stirling_Formula: theory HOL-Computational_Algebra.Formal_Laurent_Series
Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt
Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel
Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition
Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
Stirling_Formula: theory HOL-Algebra.Ideal
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.Jordan_Normal_Form_Existence
Stirling_Formula: theory HOL-Algebra.RingHom
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
Stirling_Formula: theory HOL-Algebra.UnivPoly
Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius
Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect
Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux
Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
Stirling_Formula: theory HOL-Computational_Algebra.Computational_Algebra
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
Stirling_Formula: theory HOL-Algebra.Multiplicative_Group
Stirling_Formula: theory HOL-Number_Theory.Residues
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
Stirling_Formula: theory HOL-Number_Theory.Euler_Criterion
Stirling_Formula: theory HOL-Number_Theory.Pocklington
Stirling_Formula: theory HOL-Number_Theory.Gauss
Timing Affine_Arithmetic (4 threads, 330.483s elapsed time, 1146.092s cpu time, 97.836s GC time, factor 3.47)
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:07:13 elapsed time, 0:23:09 cpu time, factor 3.21)
Stirling_Formula: theory HOL-Number_Theory.Quadratic_Reciprocity
Stirling_Formula: theory HOL-Number_Theory.Residue_Primitive_Roots
Stirling_Formula: theory HOL-Number_Theory.Number_Theory
Euler_MacLaurin: theory HOL-Computational_Algebra.Fraction_Field
Euler_MacLaurin: theory HOL-Computational_Algebra.Nth_Powers
Euler_MacLaurin: theory HOL-Computational_Algebra.Squarefree
Euler_MacLaurin: theory HOL-Computational_Algebra.Group_Closure
Euler_MacLaurin: theory HOL-Number_Theory.Cong
Euler_MacLaurin: theory HOL-Algebra.Congruence
Stirling_Formula: theory Bernoulli.Bernoulli_FPS
Euler_MacLaurin: theory HOL-Library.Function_Algebras
Euler_MacLaurin: theory HOL-Library.More_List
Euler_MacLaurin: theory HOL-Computational_Algebra.Normalized_Fraction
Euler_MacLaurin: theory HOL-Library.Power_By_Squaring
Euler_MacLaurin: theory HOL-Algebra.Order
Euler_MacLaurin: theory HOL-Library.Stirling
Euler_MacLaurin: theory HOL-Number_Theory.Mod_Exp
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
Euler_MacLaurin: theory HOL-Number_Theory.Eratosthenes
Euler_MacLaurin: theory Bernoulli.Bernoulli
Euler_MacLaurin: theory HOL-Computational_Algebra.Polynomial
Euler_MacLaurin: theory HOL-Library.Landau_Symbols
Euler_MacLaurin: theory Bernoulli.Periodic_Bernpoly
Euler_MacLaurin: theory HOL-Number_Theory.Fib
Euler_MacLaurin: theory HOL-Algebra.Lattice
Stirling_Formula: theory Stirling_Formula.Ln_Gamma_Asymptotics
Euler_MacLaurin: theory HOL-Number_Theory.Prime_Powers
Euler_MacLaurin: theory HOL-Algebra.Complete_Lattice
Euler_MacLaurin: theory HOL-Number_Theory.Totient
Euler_MacLaurin: theory Landau_Symbols.Group_Sort
Euler_MacLaurin: theory HOL-Algebra.Group
Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products
Euler_MacLaurin: theory HOL-Algebra.Coset
Euler_MacLaurin: theory HOL-Algebra.FiniteProduct
Euler_MacLaurin: theory HOL-Algebra.Ring
Euler_MacLaurin: theory HOL-Algebra.Generated_Groups
Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs
Euler_MacLaurin: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Euler_MacLaurin: theory HOL-Computational_Algebra.Polynomial_FPS
Euler_MacLaurin: theory HOL-Computational_Algebra.Polynomial_Factorial
Euler_MacLaurin: theory Landau_Symbols.Landau_More
Euler_MacLaurin: theory HOL-Computational_Algebra.Formal_Laurent_Series
Timing CryptHOL (4 threads, 103.178s elapsed time, 370.364s cpu time, 24.548s GC time, factor 3.59)
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:48 elapsed time, 0:08:18 cpu time, factor 2.96)
Building Game_Based_Crypto ...
Euler_MacLaurin: theory HOL-Algebra.AbelCoset
Timing Density_Compiler (4 threads, 124.509s elapsed time, 273.480s cpu time, 4.616s GC time, factor 2.20)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Density_Compiler
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
Game_Based_Crypto: theory Game_Based_Crypto.PRF_UHF
Euler_MacLaurin: theory HOL-Algebra.Module
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
Game_Based_Crypto: theory Game_Based_Crypto.Elgamal
Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA
Euler_MacLaurin: theory HOL-Algebra.Ideal
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
Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal
Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA
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
Euler_MacLaurin: theory HOL-Algebra.RingHom
Timing Density_Compiler (4 threads, 124.509s elapsed time, 273.480s cpu time, 4.616s GC time, factor 2.20)
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:15 elapsed time, 0:04:51 cpu time, factor 2.16)
Running Constructive_Cryptography ...
Euler_MacLaurin: theory HOL-Algebra.UnivPoly
Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec
Constructive_Cryptography: theory Constructive_Cryptography.More_CryptHOL
Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions
Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto
Constructive_Cryptography: theory Constructive_Cryptography.Resource
Constructive_Cryptography: theory Constructive_Cryptography.Converter
Euler_MacLaurin: theory HOL-Algebra.Multiplicative_Group
Euler_MacLaurin: theory HOL-Computational_Algebra.Computational_Algebra
Euler_MacLaurin: theory HOL-Number_Theory.Residues
Constructive_Cryptography: theory Constructive_Cryptography.Converter_Rewrite
Constructive_Cryptography: theory Constructive_Cryptography.Random_System
Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher
Timing Game_Based_Crypto (4 threads, 33.937s elapsed time, 121.508s cpu time, 3.140s GC time, factor 3.58)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Game_Based_Crypto
Euler_MacLaurin: theory HOL-Number_Theory.Euler_Criterion
Euler_MacLaurin: theory HOL-Number_Theory.Pocklington
Constructive_Cryptography: theory Constructive_Cryptography.Wiring
Euler_MacLaurin: theory HOL-Number_Theory.Gauss
Euler_MacLaurin: theory HOL-Number_Theory.Residue_Primitive_Roots
Euler_MacLaurin: theory HOL-Number_Theory.Quadratic_Reciprocity
Euler_MacLaurin: theory HOL-Number_Theory.Number_Theory
Euler_MacLaurin: theory Bernoulli.Bernoulli_FPS
Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography
Timing Probabilistic_Prime_Tests (4 threads, 246.103s elapsed time, 930.016s cpu time, 99.596s GC time, factor 3.78)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Prime_Tests
Constructive_Cryptography: theory Constructive_Cryptography.System_Construction
Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
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
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
Timing Probabilistic_Prime_Tests (4 threads, 246.103s elapsed time, 930.016s cpu time, 99.596s GC time, factor 3.78)
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:12 elapsed time, 0:15:42 cpu time, factor 3.73)
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA
Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
Zeta_Function: theory Bernoulli.Bernoulli_Zeta
Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code
Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad
Timing Deep_Learning (4 threads, 188.864s elapsed time, 644.588s cpu time, 42.040s GC time, factor 3.41)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Deep_Learning
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_ScaleR2
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
Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel
Zeta_Function: theory Winding_Number_Eval.Missing_Analysis
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
Zeta_Function: theory HOL-Eisbach.Eisbach_Tools
Constructive_Cryptography: theory Constructive_Cryptography.Examples
Timing Deep_Learning (4 threads, 188.864s elapsed time, 644.588s cpu time, 42.040s GC time, factor 3.41)
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:16 elapsed time, 0:10:59 cpu time, factor 3.35)
Zeta_Function: theory Sturm_Tarski.Sturm_Tarski
Hermite: theory Hermite.Hermite
Zeta_Function: theory Budan_Fourier.BF_Misc
Zeta_Function: theory Winding_Number_Eval.Missing_Algebraic
Zeta_Function: theory Winding_Number_Eval.Missing_Transcendental
Zeta_Function: theory Winding_Number_Eval.Cauchy_Index_Theorem
Hermite: theory Hermite.Hermite_IArrays
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA_Reachability
Zeta_Function: theory Winding_Number_Eval.Winding_Number_Eval
Zeta_Function: theory Zeta_Function.Zeta_Function
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
Timing Stirling_Formula (4 threads, 146.166s elapsed time, 480.900s cpu time, 27.992s GC time, factor 3.29)
Timing Game_Based_Crypto (4 threads, 33.937s elapsed time, 121.508s cpu time, 3.140s GC time, factor 3.58)
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:17 elapsed time, 0:03:16 cpu time, factor 2.52)
Running Multi_Party_Computation ...
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
Timing Differential_Dynamic_Logic (4 threads, 254.538s elapsed time, 557.520s cpu time, 33.128s GC time, factor 2.19)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Dynamic_Logic
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
Multi_Party_Computation: theory Multi_Party_Computation.Malicious_Defs
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
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
Multi_Party_Computation: theory Multi_Party_Computation.Uniform_Sampling
Multi_Party_Computation: theory HOL-Number_Theory.Totient
Multi_Party_Computation: theory Multi_Party_Computation.Cyclic_Group_Ext
Multi_Party_Computation: theory Multi_Party_Computation.ETP_OT
Multi_Party_Computation: theory Multi_Party_Computation.DH_Ext
Multi_Party_Computation: theory Multi_Party_Computation.Noar_Pinkas_OT
Multi_Party_Computation: theory Multi_Party_Computation.OT14
Multi_Party_Computation: theory HOL-Algebra.AbelCoset
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
Multi_Party_Computation: theory HOL-Algebra.Module
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 Probabilistic_Timed_Automata (4 threads, 202.364s elapsed time, 595.112s cpu time, 25.928s GC time, factor 2.94)
Multi_Party_Computation: theory Multi_Party_Computation.GMW
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Timed_Automata
Timing Differential_Dynamic_Logic (4 threads, 254.538s elapsed time, 557.520s cpu time, 33.128s GC time, factor 2.19)
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:27 elapsed time, 0:09:39 cpu time, factor 2.16)
Multi_Party_Computation: theory Multi_Party_Computation.Secure_Multiplication
Multi_Party_Computation: theory HOL-Algebra.Ideal
Bernoulli: theory HOL-Computational_Algebra.Fraction_Field
Bernoulli: theory HOL-Computational_Algebra.Group_Closure
Bernoulli: theory HOL-Computational_Algebra.Nth_Powers
Bernoulli: theory HOL-Computational_Algebra.Squarefree
Bernoulli: theory HOL-Number_Theory.Cong
Bernoulli: theory HOL-Algebra.Congruence
Bernoulli: theory HOL-Library.More_List
Multi_Party_Computation: theory HOL-Algebra.RingHom
Bernoulli: theory HOL-Library.Power_By_Squaring
Bernoulli: theory HOL-Algebra.Order
Bernoulli: theory HOL-Library.Stirling
Bernoulli: theory HOL-Computational_Algebra.Normalized_Fraction
Bernoulli: theory HOL-Number_Theory.Mod_Exp
Bernoulli: theory HOL-Number_Theory.Eratosthenes
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
Bernoulli: theory Bernoulli.Bernoulli
Bernoulli: theory HOL-Computational_Algebra.Polynomial
Bernoulli: theory HOL-Number_Theory.Fib
Multi_Party_Computation: theory HOL-Algebra.UnivPoly
Bernoulli: theory Bernoulli.Periodic_Bernpoly
Timing Probabilistic_Timed_Automata (4 threads, 202.364s elapsed time, 595.112s cpu time, 25.928s GC time, factor 2.94)
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:31 elapsed time, 0:10:11 cpu time, factor 2.89)
Bernoulli: theory HOL-Number_Theory.Prime_Powers
Bernoulli: theory HOL-Number_Theory.Totient
Bernoulli: theory HOL-Algebra.Lattice
Bernoulli: theory HOL-Algebra.Complete_Lattice
Taylor_Models: theory HOL-Decision_Procs.Rat_Pair
Taylor_Models: theory HOL-Decision_Procs.Polynomial_List
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
Bernoulli: theory HOL-Algebra.Group
Bernoulli: theory HOL-Algebra.Coset
Bernoulli: theory HOL-Algebra.FiniteProduct
Bernoulli: theory HOL-Algebra.Ring
Bernoulli: theory HOL-Algebra.Generated_Groups
Bernoulli: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Bernoulli: theory HOL-Computational_Algebra.Polynomial_FPS
Bernoulli: theory HOL-Computational_Algebra.Polynomial_Factorial
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
Bernoulli: theory HOL-Computational_Algebra.Formal_Laurent_Series
Timing Zeta_Function (4 threads, 61.676s elapsed time, 190.324s cpu time, 4.708s GC time, factor 3.09)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Zeta_Function
Multi_Party_Computation: theory HOL-Algebra.Multiplicative_Group
Bernoulli: theory HOL-Algebra.AbelCoset
Bernoulli: theory HOL-Algebra.Module
Multi_Party_Computation: theory HOL-Number_Theory.Residues
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
Bernoulli: theory HOL-Algebra.Ideal
Taylor_Models: theory Taylor_Models.Polynomial_Expression
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
Bernoulli: theory HOL-Algebra.RingHom
Bernoulli: theory HOL-Algebra.UnivPoly
Timing Euler_MacLaurin (4 threads, 145.838s elapsed time, 489.180s cpu time, 28.092s GC time, factor 3.35)
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
Timing Constructive_Cryptography (4 threads, 118.929s elapsed time, 393.040s cpu time, 5.896s GC time, factor 3.30)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Constructive_Cryptography
Timing Stirling_Formula (4 threads, 146.166s elapsed time, 480.900s cpu time, 27.992s GC time, factor 3.29)
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:03:20 elapsed time, 0:09:39 cpu time, factor 2.88)
Timing Euler_MacLaurin (4 threads, 145.838s elapsed time, 489.180s cpu time, 28.092s GC time, factor 3.35)
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:02:31 elapsed time, 0:08:20 cpu time, factor 3.30)
Bernoulli: theory HOL-Computational_Algebra.Computational_Algebra
Bernoulli: theory HOL-Algebra.Multiplicative_Group
List_Update: theory HOL-Library.While_Combinator
List_Update: theory List_Update.Prob_Theory
List_Update: theory List_Update.On_Off
List_Update: theory List_Update.Bit_Strings
List_Update: theory List-Index.List_Index
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
List_Update: theory Regular-Sets.Regular_Set
Gauss_Jordan: theory HOL-Library.Code_Target_Numeral
List_Update: theory List_Update.Inversion
List_Update: theory List_Update.Swaps
Gauss_Jordan: theory Rank_Nullity_Theorem.Dual_Order
List_Update: theory List_Update.Competitive_Analysis
Gauss_Jordan: theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell
Gauss_Jordan: theory Rank_Nullity_Theorem.Mod_Type
Gauss_Jordan: theory Gauss_Jordan.Code_Z2
Gauss_Jordan: theory Gauss_Jordan.IArray_Addenda
List_Update: theory List_Update.Move_to_Front
Bernoulli: theory HOL-Number_Theory.Residues
List_Update: theory Regular-Sets.Regular_Exp
Gauss_Jordan: theory Rank_Nullity_Theorem.Miscellaneous
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
Bernoulli: theory HOL-Number_Theory.Euler_Criterion
Bernoulli: theory HOL-Number_Theory.Pocklington
Timing Constructive_Cryptography (4 threads, 118.929s elapsed time, 393.040s cpu time, 5.896s GC time, factor 3.30)
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:09 elapsed time, 0:06:51 cpu time, factor 3.18)
Running Winding_Number_Eval ...
Bernoulli: theory HOL-Number_Theory.Gauss
Bernoulli: theory HOL-Number_Theory.Quadratic_Reciprocity
Bernoulli: theory HOL-Number_Theory.Residue_Primitive_Roots
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
Bernoulli: theory HOL-Number_Theory.Number_Theory
Gauss_Jordan: theory Gauss_Jordan.Rank
Gauss_Jordan: theory Gauss_Jordan.Elementary_Operations
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
Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial
Gauss_Jordan: theory Gauss_Jordan.Matrix_To_IArray
List_Update: theory Regular-Sets.NDerivative
Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan
Winding_Number_Eval: theory HOL-Eisbach.Eisbach_Tools
Winding_Number_Eval: theory Winding_Number_Eval.Missing_Topology
List_Update: theory List_Update.MTF2_Effects
Bernoulli: theory Bernoulli.Bernoulli_FPS
List_Update: theory List_Update.Partial_Cost_Model
List_Update: theory List_Update.BIT
Winding_Number_Eval: theory Winding_Number_Eval.Missing_Analysis
Taylor_Models: theory HOL-Library.Function_Algebras
Taylor_Models: theory Taylor_Models.Horner_Eval
Taylor_Models: theory Taylor_Models.Float_Topology
Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional
Winding_Number_Eval: theory HOL-Computational_Algebra.Normalized_Fraction
Taylor_Models: theory Taylor_Models.Taylor_Models_Misc
List_Update: theory List_Update.List_Factoring
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_IArrays
Gauss_Jordan: theory Gauss_Jordan.Linear_Maps
Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_PA
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
Bernoulli: theory Bernoulli.Bernoulli_Zeta
Gauss_Jordan: theory Gauss_Jordan.System_Of_Equations
Gauss_Jordan: theory Gauss_Jordan.Determinants_IArrays
Taylor_Models: theory Taylor_Models.Taylor_Models
Gauss_Jordan: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces_IArrays
Gauss_Jordan: theory Gauss_Jordan.Inverse_IArrays
Timing Zeta_Function (4 threads, 61.676s elapsed time, 190.324s cpu time, 4.708s GC time, factor 3.09)
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:42 elapsed time, 0:04:18 cpu time, factor 2.53)
Gauss_Jordan: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
List_Update: theory Regular-Sets.Equivalence_Checking
Gauss_Jordan: theory Gauss_Jordan.System_Of_Equations_IArrays
List_Update: theory List_Update.RExp_Var
List_Update: theory List_Update.BIT_pairwise
Gauss_Jordan: theory Gauss_Jordan.Examples_Gauss_Jordan_IArrays
Girth_Chromatic: theory HOL-Library.Code_Abstract_Nat
Girth_Chromatic: theory HOL-Library.Code_Target_Int
Girth_Chromatic: theory HOL-Decision_Procs.Dense_Linear_Order
Girth_Chromatic: theory HOL-Library.Lattice_Algebras
Girth_Chromatic: theory HOL-Library.Code_Target_Nat
List_Update: theory List_Update.OPT2
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
List_Update: theory List_Update.Phase_Partitioning
Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays
List_Update: theory List_Update.BIT_2comp_on2
List_Update: theory List_Update.TS
Winding_Number_Eval: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays_SML
Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial_Factorial
Gauss_Jordan: theory Gauss_Jordan.Code_Rational
Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays_Haskell
List_Update: theory List_Update.Comb
Girth_Chromatic: theory HOL-Library.Interval
Girth_Chromatic: theory HOL-Library.Float
Girth_Chromatic: theory HOL-Library.Interval_Float
Girth_Chromatic: theory HOL-Decision_Procs.Approximation_Bounds
Timing Hermite (4 threads, 105.276s elapsed time, 236.772s cpu time, 14.444s GC time, factor 2.25)
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
Girth_Chromatic: theory HOL-Decision_Procs.Approximation
Timing Hermite (4 threads, 105.276s elapsed time, 236.772s cpu time, 14.444s GC time, factor 2.25)
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:52 elapsed time, 0:04:09 cpu time, factor 2.22)
Running Hidden_Markov_Models ...
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
Hidden_Markov_Models: theory Monad_Memo_DP.State_Heap_Misc
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
Winding_Number_Eval: theory Sturm_Tarski.PolyMisc
Winding_Number_Eval: theory Sturm_Tarski.Sturm_Tarski
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
Winding_Number_Eval: theory Budan_Fourier.BF_Misc
Taylor_Models: theory Taylor_Models.Experiments
Winding_Number_Eval: theory Winding_Number_Eval.Missing_Algebraic
Hidden_Markov_Models: theory Monad_Memo_DP.DP_CRelVH
Hidden_Markov_Models: theory Monad_Memo_DP.Transform_Cmd
Hidden_Markov_Models: theory Monad_Memo_DP.State_Main
Winding_Number_Eval: theory Winding_Number_Eval.Missing_Transcendental
Winding_Number_Eval: theory Winding_Number_Eval.Cauchy_Index_Theorem
Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval
Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval_Examples
Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix
Stochastic_Matrices: theory Stochastic_Matrices.Eigenspace
Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Vector_PMF
Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models
Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius
Timing Stochastic_Matrices (4 threads, 308.100s elapsed time, 843.956s cpu time, 49.296s GC time, factor 2.74)
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
Timing Stochastic_Matrices (4 threads, 308.100s elapsed time, 843.956s cpu time, 49.296s GC time, factor 2.74)
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:14 elapsed time, 0:14:16 cpu time, factor 2.72)
Running Sigma_Commit_Crypto ...
Timing Taylor_Models (4 threads, 104.123s elapsed time, 295.924s cpu time, 14.600s GC time, factor 2.84)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models
Sigma_Commit_Crypto: theory HOL-Number_Theory.Cong
Sigma_Commit_Crypto: theory HOL-Algebra.FiniteProduct
Sigma_Commit_Crypto: theory HOL-Algebra.Generated_Groups
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Xor
Sigma_Commit_Crypto: theory HOL-Algebra.Ring
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Commitment_Schemes
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_Protocols
Sigma_Commit_Crypto: theory HOL-Number_Theory.Totient
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Cyclic_Group_Ext
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Uniform_Sampling
Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation
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
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Discrete_Log
Timing Taylor_Models (4 threads, 104.123s elapsed time, 295.924s cpu time, 14.600s GC time, factor 2.84)
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:01:51 elapsed time, 0:05:09 cpu time, factor 2.78)
Running Differential_Game_Logic ...
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_AND
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Sigma_OR
Differential_Game_Logic: theory Differential_Game_Logic.Lib
Differential_Game_Logic: theory Differential_Game_Logic.Identifiers
Differential_Game_Logic: theory Differential_Game_Logic.Syntax
Sigma_Commit_Crypto: theory HOL-Algebra.AbelCoset
Sigma_Commit_Crypto: theory HOL-Algebra.Module
Timing Multi_Party_Computation (4 threads, 132.114s elapsed time, 486.612s cpu time, 13.824s GC time, factor 3.68)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Multi_Party_Computation
Sigma_Commit_Crypto: theory HOL-Algebra.Ideal
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
Differential_Game_Logic: theory Differential_Game_Logic.Ids
Differential_Game_Logic: theory Differential_Game_Logic.Denotational_Semantics
Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic
Sigma_Commit_Crypto: theory HOL-Algebra.RingHom
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
Sigma_Commit_Crypto: theory HOL-Algebra.UnivPoly
Timing Multi_Party_Computation (4 threads, 132.114s elapsed time, 486.612s cpu time, 13.824s GC time, factor 3.68)
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:21 elapsed time, 0:08:23 cpu time, factor 3.57)
Running Linear_Recurrences ...
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
Linear_Recurrences: theory HOL-Library.BNF_Corec
Linear_Recurrences: theory HOL-Computational_Algebra.Group_Closure
Linear_Recurrences: theory HOL-Computational_Algebra.Nth_Powers
Linear_Recurrences: theory HOL-Computational_Algebra.Squarefree
Linear_Recurrences: theory HOL-Library.Code_Abstract_Nat
Linear_Recurrences: theory HOL-Library.Code_Target_Nat
Linear_Recurrences: theory HOL-Library.Code_Target_Int
Differential_Game_Logic: theory Differential_Game_Logic.USubst
Linear_Recurrences: theory HOL-Library.Stirling
Linear_Recurrences: theory HOL-Library.Code_Target_Numeral
Linear_Recurrences: theory HOL-Library.Sublist
Linear_Recurrences: theory HOL-Real_Asymp.Inst_Existentials
Linear_Recurrences: theory Polynomial_Interpolation.Missing_Unsorted
Linear_Recurrences: theory HOL-Computational_Algebra.Polynomial_FPS
Linear_Recurrences: theory HOL-Computational_Algebra.Formal_Laurent_Series
Linear_Recurrences: theory HOL-Library.Landau_Symbols
Timing Girth_Chromatic (4 threads, 73.995s elapsed time, 190.684s cpu time, 12.744s GC time, factor 2.58)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic
Timing Gauss_Jordan (4 threads, 89.843s elapsed time, 323.496s cpu time, 7.160s GC time, factor 3.60)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Gauss_Jordan
Linear_Recurrences: theory Polynomial_Interpolation.Missing_Polynomial
Timing Bernoulli (4 threads, 131.883s elapsed time, 428.740s cpu time, 28.452s GC time, factor 3.25)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli
Linear_Recurrences: theory Polynomial_Factorization.Order_Polynomial
Linear_Recurrences: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
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
Differential_Game_Logic: theory Differential_Game_Logic.Differential_Game_Logic
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
Linear_Recurrences: theory Matrix.Utility
Linear_Recurrences: theory HOL-Computational_Algebra.Computational_Algebra
Linear_Recurrences: theory Polynomial_Interpolation.Ring_Hom
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
Timing List_Update (4 threads, 95.383s elapsed time, 288.416s cpu time, 15.828s GC time, factor 3.02)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/List_Update
Linear_Recurrences: theory Linear_Recurrences.Eulerian_Polynomials
Timing Winding_Number_Eval (4 threads, 88.207s elapsed time, 225.616s cpu time, 6.224s GC time, factor 2.56)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Winding_Number_Eval
Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Common
Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Misc
Linear_Recurrences: theory HOL-Real_Asymp.Multiseries_Expansion
Linear_Recurrences: theory Linear_Recurrences.RatFPS
Linear_Recurrences: theory Linear_Recurrences.Factorizations
Timing Bernoulli (4 threads, 131.883s elapsed time, 428.740s cpu time, 28.452s GC time, factor 3.25)
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:02:18 elapsed time, 0:07:21 cpu time, factor 3.18)
Running Prime_Harmonic_Series ...
Linear_Recurrences: theory Linear_Recurrences.Partial_Fraction_Decomposition
Prime_Harmonic_Series: theory HOL-Algebra.Congruence
Prime_Harmonic_Series: theory HOL-Library.Power_By_Squaring
Prime_Harmonic_Series: theory HOL-Number_Theory.Cong
Prime_Harmonic_Series: theory HOL-Number_Theory.Eratosthenes
Linear_Recurrences: theory Polynomial_Interpolation.Ring_Hom_Poly
Sigma_Commit_Crypto: theory HOL-Algebra.Multiplicative_Group
Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Solver
Prime_Harmonic_Series: theory HOL-Number_Theory.Fib
Prime_Harmonic_Series: theory HOL-Number_Theory.Prime_Powers
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
Timing Gauss_Jordan (4 threads, 89.843s elapsed time, 323.496s cpu time, 7.160s GC time, factor 3.60)
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:40 elapsed time, 0:05:42 cpu time, factor 3.41)
Prime_Harmonic_Series: theory HOL-Algebra.Order
Linear_Recurrences: theory Linear_Recurrences.Linear_Homogenous_Recurrences
Prime_Harmonic_Series: theory HOL-Number_Theory.Mod_Exp
Linear_Recurrences: theory Polynomial_Factorization.Square_Free_Factorization
Prime_Harmonic_Series: theory HOL-Number_Theory.Totient
Prime_Harmonic_Series: theory HOL-Algebra.Lattice
Akra_Bazzi: theory HOL-Library.Code_Abstract_Nat
Akra_Bazzi: theory HOL-Library.Code_Target_Int
Akra_Bazzi: theory HOL-Decision_Procs.Dense_Linear_Order
Akra_Bazzi: theory HOL-Library.Function_Algebras
Akra_Bazzi: theory HOL-Library.Code_Target_Nat
Linear_Recurrences: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
Akra_Bazzi: theory Akra_Bazzi.Eval_Numeral
Akra_Bazzi: theory HOL-Library.Landau_Symbols
Akra_Bazzi: theory HOL-Library.Code_Target_Numeral
Akra_Bazzi: theory HOL-Library.Lattice_Algebras
Akra_Bazzi: theory HOL-Library.Log_Nat
Akra_Bazzi: theory Landau_Symbols.Group_Sort
Sigma_Commit_Crypto: theory HOL-Number_Theory.Residues
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
Prime_Harmonic_Series: theory HOL-Algebra.Complete_Lattice
Timing Winding_Number_Eval (4 threads, 88.207s elapsed time, 225.616s cpu time, 6.224s GC time, factor 2.56)
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:36 elapsed time, 0:04:00 cpu time, factor 2.48)
Prime_Harmonic_Series: theory HOL-Algebra.Group
Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Number_Theory_Aux
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Chaum_Pedersen_Sigma_Commit
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Okamoto_Sigma_Commit
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Pedersen
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Rivest
Akra_Bazzi: theory Landau_Symbols.Landau_Real_Products
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
Pi_Transcendental: theory HOL-Computational_Algebra.Group_Closure
Pi_Transcendental: theory HOL-Computational_Algebra.Fraction_Field
Pi_Transcendental: theory HOL-Library.BNF_Corec
Pi_Transcendental: theory HOL-Computational_Algebra.Nth_Powers
Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree
Prime_Harmonic_Series: theory HOL-Algebra.Coset
Prime_Harmonic_Series: theory HOL-Algebra.FiniteProduct
Timing List_Update (4 threads, 95.383s elapsed time, 288.416s cpu time, 15.828s GC time, factor 3.02)
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:47 elapsed time, 0:05:16 cpu time, factor 2.95)
Running Probabilistic_Noninterference ...
Pi_Transcendental: theory HOL-Library.Fun_Lexorder
Pi_Transcendental: theory HOL-Library.Groups_Big_Fun
Prime_Harmonic_Series: theory HOL-Algebra.Ring
Pi_Transcendental: theory HOL-Real_Asymp.Inst_Existentials
Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Pi_Transcendental: theory HOL-Library.Poly_Mapping
Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_FPS
Sigma_Commit_Crypto: theory Sigma_Commit_Crypto.Schnorr_Sigma_Commit
Pi_Transcendental: theory HOL-Computational_Algebra.Normalized_Fraction
Prime_Harmonic_Series: theory HOL-Algebra.Generated_Groups
Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_Factorial
Pi_Transcendental: theory HOL-Computational_Algebra.Formal_Laurent_Series
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 HOL-Library.Interval
Akra_Bazzi: theory HOL-Library.Float
Pi_Transcendental: theory Polynomials.MPoly_Type
Probabilistic_Noninterference: theory Coinductive.Coinductive_List
Akra_Bazzi: theory Landau_Symbols.Landau_Simprocs
Pi_Transcendental: theory Polynomials.More_MPoly_Type
Akra_Bazzi: theory Landau_Symbols.Landau_More
Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Library
Pi_Transcendental: theory HOL-Library.Landau_Symbols
Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Asymptotics
Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Real
Prime_Harmonic_Series: theory HOL-Algebra.AbelCoset
Akra_Bazzi: theory HOL-Library.Interval_Float
Prime_Harmonic_Series: theory HOL-Algebra.Module
Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi
Pi_Transcendental: theory HOL-Real_Asymp.Eventuallize
Pi_Transcendental: theory HOL-Real_Asymp.Lazy_Eval
Akra_Bazzi: theory HOL-Decision_Procs.Approximation_Bounds
Akra_Bazzi: theory Akra_Bazzi.Master_Theorem
Timing Hidden_Markov_Models (4 threads, 76.740s elapsed time, 139.608s cpu time, 17.776s GC time, factor 1.82)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Hidden_Markov_Models
Pi_Transcendental: theory HOL-Real_Asymp.Multiseries_Expansion
Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Method
Prime_Harmonic_Series: theory HOL-Algebra.Ideal
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
Probabilistic_Noninterference: theory Coinductive.Coinductive_Stream
Timing Hidden_Markov_Models (4 threads, 76.740s elapsed time, 139.608s cpu time, 17.776s GC time, factor 1.82)
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:23 elapsed time, 0:02:32 cpu time, factor 1.82)
Running Irrationality_J_Hancl ...
Akra_Bazzi: theory HOL-Decision_Procs.Approximation
Probabilistic_Noninterference: theory Markov_Models.Markov_Models_Auxiliary
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
Prime_Harmonic_Series: theory HOL-Algebra.RingHom
Probabilistic_Noninterference: theory Markov_Models.Discrete_Time_Markov_Chain
Prime_Harmonic_Series: theory HOL-Algebra.UnivPoly
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Interface
Irrationality_J_Hancl: theory HOL-Library.Interval
Irrationality_J_Hancl: theory HOL-Library.Float
Linear_Recurrences: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
Linear_Recurrences: theory HOL-Real_Asymp.Real_Asymp
Irrationality_J_Hancl: theory HOL-Library.Interval_Float
Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Asymptotics
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Language_Semantics
Timing Girth_Chromatic (4 threads, 73.995s elapsed time, 190.684s cpu time, 12.744s GC time, factor 2.58)
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:02:00 elapsed time, 0:04:30 cpu time, factor 2.25)
Irrationality_J_Hancl: theory HOL-Decision_Procs.Approximation_Bounds
Ergodic_Theory: theory Ergodic_Theory.Fekete
Ergodic_Theory: theory Ergodic_Theory.SG_Library_Complement
Ergodic_Theory: theory Ergodic_Theory.Kohlberg_Neyman_Karlsson
Ergodic_Theory: theory Ergodic_Theory.Asymptotic_Density
Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra
Ergodic_Theory: theory Ergodic_Theory.Measure_Preserving_Transformations
Prime_Harmonic_Series: theory HOL-Algebra.Multiplicative_Group
Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library
Pi_Transcendental: theory Symmetric_Polynomials.Vieta
Ergodic_Theory: theory Ergodic_Theory.Recurrence
Irrationality_J_Hancl: theory HOL-Decision_Procs.Approximation
Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Resumption_Based
Ergodic_Theory: theory Ergodic_Theory.Invariants
Ergodic_Theory: theory Ergodic_Theory.Transfer_Operator
Ergodic_Theory: theory Ergodic_Theory.Normalizing_Sequences
Ergodic_Theory: theory Ergodic_Theory.Ergodicity
Prime_Harmonic_Series: theory HOL-Number_Theory.Residues
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Compositionality
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Trace_Based
Ergodic_Theory: theory Ergodic_Theory.Kingman
Timing Sigma_Commit_Crypto (4 threads, 77.558s elapsed time, 274.368s cpu time, 11.068s GC time, factor 3.54)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Sigma_Commit_Crypto
Prime_Harmonic_Series: theory HOL-Number_Theory.Euler_Criterion
Prime_Harmonic_Series: theory HOL-Number_Theory.Gauss
Prime_Harmonic_Series: theory HOL-Number_Theory.Pocklington
Prime_Harmonic_Series: theory HOL-Number_Theory.Quadratic_Reciprocity
Prime_Harmonic_Series: theory HOL-Number_Theory.Residue_Primitive_Roots
Ergodic_Theory: theory Ergodic_Theory.Gouezel_Karlsson
Prime_Harmonic_Series: theory HOL-Number_Theory.Number_Theory
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Syntactic_Criteria
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
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Sigma_Commit_Crypto/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Sigma_Commit_Crypto/outline.pdf
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Concrete
Timing Sigma_Commit_Crypto (4 threads, 77.558s elapsed time, 274.368s cpu time, 11.068s GC time, factor 3.54)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Sigma_Commit_Crypto
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Sigma_Commit_Crypto/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Sigma_Commit_Crypto/outline.pdf
Finished Sigma_Commit_Crypto (0:01:26 elapsed time, 0:04:49 cpu time, factor 3.36)
Pi_Transcendental: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
Green: theory Green.General_Utils
Pi_Transcendental: theory HOL-Real_Asymp.Real_Asymp
Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental
Timing Differential_Game_Logic (4 threads, 84.420s elapsed time, 138.816s cpu time, 4.220s GC time, factor 1.64)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Differential_Game_Logic
Green: theory Green.SymmetricR2Shapes
Green: theory Green.CircExample
Green: theory Green.DiamExample
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
Timing Differential_Game_Logic (4 threads, 84.420s elapsed time, 138.816s cpu time, 4.220s GC time, factor 1.64)
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:32 elapsed time, 0:02:32 cpu time, factor 1.66)
Fourier: theory HOL-Library.BNF_Corec
Fourier: theory HOL-Real_Asymp.Inst_Existentials
Fourier: theory Fourier.Confine
Fourier: theory HOL-Library.Landau_Symbols
Fourier: theory Fourier.Fourier_Aux2
Fourier: theory Fourier.Periodic
Fourier: theory Ergodic_Theory.SG_Library_Complement
Fourier: theory HOL-Real_Asymp.Eventuallize
Fourier: theory HOL-Real_Asymp.Lazy_Eval
Timing Linear_Recurrences (4 threads, 83.238s elapsed time, 317.172s cpu time, 12.200s GC time, factor 3.81)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Recurrences
Fourier: theory Lp.Functional_Spaces
Fourier: theory Fourier.Lspace
Fourier: theory Fourier.Square_Integrable
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
Timing Linear_Recurrences (4 threads, 83.238s elapsed time, 317.172s cpu time, 12.200s GC time, factor 3.81)
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:29 cpu time, factor 3.67)
Building Applicative_Lifting ...
Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Approximation
Akra_Bazzi: theory Akra_Bazzi.Master_Theorem_Examples
Fourier: theory HOL-Real_Asymp.Multiseries_Expansion
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
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
Applicative_Lifting: theory Applicative_Lifting.Applicative_Sum
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
Applicative_Lifting: theory Applicative_Lifting.Applicative_Vector
Timing Prime_Harmonic_Series (4 threads, 83.931s elapsed time, 306.456s cpu time, 19.928s GC time, factor 3.65)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Harmonic_Series
Applicative_Lifting: theory Applicative_Lifting.Beta_Eta
Applicative_Lifting: theory Applicative_Lifting.Applicative_PMF
Applicative_Lifting: theory Applicative_Lifting.Combinators
Applicative_Lifting: theory Applicative_Lifting.Idiomatic_Terms
Timing Akra_Bazzi (4 threads, 82.142s elapsed time, 278.516s cpu time, 17.560s GC time, factor 3.39)
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/Prime_Harmonic_Series/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Harmonic_Series/outline.pdf
Applicative_Lifting: theory Applicative_Lifting.Applicative_Functor
Applicative_Lifting: theory Applicative_Lifting.Tree_Relabelling
Timing Prime_Harmonic_Series (4 threads, 83.931s elapsed time, 306.456s cpu time, 19.928s 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:29 elapsed time, 0:05:16 cpu time, factor 3.55)
Timing Pi_Transcendental (4 threads, 81.241s elapsed time, 263.220s cpu time, 16.864s GC time, factor 3.24)
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/Akra_Bazzi/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Akra_Bazzi/outline.pdf
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
Timing Akra_Bazzi (4 threads, 82.142s elapsed time, 278.516s cpu time, 17.560s GC time, factor 3.39)
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:29 elapsed time, 0:04:52 cpu time, factor 3.27)
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
Timing Probabilistic_Noninterference (4 threads, 82.196s elapsed time, 269.912s cpu time, 7.636s GC time, factor 3.28)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_Noninterference
Timing Pi_Transcendental (4 threads, 81.241s elapsed time, 263.220s cpu time, 16.864s GC time, factor 3.24)
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:27 elapsed time, 0:04:34 cpu time, factor 3.14)
DiscretePricing: theory DiscretePricing.Filtration
DiscretePricing: theory DiscretePricing.Generated_Subalgebra
Applicative_Lifting: theory Applicative_Lifting.Applicative_Examples
DiscretePricing: theory DiscretePricing.Disc_Cond_Expect
MFMC_Countable: theory Flow_Networks.Graph
MFMC_Countable: theory HOL-Library.Transitive_Closure_Table
MFMC_Countable: theory HOL-Library.While_Combinator
MFMC_Countable: theory HOL-Library.Bourbaki_Witt_Fixpoint
DiscretePricing: theory DiscretePricing.Martingale
DiscretePricing: theory DiscretePricing.Infinite_Coin_Toss_Space
Irrationality_J_Hancl: theory Irrationality_J_Hancl.Irrationality_J_Hancl
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-Library.Interval
Dirichlet_L: theory HOL-Library.Float
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 Probabilistic_Noninterference (4 threads, 82.196s elapsed time, 269.912s cpu time, 7.636s GC time, factor 3.28)
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:30 elapsed time, 0:04:52 cpu time, factor 3.22)
Building Randomised_Social_Choice ...
MFMC_Countable: theory Flow_Networks.Residual_Graph
Timing Irrationality_J_Hancl (4 threads, 76.414s elapsed time, 194.192s cpu time, 6.756s GC time, factor 2.54)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Irrationality_J_Hancl
MFMC_Countable: theory Flow_Networks.Augmenting_Flow
MFMC_Countable: theory Flow_Networks.Augmenting_Path
Dirichlet_L: theory HOL-Library.Interval_Float
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
MFMC_Countable: theory Flow_Networks.Ford_Fulkerson
Randomised_Social_Choice: theory Randomised_Social_Choice.Order_Predicates
MFMC_Countable: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds
DiscretePricing: theory DiscretePricing.Geometric_Random_Walk
MFMC_Countable: theory MFMC_Countable.MFMC_Finite
Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profiles
DiscretePricing: theory DiscretePricing.Fair_Price
Applicative_Lifting: theory Applicative_Lifting.Abstract_AF
MFMC_Countable: theory MFMC_Countable.Matrix_For_Marginals
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
Randomised_Social_Choice: theory Randomised_Social_Choice.Elections
Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profile_Cmd
Randomised_Social_Choice: theory Randomised_Social_Choice.Utility_Functions
Applicative_Lifting: theory Applicative_Lifting.Applicative_Test
MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation
Timing Irrationality_J_Hancl (4 threads, 76.414s elapsed time, 194.192s cpu time, 6.756s GC time, factor 2.54)
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:22 elapsed time, 0:03:26 cpu time, factor 2.49)
Building Prime_Distribution_Elementary ...
Randomised_Social_Choice: theory Randomised_Social_Choice.Stochastic_Dominance
Timing Applicative_Lifting (4 threads, 26.150s elapsed time, 75.852s cpu time, 4.108s GC time, factor 2.90)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Applicative_Lifting
Randomised_Social_Choice: theory Randomised_Social_Choice.SD_Efficiency
Randomised_Social_Choice: theory Randomised_Social_Choice.Social_Decision_Schemes
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
Dirichlet_L: theory Bertrands_Postulate.Bertrand
DiscretePricing: theory DiscretePricing.CRR_Model
Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions
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
Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Dictatorship
Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Automation
Randomised_Social_Choice: theory Randomised_Social_Choice.SDS_Lowering
Randomised_Social_Choice: theory Randomised_Social_Choice.Random_Serial_Dictatorship
Randomised_Social_Choice: theory Randomised_Social_Choice.Randomised_Social_Choice
Fourier: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
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
Timing Randomised_Social_Choice (4 threads, 14.460s elapsed time, 53.792s cpu time, 1.848s GC time, factor 3.72)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_Social_Choice
Timing Ergodic_Theory (4 threads, 76.928s elapsed time, 260.832s cpu time, 5.496s GC time, factor 3.39)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ergodic_Theory
Fourier: theory HOL-Real_Asymp.Real_Asymp
Fourier: theory Fourier.Fourier
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
Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds
Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
DiscretePricing: theory DiscretePricing.Option_Price_Examples
Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula
Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences
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
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, 76.928s elapsed time, 260.832s cpu time, 5.496s GC time, factor 3.39)
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:31 elapsed time, 0:04:43 cpu time, factor 3.10)
Smooth_Manifolds: theory HOL-Library.Quotient_Syntax
Smooth_Manifolds: theory HOL-Library.Function_Algebras
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 Green (4 threads, 74.691s elapsed time, 250.688s cpu time, 3.468s GC time, factor 3.36)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Green
Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On_With
Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On
Timing Fourier (4 threads, 68.427s elapsed time, 254.668s cpu time, 8.684s GC time, factor 3.72)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fourier
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
Timing Green (4 threads, 74.691s elapsed time, 250.688s cpu time, 3.468s GC time, factor 3.36)
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:24 elapsed time, 0:04:33 cpu time, factor 3.22)
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
Treaps: theory HOL-Data_Structures.Set_Specs
Treaps: theory List-Index.List_Index
Treaps: theory HOL-Data_Structures.Tree_Set
Timing Applicative_Lifting (4 threads, 26.150s elapsed time, 75.852s cpu time, 4.108s GC time, factor 2.90)
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:05 elapsed time, 0:02:23 cpu time, factor 2.18)
Treaps: theory Comparison_Sort_Lower_Bound.Linorder_Relations
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fourier/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fourier/outline.pdf
Timing Fourier (4 threads, 68.427s elapsed time, 254.668s cpu time, 8.684s GC time, factor 3.72)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fourier
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fourier/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fourier/outline.pdf
Finished Fourier (0:01:15 elapsed time, 0:04:28 cpu time, factor 3.54)
Running Probabilistic_System_Zoo ...
Smooth_Manifolds: theory Smooth_Manifolds.Analysis_More
Timing Randomised_Social_Choice (4 threads, 14.460s elapsed time, 53.792s cpu time, 1.848s GC time, factor 3.72)
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:46 elapsed time, 0:01:46 cpu time, factor 2.30)
Treaps: theory Landau_Symbols.Landau_Real_Products
Stern_Brocot: theory HOL-Library.BNF_Corec
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
Probabilistic_System_Zoo: theory HOL-Cardinals.Wellfounded_More
Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Relation
Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Embedding
SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Constructions
Smooth_Manifolds: theory Smooth_Manifolds.Chart
Smooth_Manifolds: theory Smooth_Manifolds.Smooth
Timing Prime_Distribution_Elementary (4 threads, 40.684s elapsed time, 148.640s cpu time, 2.972s GC time, factor 3.65)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary
Smooth_Manifolds: theory Smooth_Manifolds.Topological_Manifold
Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Order_Relation
Probabilistic_System_Zoo: theory HOL-Cardinals.Ordinal_Arithmetic
Smooth_Manifolds: theory Smooth_Manifolds.Bump_Function
Smooth_Manifolds: theory Smooth_Manifolds.Differentiable_Manifold
Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Arithmetic
Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinals
Treaps: theory Landau_Symbols.Landau_Simprocs
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
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
Treaps: theory Landau_Symbols.Landau_More
Treaps: theory Quick_Sort_Cost.Randomised_Quick_Sort
Smooth_Manifolds: theory Smooth_Manifolds.Tangent_Space
Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Nonempty_Bounded_Set
Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Probabilistic_Hierarchy
Dirichlet_L: theory Dirichlet_L.Group_Adjoin
Stern_Brocot: theory Stern_Brocot.Cotree
Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters
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
Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters
Treaps: theory Quick_Sort_Cost.Quick_Sort_Average_Case
Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions
Treaps: theory Random_BSTs.Random_BSTs
Smooth_Manifolds: theory Smooth_Manifolds.Cotangent_Space
Timing DiscretePricing (4 threads, 65.610s elapsed time, 222.516s cpu time, 7.916s GC time, factor 3.39)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DiscretePricing
Treaps: theory Treaps.Probability_Misc
Timing MFMC_Countable (4 threads, 65.690s elapsed time, 205.580s cpu time, 6.176s GC time, factor 3.13)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MFMC_Countable
Treaps: theory Treaps.Random_List_Permutation
Treaps: theory Treaps.Treap_Sort_and_BSTs
Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
Treaps: theory Treaps.Random_Treap
Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem
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 Smooth_Manifolds (4 threads, 38.472s elapsed time, 112.704s cpu time, 3.860s GC time, factor 2.93)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Smooth_Manifolds
Timing DiscretePricing (4 threads, 65.610s elapsed time, 222.516s cpu time, 7.916s GC time, factor 3.39)
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:17 elapsed time, 0:04:01 cpu time, factor 3.13)
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
Timing MFMC_Countable (4 threads, 65.690s elapsed time, 205.580s cpu time, 6.176s GC time, factor 3.13)
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:16 elapsed time, 0:03:43 cpu time, factor 2.92)
Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi
Timing Dirichlet_L (4 threads, 79.895s elapsed time, 255.416s cpu time, 7.708s GC time, factor 3.20)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dirichlet_L
Monomorphic_Monad: theory HOL-Library.Countable_Set_Type
Quick_Sort_Cost: theory HOL-Library.Function_Algebras
Quick_Sort_Cost: theory HOL-Library.Landau_Symbols
Quick_Sort_Cost: theory Landau_Symbols.Group_Sort
Quick_Sort_Cost: theory List-Index.List_Index
Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi_Counterexample
Quick_Sort_Cost: theory Comparison_Sort_Lower_Bound.Linorder_Relations
Monomorphic_Monad: theory Monomorphic_Monad.Monomorphic_Monad
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
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
Quick_Sort_Cost: theory Landau_Symbols.Landau_Real_Products
Timing Smooth_Manifolds (4 threads, 38.472s elapsed time, 112.704s cpu time, 3.860s GC time, factor 2.93)
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
Finished Smooth_Manifolds (0:00:46 elapsed time, 0:02:07 cpu time, factor 2.75)
Timing Dirichlet_L (4 threads, 79.895s elapsed time, 255.416s cpu time, 7.708s GC time, factor 3.20)
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:26 elapsed time, 0:04:27 cpu time, factor 3.08)
Timing Probabilistic_System_Zoo (4 threads, 29.357s elapsed time, 105.532s cpu time, 4.740s GC time, factor 3.59)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo
Tarskis_Geometry: theory HOL-Algebra.Congruence
Tarskis_Geometry: theory HOL-Library.Quadratic_Discriminant
Tarskis_Geometry: theory Tarskis_Geometry.Metric
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
Tarskis_Geometry: theory Tarskis_Geometry.Miscellany
UpDown_Scheme: theory HOL-Library.Monad_Syntax
UpDown_Scheme: theory HOL-Imperative_HOL.Heap
Tarskis_Geometry: theory Tarskis_Geometry.Linear_Algebra2
Tarskis_Geometry: theory Tarskis_Geometry.Tarski
UpDown_Scheme: theory UpDown_Scheme.Grid_Point
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Syntax_Match
UpDown_Scheme: theory Automatic_Refinement.Misc
Tarskis_Geometry: theory Tarskis_Geometry.Euclid_Tarski
Tarskis_Geometry: theory HOL-Algebra.Order
Timing Treaps (4 threads, 36.568s elapsed time, 120.632s cpu time, 3.996s GC time, factor 3.30)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Treaps
UpDown_Scheme: theory UpDown_Scheme.Grid
UpDown_Scheme: theory HOL-Imperative_HOL.Heap_Monad
Quick_Sort_Cost: theory Landau_Symbols.Landau_Simprocs
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
Tarskis_Geometry: theory HOL-Algebra.Lattice
Quick_Sort_Cost: theory Landau_Symbols.Landau_More
Quick_Sort_Cost: theory Quick_Sort_Cost.Randomised_Quick_Sort
UpDown_Scheme: theory UpDown_Scheme.UpDown_Scheme
Timing Probabilistic_System_Zoo (4 threads, 29.357s elapsed time, 105.532s cpu time, 4.740s GC time, factor 3.59)
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:35 elapsed time, 0:02:04 cpu time, factor 3.53)
Running Prime_Number_Theorem ...
Tarskis_Geometry: theory HOL-Algebra.Complete_Lattice
UpDown_Scheme: theory UpDown_Scheme.Triangular_Function
UpDown_Scheme: theory HOL-Imperative_HOL.Array
Tarskis_Geometry: theory HOL-Algebra.Group
UpDown_Scheme: theory UpDown_Scheme.Down
UpDown_Scheme: theory UpDown_Scheme.Up
UpDown_Scheme: theory HOL-Imperative_HOL.Ref
Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
Prime_Number_Theorem: theory Stirling_Formula.Stirling_Formula
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
Timing SDS_Impossibility (4 threads, 34.839s elapsed time, 86.160s cpu time, 1.992s GC time, factor 2.47)
UpDown_Scheme: theory HOL-Imperative_HOL.Imperative_HOL
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/SDS_Impossibility
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Run
UpDown_Scheme: theory UpDown_Scheme.Up_Down
Timing Prime_Distribution_Elementary (4 threads, 40.684s elapsed time, 148.640s cpu time, 2.972s GC time, factor 3.65)
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:01:17 elapsed time, 0:03:30 cpu time, factor 2.70)
Quick_Sort_Cost: theory Quick_Sort_Cost.Quick_Sort_Average_Case
Timing Treaps (4 threads, 36.568s elapsed time, 120.632s cpu time, 3.996s GC time, factor 3.30)
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.09)
Tarskis_Geometry: theory Tarskis_Geometry.Action
Tarskis_Geometry: theory Tarskis_Geometry.Projective
Prime_Number_Theorem: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Counting_Functions
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Assertions
Timing Quick_Sort_Cost (4 threads, 13.425s elapsed time, 50.668s cpu time, 1.876s GC time, factor 3.77)
Lp: theory Ergodic_Theory.SG_Library_Complement
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quick_Sort_Cost
Quaternions: theory Quaternions.Quaternions
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
Lp: theory Lp.Functional_Spaces
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Hoare_Triple
Timing SDS_Impossibility (4 threads, 34.839s elapsed time, 86.160s cpu time, 1.992s GC time, factor 2.47)
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:40 elapsed time, 0:01:37 cpu time, factor 2.39)
Running Kuratowski_Closure_Complement ...
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Automation
Tarskis_Geometry: theory Tarskis_Geometry.Hyperbolic_Tarski
Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem
Prime_Number_Theorem: theory Prime_Number_Theorem.Mertens_Theorems
Kuratowski_Closure_Complement: theory Kuratowski_Closure_Complement.KuratowskiClosureComplementTheorem
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Sep_Main
UpDown_Scheme: theory UpDown_Scheme.Imperative
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
Stern_Brocot: theory Stern_Brocot.Bird_Tree
Timing Stern_Brocot (4 threads, 44.381s elapsed time, 70.792s cpu time, 3.700s GC time, factor 1.60)
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
Timing Stern_Brocot (4 threads, 44.381s elapsed time, 70.792s cpu time, 3.700s GC time, factor 1.60)
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:24 cpu time, factor 1.64)
Monomorphic_Monad: theory Monomorphic_Monad.Interpreter
Monomorphic_Monad: theory Monomorphic_Monad.Just_Do_It_Examples
Monomorphic_Monad: theory Monomorphic_Monad.Monad_Overloading
pGCL: theory pGCL.Expectations
pGCL: theory pGCL.Transformers
pGCL: theory pGCL.LoopInduction
pGCL: theory pGCL.Sublinearity
pGCL: theory pGCL.StructuredReasoning
Timing Tarskis_Geometry (4 threads, 27.140s elapsed time, 97.708s cpu time, 3.464s GC time, factor 3.60)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Tarskis_Geometry
Timing UpDown_Scheme (4 threads, 27.673s elapsed time, 106.288s cpu time, 3.932s GC time, factor 3.84)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/UpDown_Scheme
Timing Monomorphic_Monad (4 threads, 34.314s elapsed time, 61.136s cpu time, 2.960s GC time, factor 1.78)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monomorphic_Monad
pGCL: theory pGCL.LoopExamples
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
Timing Quaternions (4 threads, 23.803s elapsed time, 30.612s cpu time, 0.892s GC time, factor 1.29)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quaternions
Timing UpDown_Scheme (4 threads, 27.673s elapsed time, 106.288s cpu time, 3.932s GC time, factor 3.84)
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:33 elapsed time, 0:01:57 cpu time, factor 3.47)
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
Timing Kuratowski_Closure_Complement (4 threads, 21.838s elapsed time, 64.416s cpu time, 1.632s GC time, factor 2.95)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement
Timing Lp (4 threads, 25.756s elapsed time, 79.876s cpu time, 1.252s GC time, factor 3.10)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lp
Timing Monomorphic_Monad (4 threads, 34.314s elapsed time, 61.136s cpu time, 2.960s 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:15 cpu time, factor 1.80)
HOL-Analysis-ex: theory HOL-Analysis-ex.Metric_Arith_Examples
HOL-Analysis-ex: theory HOL-Analysis-ex.Approximations
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 Prime_Number_Theorem (4 threads, 28.819s elapsed time, 96.412s cpu time, 1.900s GC time, factor 3.35)
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/Quaternions/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Quaternions/outline.pdf
Timing Tarskis_Geometry (4 threads, 27.140s elapsed time, 97.708s cpu time, 3.464s GC time, factor 3.60)
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:36 elapsed time, 0:01:53 cpu time, factor 3.12)
Octonions: theory Octonions.Cross_Product_7
Timing Quaternions (4 threads, 23.803s elapsed time, 30.612s cpu time, 0.892s GC time, factor 1.29)
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:28 elapsed time, 0:00:40 cpu time, factor 1.41)
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/Kuratowski_Closure_Complement/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement/outline.pdf
Timing Quick_Sort_Cost (4 threads, 13.425s elapsed time, 50.668s cpu time, 1.876s GC time, factor 3.77)
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:43 elapsed time, 0:01:41 cpu time, factor 2.32)
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
Timing Kuratowski_Closure_Complement (4 threads, 21.838s elapsed time, 64.416s cpu time, 1.632s 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:27 elapsed time, 0:01:15 cpu time, factor 2.75)
Running Neumann_Morgenstern_Utility ...
Octonions: theory Octonions.Octonions
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 Lp (4 threads, 25.756s elapsed time, 79.876s cpu time, 1.252s GC time, factor 3.10)
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:32 elapsed time, 0:01:31 cpu time, factor 2.83)
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
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
Random_BSTs: theory HOL-Data_Structures.Set_Specs
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
Random_BSTs: theory HOL-Data_Structures.Tree_Set
Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries
Error_Function: theory HOL-Library.Function_Algebras
Error_Function: theory HOL-Library.Landau_Symbols
Error_Function: theory Landau_Symbols.Group_Sort
Catalan_Numbers: theory Landau_Symbols.Landau_Real_Products
Timing pGCL (4 threads, 20.797s elapsed time, 80.140s cpu time, 1.908s GC time, factor 3.85)
Timing Prime_Number_Theorem (4 threads, 28.819s elapsed time, 96.412s cpu time, 1.900s GC time, factor 3.35)
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:50 cpu time, factor 3.00)
Running HOL-Probability-ex ...
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/pGCL
Random_BSTs: theory Random_BSTs.Random_BSTs
Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions
Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem
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
Error_Function: theory Error_Function.Error_Function
Error_Function: theory Landau_Symbols.Landau_Real_Products
Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility
Catalan_Numbers: theory Landau_Symbols.Landau_Simprocs
Catalan_Numbers: theory Landau_Symbols.Landau_More
Timing Random_BSTs (4 threads, 7.471s elapsed time, 13.764s cpu time, 0.580s GC time, factor 1.84)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_BSTs
Catalan_Numbers: theory Catalan_Numbers.Catalan_Numbers
Cayley_Hamilton: theory Cayley_Hamilton.Cayley_Hamilton
Error_Function: theory Landau_Symbols.Landau_Simprocs
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
Timing Cayley_Hamilton (4 threads, 12.771s elapsed time, 41.632s cpu time, 1.656s GC time, factor 3.26)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cayley_Hamilton
Error_Function: theory Landau_Symbols.Landau_More
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
Timing pGCL (4 threads, 20.797s elapsed time, 80.140s cpu time, 1.908s GC time, factor 3.85)
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:39 cpu time, factor 3.17)
Error_Function: theory Error_Function.Error_Function_Asymptotics
Timing Catalan_Numbers (4 threads, 12.393s elapsed time, 41.296s cpu time, 1.832s GC time, factor 3.33)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Catalan_Numbers
Timing Octonions (4 threads, 16.423s elapsed time, 57.092s cpu time, 1.568s GC time, factor 3.48)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Octonions
Timing Neumann_Morgenstern_Utility (4 threads, 12.379s elapsed time, 41.664s cpu time, 1.068s GC time, factor 3.37)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Neumann_Morgenstern_Utility
IMO2019: theory IMO2019.IMO2019_Q5
IMO2019: theory IMO2019.IMO2019_Q1
IMO2019: theory IMO2019.IMO2019_Q4
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 Error_Function (4 threads, 11.950s elapsed time, 43.016s cpu time, 1.704s GC time, factor 3.60)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Error_Function
Timing HOL-Probability-ex (4 threads, 9.668s elapsed time, 27.780s cpu time, 0.828s GC time, factor 2.87)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability-ex
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
Timing Cayley_Hamilton (4 threads, 12.771s elapsed time, 41.632s cpu time, 1.656s GC time, factor 3.26)
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:51 cpu time, factor 2.91)
Running Lower_Semicontinuous ...
Timing HOL-Analysis-ex (4 threads, 19.527s elapsed time, 57.960s cpu time, 0.688s GC time, factor 2.97)
Timing HOL-Probability-ex (4 threads, 9.668s elapsed time, 27.780s cpu time, 0.828s GC time, factor 2.87)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability-ex
Finished HOL-Probability-ex (0:00:12 elapsed time, 0:00:30 cpu time, factor 2.48)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis-ex
Timing Catalan_Numbers (4 threads, 12.393s elapsed time, 41.296s cpu time, 1.832s GC time, factor 3.33)
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:17 elapsed time, 0:00:51 cpu time, factor 2.93)
Running Rank_Nullity_Theorem ...
Timing HOL-Analysis-ex (4 threads, 19.527s elapsed time, 57.960s cpu time, 0.688s GC time, factor 2.97)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis-ex
Finished HOL-Analysis-ex (0:00:21 elapsed time, 0:00:59 cpu time, factor 2.78)
Running Random_Graph_Subgraph_Threshold ...
Lower_Semicontinuous: theory Lower_Semicontinuous.Lower_Semicontinuous
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
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
Rank_Nullity_Theorem: theory HOL-Library.Function_Algebras
Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dual_Order
Laplace_Transform: theory Laplace_Transform.Laplace_Transform_Library
Laplace_Transform: theory Laplace_Transform.Lerch_Lemma
Laplace_Transform: theory Laplace_Transform.Piecewise_Continuous
Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Mod_Type
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
Timing Octonions (4 threads, 16.423s elapsed time, 57.092s cpu time, 1.568s GC time, factor 3.48)
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:07 cpu time, factor 3.11)
Timing Error_Function (4 threads, 11.950s elapsed time, 43.016s cpu time, 1.704s GC time, factor 3.60)
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:16 elapsed time, 0:00:52 cpu time, factor 3.13)
Running First_Welfare_Theorem ...
Running Comparison_Sort_Lower_Bound ...
Laplace_Transform: theory Laplace_Transform.Existence
Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
Timing Neumann_Morgenstern_Utility (4 threads, 12.379s elapsed time, 41.664s cpu time, 1.068s GC time, factor 3.37)
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:18 elapsed time, 0:00:52 cpu time, factor 2.89)
Running Stewart_Apollonius ...
Laplace_Transform: theory Laplace_Transform.Uniqueness
Laplace_Transform: theory Laplace_Transform.Laplace_Transform
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
First_Welfare_Theorem: theory First_Welfare_Theorem.Consumers
First_Welfare_Theorem: theory First_Welfare_Theorem.Preferences
Comparison_Sort_Lower_Bound: theory HOL-Library.Multiset_Permutations
Comparison_Sort_Lower_Bound: theory List-Index.List_Index
Stewart_Apollonius: theory Triangle.Angles
Stewart_Apollonius: theory Triangle.Triangle
Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Miscellaneous
Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
Stewart_Apollonius: theory Stewart_Apollonius.Stewart_Apollonius
First_Welfare_Theorem: theory First_Welfare_Theorem.Utility_Functions
First_Welfare_Theorem: theory First_Welfare_Theorem.Common
Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
First_Welfare_Theorem: theory First_Welfare_Theorem.Arrow_Debreu_Model
First_Welfare_Theorem: theory First_Welfare_Theorem.Exchange_Economy
Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Fundamental_Subspaces
First_Welfare_Theorem: theory First_Welfare_Theorem.Private_Ownership_Economy
Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dim_Formula
Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
Timing Stewart_Apollonius (4 threads, 3.922s elapsed time, 7.020s cpu time, 0.180s GC time, factor 1.79)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius
Timing Laplace_Transform (4 threads, 6.959s elapsed time, 27.044s cpu time, 0.428s GC time, factor 3.89)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Laplace_Transform
Timing IMO2019 (4 threads, 10.435s elapsed time, 15.416s cpu time, 0.172s GC time, factor 1.48)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/IMO2019
Timing Rank_Nullity_Theorem (4 threads, 7.754s elapsed time, 15.112s cpu time, 0.668s GC time, factor 1.95)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem
Timing Lower_Semicontinuous (4 threads, 8.577s elapsed time, 20.232s cpu time, 0.420s GC time, factor 2.36)
Timing Random_Graph_Subgraph_Threshold (4 threads, 7.146s elapsed time, 21.220s cpu time, 0.428s GC time, factor 2.97)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Random_Graph_Subgraph_Threshold
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lower_Semicontinuous
Timing First_Welfare_Theorem (4 threads, 7.030s elapsed time, 23.876s cpu time, 0.584s GC time, factor 3.40)
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/Stewart_Apollonius/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius/outline.pdf
Timing Comparison_Sort_Lower_Bound (4 threads, 6.837s elapsed time, 19.416s cpu time, 0.788s GC time, factor 2.84)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Comparison_Sort_Lower_Bound
Timing Stewart_Apollonius (4 threads, 3.922s elapsed time, 7.020s cpu time, 0.180s GC time, factor 1.79)
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:16 cpu time, factor 1.94)
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/IMO2019/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/IMO2019/outline.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Laplace_Transform/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Laplace_Transform/outline.pdf
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
Timing Laplace_Transform (4 threads, 6.959s elapsed time, 27.044s cpu time, 0.428s GC time, factor 3.89)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Laplace_Transform
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Laplace_Transform/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Laplace_Transform/outline.pdf
Finished Laplace_Transform (0:00:12 elapsed time, 0:00:37 cpu time, factor 3.01)
Timing IMO2019 (4 threads, 10.435s elapsed time, 15.416s cpu time, 0.172s GC time, factor 1.48)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/IMO2019
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/IMO2019/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/IMO2019/outline.pdf
Finished IMO2019 (0:00:16 elapsed time, 0:00:26 cpu time, factor 1.61)
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
Triangle: theory Triangle.Angles
Timing Rank_Nullity_Theorem (4 threads, 7.754s elapsed time, 15.112s cpu time, 0.668s GC time, factor 1.95)
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:12 elapsed time, 0:00:25 cpu time, factor 1.96)
Running Source_Coding_Theorem ...
Triangle: theory Triangle.Triangle
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.577s elapsed time, 20.232s cpu time, 0.420s GC time, factor 2.36)
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:30 cpu time, factor 2.19)
Timing Random_Graph_Subgraph_Threshold (4 threads, 7.146s elapsed time, 21.220s cpu time, 0.428s GC time, factor 2.97)
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.47)
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 Comparison_Sort_Lower_Bound (4 threads, 6.837s elapsed time, 19.416s cpu time, 0.788s GC time, factor 2.84)
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:12 elapsed time, 0:00:29 cpu time, factor 2.43)
Running Minkowskis_Theorem ...
Buffons_Needle: theory Buffons_Needle.Buffons_Needle
Chord_Segments: theory Triangle.Triangle
Chord_Segments: theory Chord_Segments.Chord_Segments
Timing First_Welfare_Theorem (4 threads, 7.030s elapsed time, 23.876s cpu time, 0.584s GC time, factor 3.40)
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:34 cpu time, factor 2.76)
Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
Cartan_FP: theory Cartan_FP.Cartan
Fisher_Yates: theory Fisher_Yates.Fisher_Yates
Minkowskis_Theorem: theory Minkowskis_Theorem.Minkowskis_Theorem
Timing Random_BSTs (4 threads, 7.471s elapsed time, 13.764s cpu time, 0.580s GC time, factor 1.84)
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:32 elapsed time, 0:00:55 cpu time, factor 1.73)
Ptolemys_Theorem: theory Ptolemys_Theorem.Ptolemys_Theorem
Timing Cartan_FP (4 threads, 1.399s elapsed time, 4.852s cpu time, 0.000s GC time, factor 3.47)
Timing Triangle (4 threads, 3.673s elapsed time, 6.064s cpu time, 0.164s GC time, factor 1.65)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Cartan_FP
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Triangle
Timing Minkowskis_Theorem (4 threads, 1.264s elapsed time, 4.272s cpu time, 0.000s GC time, factor 3.38)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem
Timing Ptolemys_Theorem (4 threads, 1.002s elapsed time, 2.760s cpu time, 0.000s GC time, factor 2.76)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Ptolemys_Theorem
Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
Timing Chord_Segments (4 threads, 3.877s elapsed time, 8.044s cpu time, 0.124s GC time, factor 2.07)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Chord_Segments
Timing Buffons_Needle (4 threads, 3.827s elapsed time, 11.412s cpu time, 0.084s GC time, factor 2.98)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle
Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
Timing Fisher_Yates (4 threads, 2.846s elapsed time, 8.272s cpu time, 0.112s GC time, factor 2.91)
Timing Source_Coding_Theorem (4 threads, 3.475s elapsed time, 9.224s cpu time, 0.120s GC time, factor 2.65)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Source_Coding_Theorem
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/Triangle/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Triangle/outline.pdf
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
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 Cartan_FP (4 threads, 1.399s elapsed time, 4.852s cpu time, 0.000s GC time, factor 3.47)
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.33)
Timing Triangle (4 threads, 3.673s elapsed time, 6.064s cpu time, 0.164s GC time, factor 1.65)
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.84)
Running 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 Minkowskis_Theorem (4 threads, 1.264s elapsed time, 4.272s cpu time, 0.000s GC time, factor 3.38)
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:06 elapsed time, 0:00:14 cpu time, factor 2.31)
Timing Ptolemys_Theorem (4 threads, 1.002s elapsed time, 2.760s cpu time, 0.000s GC time, factor 2.76)
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:12 cpu time, factor 2.13)
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
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
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
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
Timing Chord_Segments (4 threads, 3.877s elapsed time, 8.044s cpu time, 0.124s GC time, factor 2.07)
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.03)
Timing Source_Coding_Theorem (4 threads, 3.475s elapsed time, 9.224s cpu time, 0.120s GC time, factor 2.65)
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:18 cpu time, factor 2.22)
Timing Buffons_Needle (4 threads, 3.827s elapsed time, 11.412s cpu time, 0.084s GC time, factor 2.98)
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:08 elapsed time, 0:00:21 cpu time, factor 2.37)
Timing Fisher_Yates (4 threads, 2.846s elapsed time, 8.272s cpu time, 0.112s GC time, factor 2.91)
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)
Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
Timing Monad_Normalisation (4 threads, 0.852s elapsed time, 1.436s cpu time, 0.000s GC time, factor 1.68)
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
Timing Randomised_BSTs (4 threads, 7.921s elapsed time, 26.760s cpu time, 0.584s GC time, factor 3.38)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Randomised_BSTs
Timing Monad_Normalisation (4 threads, 0.852s elapsed time, 1.436s cpu time, 0.000s GC time, factor 1.68)
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:11 cpu time, factor 1.95)
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.921s elapsed time, 26.760s cpu time, 0.584s GC time, factor 3.38)
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.75)
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, 1141.263s elapsed time, 4094.780s cpu time, 669.676s GC time, factor 3.59)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Numerics
Timing HOL-ODE-Numerics (4 threads, 1141.263s elapsed time, 4094.780s cpu time, 669.676s GC time, factor 3.59)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Numerics
Finished HOL-ODE-Numerics (0:20:32 elapsed time, 1:13:24 cpu time, factor 3.57)
Building Lorenz_Approximation ...
HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
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
Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
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, 226.595s elapsed time, 506.684s cpu time, 41.188s GC time, factor 2.24)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_Approximation
Timing Lorenz_Approximation (4 threads, 226.595s elapsed time, 506.684s cpu time, 41.188s GC time, factor 2.24)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_Approximation
Finished Lorenz_Approximation (0:04:31 elapsed time, 0:09:44 cpu time, factor 2.16)
Lorenz_C0: theory Lorenz_C0.Lorenz_C0
Lorenz_C1: theory Lorenz_C1.Lorenz_C1
Timing Lorenz_C1 (4 threads, 0.971s elapsed time, 1.660s cpu time, 0.000s GC time, factor 1.71)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_C1
Timing Lorenz_C1 (4 threads, 0.971s elapsed time, 1.660s cpu time, 0.000s GC time, factor 1.71)
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.15)
Timing HOL-ODE-Examples (4 threads, 473.002s elapsed time, 1340.600s cpu time, 10.800s GC time, factor 2.83)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Examples
Timing HOL-ODE-Examples (4 threads, 473.002s elapsed time, 1340.600s cpu time, 10.800s GC time, factor 2.83)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Examples
Finished HOL-ODE-Examples (0:07:55 elapsed time, 0:22:23 cpu time, factor 2.82)
Timing HOL-ODE-ARCH-COMP (4 threads, 529.324s elapsed time, 1197.356s cpu time, 30.060s 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, 529.324s elapsed time, 1197.356s cpu time, 30.060s 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:52 elapsed time, 0:20:00 cpu time, factor 2.26)
Timing Lorenz_C0 (4 threads, 1569.320s elapsed time, 6194.468s cpu time, 40.568s GC time, factor 3.95)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_C0
Timing Lorenz_C0 (4 threads, 1569.320s elapsed time, 6194.468s cpu time, 40.568s GC time, factor 3.95)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_C0
Finished Lorenz_C0 (0:26:12 elapsed time, 1:43:17 cpu time, factor 3.94)
Group AFP: 3:30:06 elapsed time, 10:44:37 cpu time, factor 3.07
Group main: 0:13:36 elapsed time, 0:42:17 cpu time, factor 3.11
Group doc: 0:00:00 elapsed time
Group timing: 0:16:17 elapsed time, 0:50:54 cpu time, factor 3.13
Group large: 0:34:12 elapsed time, 2:05:45 cpu time, factor 3.68
Group no_doc: 0:00:00 elapsed time
Overall: 1:06:54 elapsed time, 11:36:32 cpu time, factor 10.41
[32mSuccess: Generated topics.html[0m
[32mSuccess: Generated index.html[0m
[32mSuccess: Generated html files for 501 entries[0m
[32mSuccess: Generated statistics.html[0m
[32mSuccess: Generated download.html[0m
[32mSuccess: Generated about.html[0m
[32mSuccess: Generated citing.html[0m
[32mSuccess: Generated updating.html[0m
[32mSuccess: Generated search.html[0m
[32mSuccess: Generated submitting.html[0m
[32mSuccess: Generated using.html[0m
[32mSuccess: Generated rss.xml[0m
[32mSuccess: Generated status.html[0m
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