Started by an SCM change
[EnvInject] - Loading node environment variables.
Building remotely on workermta1 (mta_big) in workspace /media/data/jenkins/workspace/isabelle-all
[isabelle-all] $ hg showconfig paths.default
[isabelle-all] $ hg pull --rev default
pulling from http://isabelle.in.tum.de/repos/isabelle/
searching for changes
no changes found
[isabelle-all] $ hg update --clean --rev default
6 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 ab8aad4aa76e11e15da6b17a10de5e0cfa93eefc --template exists\n
exists
[isabelle-all] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(ab8aad4aa76e11e15da6b17a10de5e0cfa93eefc)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
[afp] $ hg pull --rev default
pulling from https://bitbucket.org/isa-afp/afp-devel/
no changes found
[afp] $ hg update --clean --rev default
469 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 08edeafdffe13606003e088c2f2f509ae5182fa9 --template exists\n
exists
[afp] $ hg log --template "{desc|xmlescape}{file_adds|stringify|xmlescape}{file_dels|stringify|xmlescape}{files|stringify|xmlescape}{parents}\n" --rev "ancestors('default') and not ancestors(08edeafdffe13606003e088c2f2f509ae5182fa9)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-all] $ /bin/sh -xe /tmp/jenkins3446293230243963596.sh
+ Admin/jenkins/run_build all
+ set -e
+ PROFILE=all
+ shift
+ bin/isabelle components -a
+ bin/isabelle jedit -bf
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
+ bin/isabelle ocaml_setup
The following actions will be performed:
∗ install base-bigarray base
∗ install ocaml-base-compiler 4.05.0 [required by ocaml]
∗ install base-threads base
∗ install conf-gmp 1
∗ install conf-perl 1
∗ install base-unix base
∗ install conf-m4 1
∗ install ocaml-config 1 [required by ocaml]
∗ install ocaml 4.05.0 [required by ocamlfind, zarith]
∗ install ocamlfind 1.8.0
∗ install zarith 1.7
===== ∗ 11 =====
<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ocaml-base-compiler.4.05.0] found in cache
[ocamlfind.1.8.0] found in cache
[zarith.1.7] found in cache
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
∗ installed conf-gmp.1
∗ installed conf-m4.1
∗ installed conf-perl.1
∗ installed ocaml-base-compiler.4.05.0
∗ installed ocaml-config.1
∗ installed ocaml.4.05.0
∗ installed ocamlfind.1.8.0
∗ installed zarith.1.7
Done.
# Run eval $(opam env) to update the current shell environment
[NOTE] Package zarith is already installed (current version is 1.7).
+ bin/isabelle ghc_setup
stack will use a sandboxed GHC it installed
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
The Glorious Glasgow Haskell Compilation System, version 8.4.4
+ bin/isabelle ci_build_all
=== CONFIGURATION ===
ISABELLE_BUILD_OPTIONS=""
ML_PLATFORM="x86_64-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-5.8/x86_64-linux"
ML_SYSTEM="polyml-5.8"
ML_OPTIONS="-H 4000 --maxheap 8G"
jobs = 10, threads = 4, numa = false
=== BUILD ===
Build started at Fri, 22 Mar 2019 12:42:25 GMT
Isabelle id 35ba13ac6e5c
AFP id 08edeafdffe1
=== LOG ===
Session Pure/Pure
Session CTT/CTT
Session Cube/Cube
Session FOL/FOL
Session CCL/CCL
Session FOL/FOL-ex
Session FOLP/FOLP
Session FOLP/FOLP-ex
Session HOL/HOL (main)
Session AFP/AVL-Trees (AFP)
Session AFP/AWN (AFP)
Session AFP/Abortable_Linearizable_Modules (AFP)
Session AFP/Abstract-Hoare-Logics (AFP)
Session AFP/AnselmGod (AFP)
Session AFP/AxiomaticCategoryTheory (AFP)
Session AFP/BinarySearchTree (AFP)
Session AFP/Binomial-Queues (AFP)
Session AFP/Bondy (AFP)
Session AFP/Bounded_Deducibility_Security (AFP)
Session AFP/BytecodeLogicJmlTypes (AFP)
Session AFP/CISC-Kernel (AFP)
Session AFP/CYK (AFP)
Session AFP/Cauchy (AFP)
Session AFP/Sqrt_Babylonian (AFP)
Session Doc/Classes (doc)
Session AFP/ClockSynchInst (AFP)
Session AFP/Compiling-Exceptions-Correctly (AFP)
Session AFP/ComponentDependencies (AFP)
Session AFP/Concurrent_Revisions (AFP)
Session AFP/Constructor_Funs (AFP)
Session AFP/CryptoBasedCompositionalProperties (AFP)
Session AFP/DPT-SAT-Solver (AFP)
Session AFP/Depth-First-Search (AFP)
Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
Session AFP/DiskPaxos (AFP)
Session AFP/Example-Submission (AFP)
Session AFP/FFT (AFP)
Session AFP/FLP (AFP)
Session AFP/FeatherweightJava (AFP)
Session AFP/Featherweight_OCL (AFP)
Session AFP/FileRefinement (AFP)
Session AFP/FocusStreamsCaseStudies (AFP)
Session AFP/Free-Boolean-Algebra (AFP)
Session AFP/FunWithFunctions (AFP)
Session AFP/FunWithTilings (AFP)
Session Doc/Functions (doc)
Session AFP/GPU_Kernel_PL (AFP)
Session AFP/Gauss-Jordan-Elim-Fun (AFP)
Session AFP/GenClock (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/Generic_Deriving (AFP)
Session AFP/GewirthPGCProof (AFP)
Session AFP/GoedelGod (AFP)
Session HOL/HOL-Eisbach
Session AFP/Allen_Calculus (AFP)
Session AFP/Dependent_SIFUM_Type_Systems (AFP)
Session AFP/Dependent_SIFUM_Refinement (AFP)
Session Doc/Eisbach (doc)
Session HOL/HOL-Hoare
Session AFP/Case_Labeling (AFP)
Session HOL/HOL-Hoare_Parallel (timing)
Session HOL/HOL-IMPP
Session HOL/HOL-IOA
Session HOL/HOL-Import
Session HOL/HOL-Lattice
Session HOL/HOL-Library (main timing)
Session AFP/ArrowImpossibilityGS (AFP)
Session AFP/Auto2_HOL (AFP)
Session AFP/BNF_CC (AFP)
Session AFP/BNF_Operations (AFP)
Session AFP/Binomial-Heaps (AFP)
Session AFP/Boolean_Expression_Checkers (AFP)
Session AFP/Buildings (AFP)
Session AFP/CRDT (AFP)
Session AFP/IMAP-CRDT (AFP)
Session AFP/Card_Multisets (AFP)
Session AFP/Card_Number_Partitions (AFP)
Session AFP/Category (AFP)
Session AFP/Category3 (AFP)
Session AFP/MonoidalCategory (AFP)
Session Doc/Codegen (doc)
Session AFP/CofGroups (AFP)
Session AFP/Completeness (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/Concurrent_Ref_Alg (AFP)
Session AFP/CoreC++ (AFP)
Session AFP/Core_DOM (AFP)
Session Doc/Datatypes (doc)
Session Doc/Corec (doc)
Session AFP/Decl_Sem_Fun_PL (AFP)
Session AFP/Derangements (AFP)
Session AFP/Discrete_Summation (AFP)
Session AFP/Card_Partitions (AFP)
Session AFP/Bell_Numbers_Spivey (AFP)
Session AFP/Card_Equiv_Relations (AFP)
Session AFP/Efficient-Mergesort (AFP)
Session AFP/Encodability_Process_Calculi (AFP)
Session AFP/Epistemic_Logic (AFP)
Session AFP/Euler_Partition (AFP)
Session AFP/FOL-Fitting (AFP)
Session AFP/FOL_Harrison (AFP)
Session AFP/Factored_Transition_System_Bounding (AFP)
Session AFP/Falling_Factorial_Sum (AFP)
Session AFP/FinFun (AFP)
Session AFP/Finger-Trees (AFP)
Session AFP/Graph_Saturation (AFP)
Session AFP/Graph_Theory (AFP)
Session AFP/ShortestPath (AFP)
Session AFP/Group-Ring-Module (AFP)
Session AFP/Valuation (AFP)
Session HOL/HOL-Auth (timing)
Session HOL/HOL-UNITY (timing)
Session HOL/HOL-Bali (timing)
Session HOL/HOL-Cardinals (timing)
Session AFP/Ordinals_and_Cardinals (AFP)
Session AFP/Sort_Encodings (AFP)
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/JNF-HOL-Lib (AFP)
Session AFP/Localization_Ring (AFP)
Session AFP/Orbit_Stabiliser (AFP)
Session AFP/Perfect-Number-Thm (AFP)
Session AFP/Secondary_Sylow (AFP)
Session AFP/Jordan_Hoelder (AFP)
Session AFP/VectorSpace (AFP)
Session HOL/HOL-Analysis (main timing)
Session AFP/Bernoulli (AFP)
Session AFP/Cartan_FP (AFP)
Session AFP/Cayley_Hamilton (AFP)
Session AFP/Coinductive (AFP)
Session AFP/DynamicArchitectures (AFP)
Session AFP/Architectural_Design_Patterns (AFP)
Session AFP/Lazy-Lists-II (AFP)
Session AFP/Stream_Fusion_Code (AFP)
Session AFP/Topology (AFP)
Session AFP/First_Welfare_Theorem (AFP)
Session AFP/Green (AFP)
Session HOL/HOL-Analysis-ex
Session HOL/HOL-Probability (main timing)
Session AFP/Buffons_Needle (AFP)
Session AFP/Density_Compiler (AFP)
Session AFP/DiscretePricing (AFP)
Session AFP/Ergodic_Theory (AFP)
Session AFP/Gromov_Hyperbolicity (AFP)
Session AFP/Fisher_Yates (AFP)
Session AFP/Girth_Chromatic (AFP)
Session AFP/Random_Graph_Subgraph_Threshold (AFP)
Session HOL/HOL-Probability-ex (timing)
Session AFP/Lp (AFP)
Session AFP/Markov_Models (AFP)
Session AFP/Monad_Normalisation (AFP)
Session AFP/Monomorphic_Monad (AFP)
Session AFP/Neumann_Morgenstern_Utility (AFP)
Session AFP/Probabilistic_Noninterference (AFP)
Session AFP/Probabilistic_System_Zoo (AFP)
Session AFP/Probabilistic_System_Zoo-Non_BNFs (AFP)
Session AFP/Source_Coding_Theorem (AFP)
Session AFP/Irrationality_J_Hancl (AFP)
Session AFP/Kuratowski_Closure_Complement (AFP)
Session AFP/Lower_Semicontinuous (AFP)
Session AFP/Minkowskis_Theorem (AFP)
Session AFP/Octonions (AFP)
Session AFP/Probabilistic_System_Zoo-BNFs (AFP)
Session AFP/Ptolemys_Theorem (AFP)
Session AFP/Quaternions (AFP)
Session AFP/Rank_Nullity_Theorem (AFP)
Session AFP/Gauss_Jordan (AFP)
Session AFP/Echelon_Form (AFP)
Session AFP/Hermite (AFP)
Session AFP/Tarskis_Geometry (AFP)
Session AFP/Triangle (AFP)
Session AFP/Chord_Segments (AFP)
Session AFP/Stewart_Apollonius (AFP)
Session AFP/pGCL (AFP)
Session HOL/HOL-Isar_Examples
Session HOL/HOL-Nonstandard_Analysis (timing)
Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
Session HOL/HOL-Number_Theory (main timing)
Session AFP/E_Transcendental (AFP)
Session AFP/Elliptic_Curves_Group_Law (AFP)
Session AFP/Fermat3_4 (AFP)
Session HOL/HOL-Data_Structures (timing)
Session HOL/HOL-ex (timing)
Session AFP/Automatic_Refinement (AFP)
Session HOL/HOL-Codegenerator_Test
Session AFP/Lehmer (AFP)
Session AFP/Pratt_Certificate (AFP)
Session AFP/Bertrands_Postulate (AFP)
Session AFP/Prime_Harmonic_Series (AFP)
Session AFP/RSAPSS (AFP)
Session AFP/SumSquares (AFP)
Session AFP/Liouville_Numbers (AFP)
Session AFP/Mason_Stothers (AFP)
Session AFP/Polynomial_Interpolation (AFP)
Session AFP/Probabilistic_Prime_Tests (AFP)
Session AFP/Rep_Fin_Groups (AFP)
Session AFP/Sturm_Sequences (AFP)
Session AFP/Special_Function_Bounds (AFP)
Session AFP/Sturm_Tarski (AFP)
Session AFP/Budan_Fourier (AFP)
Session AFP/Winding_Number_Eval (AFP)
Session AFP/Count_Complex_Roots (AFP)
Session HOL/HOL-Corec_Examples (timing)
Session HOL/HOL-Datatype_Examples (timing)
Session HOL/HOL-Hahn_Banach
Session HOL/HOL-IMP (timing)
Session AFP/Abs_Int_ITP2012 (AFP)
Session HOL/HOL-Imperative_HOL (timing)
Session AFP/Auto2_Imperative_HOL (AFP)
Session AFP/Imperative_Insertion_Sort (AFP)
Session HOL/HOL-Induct
Session HOL/HOL-Matrix_LP
Session HOL/HOL-Metis_Examples (timing)
Session HOL/HOL-MicroJava (timing)
Session HOL/HOL-Mutabelle
Session HOL/HOL-Nitpick_Examples
Session HOL/HOL-Nominal
Session AFP/CCS (AFP)
Session HOL/HOL-Nominal-Examples (timing)
Session AFP/Lam-ml-Normalization (AFP)
Session AFP/Pi_Calculus (AFP)
Session AFP/Psi_Calculi (AFP)
Session AFP/SequentInvertibility (AFP)
Session HOL/HOL-Predicate_Compile_Examples (timing)
Session HOL/HOL-Quickcheck_Examples (timing)
Session HOL/HOL-SET_Protocol (timing)
Session HOL/HOL-TPTP
Session HOL/HOL-Unix
Session HOL/HOL-ZF
Session AFP/Category2 (AFP)
Session AFP/HereditarilyFinite (AFP)
Session AFP/HyperCTL (AFP)
Session AFP/Integration (AFP)
Session AFP/Isabelle_Meta_Model (AFP)
Session AFP/LTL (AFP)
Session AFP/Stuttering_Equivalence (AFP)
Session AFP/Lambda_Free_RPOs (AFP)
Session AFP/Lambda_Free_EPO (AFP)
Session AFP/Landau_Symbols (AFP)
Session AFP/Akra_Bazzi (AFP)
Session AFP/Catalan_Numbers (AFP)
Session AFP/Error_Function (AFP)
Session AFP/Euler_MacLaurin (AFP)
Session AFP/Stirling_Formula (AFP)
Session AFP/LightweightJava (AFP)
Session AFP/LinearQuantifierElim (AFP)
Session AFP/List-Infinite (AFP)
Session AFP/Nat-Interval-Logic (AFP)
Session AFP/AutoFocus-Stream (AFP)
Session AFP/MuchAdoAboutTwo (AFP)
Session AFP/Optics (AFP)
Session AFP/UTP-Toolkit (AFP)
Session AFP/UTP (AFP)
Session AFP/Order_Lattice_Props (AFP)
Session AFP/POPLmark-deBruijn (AFP)
Session AFP/Pairing_Heap (AFP)
Session AFP/Password_Authentication_Protocol (AFP)
Session AFP/Pell (AFP)
Session AFP/Presburger-Automata (AFP)
Session AFP/Priority_Queue_Braun (AFP)
Session AFP/Program-Conflict-Analysis (AFP)
Session AFP/Regular-Sets (AFP)
Session AFP/Abstract-Rewriting (AFP)
Session AFP/Decreasing-Diagrams (AFP)
Session AFP/First_Order_Terms (AFP)
Session AFP/Matrix (AFP)
Session AFP/Matrix_Tensor (AFP)
Session AFP/Knot_Theory (AFP)
Session AFP/Coinductive_Languages (AFP)
Session AFP/Finite_Automata_HF (AFP)
Session AFP/Functional-Automata (AFP)
Session AFP/Posix-Lexing (AFP)
Session AFP/Ribbon_Proofs (AFP)
Session AFP/SATSolverVerification (AFP)
Session AFP/Selection_Heap_Sort (AFP)
Session AFP/Simplex (AFP)
Session AFP/Farkas (AFP)
Session AFP/Skew_Heap (AFP)
Session AFP/Splay_Tree (AFP)
Session AFP/Amortized_Complexity (AFP)
Session AFP/Dynamic_Tables (AFP)
Session AFP/Root_Balanced_Tree (AFP)
Session AFP/Stable_Matching (AFP)
Session AFP/SuperCalc (AFP)
Session AFP/Tail_Recursive_Functions (AFP)
Session AFP/TortoiseHare (AFP)
Session AFP/Trie (AFP)
Session AFP/Flyspeck-Tame (AFP)
Session AFP/Twelvefold_Way (AFP)
Session AFP/Vickrey_Clarke_Groves (AFP)
Session HOL/HOL-Mirabelle
Session HOL/HOL-Mirabelle-ex
Session HOL/HOL-NanoJava
Session HOL/HOL-Prolog
Session HOL/HOL-Real_Asymp
Session HOL/HOL-Real_Asymp-Manual
Session HOL/HOL-Statespace
Session HOL/HOL-TLA
Session HOL/HOL-TLA-Buffer
Session HOL/HOL-TLA-Inc
Session HOL/HOL-TLA-Memory
Session HOL/HOL-Types_To_Sets
Session AFP/Smooth_Manifolds (AFP)
Session HOL/HOL-Word (main timing)
Session HOL/HOL-SPARK
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session HOL/HOL-SPARK-Manual
Session HOL/HOL-Word-SMT_Examples (timing)
Session AFP/Kleene_Algebra (AFP)
Session AFP/KAT_and_DRA (AFP)
Session AFP/Multirelations (AFP)
Session AFP/Quantales (AFP)
Session AFP/Transformer_Semantics (AFP)
Session AFP/Regular_Algebras (AFP)
Session AFP/Relation_Algebra (AFP)
Session AFP/Residuated_Lattices (AFP)
Session AFP/LEM (AFP)
Session AFP/Native_Word (AFP)
Session AFP/WebAssembly (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Collections (AFP)
Session AFP/Abstract_Completeness (AFP)
Session AFP/Abstract_Soundness (AFP)
Session AFP/Incredible_Proof_Machine (AFP)
Session AFP/Deriving (AFP)
Session AFP/CAVA_Base (AFP)
Session AFP/CAVA_Automata (AFP)
Session AFP/DFS_Framework (AFP)
Session AFP/Gabow_SCC (AFP)
Session AFP/LTL_to_GBA (AFP)
Session AFP/Promela (AFP)
Session AFP/Containers (AFP)
Session AFP/Collections_Examples (AFP)
Session AFP/Containers-Benchmarks (AFP)
Session AFP/Datatype_Order_Generator (AFP)
Session AFP/Old_Datatype_Show (AFP)
Session AFP/Show (AFP)
Session AFP/JNF-AFP-Lib (AFP)
Session AFP/Real_Impl (AFP)
Session AFP/QR_Decomposition (AFP)
Session AFP/Dijkstra_Shortest_Path (AFP)
Session AFP/Koenigsberg_Friendship (AFP)
Session AFP/Transition_Systems_and_Automata (AFP)
Session AFP/Buchi_Complementation (AFP)
Session AFP/Partial_Order_Reduction (AFP)
Session AFP/SM_Base (AFP)
Session AFP/SM (AFP)
Session AFP/CAVA_Setup (AFP)
Session AFP/CAVA_LTL_Modelchecker (AFP)
Session AFP/Transitive-Closure (AFP)
Session AFP/KBPs (AFP)
Session AFP/Tree-Automata (AFP)
Session AFP/SPARCv8 (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/Separata (AFP)
Session AFP/Separation_Logic_Imperative_HOL (AFP)
Session AFP/Sepref_Prereq (AFP)
Session AFP/ROBDD (AFP)
Session AFP/UpDown_Scheme (AFP)
Session AFP/Word_Lib (AFP)
Session AFP/Complx (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/CakeML (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Routing (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/LOFT (AFP)
Session HOL/HOLCF (main timing)
Session AFP/Circus (AFP)
Session HOL/HOLCF-IMP
Session HOL/HOLCF-Library
Session HOL/HOLCF-FOCUS
Session HOL/HOLCF-ex
Session AFP/PCF (AFP)
Session AFP/HOLCF-Prelude (AFP)
Session HOL/HOLCF-Tutorial
Session HOL/IOA (timing)
Session HOL/IOA-ABP
Session HOL/IOA-NTP
Session HOL/IOA-Storage
Session HOL/IOA-ex
Session AFP/Shivers-CFA (AFP)
Session AFP/Stream-Fusion (AFP)
Session AFP/Tycon (AFP)
Session AFP/WorkerWrapper (AFP)
Session AFP/Heard_Of (AFP)
Session AFP/Consensus_Refined (AFP)
Session AFP/Hoare_Time (AFP)
Session AFP/HotelKeyCards (AFP)
Session Doc/How_to_Prove_it (no_doc)
Session AFP/Huffman (AFP)
Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
Session AFP/IMP2 (AFP)
Session Doc/Implementation (doc)
Session AFP/Impossible_Geometry (AFP)
Session AFP/Inductive_Confidentiality (AFP)
Session AFP/InfPathElimination (AFP)
Session Doc/Isar_Ref (doc)
Session Doc/JEdit (doc)
Session AFP/JiveDataStoreModel (AFP)
Session AFP/KAD (AFP)
Session AFP/Algebraic_VCs (AFP)
Session AFP/Key_Agreement_Strong_Adversaries (AFP)
Session AFP/LambdaMu (AFP)
Session AFP/LatticeProperties (AFP)
Session AFP/DataRefinementIBP (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Lazy_Case (AFP)
Session AFP/Dict_Construction (AFP)
Session AFP/Lifting_Definition_Option (AFP)
Session AFP/List-Index (AFP)
Session AFP/Affine_Arithmetic (AFP)
Session AFP/Taylor_Models (AFP)
Session AFP/Comparison_Sort_Lower_Bound (AFP)
Session AFP/Formula_Derivatives (AFP)
Session AFP/Formula_Derivatives-Examples (AFP)
Session AFP/Higher_Order_Terms (AFP)
Session AFP/Jinja (AFP)
Session AFP/HRB-Slicing (AFP)
Session AFP/InformationFlowSlicing_Inter (AFP)
Session AFP/Slicing (AFP)
Session AFP/Formal_SSA (AFP)
Session AFP/Minimal_SSA (AFP)
Session AFP/InformationFlowSlicing (AFP)
Session AFP/LTL_to_DRA (AFP)
Session AFP/List_Update (AFP)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/Differential_Dynamic_Logic (AFP)
Session AFP/HOL-ODE-Numerics (AFP)
Session AFP/HOL-ODE-ARCH-COMP (AFP)
Session AFP/HOL-ODE-Examples (AFP large)
Session AFP/Lorenz_Approximation (AFP)
Session AFP/Lorenz_C0 (AFP large)
Session AFP/Lorenz_C1 (AFP large)
Session AFP/Quick_Sort_Cost (AFP)
Session AFP/Random_BSTs (AFP)
Session AFP/Randomised_BSTs (AFP)
Session AFP/Treaps (AFP)
Session AFP/Randomised_Social_Choice (AFP)
Session AFP/Fishburn_Impossibility (AFP)
Session AFP/SDS_Impossibility (AFP)
Session AFP/Refine_Imperative_HOL (AFP)
Session AFP/Floyd_Warshall (AFP)
Session AFP/Sepref_Basic (AFP)
Session AFP/Sepref_IICF (AFP)
Session AFP/Flow_Networks (AFP)
Session AFP/EdmondsKarp_Maxflow (AFP)
Session AFP/MFMC_Countable (AFP)
Session AFP/Prpu_Maxflow (AFP)
Session AFP/Knuth_Morris_Pratt (AFP)
Session AFP/VerifyThis2018 (AFP)
Session AFP/List_Interleaving (AFP)
Session AFP/List_Inversions (AFP)
Session AFP/LocalLexing (AFP)
Session Doc/Locales (doc)
Session AFP/Lowe_Ontological_Argument (AFP)
Session AFP/MSO_Regex_Equivalence (AFP)
Session Doc/Main (doc)
Session AFP/Marriage (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Matroids (AFP)
Session AFP/Kruskal (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/Median_Of_Medians_Selection (AFP)
Session AFP/Menger (AFP)
Session AFP/MiniML (AFP)
Session AFP/Modular_Assembly_Kit_Security (AFP)
Session AFP/Monad_Memo_DP (AFP)
Session AFP/Hidden_Markov_Models (AFP)
Session AFP/Optimal_BST (AFP)
Session AFP/MonoBoolTranAlgebra (AFP)
Session AFP/Name_Carrying_Type_Inference (AFP)
Session AFP/Network_Security_Policy_Verification (AFP)
Session AFP/No_FTL_observers (AFP)
Session AFP/Nominal2 (AFP)
Session AFP/Incompleteness (AFP)
Session AFP/Surprise_Paradox (AFP)
Session AFP/Launchbury (AFP)
Session AFP/Call_Arity (AFP)
Session AFP/Modal_Logics_for_NTS (AFP)
Session AFP/Rewriting_Z (AFP)
Session AFP/Noninterference_CSP (AFP)
Session AFP/Noninterference_Ipurge_Unwinding (AFP)
Session AFP/Noninterference_Generic_Unwinding (AFP)
Session AFP/Noninterference_Inductive_Unwinding (AFP)
Session AFP/Noninterference_Sequential_Composition (AFP)
Session AFP/Noninterference_Concurrent_Composition (AFP)
Session AFP/NormByEval (AFP)
Session AFP/OpSets (AFP)
Session AFP/Open_Induction (AFP)
Session AFP/Well_Quasi_Orders (AFP)
Session AFP/Decreasing-Diagrams-II (AFP)
Session AFP/Myhill-Nerode (AFP)
Session AFP/Polynomials (AFP)
Session AFP/Symmetric_Polynomials (AFP)
Session AFP/Pi_Transcendental (AFP)
Session AFP/Ordinal (AFP)
Session AFP/Nested_Multisets_Ordinals (AFP)
Session AFP/Lambda_Free_KBOs (AFP)
Session AFP/Ordered_Resolution_Prover (AFP)
Session AFP/PLM (AFP)
Session AFP/PSemigroupsConvolution (AFP)
Session AFP/Paraconsistency (AFP)
Session AFP/Parity_Game (AFP)
Session AFP/Partial_Function_MR (AFP)
Session AFP/Certification_Monads (AFP)
Session AFP/XML (AFP)
Session AFP/Pre_Polynomial_Factorization (AFP)
Session AFP/Polynomial_Factorization (AFP)
Session AFP/Dirichlet_Series (AFP)
Session AFP/Zeta_Function (AFP)
Session AFP/Dirichlet_L (AFP)
Session AFP/Prime_Number_Theorem (AFP)
Session AFP/Prime_Distribution_Elementary (AFP)
Session AFP/Functional_Ordered_Resolution_Prover (AFP)
Session AFP/Jordan_Normal_Form (AFP)
Session AFP/Deep_Learning (AFP)
Session AFP/Groebner_Bases (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/Pre_BZ (AFP)
Session AFP/Berlekamp_Zassenhaus (AFP)
Session AFP/Algebraic_Numbers (AFP)
Session AFP/LLL_Basis_Reduction (AFP)
Session AFP/LLL_Factorization (AFP)
Session AFP/Linear_Recurrences_Solver (AFP)
Session AFP/Probabilistic_While (AFP)
Session AFP/Pop_Refinement (AFP)
Session AFP/Possibilistic_Noninterference (AFP)
Session Doc/Prog_Prove (doc)
Session AFP/Projective_Geometry (AFP)
Session AFP/Proof_Strategy_Language (AFP)
Session AFP/PropResPI (AFP)
Session AFP/Propositional_Proof_Systems (AFP)
Session AFP/PseudoHoops (AFP)
Session AFP/Ramsey-Infinite (AFP)
Session AFP/Recursion-Theory-I (AFP)
Session AFP/Minsky_Machines (AFP)
Session AFP/RefinementReactive (AFP)
Session AFP/Resolution_FOL (AFP)
Session AFP/Robbins-Conjecture (AFP)
Session AFP/Roy_Floyd_Warshall (AFP)
Session AFP/SIFPL (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/Security_Protocol_Refinement (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Simpl (AFP)
Session AFP/BDD (AFP)
Session AFP/Planarity_Certificates (AFP)
Session AFP/Statecharts (AFP)
Session AFP/Stone_Algebras (AFP)
Session AFP/Stone_Relation_Algebras (AFP)
Session AFP/Stone_Kleene_Relation_Algebras (AFP)
Session AFP/Aggregation_Algebras (AFP)
Session AFP/Store_Buffer_Reduction (AFP)
Session AFP/Strong_Security (AFP)
Session Doc/Sugar (doc)
Session AFP/TLA (AFP)
Session AFP/Timed_Automata (AFP)
Session AFP/Probabilistic_Timed_Automata (AFP)
Session AFP/Transitive-Closure-II (AFP)
Session AFP/Tree_Decomposition (AFP)
Session Doc/Tutorial (doc)
Session Doc/Typeclass_Hierarchy (doc)
Session AFP/Types_Tableaus_and_Goedels_God (AFP)
Session AFP/UPF (AFP)
Session AFP/UPF_Firewall (AFP)
Session AFP/Universal_Turing_Machine (AFP)
Session AFP/Verified-Prover (AFP)
Session AFP/VolpanoSmith (AFP)
Session AFP/WHATandWHERE_Security (AFP)
Session AFP/Weight_Balanced_Trees (AFP)
Session HOL/HOL-Proofs (timing)
Session HOL/HOL-Proofs-Extraction (timing)
Session HOL/HOL-Proofs-Lambda (timing)
Session AFP/Applicative_Lifting (AFP)
Session AFP/CryptHOL (AFP)
Session AFP/Constructive_Cryptography (AFP)
Session AFP/Game_Based_Crypto (AFP)
Session AFP/Free-Groups (AFP)
Session AFP/Locally-Nameless-Sigma (AFP)
Session AFP/Stern_Brocot (AFP)
Session HOL/HOL-Proofs-ex
Session Tools/Haskell
Session Doc/Intro (doc)
Session LCF/LCF
Session Doc/Logics (doc)
Session Doc/Nitpick (doc)
Session Tools/SML
Session Sequents/Sequents
Session Doc/Sledgehammer (doc)
Session Tools/Spec_Check
Session AFP/Regex_Equivalence (AFP)
Session Doc/System (doc)
Session ZF/ZF (main timing)
Session Doc/Logics_ZF (doc)
Session ZF/ZF-AC
Session ZF/ZF-Coind
Session ZF/ZF-Constructible
Session ZF/ZF-IMP
Session ZF/ZF-Induct
Session ZF/ZF-UNITY (timing)
Session ZF/ZF-Resid
Session ZF/ZF-ex
Building HOL-Analysis ...
Building LLL_Basis_Reduction ...
Running Perron_Frobenius ...
Building Coinductive ...
Running Higher_Order_Terms ...
Running Lambda_Free_EPO ...
Running Lambda_Free_KBOs ...
Running Lambda_Free_RPOs ...
Running Functional_Ordered_Resolution_Prover ...
Running Noninterference_Generic_Unwinding ...
HOL-Analysis: theory HOL-Library.Cancellation
HOL-Analysis: theory HOL-Library.Disjoint_Sets
HOL-Analysis: theory HOL-Library.FuncSet
HOL-Analysis: theory HOL-Library.Infinite_Set
Higher_Order_Terms: theory HOL-Library.Adhoc_Overloading
Higher_Order_Terms: theory HOL-Library.Conditional_Parametricity
Higher_Order_Terms: theory HOL-Library.AList
Higher_Order_Terms: theory HOL-Library.Nat_Bijection
HOL-Analysis: theory HOL-Library.Nat_Bijection
Coinductive: theory Coinductive.Resumption
Coinductive: theory HOL-Analysis.Inner_Product
Coinductive: theory HOL-Analysis.Abstract_Topology
Coinductive: theory HOL-Analysis.L2_Norm
Higher_Order_Terms: theory HOL-Library.Monad_Syntax
HOL-Analysis: theory HOL-Library.Old_Datatype
Higher_Order_Terms: theory HOL-Library.State_Monad
Noninterference_Generic_Unwinding: theory Noninterference_Generic_Unwinding.GenericUnwinding
Coinductive: theory HOL-Analysis.Product_Vector
Lambda_Free_EPO: theory HOL-Cardinals.Order_Union
Lambda_Free_EPO: theory Lambda_Free_RPOs.Lambda_Free_Util
Lambda_Free_RPOs: theory HOL-Cardinals.Order_Union
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Util
Higher_Order_Terms: theory HOL-Library.Old_Datatype
Lambda_Free_EPO: theory HOL-Cardinals.Wellorder_Extension
HOL-Analysis: theory HOL-Library.Phantom_Type
Higher_Order_Terms: theory List-Index.List_Index
HOL-Analysis: theory HOL-Library.Multiset
HOL-Analysis: theory HOL-Library.Product_Plus
Lambda_Free_RPOs: theory HOL-Cardinals.Wellorder_Extension
HOL-Analysis: theory HOL-Library.Product_Order
HOL-Analysis: theory HOL-Library.Set_Algebras
Perron_Frobenius: theory HOL-Eisbach.Eisbach
Perron_Frobenius: theory HOL-Analysis.Continuum_Not_Denumerable
Perron_Frobenius: theory HOL-Types_To_Sets.Types_To_Sets
Perron_Frobenius: theory HOL-Analysis.Abstract_Topology
HOL-Analysis: theory HOL-Library.Countable
HOL-Analysis: theory HOL-Analysis.Inner_Product
LLL_Basis_Reduction: theory LLL_Basis_Reduction.More_IArray
LLL_Basis_Reduction: theory LLL_Basis_Reduction.Cost
LLL_Basis_Reduction: theory LLL_Basis_Reduction.List_Representation
LLL_Basis_Reduction: theory Algebraic_Numbers.Bivariate_Polynomials
Higher_Order_Terms: theory HOL-Library.Countable
Perron_Frobenius: theory HOL-Analysis.Inner_Product
HOL-Analysis: theory HOL-Library.Cardinality
Coinductive: theory Coinductive.Coinductive_Nat
Perron_Frobenius: theory HOL-Analysis.L2_Norm
Lambda_Free_EPO: theory Lambda_Free_RPOs.Infinite_Chain
Coinductive: theory HOL-Analysis.Elementary_Topology
Lambda_Free_EPO: theory Lambda_Free_RPOs.Lambda_Free_Term
Perron_Frobenius: theory HOL-Analysis.Operator_Norm
Coinductive: theory HOL-Analysis.Euclidean_Space
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Infinite_Chain
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_Term
Lambda_Free_EPO: theory Lambda_Free_RPOs.Extension_Orders
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Extension_Orders
Perron_Frobenius: theory HOL-Analysis.Product_Vector
Perron_Frobenius: theory Polynomial_Factorization.Polynomial_Divisibility
Perron_Frobenius: theory Sturm_Sequences.Misc_Polynomial
Perron_Frobenius: theory Sturm_Sequences.Sturm_Library
Perron_Frobenius: theory Sturm_Sequences.Sturm_Theorem
LLL_Basis_Reduction: theory Algebraic_Numbers.Resultant
Perron_Frobenius: theory HOL-Analysis.Norm_Arith
Coinductive: theory Coinductive.Coinductive_List
HOL-Analysis: theory HOL-Analysis.L2_Norm
HOL-Analysis: theory HOL-Analysis.Operator_Norm
HOL-Analysis: theory HOL-Library.Countable_Set
HOL-Analysis: theory HOL-Analysis.Poly_Roots
HOL-Analysis: theory HOL-Library.Numeral_Type
HOL-Analysis: theory HOL-Analysis.Product_Vector
Perron_Frobenius: theory Polynomial_Factorization.Square_Free_Factorization
Higher_Order_Terms: theory HOL-Library.FSet
Perron_Frobenius: theory HOL-Analysis.Elementary_Topology
HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Fun_More
Functional_Ordered_Resolution_Prover: theory Deriving.Generator_Aux
Functional_Ordered_Resolution_Prover: theory Deriving.Comparator
Functional_Ordered_Resolution_Prover: theory Deriving.Derive_Manager
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Transitive_Closure_More
Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Order_Union
Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Generator
Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Wellorder_Extension
Coinductive: theory HOL-Analysis.Linear_Algebra
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Option_Monad
HOL-Analysis: theory HOL-Library.Set_Idioms
HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable
Perron_Frobenius: theory HOL-Analysis.Euclidean_Space
Coinductive: theory HOL-Analysis.Norm_Arith
HOL-Analysis: theory HOL-Analysis.Abstract_Topology
Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Instances
HOL-Analysis: theory HOL-Analysis.Elementary_Topology
Functional_Ordered_Resolution_Prover: theory Nested_Multisets_Ordinals.Multiset_More
Coinductive: theory HOL-Analysis.Abstract_Topology_2
Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Seq
Functional_Ordered_Resolution_Prover: theory Deriving.Compare
Functional_Ordered_Resolution_Prover: theory Deriving.Comparator_Generator
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Encoding
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_App
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Std
Lambda_Free_EPO: theory Lambda_Free_EPO.Embeddings
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Seq_More
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Clausal_Logic
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unifiers
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term_Pair_Multiset
LLL_Basis_Reduction: theory LLL_Basis_Reduction.Missing_Lemmas
Perron_Frobenius: theory HOL-Analysis.Abstract_Limits
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Subsumption
Lambda_Free_KBOs: theory HOL-Cardinals.Order_Union
Lambda_Free_KBOs: theory Abstract-Rewriting.Seq
Lambda_Free_KBOs: theory HOL-Library.While_Combinator
Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Free_Util
HOL-Analysis: theory HOL-Analysis.Euclidean_Space
Perron_Frobenius: theory Sturm_Sequences.Sturm_Method
Lambda_Free_KBOs: theory HOL-Cardinals.Wellorder_Extension
Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits
Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Generator
Lambda_Free_KBOs: theory Matrix.Utility
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPO_Optim
Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits_Bit
Lambda_Free_KBOs: theory Regular-Sets.Regular_Set
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Herbrand_Interpretation
HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring
Functional_Ordered_Resolution_Prover: theory HOL-Word.Misc_Numeric
Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Instances
Perron_Frobenius: theory HOL-Analysis.Abstract_Topology_2
Functional_Ordered_Resolution_Prover: theory HOL-Word.Bit_Representation
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Ground_Resolution_Model
Coinductive: theory HOL-Analysis.Connected
Coinductive: theory HOL-Analysis.Elementary_Metric_Spaces
Lambda_Free_RPOs: theory Lambda_Free_RPOs.Lambda_Free_RPOs
Perron_Frobenius: theory Rank_Nullity_Theorem.Dual_Order
Lambda_Free_KBOs: theory Lambda_Free_RPOs.Infinite_Chain
Perron_Frobenius: theory HOL-Analysis.Finite_Cartesian_Product
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Inference_System
Lambda_Free_KBOs: theory Lambda_Free_RPOs.Extension_Orders
Perron_Frobenius: theory HOL-Analysis.Linear_Algebra
Functional_Ordered_Resolution_Prover: theory HOL-Word.Word_Miscellaneous
Functional_Ordered_Resolution_Prover: theory HOL-Word.Bits_Int
Lambda_Free_EPO: theory Lambda_Free_EPO.Chop
Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Free_Term
Functional_Ordered_Resolution_Prover: theory HOL-Word.Misc_Typedef
Functional_Ordered_Resolution_Prover: theory Deriving.Countable_Generator
Higher_Order_Terms: theory HOL-Library.Finite_Map
Lambda_Free_EPO: theory Lambda_Free_EPO.Lambda_Free_EPO
Functional_Ordered_Resolution_Prover: theory Coinductive.Coinductive_Nat
HOL-Analysis: theory HOL-Library.Permutations
Functional_Ordered_Resolution_Prover: theory Matrix.Utility
Functional_Ordered_Resolution_Prover: theory Polynomial_Factorization.Missing_List
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Ordered_Ground_Resolution
Perron_Frobenius: theory HOL-Analysis.Convex
Perron_Frobenius: theory HOL-Analysis.Connected
Perron_Frobenius: theory HOL-Analysis.Elementary_Metric_Spaces
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Unordered_Ground_Resolution
Functional_Ordered_Resolution_Prover: theory HOL-Word.Bool_List_Representation
Functional_Ordered_Resolution_Prover: theory Coinductive.Coinductive_List
HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product
Lambda_Free_KBOs: theory Regular-Sets.Regular_Exp
Functional_Ordered_Resolution_Prover: theory Open_Induction.Restricted_Predicates
Perron_Frobenius: theory HOL-Analysis.Cartesian_Space
HOL-Analysis: theory HOL-Analysis.Linear_Algebra
Functional_Ordered_Resolution_Prover: theory Native_Word.More_Bits_Int
Functional_Ordered_Resolution_Prover: theory HOL-Word.Word
HOL-Analysis: theory HOL-Analysis.Abstract_Limits
Coinductive: theory HOL-Analysis.Elementary_Normed_Spaces
Lambda_Free_KBOs: theory Lambda_Free_RPOs.Lambda_Encoding
HOL-Analysis: theory HOL-Library.Discrete
HOL-Analysis: theory HOL-Library.Indicator_Function
HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2
Perron_Frobenius: theory HOL-Analysis.Elementary_Normed_Spaces
HOL-Analysis: theory HOL-Analysis.Convex
Perron_Frobenius: theory HOL-Analysis.Determinants
Coinductive: theory HOL-Analysis.Topology_Euclidean_Space
Coinductive: theory Coinductive.Coinductive_List_Prefix
Perron_Frobenius: theory HOL-Analysis.Topology_Euclidean_Space
Coinductive: theory Coinductive.Hamming_Stream
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Map2
HOL-Analysis: theory HOL-Analysis.Cartesian_Space
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Abstract_Substitution
Coinductive: theory Coinductive.Koenigslemma
Lambda_Free_KBOs: theory Regular-Sets.NDerivative
Lambda_Free_KBOs: theory Regular-Sets.Relation_Interpretation
Coinductive: theory Coinductive.LMirror
Coinductive: theory Coinductive.Lazy_LList
Coinductive: theory Coinductive.Quotient_Coinductive_List
HOL-Analysis: theory HOL-Analysis.Connected
Functional_Ordered_Resolution_Prover: theory Native_Word.Bits_Integer
Coinductive: theory Coinductive.TLList
Coinductive: theory Coinductive.Coinductive_Stream
HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces
HOL-Analysis: theory HOL-Library.Liminf_Limsup
HOL-Analysis: theory HOL-Analysis.Determinants
HOL-Analysis: theory HOL-Library.Nonpos_Ints
Coinductive: theory HOL-Analysis.Extended_Real_Limits
HOL-Analysis: theory HOL-Library.Order_Continuity
HOL-Analysis: theory HOL-Library.Periodic_Fun
HOL-Analysis: theory HOL-Library.Sum_of_Squares
HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm
Perron_Frobenius: theory HOL-Analysis.Convex_Euclidean_Space
Perron_Frobenius: theory HOL-Analysis.Extended_Real_Limits
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Set
HOL-Analysis: theory HOL-Library.Extended_Nat
HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/outline.pdf
Lambda_Free_RPOs FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Lambda_Free_RPOs)
assumes "rpo_optim ground_heads_var (>\<^sub>s) extf arity_sym arity_var"
Proofs for inductive predicate(s) "gt"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
locale rpo
fixes ground_heads_var :: "'v \ 's set"
and
gt_sym :: "'s \ 's \ bool"
(infix \>\<^sub>s\ 50)
and
extf ::
"'s \ (('s, 'v) tm
\ ('s, 'v) tm \ bool)
\ ('s, 'v) tm list
\ ('s, 'v) tm list \ bool"
and arity_sym :: "'s \ enat"
and arity_var :: "'v \ enat"
assumes "rpo ground_heads_var (>\<^sub>s) extf arity_sym arity_var"
### theory "Lambda_Free_RPOs.Lambda_Free_RPO_Optim"
### 0.788s elapsed time, 2.928s cpu time, 0.000s GC time
Loading theory "Lambda_Free_RPOs.Lambda_Free_RPOs"
locale simple_rpo_instances
### theory "Lambda_Free_RPOs.Lambda_Free_RPOs"
### 1.133s elapsed time, 4.528s cpu time, 0.000s GC time
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/outline -o pdf -n outline -t /proof,/ML
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_RPOs/document -o pdf -n document
*** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy")
Coinductive: theory Coinductive.CCPO_Topology
Lambda_Free_KBOs: theory Regular-Sets.Equivalence_Checking
Coinductive: theory Coinductive.Lazy_TLList
Perron_Frobenius: theory HOL-Analysis.Function_Topology
Lambda_Free_KBOs: theory Regular-Sets.Regexp_Method
HOL-Analysis: theory HOL-Library.Extended_Real
Coinductive: theory Coinductive.Quotient_TLList
Perron_Frobenius: theory HOL-Analysis.Starlike
Perron_Frobenius: theory HOL-Analysis.Summation_Tests
Coinductive: theory Coinductive.TLList_CCPO
Functional_Ordered_Resolution_Prover: theory Native_Word.Word_Misc
Lambda_Free_KBOs: theory Abstract-Rewriting.Abstract_Rewriting
Coinductive: theory Coinductive.LList_CCPO_Topology
Coinductive: theory Coinductive.Coinductive
Coinductive: theory Coinductive.TLList_CCPO_Examples
Perron_Frobenius: theory HOL-Analysis.Uniform_Limit
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Exp
HOL-Analysis: theory HOL-Analysis.Norm_Arith
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Lazy_List_Liminf
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Lazy_List_Chain
Perron_Frobenius: theory HOL-Analysis.Bounded_Linear_Function
HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space
Coinductive: theory Coinductive.Coinductive_Examples
Lambda_Free_KBOs: theory Abstract-Rewriting.SN_Orders
Perron_Frobenius: theory HOL-Analysis.Continuous_Extension
Perron_Frobenius: theory HOL-Analysis.Path_Connected
Higher_Order_Terms: theory Higher_Order_Terms.Term_Utils
Higher_Order_Terms: theory Higher_Order_Terms.Find_First
Higher_Order_Terms: theory Higher_Order_Terms.Disjoint_Sets
HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real
Lambda_Free_KBOs: theory Polynomials.Polynomials
Higher_Order_Terms: theory Deriving.Derive_Manager
Higher_Order_Terms: theory HOL-Library.Cancellation
Higher_Order_Terms: theory HOL-Library.Infinite_Set
Higher_Order_Terms: theory HOL-ex.Unification
Higher_Order_Terms: theory Datatype_Order_Generator.Derive_Aux
Higher_Order_Terms: theory Datatype_Order_Generator.Order_Generator
Higher_Order_Terms: theory HOL-Library.Countable_Set
Functional_Ordered_Resolution_Prover: theory Regular-Sets.NDerivative
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Relation_Interpretation
Higher_Order_Terms: theory Higher_Order_Terms.Fresh_Monad
Higher_Order_Terms: theory HOL-Library.Multiset
Higher_Order_Terms: theory Higher_Order_Terms.Name
Higher_Order_Terms: theory HOL-Library.Countable_Complete_Lattices
HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Function_Topology
HOL-Analysis: theory HOL-Computational_Algebra.Primes
Perron_Frobenius: theory HOL-Analysis.Homotopy
Higher_Order_Terms: theory Higher_Order_Terms.Fresh_Class
HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series
HOL-Analysis: theory HOL-Analysis.Product_Topology
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding
Noninterference_Generic_Unwinding FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Noninterference_Generic_Unwinding)
Loading theory "Noninterference_Generic_Unwinding.GenericUnwinding"
Proofs for inductive predicate(s) "rel_induct_auxp"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
*** Failed to apply initial proof method (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"):
*** goal (1 subgoal):
*** 1. unaffected_domains I D {D y} (ys @ [y']) \ {}
*** At command "proof" (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy")
*** Failed to apply initial proof method (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"):
*** goal (1 subgoal):
*** 1. unaffected_domains I D {D y} (zs @ [z]) \ {}
*** At command "proof" (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy")
### theory "Noninterference_Generic_Unwinding.GenericUnwinding"
### 2.071s elapsed time, 4.940s cpu time, 0.156s GC time
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/outline -o pdf -n outline -t /proof,/ML
*** Failed to build document in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/outline"
*** Failed to apply initial proof method (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"):
*** goal (1 subgoal):
*** 1. unaffected_domains I D {D y} (zs @ [z]) \ {}
*** At command "proof" (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy")
*** Failed to apply initial proof method (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"):
*** goal (1 subgoal):
*** 1. unaffected_domains I D {D y} (ys @ [y']) \ {}
*** At command "proof" (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy")
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/outline.pdf
Lambda_Free_EPO FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Lambda_Free_EPO)
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_chop"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_diff"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_same"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
### theory "Lambda_Free_EPO.Lambda_Free_EPO"
### 1.224s elapsed time, 4.532s cpu time, 0.180s GC time
\?X \ ?C; ?A \ ?X\
\ ?A \ \ ?C
?P ?a \ ?a \ {x. ?P x}
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_EPO/outline -o pdf -n outline -t /proof,/ML
*** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy")
HOL-Analysis: theory HOL-Analysis.Sigma_Algebra
Higher_Order_Terms: theory Higher_Order_Terms.Term_Class
HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits
HOL-Analysis: theory HOL-Analysis.Starlike
Higher_Order_Terms: theory HOL-Library.Order_Continuity
HOL-Analysis: theory HOL-Analysis.Summation_Tests
Higher_Order_Terms: theory HOL-Library.Extended_Nat
Perron_Frobenius: theory HOL-Analysis.Homeomorphism
LLL_Basis_Reduction: theory LLL_Basis_Reduction.Norms
Functional_Ordered_Resolution_Prover: theory Native_Word.Uint32
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Equivalence_Checking
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regexp_Method
Perron_Frobenius: theory HOL-Analysis.Brouwer_Fixpoint
HOL-Analysis: theory HOL-Analysis.Uniform_Limit
HOL-Analysis: theory HOL-Analysis.Measurable
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Proving_Process
Higher_Order_Terms: theory HOL-Library.Multiset_Order
Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Abstract_Rewriting
HOL-Analysis: theory HOL-Analysis.Continuous_Extension
HOL-Analysis: theory HOL-Analysis.Path_Connected
Higher_Order_Terms: theory Lambda_Free_RPOs.Lambda_Free_Util
HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function
HOL-Analysis: theory HOL-Analysis.Measure_Space
Functional_Ordered_Resolution_Prover: theory Collections.HashCode
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Util
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.Standard_Redundancy
Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Generator
Higher_Order_Terms: theory Lambda_Free_RPOs.Lambda_Free_Term
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.FO_Ordered_Resolution
Perron_Frobenius: theory HOL-Analysis.Derivative
HOL-Analysis: theory HOL-Analysis.T1_Spaces
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_App
HOL-Analysis: theory HOL-Analysis.Tagged_Division
Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Instances
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Matching
Functional_Ordered_Resolution_Prover: theory Deriving.Derive
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Std
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Unification
HOL-Analysis: theory HOL-Analysis.Homotopy
Higher_Order_Terms: theory Higher_Order_Terms.Nterm
Higher_Order_Terms: theory Higher_Order_Terms.Term
HOL-Analysis: theory HOL-Analysis.Locally
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBO_Basic
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unification
Functional_Ordered_Resolution_Prover: theory Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover
Higher_Order_Terms: theory Higher_Order_Terms.Unification_Compat
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Encoding_KBO
Perron_Frobenius: theory HOL-Analysis.Cartesian_Euclidean_Space
Higher_Order_Terms: theory Higher_Order_Terms.Pats
HOL-Analysis: theory HOL-Analysis.Caratheodory
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Matching
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.IsaFoR_Term
Higher_Order_Terms: theory Higher_Order_Terms.Lambda_Free_Compat
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs
Higher_Order_Terms: theory Higher_Order_Terms.Term_to_Nterm
Perron_Frobenius: theory Rank_Nullity_Theorem.Mod_Type
HOL-Analysis: theory HOL-Analysis.Homeomorphism
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover
HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Executable_Subsumption
Perron_Frobenius: theory Rank_Nullity_Theorem.Miscellaneous
Lambda_Free_KBOs: theory Lambda_Free_KBOs.Lambda_Free_KBOs
HOL-Analysis: theory HOL-Analysis.Derivative
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover
HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems
HOL-Analysis: theory HOL-Analysis.Cross3
HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem
HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Polytope
HOL-Analysis: theory HOL-Analysis.Arcwise_Connected
HOL-Analysis: theory HOL-Analysis.Borel_Space
HOL-Analysis: theory HOL-Analysis.Lipschitz
HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
HOL-Analysis: theory HOL-Analysis.Regularity
LLL_Basis_Reduction: theory LLL_Basis_Reduction.Int_Rat_Operations
LLL_Basis_Reduction: theory HOL-Eisbach.Eisbach
LLL_Basis_Reduction: theory Perron_Frobenius.Bij_Nat
LLL_Basis_Reduction: theory Perron_Frobenius.Cancel_Card_Constraint
LLL_Basis_Reduction: theory HOL-Analysis.Abstract_Topology
LLL_Basis_Reduction: theory HOL-Analysis.Continuum_Not_Denumerable
LLL_Basis_Reduction: theory HOL-Analysis.Inner_Product
HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure
LLL_Basis_Reduction: theory HOL-Analysis.L2_Norm
LLL_Basis_Reduction: theory HOL-Analysis.Operator_Norm
LLL_Basis_Reduction: theory HOL-Analysis.Product_Vector
LLL_Basis_Reduction: theory HOL-Analysis.Norm_Arith
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/outline.pdf
Higher_Order_Terms FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Higher_Order_Terms)
### Introduced fixed type variable(s): 'd, 'e in "f__"
### Introduced fixed type variable(s): 'd in "X__"
### Introduced fixed type variable(s): 'd, 'e, 'f in "R__" or "S__"
### Introduced fixed type variable(s): 'd, 'e in "R__"
### Ignoring duplicate rewrite rule:
### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1)
### Ignoring duplicate rewrite rule:
### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1)
### Introduced fixed type variable(s): 'd in "z__"
### Introduced fixed type variable(s): 'd in "P__"
*** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy")
### Metis: Unused theorems: "Term_Class.list_comb_cond_inj_2"
### Metis: Unused theorems: "Term_Class.list_comb_cond_inj_1"
### Rule already declared as introduction (intro)
### \rel_option ?R ?x ?y;
### \a b. ?R a b \ rel_option ?R (?f a) (?g b)\
### \ rel_option ?R (?x \ ?f) (?y \ ?g)
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Higher_Order_Terms/outline -o pdf -n outline -t /proof,/ML
*** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy")
HOL-Analysis: theory HOL-Analysis.Embed_Measure
HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure
LLL_Basis_Reduction: theory HOL-Analysis.Elementary_Topology
LLL_Basis_Reduction: theory HOL-Analysis.Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Bochner_Integration
LLL_Basis_Reduction: theory HOL-Analysis.Abstract_Limits
LLL_Basis_Reduction: theory HOL-Analysis.Finite_Cartesian_Product
LLL_Basis_Reduction: theory HOL-Analysis.Linear_Algebra
LLL_Basis_Reduction: theory HOL-Analysis.Abstract_Topology_2
HOL-Analysis: theory HOL-Analysis.Complete_Measure
HOL-Analysis: theory HOL-Analysis.Radon_Nikodym
LLL_Basis_Reduction: theory HOL-Analysis.Convex
HOL-Analysis: theory HOL-Analysis.Set_Integral
HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure
LLL_Basis_Reduction: theory HOL-Analysis.Connected
HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum
LLL_Basis_Reduction: theory HOL-Analysis.Cartesian_Space
LLL_Basis_Reduction: theory HOL-Analysis.Elementary_Metric_Spaces
HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration
LLL_Basis_Reduction: theory HOL-Analysis.Determinants
LLL_Basis_Reduction: theory HOL-Analysis.Elementary_Normed_Spaces
LLL_Basis_Reduction: theory HOL-Analysis.Topology_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function
HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
HOL-Analysis: theory HOL-Analysis.Integral_Test
LLL_Basis_Reduction: theory HOL-Analysis.Convex_Euclidean_Space
LLL_Basis_Reduction: theory HOL-Analysis.Extended_Real_Limits
LLL_Basis_Reduction: theory HOL-Analysis.Function_Topology
HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics
LLL_Basis_Reduction: theory HOL-Analysis.Starlike
LLL_Basis_Reduction: theory HOL-Analysis.Summation_Tests
HOL-Analysis: theory HOL-Analysis.Improper_Integral
HOL-Analysis: theory HOL-Analysis.Interval_Integral
HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution
LLL_Basis_Reduction: theory HOL-Analysis.Uniform_Limit
HOL-Analysis: theory HOL-Analysis.Complex_Transcendental
LLL_Basis_Reduction: theory HOL-Analysis.Bounded_Linear_Function
LLL_Basis_Reduction: theory HOL-Analysis.Continuous_Extension
LLL_Basis_Reduction: theory HOL-Analysis.Path_Connected
HOL-Analysis: theory HOL-Analysis.Cauchy_Integral_Theorem
HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem
HOL-Analysis: theory HOL-Analysis.Infinite_Products
HOL-Analysis: theory HOL-Analysis.Further_Topology
HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers
LLL_Basis_Reduction: theory HOL-Analysis.Homotopy
HOL-Analysis: theory HOL-Analysis.Jordan_Curve
LLL_Basis_Reduction: theory HOL-Analysis.Homeomorphism
HOL-Analysis: theory HOL-Analysis.Conformal_Mappings
LLL_Basis_Reduction: theory HOL-Analysis.Brouwer_Fixpoint
HOL-Analysis: theory HOL-Analysis.FPS_Convergence
HOL-Analysis: theory HOL-Analysis.Great_Picard
HOL-Analysis: theory HOL-Analysis.Gamma_Function
LLL_Basis_Reduction: theory HOL-Analysis.Derivative
HOL-Analysis: theory HOL-Analysis.Riemann_Mapping
HOL-Analysis: theory HOL-Analysis.Winding_Numbers
LLL_Basis_Reduction: theory HOL-Analysis.Cartesian_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Ball_Volume
LLL_Basis_Reduction: theory Perron_Frobenius.HMA_Connect
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
LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_2
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/outline.pdf
Lambda_Free_KBOs FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Lambda_Free_KBOs)
Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_diff"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
Proofs for inductive predicate(s) "gt_same"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the induction rule ...
Proving the simplification rules ...
consts
subst_zpassign ::
"('v \ ('s, 'v) tm)
\ ('v pvar \ zhmultiset)
\ 'v pvar \ zhmultiset"
### theory "Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs"
### 4.081s elapsed time, 8.380s cpu time, 0.344s GC time
Loading theory "Lambda_Free_KBOs.Lambda_Free_KBOs"
locale simple_kbo_instances
### theory "Lambda_Free_KBOs.Lambda_Free_KBOs"
### 1.424s elapsed time, 2.980s cpu time, 0.276s GC time
Found termination order: "size <*mlex*> {}"
"(>\<^sub>h\<^sub>d)"
:: "('s, 'v) hd \ ('s, 'v) hd \ bool"
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/outline -o pdf -n outline -t /proof,/ML
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lambda_Free_KBOs/document -o pdf -n document
*** Failed to finish proof (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 160 of "$AFP/Lambda_Free_RPOs/Lambda_Free_Util.thy")
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/outline.pdf
Functional_Ordered_Resolution_Prover FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Functional_Ordered_Resolution_Prover)
compare_order: register types in class compare_order, options: (linorder) or ()
countable: register datatypes is class countable
equality: generate an equality function, options are () and (eq)
hash_code: generate a hash function, options are () and (hashcode)
hashable: register types in class hashable
linorder: register types in class linorder, options: (linorder) or ()
*** Failed to finish proof (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy")
### Ignoring duplicate rewrite rule:
### mset (filter ?P1 ?xs1) \ filter_mset ?P1 (mset ?xs1)
Testing conjecture with Quickcheck-narrowing...
[1 of 5] Compiling Data_Bits ( /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Data_Bits.hs.hs, /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Data_Bits.hs.o )
[2 of 5] Compiling Typerep ( /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Typerep.hs.hs, /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Typerep.hs.o )
[3 of 5] Compiling Generated_Code ( /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Generated_Code.hs, /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Generated_Code.o )
[4 of 5] Compiling Narrowing_Engine ( /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Narrowing_Engine.hs, /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Narrowing_Engine.o )
[5 of 5] Compiling Main ( /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Main.hs, /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/Main.o )
Linking /tmp/isabelle-jenkins/process5929168512801472241/Quickcheck_Narrowing4614754/isabelle_quickcheck_narrowing ...
Quickcheck found no counterexample.
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/outline -o pdf -n outline -t /proof,/ML
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover/document -o pdf -n document
*** Failed to finish proof (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy"):
*** goal (1 subgoal):
*** 1. \Q x z.
*** \x \ Q;
*** \y.
*** (y, f z) \ r \ y \ range f\
*** \ \z\Q.
*** \y.
*** (f y, f z) \ r \
*** y \ Q
*** At command "by" (line 78 of "$AFP/Functional_Ordered_Resolution_Prover/Deterministic_FO_Ordered_Resolution_Prover.thy")
Timing Coinductive (4 threads, 95.740s elapsed time, 334.604s cpu time, 15.216s GC time, factor 3.49)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Coinductive
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Coinductive/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Coinductive/outline.pdf
Finished Coinductive (0:02:06 elapsed time, 0:06:40 cpu time, factor 3.18)
Building DynamicArchitectures ...
Running Stream_Fusion_Code ...
Running Topology ...
Running Lazy-Lists-II ...
Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion
DynamicArchitectures: theory DynamicArchitectures.Configuration_Traces
Topology: theory Topology.Topology
Topology: theory Lazy-Lists-II.LList2
Lazy-Lists-II: theory Lazy-Lists-II.LList2
Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_List
DynamicArchitectures: theory DynamicArchitectures.Dynamic_Architecture_Calculus
Topology: theory Topology.LList_Topology
Timing Lazy-Lists-II (4 threads, 2.003s elapsed time, 5.212s cpu time, 0.236s GC time, factor 2.60)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lazy-Lists-II
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lazy-Lists-II/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lazy-Lists-II/outline.pdf
Finished Lazy-Lists-II (0:00:07 elapsed time, 0:00:15 cpu time, factor 2.19)
Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_LList
Timing Topology (4 threads, 4.952s elapsed time, 17.164s cpu time, 0.700s GC time, factor 3.47)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Topology
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Topology/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Topology/outline.pdf
Finished Topology (0:00:10 elapsed time, 0:00:27 cpu time, factor 2.71)
Stream_Fusion_Code: theory Stream_Fusion_Code.Stream_Fusion_Examples
LLL_Basis_Reduction: theory LLL_Basis_Reduction.Gram_Schmidt_Int
Timing Stream_Fusion_Code (4 threads, 11.653s elapsed time, 34.180s cpu time, 1.168s GC time, factor 2.93)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stream_Fusion_Code
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stream_Fusion_Code/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stream_Fusion_Code/outline.pdf
Finished Stream_Fusion_Code (0:00:17 elapsed time, 0:00:45 cpu time, factor 2.61)
Timing DynamicArchitectures (4 threads, 8.878s elapsed time, 30.092s cpu time, 0.624s GC time, factor 3.39)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DynamicArchitectures
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DynamicArchitectures/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/DynamicArchitectures/outline.pdf
Finished DynamicArchitectures (0:00:31 elapsed time, 0:01:09 cpu time, factor 2.21)
Running Architectural_Design_Patterns ...
Architectural_Design_Patterns: theory Architectural_Design_Patterns.Auxiliary
Architectural_Design_Patterns: theory Architectural_Design_Patterns.Singleton
Architectural_Design_Patterns: theory Architectural_Design_Patterns.RF_LTL
Architectural_Design_Patterns: theory Architectural_Design_Patterns.Publisher_Subscriber
Architectural_Design_Patterns: theory Architectural_Design_Patterns.Blockchain
Architectural_Design_Patterns: theory Architectural_Design_Patterns.Blackboard
Timing Architectural_Design_Patterns (4 threads, 23.787s elapsed time, 59.348s cpu time, 3.440s GC time, factor 2.50)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Architectural_Design_Patterns
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Architectural_Design_Patterns/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Architectural_Design_Patterns/outline.pdf
Finished Architectural_Design_Patterns (0:00:31 elapsed time, 0:01:12 cpu time, factor 2.32)
Perron_Frobenius: theory Perron_Frobenius.Cancel_Card_Constraint
Perron_Frobenius: theory Perron_Frobenius.Bij_Nat
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 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 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, 209.636s elapsed time, 716.348s cpu time, 27.796s GC time, factor 3.42)
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:37 elapsed time, 0:12:09 cpu time, factor 3.36)
LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL
LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Impl
LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Complexity
LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Number_Bounds
LLL_Basis_Reduction: theory LLL_Basis_Reduction.LLL_Certification
LLL_Basis_Reduction: theory LLL_Basis_Reduction.FPLLL_Solver
Timing LLL_Basis_Reduction (4 threads, 415.938s elapsed time, 1137.952s cpu time, 104.932s GC time, factor 2.74)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Basis_Reduction
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Basis_Reduction/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Basis_Reduction/outline.pdf
Finished LLL_Basis_Reduction (0:07:52 elapsed time, 0:20:38 cpu time, factor 2.62)
Running LLL_Factorization ...
LLL_Factorization: theory LLL_Factorization.Sub_Sums
LLL_Factorization: theory LLL_Factorization.Missing_Dvd_Int_Poly
LLL_Factorization: theory LLL_Factorization.Factor_Bound_2
LLL_Factorization: theory LLL_Factorization.LLL_Factorization_Impl
LLL_Factorization: theory LLL_Factorization.LLL_Factorization
LLL_Factorization: theory LLL_Factorization.Factorization_Algorithm_16_22
LLL_Factorization: theory LLL_Factorization.Modern_Computer_Algebra_Problem
Timing LLL_Factorization (4 threads, 47.586s elapsed time, 124.564s cpu time, 5.576s GC time, factor 2.62)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Factorization
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Factorization/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LLL_Factorization/outline.pdf
Finished LLL_Factorization (0:00:54 elapsed time, 0:02:16 cpu time, factor 2.50)
Timing HOL-Analysis (4 threads, 509.795s elapsed time, 1728.152s cpu time, 58.160s GC time, factor 3.39)
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:09:56 elapsed time, 0:30:58 cpu time, factor 3.11)
Building Ordinary_Differential_Equations ...
Building HOL-Probability ...
Running Smooth_Manifolds ...
Building Affine_Arithmetic ...
Building Echelon_Form ...
Building Dirichlet_Series ...
Building Count_Complex_Roots ...
Building E_Transcendental ...
Running QR_Decomposition ...
Running Gromov_Hyperbolicity ...
Smooth_Manifolds: theory HOL-Library.Function_Algebras
Smooth_Manifolds: theory HOL-Library.Quotient_Syntax
Smooth_Manifolds: theory HOL-Types_To_Sets.Prerequisites
Smooth_Manifolds: theory HOL-Types_To_Sets.Types_To_Sets
Ordinary_Differential_Equations: theory HOL-Decision_Procs.Dense_Linear_Order
Smooth_Manifolds: theory HOL-Library.Quotient_Set
HOL-Probability: theory HOL-Library.AList
Ordinary_Differential_Equations: theory HOL-Library.Code_Abstract_Nat
Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Int
HOL-Probability: theory HOL-Library.Adhoc_Overloading
Ordinary_Differential_Equations: theory HOL-Word.Bits
HOL-Probability: theory HOL-Library.Conditional_Parametricity
HOL-Probability: theory HOL-Library.Lattice_Syntax
HOL-Probability: theory HOL-Library.Complete_Partial_Order2
Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Nat
Echelon_Form: theory HOL-Computational_Algebra.Fraction_Field
Echelon_Form: theory HOL-Library.Bit
Echelon_Form: theory HOL-Library.Code_Abstract_Nat
Echelon_Form: theory HOL-Library.Code_Target_Int
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-Word.Misc_Numeric
HOL-Probability: theory HOL-Library.Monad_Syntax
Affine_Arithmetic: theory HOL-Library.Adhoc_Overloading
Echelon_Form: theory HOL-Library.Code_Target_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
Count_Complex_Roots: theory HOL-Computational_Algebra.Field_as_Ring
Ordinary_Differential_Equations: theory HOL-Word.Bit_Representation
Ordinary_Differential_Equations: theory HOL-Library.Diagonal_Subsequence
HOL-Probability: theory HOL-Library.Mapping
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
Ordinary_Differential_Equations: theory HOL-Library.Code_Target_Numeral
Echelon_Form: theory HOL-Library.Function_Algebras
Affine_Arithmetic: theory HOL-Library.Monad_Syntax
Ordinary_Differential_Equations: theory HOL-Library.Lattice_Algebras
Smooth_Manifolds: theory HOL-Types_To_Sets.Group_On_With
Gromov_Hyperbolicity: theory HOL-Library.Cardinal_Notations
Echelon_Form: theory HOL-Library.Code_Target_Numeral
Affine_Arithmetic: theory HOL-Library.Bit
Affine_Arithmetic: theory Deriving.Equality_Generator
Gromov_Hyperbolicity: theory HOL-Library.Code_Abstract_Nat
Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Int
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
Ordinary_Differential_Equations: theory HOL-Library.Log_Nat
Echelon_Form: theory HOL-Library.IArray
Dirichlet_Series: theory HOL-Computational_Algebra.Fraction_Field
Dirichlet_Series: theory HOL-Computational_Algebra.Group_Closure
Dirichlet_Series: theory HOL-Library.Adhoc_Overloading
Dirichlet_Series: theory HOL-Library.BNF_Corec
Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Nat
Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial
Echelon_Form: theory HOL-Library.More_List
HOL-Probability: theory HOL-Library.Stream
Dirichlet_Series: theory HOL-Library.Monad_Syntax
Gromov_Hyperbolicity: theory HOL-Library.Lattice_Algebras
Gromov_Hyperbolicity: theory HOL-Cardinals.Wellfounded_More
Dirichlet_Series: theory HOL-Computational_Algebra.Nth_Powers
Ordinary_Differential_Equations: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Relation
Echelon_Form: theory Gauss_Jordan.Code_Bit
Echelon_Form: theory Gauss_Jordan.Code_Set
Gromov_Hyperbolicity: theory HOL-Library.Code_Target_Numeral
E_Transcendental: theory HOL-Number_Theory.Eratosthenes
E_Transcendental: theory HOL-Computational_Algebra.Polynomial
Echelon_Form: theory HOL-Computational_Algebra.Field_as_Ring
Echelon_Form: theory HOL-Computational_Algebra.Polynomial
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Bounded_Linear_Operator
Gromov_Hyperbolicity: theory HOL-Library.Log_Nat
Ordinary_Differential_Equations: theory HOL-Word.Bits_Int
QR_Decomposition: theory Deriving.Derive_Manager
QR_Decomposition: theory Deriving.Generator_Aux
QR_Decomposition: theory HOL-Library.Bit
QR_Decomposition: theory Real_Impl.Real_Impl_Auxiliary
Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Embedding
Affine_Arithmetic: theory Deriving.Equality_Instances
QR_Decomposition: theory HOL-Library.Code_Abstract_Nat
Dirichlet_Series: theory HOL-Computational_Algebra.Squarefree
Affine_Arithmetic: theory HOL-Library.Boolean_Algebra
QR_Decomposition: theory HOL-Library.Code_Target_Int
Affine_Arithmetic: theory HOL-Library.Permutation
QR_Decomposition: theory HOL-Library.Code_Target_Nat
Count_Complex_Roots: theory HOL-Eisbach.Eisbach_Tools
Count_Complex_Roots: theory Winding_Number_Eval.Missing_Analysis
Affine_Arithmetic: theory Deriving.Compare
Gromov_Hyperbolicity: theory Ergodic_Theory.Fekete
QR_Decomposition: theory HOL-Library.Function_Algebras
Affine_Arithmetic: theory Deriving.Comparator_Generator
QR_Decomposition: theory HOL-Library.IArray
E_Transcendental: theory HOL-Number_Theory.Fib
Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On_With
Affine_Arithmetic: theory HOL-Library.Char_ord
Count_Complex_Roots: theory Winding_Number_Eval.Missing_Topology
QR_Decomposition: theory HOL-Library.Code_Target_Numeral
HOL-Probability: theory HOL-Library.Rewrite
Dirichlet_Series: theory HOL-Number_Theory.Cong
Gromov_Hyperbolicity: theory HOL-Cardinals.Wellorder_Constructions
Dirichlet_Series: theory HOL-Library.Code_Abstract_Nat
Dirichlet_Series: theory HOL-Library.Code_Target_Nat
Echelon_Form: theory HOL-Computational_Algebra.Normalized_Fraction
Affine_Arithmetic: theory HOL-Library.Code_Abstract_Nat
QR_Decomposition: theory Gauss_Jordan.Code_Set
Count_Complex_Roots: theory HOL-Computational_Algebra.Normalized_Fraction
Echelon_Form: theory Gauss_Jordan.IArray_Addenda
Affine_Arithmetic: theory HOL-Library.Code_Target_Nat
QR_Decomposition: theory Cauchy.CauchysMeanTheorem
Echelon_Form: theory Cayley_Hamilton.Square_Matrix
E_Transcendental: theory HOL-Number_Theory.Prime_Powers
QR_Decomposition: theory HOL-Library.Code_Real_Approx_By_Float
QR_Decomposition: theory Gauss_Jordan.Code_Bit
Dirichlet_Series: theory HOL-Library.Code_Target_Int
QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
HOL-Probability: theory HOL-Library.AList_Mapping
E_Transcendental: theory HOL-Number_Theory.Mod_Exp
E_Transcendental: theory HOL-Algebra.Order
Dirichlet_Series: theory HOL-Computational_Algebra.Normalized_Fraction
Affine_Arithmetic: theory HOL-Library.Code_Target_Int
HOL-Probability: theory HOL-Library.Sublist
Affine_Arithmetic: theory HOL-Library.Mapping
Dirichlet_Series: theory HOL-Library.Code_Target_Numeral
QR_Decomposition: theory Rank_Nullity_Theorem.Dual_Order
Dirichlet_Series: theory HOL-Algebra.Congruence
Affine_Arithmetic: theory HOL-Library.Code_Target_Numeral
Echelon_Form: theory Rank_Nullity_Theorem.Dual_Order
QR_Decomposition: theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell
QR_Decomposition: theory Rank_Nullity_Theorem.Mod_Type
QR_Decomposition: theory QR_Decomposition.IArray_Addenda_QR
HOL-Probability: theory HOL-Library.Tree
QR_Decomposition: theory Show.Show
QR_Decomposition: theory Sqrt_Babylonian.Log_Impl
HOL-Probability: theory HOL-Library.FSet
Affine_Arithmetic: theory HOL-Library.Type_Length
Echelon_Form: theory Rank_Nullity_Theorem.Mod_Type
Affine_Arithmetic: theory Deriving.Compare_Generator
E_Transcendental: theory HOL-Number_Theory.Totient
QR_Decomposition: theory Sqrt_Babylonian.NthRoot_Impl
Affine_Arithmetic: theory HOL-Library.RBT_Impl
Dirichlet_Series: theory HOL-Library.Function_Algebras
Gromov_Hyperbolicity: theory HOL-Cardinals.Cardinal_Order_Relation
Ordinary_Differential_Equations: theory HOL-Word.Bool_List_Representation
Dirichlet_Series: theory HOL-Library.More_List
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Vector_Derivative_On
Smooth_Manifolds: theory HOL-Types_To_Sets.Linear_Algebra_On
Dirichlet_Series: theory HOL-Library.Power_By_Squaring
Ordinary_Differential_Equations: theory Triangle.Angles
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Gronwall
Affine_Arithmetic: theory Deriving.Compare_Instances
HOL-Probability: theory HOL-Library.Diagonal_Subsequence
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Interval_Integral_HK
HOL-Probability: theory HOL-Library.Multiset_Permutations
Ordinary_Differential_Equations: theory Triangle.Triangle
Dirichlet_Series: theory HOL-Library.Stirling
Dirichlet_Series: theory HOL-Number_Theory.Mod_Exp
Ordinary_Differential_Equations: theory List-Index.List_Index
Affine_Arithmetic: theory HOL-Word.Bits
HOL-Probability: theory HOL-Library.Linear_Temporal_Logic_on_Streams
Affine_Arithmetic: theory HOL-Word.Misc_Numeric
E_Transcendental: theory HOL-Algebra.Lattice
Affine_Arithmetic: theory HOL-Word.Bits_Bit
Affine_Arithmetic: theory HOL-Word.Bit_Representation
Dirichlet_Series: theory HOL-Algebra.Order
QR_Decomposition: theory Sqrt_Babylonian.Sqrt_Babylonian
Dirichlet_Series: theory HOL-Number_Theory.Eratosthenes
QR_Decomposition: theory Show.Show_Instances
Affine_Arithmetic: theory HOL-Word.Word_Miscellaneous
QR_Decomposition: theory Show.Show_Real
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Library_Complements
Affine_Arithmetic: theory HOL-Word.Misc_Typedef
Dirichlet_Series: theory HOL-Real_Asymp.Inst_Existentials
Dirichlet_Series: theory Bernoulli.Bernoulli
Affine_Arithmetic: theory Deriving.Countable_Generator
Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial
Affine_Arithmetic: theory HOL-Word.Bits_Int
Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Integer
QR_Decomposition: theory Real_Impl.Prime_Product
Affine_Arithmetic: theory HOL-Library.Lattice_Algebras
Dirichlet_Series: theory Bernoulli.Bernoulli_FPS
QR_Decomposition: theory Real_Impl.Real_Impl
HOL-Probability: theory HOL-Probability.Discrete_Topology
QR_Decomposition: theory Rank_Nullity_Theorem.Miscellaneous
Affine_Arithmetic: theory HOL-Library.Log_Nat
HOL-Probability: theory HOL-Probability.Essential_Supremum
E_Transcendental: theory HOL-Algebra.Complete_Lattice
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
HOL-Probability: theory HOL-Probability.Probability_Measure
Ordinary_Differential_Equations: theory HOL-Library.Float
Dirichlet_Series: theory HOL-Algebra.Lattice
Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise
HOL-Probability: theory HOL-Probability.Stopping_Time
Echelon_Form: theory Rank_Nullity_Theorem.Miscellaneous
HOL-Probability: theory HOL-Probability.Tree_Space
Gromov_Hyperbolicity: theory HOL-Library.Float
QR_Decomposition: theory Real_Impl.Real_Unique_Impl
Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_Vector
Affine_Arithmetic: theory HOL-Word.Bool_List_Representation
Dirichlet_Series: theory HOL-Library.Going_To_Filter
E_Transcendental: theory HOL-Algebra.Group
Dirichlet_Series: theory HOL-Library.Landau_Symbols
Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Strict
Dirichlet_Series: theory HOL-Algebra.Complete_Lattice
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Eexp_Eln
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Hausdorff_Distance
Affine_Arithmetic: theory Native_Word.More_Bits_Int
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Isometries
HOL-Probability: theory HOL-Library.Finite_Map
HOL-Probability: theory HOL-Probability.Conditional_Expectation
QR_Decomposition: theory Gauss_Jordan.Code_Matrix
QR_Decomposition: theory Gauss_Jordan.Rref
Affine_Arithmetic: theory HOL-Word.Word
Echelon_Form: theory Gauss_Jordan.Code_Matrix
Echelon_Form: theory Gauss_Jordan.Rref
HOL-Probability: theory HOL-Probability.Distribution_Functions
QR_Decomposition: theory Rank_Nullity_Theorem.Fundamental_Subspaces
QR_Decomposition: theory Gauss_Jordan.Elementary_Operations
QR_Decomposition: theory QR_Decomposition.Generalizations2
QR_Decomposition: theory Rank_Nullity_Theorem.Dim_Formula
Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation_Bounds
Ordinary_Differential_Equations: theory Affine_Arithmetic.Executable_Euclidean_Space
HOL-Probability: theory HOL-Probability.Weak_Convergence
Dirichlet_Series: theory HOL-Algebra.Group
Echelon_Form: theory Rank_Nullity_Theorem.Fundamental_Subspaces
HOL-Probability: theory HOL-Probability.Giry_Monad
QR_Decomposition: theory Gauss_Jordan.Rank
Echelon_Form: theory Gauss_Jordan.Elementary_Operations
HOL-Probability: theory HOL-Probability.Helly_Selection
Echelon_Form: theory Rank_Nullity_Theorem.Dim_Formula
Echelon_Form: theory Gauss_Jordan.Rank
Gromov_Hyperbolicity: theory HOL-Decision_Procs.Approximation_Bounds
E_Transcendental: theory HOL-Algebra.Coset
QR_Decomposition: theory QR_Decomposition.Matrix_To_IArray_QR
E_Transcendental: theory HOL-Algebra.FiniteProduct
QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan
Affine_Arithmetic: theory Native_Word.Bits_Integer
Affine_Arithmetic: theory HOL-Library.Float
Echelon_Form: theory Gauss_Jordan.Matrix_To_IArray
Echelon_Form: theory Gauss_Jordan.Gauss_Jordan
E_Transcendental: theory HOL-Algebra.Ring
Count_Complex_Roots: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Count_Complex_Roots: theory HOL-Computational_Algebra.Polynomial_Factorial
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Metric_Completion
Echelon_Form: theory HOL-Computational_Algebra.Polynomial_Factorial
Echelon_Form: theory Cayley_Hamilton.Cayley_Hamilton
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Gromov_Hyperbolicity
E_Transcendental: theory HOL-Algebra.Generated_Groups
Dirichlet_Series: theory Bernoulli.Periodic_Bernpoly
QR_Decomposition: theory Gauss_Jordan.Linear_Maps
Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin
Dirichlet_Series: theory HOL-Number_Theory.Fib
Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_IArrays
Echelon_Form: theory Gauss_Jordan.Linear_Maps
Dirichlet_Series: theory HOL-Algebra.Coset
Dirichlet_Series: theory HOL-Algebra.FiniteProduct
HOL-Probability: theory HOL-Probability.Probability_Mass_Function
HOL-Probability: theory HOL-Probability.Projective_Family
QR_Decomposition: theory Gauss_Jordan.Gauss_Jordan_PA
Affine_Arithmetic: theory Affine_Arithmetic.Optimize_Float
Dirichlet_Series: theory HOL-Algebra.Ring
Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA
Ordinary_Differential_Equations: theory HOL-Decision_Procs.Approximation
HOL-Probability: theory HOL-Probability.Infinite_Product_Measure
Affine_Arithmetic: theory Affine_Arithmetic.Float_Real
Affine_Arithmetic: theory HOL-Decision_Procs.Approximation_Bounds
Gromov_Hyperbolicity: theory HOL-Decision_Procs.Approximation
QR_Decomposition: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
QR_Decomposition: theory Gauss_Jordan.Determinants2
Affine_Arithmetic: theory Native_Word.Word_Misc
QR_Decomposition: theory Gauss_Jordan.Inverse
Echelon_Form: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
QR_Decomposition: theory Gauss_Jordan.System_Of_Equations
Echelon_Form: theory Gauss_Jordan.Determinants2
Echelon_Form: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays
Dirichlet_Series: theory HOL-Number_Theory.Prime_Powers
HOL-Probability: theory HOL-Probability.Independent_Family
HOL-Probability: theory HOL-Probability.Stream_Space
Dirichlet_Series: theory HOL-Algebra.Generated_Groups
Echelon_Form: theory Gauss_Jordan.Inverse
Echelon_Form: theory Gauss_Jordan.System_Of_Equations
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Gromov_Boundary
QR_Decomposition: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
Echelon_Form: theory Gauss_Jordan.Inverse_IArrays
HOL-Probability: theory HOL-Probability.PMF_Impl
Affine_Arithmetic: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
E_Transcendental: theory HOL-Algebra.AbelCoset
E_Transcendental: theory HOL-Algebra.Module
Echelon_Form: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
Smooth_Manifolds: theory Smooth_Manifolds.Analysis_More
Dirichlet_Series: theory HOL-Number_Theory.Totient
Dirichlet_Series: theory HOL-Real_Asymp.Eventuallize
Dirichlet_Series: theory HOL-Real_Asymp.Lazy_Eval
Dirichlet_Series: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Auxiliarities
HOL-Probability: theory HOL-Probability.Random_Permutations
HOL-Probability: theory HOL-Probability.SPMF
Affine_Arithmetic: theory Affine_Arithmetic.Polygon
Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_FPS
QR_Decomposition: theory QR_Decomposition.Miscellaneous_QR
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Cones
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Initial_Value_Problem
Dirichlet_Series: theory HOL-Computational_Algebra.Polynomial_Factorial
Dirichlet_Series: theory HOL-Real_Asymp.Multiseries_Expansion
QR_Decomposition: theory QR_Decomposition.Projections
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Multivariate_Taylor
Affine_Arithmetic: theory List-Index.List_Index
QR_Decomposition: theory QR_Decomposition.Gram_Schmidt
HOL-Probability: theory HOL-Probability.Convolution
Dirichlet_Series: theory HOL-Computational_Algebra.Formal_Laurent_Series
HOL-Probability: theory HOL-Probability.Information
QR_Decomposition: theory QR_Decomposition.QR_Decomposition
Affine_Arithmetic: theory Affine_Arithmetic.Executable_Euclidean_Space
QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Float
Dirichlet_Series: theory HOL-Algebra.AbelCoset
Affine_Arithmetic: theory HOL-Decision_Procs.Approximation
Smooth_Manifolds: theory Smooth_Manifolds.Smooth
Smooth_Manifolds: theory Smooth_Manifolds.Chart
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative
QR_Decomposition: theory QR_Decomposition.Gram_Schmidt_IArrays
Smooth_Manifolds: theory Smooth_Manifolds.Topological_Manifold
QR_Decomposition: theory QR_Decomposition.Least_Squares_Approximation
QR_Decomposition: theory QR_Decomposition.Examples_QR_Abstract_Symbolic
HOL-Probability: theory HOL-Probability.Distributions
QR_Decomposition: theory QR_Decomposition.QR_Decomposition_IArrays
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Flow
E_Transcendental: theory HOL-Algebra.Ideal
QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Float
Smooth_Manifolds: theory Smooth_Manifolds.Bump_Function
Smooth_Manifolds: theory Smooth_Manifolds.Differentiable_Manifold
QR_Decomposition: theory QR_Decomposition.QR_Efficient
HOL-Probability: theory HOL-Probability.Characteristic_Functions
HOL-Probability: theory HOL-Probability.Sinc_Integral
Smooth_Manifolds: theory Smooth_Manifolds.Partition_Of_Unity
Dirichlet_Series: theory HOL-Algebra.Module
Smooth_Manifolds: theory Smooth_Manifolds.Product_Manifold
Affine_Arithmetic: theory Native_Word.Uint32
Smooth_Manifolds: theory Smooth_Manifolds.Projective_Space
Smooth_Manifolds: theory Smooth_Manifolds.Sphere
HOL-Probability: theory HOL-Probability.Fin_Map
Smooth_Manifolds: theory Smooth_Manifolds.Tangent_Space
HOL-Probability: theory HOL-Probability.Levy
E_Transcendental: theory HOL-Algebra.RingHom
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Poincare_Map
HOL-Probability: theory HOL-Probability.Central_Limit_Theorem
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Form
Dirichlet_Series: theory HOL-Algebra.Ideal
HOL-Probability: theory HOL-Probability.Projective_Limit
Affine_Arithmetic: theory Collections.HashCode
Dirichlet_Series: theory Landau_Symbols.Group_Sort
Affine_Arithmetic: theory Deriving.Hash_Generator
E_Transcendental: theory HOL-Algebra.UnivPoly
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Upper_Lower_Solution
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Reachability_Analysis
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.Linear_ODE
Affine_Arithmetic: theory Deriving.Hash_Instances
Dirichlet_Series: theory Landau_Symbols.Landau_Real_Products
Affine_Arithmetic: theory Deriving.Derive
HOL-Probability: theory HOL-Probability.Probability
Affine_Arithmetic: theory Show.Show
Dirichlet_Series: theory HOL-Algebra.RingHom
Smooth_Manifolds: theory Smooth_Manifolds.Cotangent_Space
QR_Decomposition: theory QR_Decomposition.Examples_QR_IArrays_Symbolic
Affine_Arithmetic: theory Show.Show_Instances
Affine_Arithmetic: theory Affine_Arithmetic.Intersection
Dirichlet_Series: theory HOL-Algebra.UnivPoly
Dirichlet_Series: theory Landau_Symbols.Landau_Simprocs
Dirichlet_Series: theory Landau_Symbols.Landau_More
Dirichlet_Series: theory Euler_MacLaurin.Euler_MacLaurin_Landau
Echelon_Form: theory Echelon_Form.Rings2
Count_Complex_Roots: theory Sturm_Tarski.PolyMisc
Count_Complex_Roots: theory Sturm_Tarski.Sturm_Tarski
Dirichlet_Series: theory Matrix.Utility
Dirichlet_Series: theory Polynomial_Factorization.Missing_List
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
Dirichlet_Series: theory Polynomial_Factorization.Missing_Multiset
Dirichlet_Series: theory Polynomial_Factorization.Prime_Factorization
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
Dirichlet_Series: theory HOL-Computational_Algebra.Computational_Algebra
Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots
E_Transcendental: theory HOL-Number_Theory.Residues
Affine_Arithmetic: theory HOL-Library.RBT
Dirichlet_Series: theory HOL-Algebra.Multiplicative_Group
Affine_Arithmetic: theory HOL-Library.RBT_Mapping
E_Transcendental: theory HOL-Number_Theory.Euler_Criterion
E_Transcendental: theory HOL-Number_Theory.Pocklington
E_Transcendental: theory HOL-Number_Theory.Gauss
Count_Complex_Roots: theory Count_Complex_Roots.Count_Complex_Roots_Examples
E_Transcendental: theory HOL-Number_Theory.Residue_Primitive_Roots
E_Transcendental: theory HOL-Number_Theory.Quadratic_Reciprocity
E_Transcendental: theory HOL-Number_Theory.Number_Theory
Dirichlet_Series: theory HOL-Number_Theory.Residues
E_Transcendental: theory E_Transcendental.E_Transcendental
Dirichlet_Series: theory HOL-Number_Theory.Euler_Criterion
Dirichlet_Series: theory HOL-Number_Theory.Pocklington
Dirichlet_Series: theory HOL-Number_Theory.Gauss
Dirichlet_Series: theory HOL-Number_Theory.Residue_Primitive_Roots
Dirichlet_Series: theory HOL-Number_Theory.Quadratic_Reciprocity
Dirichlet_Series: theory HOL-Number_Theory.Number_Theory
Dirichlet_Series: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Misc
Dirichlet_Series: theory Dirichlet_Series.Multiplicative_Function
Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Product
Dirichlet_Series: theory Dirichlet_Series.Euler_Products
Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series
Dirichlet_Series: theory HOL-Real_Asymp.Real_Asymp
Echelon_Form: theory Echelon_Form.Cayley_Hamilton_Compatible
Dirichlet_Series: theory Dirichlet_Series.Moebius_Mu
Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton
Dirichlet_Series: theory Dirichlet_Series.More_Totient
Dirichlet_Series: theory Dirichlet_Series.Liouville_Lambda
Echelon_Form: theory Echelon_Form.Echelon_Form
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
Echelon_Form: theory Echelon_Form.Echelon_Form_Det
Echelon_Form: theory Echelon_Form.Echelon_Form_IArrays
Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.MVT_Ex
Dirichlet_Series: theory Dirichlet_Series.Dirichlet_Series_Analysis
Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_Abstract
Echelon_Form: theory Echelon_Form.Echelon_Form_Det_IArrays
Echelon_Form: theory Echelon_Form.Code_Cayley_Hamilton_IArrays
Echelon_Form: theory Echelon_Form.Echelon_Form_Inverse_IArrays
Ordinary_Differential_Equations: theory Ordinary_Differential_Equations.ODE_Analysis
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Morse_Gromov_Theorem
Echelon_Form: theory Echelon_Form.Examples_Echelon_Form_IArrays
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Bonk_Schramm_Extension
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Boundary_Extension
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Busemann_Function
Gromov_Hyperbolicity: theory Gromov_Hyperbolicity.Isometries_Classification
Affine_Arithmetic: theory Affine_Arithmetic.Floatarith_Expression
Dirichlet_Series: theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics
Affine_Arithmetic: theory Affine_Arithmetic.Straight_Line_Program
Timing E_Transcendental (4 threads, 123.489s elapsed time, 444.936s cpu time, 19.244s GC time, factor 3.60)
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:49 elapsed time, 0:08:44 cpu time, factor 3.09)
Running Pi_Transcendental ...
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Approximation
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.Group_Closure
Pi_Transcendental: theory HOL-Computational_Algebra.Squarefree
Pi_Transcendental: theory HOL-Library.Fun_Lexorder
Pi_Transcendental: theory HOL-Library.Groups_Big_Fun
Pi_Transcendental: theory HOL-Real_Asymp.Inst_Existentials
Pi_Transcendental: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Pi_Transcendental: theory Polynomials.Poly_Mapping
Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_FPS
Pi_Transcendental: theory HOL-Computational_Algebra.Normalized_Fraction
Pi_Transcendental: theory HOL-Computational_Algebra.Polynomial_Factorial
Pi_Transcendental: theory HOL-Computational_Algebra.Formal_Laurent_Series
Pi_Transcendental: theory Polynomials.MPoly_Type
Pi_Transcendental: theory Polynomials.More_MPoly_Type
Pi_Transcendental: theory HOL-Library.Landau_Symbols
Pi_Transcendental: theory HOL-Real_Asymp.Eventuallize
Pi_Transcendental: theory HOL-Real_Asymp.Lazy_Eval
Pi_Transcendental: theory HOL-Real_Asymp.Multiseries_Expansion
Timing Gromov_Hyperbolicity (4 threads, 169.040s elapsed time, 567.752s cpu time, 15.772s GC time, factor 3.36)
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:03:01 elapsed time, 0:09:48 cpu time, factor 3.23)
Running Gauss_Jordan ...
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Code
Gauss_Jordan: theory HOL-Library.Bit
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.Code_Target_Nat
Gauss_Jordan: theory HOL-Library.IArray
Gauss_Jordan: theory Gauss_Jordan.Code_Set
Gauss_Jordan: theory HOL-Library.Code_Real_Approx_By_Float
Gauss_Jordan: theory HOL-Library.Code_Target_Numeral
Gauss_Jordan: theory Rank_Nullity_Theorem.Dual_Order
Gauss_Jordan: theory Gauss_Jordan.Code_Bit
Gauss_Jordan: theory Rank_Nullity_Theorem.Mod_Type
Gauss_Jordan: theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell
Gauss_Jordan: theory Gauss_Jordan.IArray_Addenda
Affine_Arithmetic: theory Affine_Arithmetic.Print
Gauss_Jordan: theory Rank_Nullity_Theorem.Miscellaneous
Gauss_Jordan: theory Gauss_Jordan.Code_Matrix
Gauss_Jordan: theory Gauss_Jordan.Rref
Gauss_Jordan: theory Rank_Nullity_Theorem.Fundamental_Subspaces
Affine_Arithmetic: theory Affine_Arithmetic.Ex_Affine_Approximation
Affine_Arithmetic: theory Affine_Arithmetic.Ex_Ineqs
Gauss_Jordan: theory Rank_Nullity_Theorem.Dim_Formula
Gauss_Jordan: theory Gauss_Jordan.Rank
Gauss_Jordan: theory Gauss_Jordan.Elementary_Operations
Affine_Arithmetic: theory Affine_Arithmetic.Ex_Inter
Gauss_Jordan: theory Gauss_Jordan.Matrix_To_IArray
Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan
Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_IArrays
Gauss_Jordan: theory Gauss_Jordan.Linear_Maps
Timing Count_Complex_Roots (4 threads, 165.012s elapsed time, 461.184s cpu time, 11.000s GC time, factor 2.79)
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:18 elapsed time, 0:08:34 cpu time, factor 2.60)
Running Winding_Number_Eval ...
Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_PA
Gauss_Jordan: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces
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
Gauss_Jordan: theory Gauss_Jordan.Determinants2
Gauss_Jordan: theory Gauss_Jordan.Gauss_Jordan_PA_IArrays
Gauss_Jordan: theory Gauss_Jordan.Inverse
Gauss_Jordan: theory Gauss_Jordan.System_Of_Equations
Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial
Gauss_Jordan: theory Gauss_Jordan.Determinants_IArrays
Gauss_Jordan: theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces_IArrays
Gauss_Jordan: theory Gauss_Jordan.Inverse_IArrays
Winding_Number_Eval: theory HOL-Eisbach.Eisbach_Tools
Gauss_Jordan: theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract
Winding_Number_Eval: theory Winding_Number_Eval.Missing_Analysis
Gauss_Jordan: theory Gauss_Jordan.System_Of_Equations_IArrays
Winding_Number_Eval: theory Winding_Number_Eval.Missing_Topology
Winding_Number_Eval: theory HOL-Computational_Algebra.Normalized_Fraction
Gauss_Jordan: theory Gauss_Jordan.Examples_Gauss_Jordan_IArrays
Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays
Pi_Transcendental: theory HOL-Computational_Algebra.Computational_Algebra
Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays_SML
Gauss_Jordan: theory Gauss_Jordan.Code_Rational
Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library
Pi_Transcendental: theory Symmetric_Polynomials.Vieta
Gauss_Jordan: theory Gauss_Jordan.Code_Generation_IArrays_Haskell
Pi_Transcendental: theory Symmetric_Polynomials.Symmetric_Polynomials
Winding_Number_Eval: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Winding_Number_Eval: theory HOL-Computational_Algebra.Polynomial_Factorial
Timing HOL-Probability (4 threads, 160.273s elapsed time, 538.168s cpu time, 21.296s GC time, factor 3.36)
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:37 elapsed time, 0:11:33 cpu time, factor 3.18)
Building Probabilistic_While ...
Probabilistic_While: theory Flow_Networks.Graph
Probabilistic_While: theory HOL-Library.Transitive_Closure_Table
Probabilistic_While: theory HOL-Library.While_Combinator
Probabilistic_While: theory HOL-Types_To_Sets.Types_To_Sets
Probabilistic_While: theory Probabilistic_While.Bernoulli
Probabilistic_While: theory HOL-Library.Bourbaki_Witt_Fixpoint
Probabilistic_While: theory MFMC_Countable.MFMC_Misc
Probabilistic_While: theory Flow_Networks.Network
Probabilistic_While: theory Flow_Networks.Residual_Graph
Probabilistic_While: theory Flow_Networks.Augmenting_Flow
Probabilistic_While: theory Flow_Networks.Augmenting_Path
Probabilistic_While: theory Flow_Networks.Ford_Fulkerson
Probabilistic_While: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
Probabilistic_While: theory MFMC_Countable.MFMC_Finite
Pi_Transcendental: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
Probabilistic_While: theory MFMC_Countable.Matrix_For_Marginals
Probabilistic_While: theory MFMC_Countable.Rel_PMF_Characterisation
Probabilistic_While: theory Probabilistic_While.While_SPMF
Probabilistic_While: theory Probabilistic_While.Resampling
Probabilistic_While: theory Probabilistic_While.Fast_Dice_Roll
Probabilistic_While: theory Probabilistic_While.Geometric
Pi_Transcendental: theory HOL-Real_Asymp.Real_Asymp
Pi_Transcendental: theory Pi_Transcendental.Pi_Transcendental
Winding_Number_Eval: theory Sturm_Tarski.PolyMisc
Winding_Number_Eval: theory Sturm_Tarski.Sturm_Tarski
Timing QR_Decomposition (4 threads, 235.290s elapsed time, 838.768s cpu time, 23.908s GC time, factor 3.56)
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:04:02 elapsed time, 0:14:13 cpu time, factor 3.52)
Building Markov_Models ...
Winding_Number_Eval: theory Budan_Fourier.BF_Misc
Winding_Number_Eval: theory Winding_Number_Eval.Missing_Algebraic
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
Markov_Models: theory HOL-Library.Code_Target_Int
Markov_Models: theory HOL-Library.Simps_Case_Conv
Markov_Models: theory HOL-Library.IArray
Markov_Models: theory HOL-Library.While_Combinator
Winding_Number_Eval: theory Winding_Number_Eval.Missing_Transcendental
Markov_Models: theory HOL-Library.Code_Target_Numeral
Markov_Models: theory Coinductive.Coinductive_Nat
Winding_Number_Eval: theory Winding_Number_Eval.Cauchy_Index_Theorem
Markov_Models: theory Coinductive.Coinductive_List
Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval
Winding_Number_Eval: theory Winding_Number_Eval.Winding_Number_Eval_Examples
Markov_Models: theory Coinductive.Coinductive_Stream
Affine_Arithmetic: theory Affine_Arithmetic.Affine_Arithmetic
Markov_Models: theory Markov_Models.Markov_Models_Auxiliary
Markov_Models: theory Markov_Models.Discrete_Time_Markov_Chain
Markov_Models: theory Markov_Models.Discrete_Time_Markov_Process
Markov_Models: theory Markov_Models.Classifying_Markov_Chain_States
Markov_Models: theory Markov_Models.Crowds_Protocol
Markov_Models: theory Markov_Models.Gossip_Broadcast
Markov_Models: theory Markov_Models.Markov_Decision_Process
Markov_Models: theory Markov_Models.PCTL
Markov_Models: theory Markov_Models.Trace_Space_Equals_Markov_Processes
Markov_Models: theory Markov_Models.Zeroconf_Analysis
Markov_Models: theory Markov_Models.MDP_Reachability_Problem
Timing Ordinary_Differential_Equations (4 threads, 219.626s elapsed time, 684.328s cpu time, 17.048s GC time, factor 3.12)
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:30 elapsed time, 0:12:51 cpu time, factor 2.85)
Building HOL-ODE-Numerics ...
Markov_Models: theory Markov_Models.Example_A
Markov_Models: theory Markov_Models.Example_B
Markov_Models: theory Markov_Models.MDP_RP_Certification
Markov_Models: theory Markov_Models.PGCL
Markov_Models: theory Markov_Models.Continuous_Time_Markov_Chain
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 Collections.ICF_Tools
HOL-ODE-Numerics: theory Automatic_Refinement.Mk_Term_Antiquot
HOL-ODE-Numerics: theory Automatic_Refinement.Mpat_Antiquot
HOL-ODE-Numerics: theory Collections.Ord_Code_Preproc
HOL-ODE-Numerics: theory Deriving.Comparator
HOL-ODE-Numerics: theory Collections.Locale_Code
HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Util
HOL-ODE-Numerics: theory Deriving.Derive_Manager
HOL-ODE-Numerics: theory Deriving.Generator_Aux
HOL-ODE-Numerics: theory Deriving.Equality_Generator
HOL-ODE-Numerics: theory HOL-Library.AList
HOL-ODE-Numerics: theory Automatic_Refinement.Anti_Unification
HOL-ODE-Numerics: theory Automatic_Refinement.Attr_Comb
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Data
HOL-ODE-Numerics: theory Automatic_Refinement.Indep_Vars
HOL-ODE-Numerics: theory Automatic_Refinement.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.Compare
HOL-ODE-Numerics: theory Deriving.Comparator_Generator
HOL-ODE-Numerics: theory Deriving.Equality_Instances
Markov_Models: theory Markov_Models.Markov_Models
HOL-ODE-Numerics: theory HOL-Library.Adhoc_Overloading
HOL-ODE-Numerics: theory HOL-Library.Monad_Syntax
HOL-ODE-Numerics: theory HOL-Library.Bit
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 Deriving.Compare_Generator
HOL-ODE-Numerics: theory HOL-Library.Char_ord
HOL-ODE-Numerics: theory HOL-Library.Mapping
HOL-ODE-Numerics: theory HOL-Library.Option_ord
HOL-ODE-Numerics: theory Deriving.Compare_Instances
HOL-ODE-Numerics: theory HOL-Library.Parallel
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-Types_To_Sets.Types_To_Sets
HOL-ODE-Numerics: theory HOL-Word.Bits_Bit
HOL-ODE-Numerics: theory HOL-Word.Word_Miscellaneous
HOL-ODE-Numerics: theory Native_Word.More_Bits_Int
HOL-ODE-Numerics: theory HOL-Word.Misc_Typedef
HOL-ODE-Numerics: theory HOL-Word.Word
HOL-ODE-Numerics: theory Native_Word.Bits_Integer
HOL-ODE-Numerics: theory Automatic_Refinement.Refine_Lib
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.SetIterator
HOL-ODE-Numerics: theory Automatic_Refinement.Param_Tool
HOL-ODE-Numerics: theory Collections.SetIteratorOperations
HOL-ODE-Numerics: theory Automatic_Refinement.Param_HOL
Timing Probabilistic_While (4 threads, 40.700s elapsed time, 109.632s cpu time, 2.564s GC time, factor 2.69)
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:13 elapsed time, 0:02:43 cpu time, factor 2.23)
Building CryptHOL ...
HOL-ODE-Numerics: theory Automatic_Refinement.Parametricity
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Id_Ops
Timing Pi_Transcendental (4 threads, 117.342s elapsed time, 376.584s cpu time, 18.776s GC time, factor 3.21)
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:02:03 elapsed time, 0:06:27 cpu time, factor 3.15)
Timing Gauss_Jordan (4 threads, 100.887s elapsed time, 362.824s cpu time, 8.472s 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:51 elapsed time, 0:06:21 cpu time, factor 3.43)
Running Differential_Dynamic_Logic ...
Running Deep_Learning ...
HOL-ODE-Numerics: theory Collections.Assoc_List
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Fix_Rel
CryptHOL: theory HOL-Eisbach.Eisbach
CryptHOL: theory Applicative_Lifting.Applicative
CryptHOL: theory CryptHOL.Partial_Function_Set
CryptHOL: theory HOL-Library.Cardinal_Notations
CryptHOL: theory HOL-Library.Case_Converter
HOL-ODE-Numerics: theory Collections.Diff_Array
CryptHOL: theory HOL-Library.Simps_Case_Conv
CryptHOL: theory HOL-Algebra.Congruence
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Translate
CryptHOL: theory HOL-Library.Function_Algebras
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Gen_Algo
CryptHOL: theory HOL-Library.Type_Length
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Relator_Interface
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Tool
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Ids
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Lib
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Syntax
CryptHOL: theory HOL-Library.Countable_Set_Type
CryptHOL: theory HOL-Library.Landau_Symbols
Deep_Learning: theory Deep_Learning.DL_Missing_Finite_Set
Deep_Learning: theory Deep_Learning.Tensor
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
CryptHOL: theory Applicative_Lifting.Applicative_Environment
Deep_Learning: theory HOL-Library.More_List
CryptHOL: theory CryptHOL.Environment_Functor
Deep_Learning: theory Deep_Learning.Tensor_Subtensor
CryptHOL: theory Applicative_Lifting.Applicative_Set
HOL-ODE-Numerics: theory Automatic_Refinement.Autoref_Bindings_HOL
CryptHOL: theory HOL-Algebra.Order
Deep_Learning: theory Deep_Learning.Tensor_Plus
Deep_Learning: theory Polynomials.Poly_Mapping
CryptHOL: theory CryptHOL.Set_Applicative
CryptHOL: theory Coinductive.Coinductive_Nat
Deep_Learning: theory Deep_Learning.Tensor_Scalar_Mult
Deep_Learning: theory Deep_Learning.Tensor_Product
Deep_Learning: theory HOL-Computational_Algebra.Normalized_Fraction
Deep_Learning: theory Deep_Learning.Tensor_Unit_Vec
Deep_Learning: theory Deep_Learning.Tensor_Rank
Deep_Learning: theory HOL-Algebra.Order
Deep_Learning: theory Polynomial_Interpolation.Missing_Unsorted
Deep_Learning: theory HOL-Computational_Algebra.Polynomial
HOL-ODE-Numerics: theory Collections.Proper_Iterator
CryptHOL: theory Coinductive.Coinductive_List
CryptHOL: theory HOL-Algebra.Lattice
CryptHOL: theory Applicative_Lifting.Applicative_PMF
HOL-ODE-Numerics: theory Collections.It_to_It
CryptHOL: theory Monad_Normalisation.Monad_Normalisation
Deep_Learning: theory Polynomials.MPoly_Type
Deep_Learning: theory HOL-Algebra.Lattice
HOL-ODE-Numerics: theory Collections.SetIteratorGA
Deep_Learning: theory Deep_Learning.Lebesgue_Functional
Deep_Learning: theory Jordan_Normal_Form.DL_Missing_List
CryptHOL: theory Monomorphic_Monad.Monomorphic_Monad
Deep_Learning: theory Polynomials.More_MPoly_Type
Deep_Learning: theory Jordan_Normal_Form.DL_Missing_Sublist
HOL-ODE-Numerics: theory Native_Word.Code_Target_Bits_Int
CryptHOL: theory HOL-Algebra.Complete_Lattice
Deep_Learning: theory Polynomial_Interpolation.Ring_Hom
HOL-ODE-Numerics: theory Automatic_Refinement.Automatic_Refinement
HOL-ODE-Numerics: theory Collections.Intf_Comp
HOL-ODE-Numerics: theory Collections.Idx_Iterator
Deep_Learning: theory VectorSpace.FunctionLemmas
Deep_Learning: theory HOL-Algebra.Complete_Lattice
HOL-ODE-Numerics: theory Collections.Code_Target_ICF
HOL-ODE-Numerics: theory Native_Word.Word_Misc
CryptHOL: theory HOL-Algebra.Group
CryptHOL: theory CryptHOL.SPMF_Applicative
Deep_Learning: theory HOL-Algebra.Group
HOL-ODE-Numerics: theory Deriving.Countable_Generator
HOL-ODE-Numerics: theory Native_Word.Uint
CryptHOL: theory Landau_Symbols.Group_Sort
HOL-ODE-Numerics: theory Native_Word.Uint32
HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Integer
CryptHOL: theory HOL-Algebra.Coset
CryptHOL: theory Landau_Symbols.Landau_Real_Products
Deep_Learning: theory HOL-Algebra.Coset
HOL-ODE-Numerics: theory Affine_Arithmetic.Optimize_Float
Timing Winding_Number_Eval (4 threads, 97.993s elapsed time, 256.672s cpu time, 7.340s GC time, factor 2.62)
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:48 elapsed time, 0:04:34 cpu time, factor 2.53)
Running Probabilistic_Prime_Tests ...
Deep_Learning: theory HOL-Algebra.FiniteProduct
HOL-ODE-Numerics: theory Collections.HashCode
HOL-ODE-Numerics: theory Affine_Arithmetic.Float_Real
HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise
HOL-ODE-Numerics: theory Collections.Intf_Hash
Deep_Learning: theory HOL-Algebra.Ring
HOL-ODE-Numerics: theory Collections.Impl_Array_Stack
HOL-ODE-Numerics: theory Deriving.Hash_Generator
HOL-ODE-Numerics: theory Collections.Gen_Hash
HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_Vector
HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Strict
Probabilistic_Prime_Tests: theory HOL-Algebra.Exponent
Probabilistic_Prime_Tests: theory HOL-Computational_Algebra.Squarefree
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Cong
Probabilistic_Prime_Tests: theory HOL-Library.Permutation
Probabilistic_Prime_Tests: theory HOL-Algebra.Congruence
Probabilistic_Prime_Tests: theory HOL-Algebra.Cycles
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Analysis
Probabilistic_Prime_Tests: theory HOL-Library.Power_By_Squaring
HOL-ODE-Numerics: theory Deriving.Hash_Instances
HOL-ODE-Numerics: theory Deriving.Derive
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Eratosthenes
HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Form
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Fib
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Prime_Powers
HOL-ODE-Numerics: theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary
CryptHOL: theory CryptHOL.Cyclic_Group
Probabilistic_Prime_Tests: theory HOL-Algebra.Order
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Mod_Exp
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Totient
HOL-ODE-Numerics: theory Affine_Arithmetic.Polygon
HOL-ODE-Numerics: theory Affine_Arithmetic.Floatarith_Expression
CryptHOL: theory CryptHOL.Cyclic_Group_SPMF
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Denotational_Semantics
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Pretty_Printer
HOL-ODE-Numerics: theory HOL-ODE-Numerics.One_Step_Method
Deep_Learning: theory Polynomials.MPoly_Type_Univariate
CryptHOL: theory Coinductive.TLList
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Runge_Kutta
Probabilistic_Prime_Tests: theory HOL-Algebra.Lattice
Deep_Learning: theory HOL-Computational_Algebra.Polynomial_Factorial
Deep_Learning: theory Deep_Learning.Lebesgue_Zero_Set
CryptHOL: theory Landau_Symbols.Landau_Simprocs
Probabilistic_Prime_Tests: theory HOL-Algebra.Complete_Lattice
CryptHOL: theory Landau_Symbols.Landau_More
CryptHOL: theory CryptHOL.Negligible
Probabilistic_Prime_Tests: theory HOL-Algebra.Galois_Connection
Deep_Learning: theory HOL-Algebra.Module
Probabilistic_Prime_Tests: theory HOL-Algebra.Group
HOL-ODE-Numerics: theory Affine_Arithmetic.Intersection
Deep_Learning: theory Jordan_Normal_Form.Missing_Ring
Deep_Learning: theory VectorSpace.RingModuleFacts
Probabilistic_Prime_Tests: theory HOL-Algebra.Bij
Probabilistic_Prime_Tests: theory HOL-Algebra.Coset
Probabilistic_Prime_Tests: theory HOL-Algebra.FiniteProduct
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_ODE
Deep_Learning: theory VectorSpace.MonoidSums
Probabilistic_Prime_Tests: theory HOL-Algebra.Ring
Deep_Learning: theory Jordan_Normal_Form.Missing_Permutations
Deep_Learning: theory Jordan_Normal_Form.Matrix
Deep_Learning: theory VectorSpace.LinearCombinations
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Chapter
Probabilistic_Prime_Tests: theory HOL-Algebra.Group_Action
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Mono_Prover
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Misc
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Axioms
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Frechet_Correctness
Probabilistic_Prime_Tests: theory HOL-Algebra.Sylow
HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Domain
Probabilistic_Prime_Tests: theory HOL-Algebra.Divisibility
Probabilistic_Prime_Tests: theory HOL-Algebra.Zassenhaus
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Static_Semantics
HOL-ODE-Numerics: theory Refine_Monadic.RefineG_Transfer
Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Groups
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
Probabilistic_Prime_Tests: theory HOL-Algebra.Solvable_Groups
Probabilistic_Prime_Tests: theory HOL-Algebra.Exact_Sequence
Probabilistic_Prime_Tests: theory HOL-Algebra.Sym_Groups
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Det
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Basic
Probabilistic_Prime_Tests: theory HOL-Algebra.AbelCoset
Probabilistic_Prime_Tests: theory HOL-Algebra.Module
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Coincidence
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst
Deep_Learning: theory Deep_Learning.DL_Concrete_Matrices
Deep_Learning: theory Deep_Learning.DL_Flatten_Matrix
Deep_Learning: theory Deep_Learning.DL_Network
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Bound_Effect
Deep_Learning: theory Deep_Learning.Tensor_Matricization
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Axioms
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Uniform_Renaming
Deep_Learning: theory Jordan_Normal_Form.DL_Submatrix
HOL-ODE-Numerics: theory Show.Show_Instances
Deep_Learning: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
HOL-ODE-Numerics: theory HOL-Library.RBT
Markov_Models: theory Markov_Models.MDP_RP
Deep_Learning: theory VectorSpace.SumSpaces
HOL-ODE-Numerics: theory HOL-Library.RBT_Mapping
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Heuristics
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Leof
Deep_Learning: theory VectorSpace.VectorSpace
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 Jordan_Normal_Form.Column_Operations
Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal
CryptHOL: theory CryptHOL.Misc_CryptHOL
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Transfer
Deep_Learning: theory Deep_Learning.DL_Shallow_Model
HOL-ODE-Numerics: theory Refine_Monadic.Autoref_Monadic
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Automation
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Foreach
Probabilistic_Prime_Tests: theory HOL-Algebra.Ideal_Product
Probabilistic_Prime_Tests: theory HOL-Algebra.RingHom
HOL-ODE-Numerics: theory Refine_Monadic.Refine_Monadic
Probabilistic_Prime_Tests: theory HOL-Algebra.QuotRing
Probabilistic_Prime_Tests: theory HOL-Algebra.UnivPoly
HOL-ODE-Numerics: theory Collections.Gen_Iterator
Deep_Learning: theory Jordan_Normal_Form.Missing_VectorSpace
Deep_Learning: theory Jordan_Normal_Form.VS_Connect
HOL-ODE-Numerics: theory Collections.Iterator
HOL-ODE-Numerics: theory Collections.Intf_Map
Timing Dirichlet_Series (4 threads, 266.857s elapsed time, 896.416s cpu time, 54.640s GC time, factor 3.36)
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:44 elapsed time, 0:17:12 cpu time, factor 3.00)
Building Zeta_Function ...
HOL-ODE-Numerics: theory Collections.Intf_Set
Deep_Learning: theory Jordan_Normal_Form.Determinant
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
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.USubst_Lemma
CryptHOL: theory CryptHOL.Generat
CryptHOL: theory CryptHOL.List_Bits
CryptHOL: theory CryptHOL.Resumption
HOL-ODE-Numerics: theory Affine_Arithmetic.Straight_Line_Program
HOL-ODE-Numerics: theory Collections.Impl_Array_Map
HOL-ODE-Numerics: theory Collections.Impl_List_Map
Zeta_Function: theory Bernoulli.Bernoulli_Zeta
Probabilistic_Prime_Tests: theory HOL-Algebra.IntRing
Probabilistic_Prime_Tests: theory HOL-Algebra.Weak_Morphisms
HOL-ODE-Numerics: theory Collections.Impl_RBT_Map
HOL-ODE-Numerics: theory Collections.Gen_Set
HOL-ODE-Numerics: theory Collections.Impl_Array_Hash_Map
Deep_Learning: theory Deep_Learning.DL_Deep_Model
Probabilistic_Prime_Tests: theory HOL-Algebra.Chinese_Remainder
Deep_Learning: theory Jordan_Normal_Form.DL_Rank
HOL-ODE-Numerics: theory Collections.Impl_Bit_Set
CryptHOL: theory CryptHOL.Generative_Probabilistic_Value
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Proof_Checker
HOL-ODE-Numerics: theory Collections.Impl_Cfun_Set
HOL-ODE-Numerics: theory Collections.Impl_List_Set
HOL-ODE-Numerics: theory Collections.Impl_Uv_Set
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_Analysis
Zeta_Function: theory Winding_Number_Eval.Missing_Topology
Deep_Learning: theory Deep_Learning.DL_Deep_Model_Poly
Zeta_Function: theory HOL-Eisbach.Eisbach_Tools
Zeta_Function: theory Sturm_Tarski.Sturm_Tarski
Zeta_Function: theory Budan_Fourier.BF_Misc
Probabilistic_Prime_Tests: theory HOL-Algebra.Multiplicative_Group
Zeta_Function: theory Winding_Number_Eval.Missing_Algebraic
Deep_Learning: theory Deep_Learning.DL_Rank_CP_Rank
Zeta_Function: theory Winding_Number_Eval.Missing_Transcendental
Deep_Learning: theory Jordan_Normal_Form.DL_Rank_Submatrix
Zeta_Function: theory Winding_Number_Eval.Cauchy_Index_Theorem
Deep_Learning: theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity
Probabilistic_Prime_Tests: theory HOL-Algebra.Ring_Divisibility
Probabilistic_Prime_Tests: theory HOL-Algebra.Subrings
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residues
Zeta_Function: theory Winding_Number_Eval.Winding_Number_Eval
Probabilistic_Prime_Tests: theory HOL-Algebra.Embedded_Algebras
Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Rings
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Euler_Criterion
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Gauss
Zeta_Function: theory Zeta_Function.Zeta_Function
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Quadratic_Reciprocity
Probabilistic_Prime_Tests: theory HOL-Algebra.Generated_Fields
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Pocklington
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Residue_Primitive_Roots
Probabilistic_Prime_Tests: theory HOL-Number_Theory.Number_Theory
CryptHOL: theory CryptHOL.Computational_Model
CryptHOL: theory CryptHOL.GPV_Applicative
CryptHOL: theory CryptHOL.GPV_Expectation
HOL-ODE-Numerics: theory HOL-ODE-Numerics.GenCF_No_Comp
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Legendre_Symbol
HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Approximation
CryptHOL: theory CryptHOL.GPV_Bisim
CryptHOL: theory CryptHOL.CryptHOL
Probabilistic_Prime_Tests: theory HOL-Algebra.Polynomials
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Dflt_No_Comp
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Autoref_Misc
Differential_Dynamic_Logic: theory Differential_Dynamic_Logic.Differential_Dynamic_Logic
HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Code
HOL-ODE-Numerics: theory Affine_Arithmetic.Print
Probabilistic_Prime_Tests: theory HOL-Algebra.Algebra
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
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries
Timing Markov_Models (4 threads, 93.518s elapsed time, 324.156s cpu time, 12.044s GC time, factor 3.47)
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:39 elapsed time, 0:07:24 cpu time, factor 2.79)
Running Stochastic_Matrices ...
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Generalized_Primality_Test
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Residues_Nat
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Jacobi_Symbol
Stochastic_Matrices: theory HOL-Eisbach.Eisbach
Stochastic_Matrices: theory HOL-Library.Bit
Stochastic_Matrices: theory HOL-Computational_Algebra.Fraction_Field
Stochastic_Matrices: theory HOL-Algebra.Congruence
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Carmichael_Numbers
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.QuadRes
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Euler_Witness
Stochastic_Matrices: theory HOL-Library.Function_Algebras
Stochastic_Matrices: theory HOL-Library.More_List
Stochastic_Matrices: theory Perron_Frobenius.Bij_Nat
Stochastic_Matrices: theory HOL-Types_To_Sets.Types_To_Sets
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Witness
Stochastic_Matrices: theory Jordan_Normal_Form.Conjugate
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Solovay_Strassen_Test
Stochastic_Matrices: theory HOL-Algebra.Order
Stochastic_Matrices: theory HOL-Computational_Algebra.Normalized_Fraction
Stochastic_Matrices: theory Perron_Frobenius.Cancel_Card_Constraint
Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Unsorted
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Fermat_Test
Probabilistic_Prime_Tests: theory Probabilistic_Prime_Tests.Miller_Rabin_Test
Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial
Stochastic_Matrices: theory HOL-Algebra.Lattice
Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Folds
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_String
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Weak_Set
Stochastic_Matrices: theory HOL-Algebra.Complete_Lattice
Stochastic_Matrices: theory Rank_Nullity_Theorem.Dual_Order
Stochastic_Matrices: theory Rank_Nullity_Theorem.Mod_Type
Stochastic_Matrices: theory HOL-Algebra.Group
Stochastic_Matrices: theory VectorSpace.FunctionLemmas
Stochastic_Matrices: theory Rank_Nullity_Theorem.Miscellaneous
Stochastic_Matrices: theory HOL-Algebra.Coset
Stochastic_Matrices: theory HOL-Algebra.FiniteProduct
Stochastic_Matrices: theory HOL-Algebra.Ring
Stochastic_Matrices: theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra
Stochastic_Matrices: theory HOL-Computational_Algebra.Polynomial_Factorial
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Enclosure_Operations
Stochastic_Matrices: theory HOL-Algebra.Module
Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Ring
Stochastic_Matrices: theory VectorSpace.RingModuleFacts
Stochastic_Matrices: theory VectorSpace.MonoidSums
Stochastic_Matrices: theory Jordan_Normal_Form.Missing_Permutations
Stochastic_Matrices: theory Jordan_Normal_Form.Matrix
Stochastic_Matrices: theory VectorSpace.LinearCombinations
Timing Echelon_Form (4 threads, 396.386s elapsed time, 1261.264s cpu time, 143.676s GC time, factor 3.18)
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:07:13 elapsed time, 0:22:04 cpu time, factor 3.06)
Running Probabilistic_Timed_Automata ...
Stochastic_Matrices: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
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
Stochastic_Matrices: theory VectorSpace.SumSpaces
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Instantiate_Existentials
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.More_List
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence
Probabilistic_Timed_Automata: theory Timed_Automata.Floyd_Warshall
Stochastic_Matrices: theory VectorSpace.VectorSpace
Probabilistic_Timed_Automata: theory Timed_Automata.Timed_Automata
Probabilistic_Timed_Automata: theory HOL-Eisbach.Eisbach_Tools
Stochastic_Matrices: theory Jordan_Normal_Form.Column_Operations
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Finiteness
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Parallel
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Sequence_LTL
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Stream_More
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Graphs
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Default
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Unions
Probabilistic_Timed_Automata: theory Timed_Automata.DBM
Probabilistic_Timed_Automata: theory Timed_Automata.Paths_Cycles
Probabilistic_Timed_Automata: theory Timed_Automata.Regions
Stochastic_Matrices: theory Jordan_Normal_Form.Missing_VectorSpace
Stochastic_Matrices: theory Jordan_Normal_Form.VS_Connect
Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Basics
Stochastic_Matrices: theory Polynomial_Interpolation.Missing_Polynomial
Stochastic_Matrices: theory Jordan_Normal_Form.Determinant
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Vector_List
Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Normalization
Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Operations
Probabilistic_Timed_Automata: theory Timed_Automata.Closure
Stochastic_Matrices: theory Polynomial_Factorization.Order_Polynomial
Stochastic_Matrices: theory Polynomial_Interpolation.Ring_Hom_Poly
Stochastic_Matrices: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
Probabilistic_Timed_Automata: theory Timed_Automata.DBM_Zone_Semantics
Probabilistic_Timed_Automata: theory Timed_Automata.Regions_Beta
Timing Zeta_Function (4 threads, 68.905s elapsed time, 220.008s cpu time, 4.332s GC time, factor 3.19)
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:43 elapsed time, 0:04:36 cpu time, factor 2.67)
Running List_Update ...
Stochastic_Matrices: theory Jordan_Normal_Form.Gram_Schmidt
Stochastic_Matrices: theory Jordan_Normal_Form.Matrix_Kernel
Stochastic_Matrices: theory Jordan_Normal_Form.Char_Poly
List_Update: theory HOL-Library.While_Combinator
List_Update: theory List_Update.Prob_Theory
List_Update: theory List_Update.Bit_Strings
List_Update: theory List_Update.On_Off
List_Update: theory List-Index.List_Index
Stochastic_Matrices: theory Perron_Frobenius.Roots_Unity
Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form
List_Update: theory Regular-Sets.Regular_Set
List_Update: theory List_Update.Inversion
List_Update: theory List_Update.Swaps
List_Update: theory List_Update.Competitive_Analysis
Stochastic_Matrices: theory Jordan_Normal_Form.Schur_Decomposition
Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness
Probabilistic_Timed_Automata: theory Timed_Automata.Approx_Beta
List_Update: theory List_Update.Move_to_Front
List_Update: theory Regular-Sets.Regular_Exp
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Intersection
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.Lib
Stochastic_Matrices: theory Jordan_Normal_Form.Jordan_Normal_Form_Existence
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Phantom
List_Update: theory Regular-Sets.NDerivative
List_Update: theory List_Update.MTF2_Effects
List_Update: theory List_Update.Partial_Cost_Model
List_Update: theory List_Update.BIT
List_Update: theory List_Update.List_Factoring
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Invar
Stochastic_Matrices: theory Jordan_Normal_Form.Spectral_Radius
HOL-ODE-Numerics: theory Affine_Arithmetic.Affine_Arithmetic
Stochastic_Matrices: theory Perron_Frobenius.HMA_Connect
List_Update: theory Regular-Sets.Equivalence_Checking
List_Update: theory List_Update.RExp_Var
List_Update: theory List_Update.OPT2
List_Update: theory List_Update.BIT_pairwise
List_Update: theory List_Update.Phase_Partitioning
Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Aux
List_Update: theory List_Update.BIT_2comp_on2
List_Update: theory List_Update.TS
Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius
Stochastic_Matrices: theory Perron_Frobenius.Perron_Frobenius_Irreducible
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Info
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector
List_Update: theory List_Update.Comb
Timing Affine_Arithmetic (4 threads, 396.557s elapsed time, 1377.260s cpu time, 91.996s 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:58 elapsed time, 0:26:27 cpu time, factor 3.32)
Running Taylor_Models ...
Taylor_Models: theory HOL-Decision_Procs.Rat_Pair
Taylor_Models: theory HOL-Decision_Procs.Polynomial_List
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Hyperplane
Timing CryptHOL (4 threads, 122.828s elapsed time, 441.972s cpu time, 23.296s GC time, factor 3.60)
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:03:08 elapsed time, 0:09:34 cpu time, factor 3.05)
Running Constructive_Cryptography ...
Constructive_Cryptography: theory Constructive_Cryptography.More_CryptHOL
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Interval
Constructive_Cryptography: theory Constructive_Cryptography.Resource
Constructive_Cryptography: theory Constructive_Cryptography.Converter
Taylor_Models: theory Taylor_Models.Polynomial_Expression
Timing Probabilistic_Prime_Tests (4 threads, 187.742s elapsed time, 688.448s cpu time, 48.584s GC time, factor 3.67)
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:03:14 elapsed time, 0:11:41 cpu time, factor 3.60)
Running Hermite ...
Hermite: theory Hermite.Hermite
Hermite: theory Hermite.Hermite_IArrays
Constructive_Cryptography: theory Constructive_Cryptography.Converter_Rewrite
Constructive_Cryptography: theory Constructive_Cryptography.Random_System
Constructive_Cryptography: theory Constructive_Cryptography.Distinguisher
Constructive_Cryptography: theory Constructive_Cryptography.Wiring
Constructive_Cryptography: theory Constructive_Cryptography.Constructive_Cryptography
Constructive_Cryptography: theory Constructive_Cryptography.System_Construction
Timing Deep_Learning (4 threads, 216.332s elapsed time, 740.084s cpu time, 31.556s GC time, factor 3.42)
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:44 elapsed time, 0:12:33 cpu time, factor 3.36)
Running Density_Compiler ...
Density_Compiler: theory Density_Compiler.Density_Predicates
Density_Compiler: theory Density_Compiler.PDF_Transformations
Density_Compiler: theory Density_Compiler.PDF_Values
Constructive_Cryptography: theory Constructive_Cryptography.Message_Authentication_Code
Constructive_Cryptography: theory Constructive_Cryptography.One_Time_Pad
Density_Compiler: theory Density_Compiler.PDF_Semantics
Taylor_Models: theory HOL-Library.Function_Algebras
Taylor_Models: theory Taylor_Models.Float_Topology
Taylor_Models: theory Taylor_Models.Interval
Taylor_Models: theory Taylor_Models.Taylor_Models_Misc
Constructive_Cryptography: theory Constructive_Cryptography.Secure_Channel
Constructive_Cryptography: theory Constructive_Cryptography.Examples
Taylor_Models: theory Taylor_Models.Horner_Eval
Taylor_Models: theory Taylor_Models.Interval_Approximation
Taylor_Models: theory Taylor_Models.Polynomial_Expression_Additional
Density_Compiler: theory Density_Compiler.PDF_Density_Contexts
Density_Compiler: theory Density_Compiler.PDF_Target_Semantics
Density_Compiler: theory Density_Compiler.PDF_Compiler_Pred
Taylor_Models: theory Taylor_Models.Taylor_Models
Density_Compiler: theory Density_Compiler.PDF_Target_Density_Contexts
Density_Compiler: theory Density_Compiler.PDF_Compiler
Timing List_Update (4 threads, 105.239s elapsed time, 323.640s cpu time, 12.820s GC time, factor 3.08)
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:59 elapsed time, 0:05:56 cpu time, factor 2.98)
Running Linear_Recurrences ...
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_Int
Linear_Recurrences: theory HOL-Library.Code_Target_Nat
Linear_Recurrences: theory HOL-Library.Code_Target_Numeral
Linear_Recurrences: theory HOL-Library.Stirling
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
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics
Linear_Recurrences: theory Polynomial_Interpolation.Missing_Polynomial
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
Linear_Recurrences: theory Matrix.Utility
Linear_Recurrences: theory HOL-Computational_Algebra.Computational_Algebra
Linear_Recurrences: theory Polynomial_Interpolation.Ring_Hom
Linear_Recurrences: theory Linear_Recurrences.Eulerian_Polynomials
Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Common
Linear_Recurrences: theory HOL-Real_Asymp.Multiseries_Expansion
Linear_Recurrences: theory Linear_Recurrences.Linear_Recurrences_Misc
Linear_Recurrences: theory Linear_Recurrences.RatFPS
Linear_Recurrences: theory Linear_Recurrences.Factorizations
Linear_Recurrences: theory Linear_Recurrences.Partial_Fraction_Decomposition
Taylor_Models: theory Taylor_Models.Experiments
Linear_Recurrences: theory Polynomial_Interpolation.Ring_Hom_Poly
Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Solver
Linear_Recurrences: theory Polynomial_Factorization.Square_Free_Factorization
Linear_Recurrences: theory Linear_Recurrences.Linear_Homogenous_Recurrences
Linear_Recurrences: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
Timing Differential_Dynamic_Logic (4 threads, 291.706s elapsed time, 642.212s cpu time, 21.820s GC time, factor 2.20)
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:05:03 elapsed time, 0:11:01 cpu time, factor 2.18)
Building Girth_Chromatic ...
Girth_Chromatic: theory HOL-Decision_Procs.Dense_Linear_Order
Girth_Chromatic: theory HOL-Library.Code_Abstract_Nat
Girth_Chromatic: theory HOL-Library.Code_Target_Int
Girth_Chromatic: theory HOL-Library.Lattice_Algebras
Girth_Chromatic: theory HOL-Library.Code_Target_Nat
Girth_Chromatic: theory HOL-Library.Log_Nat
Girth_Chromatic: theory HOL-Library.Code_Target_Numeral
Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic_Misc
Girth_Chromatic: theory Girth_Chromatic.Ugraphs
Girth_Chromatic: theory HOL-Library.Float
Girth_Chromatic: theory HOL-Decision_Procs.Approximation_Bounds
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA
Timing Taylor_Models (4 threads, 123.531s elapsed time, 355.784s cpu time, 12.436s GC time, factor 2.88)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Taylor_Models/outline.pdf
Finished Taylor_Models (0:02:10 elapsed time, 0:06:08 cpu time, factor 2.83)
Running Probabilistic_Noninterference ...
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
Girth_Chromatic: theory HOL-Decision_Procs.Approximation
Probabilistic_Noninterference: theory Coinductive.Coinductive_List
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics
Linear_Recurrences: theory HOL-Real_Asymp.Multiseries_Expansion_Bounds
Linear_Recurrences: theory HOL-Real_Asymp.Real_Asymp
Linear_Recurrences: theory Linear_Recurrences.Rational_FPS_Asymptotics
Probabilistic_Noninterference: theory Coinductive.Coinductive_Stream
Timing Hermite (4 threads, 114.838s elapsed time, 265.576s cpu time, 23.308s GC time, factor 2.31)
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:02:01 elapsed time, 0:04:37 cpu time, factor 2.29)
Running Hidden_Markov_Models ...
Probabilistic_Noninterference: theory Markov_Models.Markov_Models_Auxiliary
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
Probabilistic_Noninterference: theory Markov_Models.Discrete_Time_Markov_Chain
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
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Interface
Probabilistic_Timed_Automata: theory Probabilistic_Timed_Automata.PTA_Reachability
Hidden_Markov_Models: theory HOL-Imperative_HOL.Array
Timing Density_Compiler (4 threads, 104.448s elapsed time, 287.576s cpu time, 5.540s GC time, factor 2.75)
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:01:53 elapsed time, 0:05:03 cpu time, factor 2.68)
Running Dirichlet_L ...
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
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
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
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Language_Semantics
Dirichlet_L: theory HOL-Library.Float
Dirichlet_L: theory HOL-Decision_Procs.Approximation_Bounds
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Resumption_Based
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Compositionality
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Trace_Based
Dirichlet_L: theory Bertrands_Postulate.Bertrand
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Syntactic_Criteria
Probabilistic_Noninterference: theory Probabilistic_Noninterference.Concrete
Timing Linear_Recurrences (4 threads, 81.692s elapsed time, 313.620s cpu time, 18.504s GC time, factor 3.84)
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:28 elapsed time, 0:05:25 cpu time, factor 3.70)
Running Ergodic_Theory ...
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
Ergodic_Theory: theory Ergodic_Theory.Measure_Preserving_Transformations
Timing Probabilistic_Timed_Automata (4 threads, 220.048s elapsed time, 638.392s cpu time, 18.040s GC time, factor 2.90)
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:47 elapsed time, 0:10:52 cpu time, factor 2.87)
Building Applicative_Lifting ...
Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Implementation
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
Girth_Chromatic: theory Girth_Chromatic.Girth_Chromatic
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
Ergodic_Theory: theory Ergodic_Theory.Recurrence
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
Ergodic_Theory: theory Ergodic_Theory.Invariants
Applicative_Lifting: theory Applicative_Lifting.Applicative_Sum
Applicative_Lifting: theory Applicative_Lifting.Applicative_State
Applicative_Lifting: theory Applicative_Lifting.Applicative_DNEList
Ergodic_Theory: theory Ergodic_Theory.Transfer_Operator
Applicative_Lifting: theory Applicative_Lifting.Applicative_Environment_Algebra
Applicative_Lifting: theory Applicative_Lifting.Applicative_Star
Applicative_Lifting: theory Applicative_Lifting.Applicative_Stream
Ergodic_Theory: theory Ergodic_Theory.Ergodicity
Ergodic_Theory: theory Ergodic_Theory.Normalizing_Sequences
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
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
Ergodic_Theory: theory Ergodic_Theory.Kingman
Applicative_Lifting: theory Applicative_Lifting.Applicative_Functor
Applicative_Lifting: theory Applicative_Lifting.Tree_Relabelling
Ergodic_Theory: theory Ergodic_Theory.Gouezel_Karlsson
Applicative_Lifting: theory Applicative_Lifting.Applicative_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
Applicative_Lifting: theory Applicative_Lifting.Abstract_AF
Applicative_Lifting: theory Applicative_Lifting.Applicative_Test
Dirichlet_L: theory Dirichlet_L.Group_Adjoin
Stochastic_Matrices: theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius
Dirichlet_L: theory Dirichlet_L.Multiplicative_Characters
Dirichlet_L: theory Dirichlet_L.Dirichlet_Characters
Dirichlet_L: theory Dirichlet_L.Dirichlet_L_Functions
Timing Stochastic_Matrices (4 threads, 286.167s elapsed time, 780.220s cpu time, 31.132s GC time, factor 2.73)
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:04:51 elapsed time, 0:13:10 cpu time, factor 2.71)
Timing Probabilistic_Noninterference (4 threads, 77.798s elapsed time, 254.244s cpu time, 7.160s GC time, factor 3.27)
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:24 elapsed time, 0:04:34 cpu time, factor 3.23)
Running MFMC_Countable ...
Running Green ...
Green: theory Green.General_Utils
Green: theory Green.Derivs
Green: theory Green.Integrals
MFMC_Countable: theory Flow_Networks.Graph
MFMC_Countable: theory HOL-Library.Transitive_Closure_Table
MFMC_Countable: theory HOL-Library.While_Combinator
Green: theory Green.Paths
Hidden_Markov_Models: theory Hidden_Markov_Models.HMM_Example
MFMC_Countable: theory HOL-Library.Bourbaki_Witt_Fixpoint
MFMC_Countable: theory MFMC_Countable.MFMC_Misc
MFMC_Countable: theory Flow_Networks.Network
MFMC_Countable: theory MFMC_Countable.Max_Flow_Min_Cut_Countable
Green: theory Green.Green
MFMC_Countable: theory Flow_Networks.Residual_Graph
Dirichlet_L: theory Dirichlet_L.Dirichlet_Theorem
Green: theory Green.SymmetricR2Shapes
Green: theory Green.CircExample
Green: theory Green.DiamExample
MFMC_Countable: theory Flow_Networks.Augmenting_Flow
Timing Girth_Chromatic (4 threads, 71.074s elapsed time, 149.552s cpu time, 5.896s GC time, factor 2.10)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Girth_Chromatic/outline.pdf
Finished Girth_Chromatic (0:01:44 elapsed time, 0:03:27 cpu time, factor 1.98)
Running DiscretePricing ...
MFMC_Countable: theory Flow_Networks.Augmenting_Path
MFMC_Countable: theory Flow_Networks.Ford_Fulkerson
MFMC_Countable: theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract
DiscretePricing: theory DiscretePricing.Filtration
DiscretePricing: theory DiscretePricing.Generated_Subalgebra
DiscretePricing: theory DiscretePricing.Disc_Cond_Expect
MFMC_Countable: theory MFMC_Countable.MFMC_Finite
MFMC_Countable: theory MFMC_Countable.Matrix_For_Marginals
MFMC_Countable: theory MFMC_Countable.Rel_PMF_Characterisation
DiscretePricing: theory DiscretePricing.Martingale
DiscretePricing: theory DiscretePricing.Infinite_Coin_Toss_Space
Timing Dirichlet_L (4 threads, 73.867s elapsed time, 233.440s cpu time, 7.408s GC time, factor 3.16)
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:21 elapsed time, 0:04:06 cpu time, factor 3.04)
Running Prime_Harmonic_Series ...
DiscretePricing: theory DiscretePricing.Geometric_Random_Walk
Prime_Harmonic_Series: theory HOL-Number_Theory.Cong
Prime_Harmonic_Series: theory HOL-Algebra.Congruence
Prime_Harmonic_Series: theory HOL-Library.Power_By_Squaring
Prime_Harmonic_Series: theory HOL-Number_Theory.Eratosthenes
Prime_Harmonic_Series: theory HOL-Number_Theory.Fib
DiscretePricing: theory DiscretePricing.Fair_Price
Prime_Harmonic_Series: theory HOL-Number_Theory.Prime_Powers
Timing Hidden_Markov_Models (4 threads, 85.880s elapsed time, 149.320s cpu time, 10.180s GC time, factor 1.74)
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:32 elapsed time, 0:02:42 cpu time, factor 1.75)
Running Akra_Bazzi ...
Prime_Harmonic_Series: theory HOL-Algebra.Order
Prime_Harmonic_Series: theory HOL-Number_Theory.Mod_Exp
Prime_Harmonic_Series: theory HOL-Number_Theory.Totient
Akra_Bazzi: theory HOL-Decision_Procs.Dense_Linear_Order
Akra_Bazzi: theory HOL-Library.Code_Abstract_Nat
Akra_Bazzi: theory HOL-Library.Code_Target_Int
Akra_Bazzi: theory HOL-Library.Function_Algebras
Akra_Bazzi: theory HOL-Library.Code_Target_Nat
Akra_Bazzi: theory Akra_Bazzi.Eval_Numeral
Akra_Bazzi: theory HOL-Library.Landau_Symbols
Akra_Bazzi: theory HOL-Library.Code_Target_Numeral
Akra_Bazzi: theory HOL-Library.Lattice_Algebras
Akra_Bazzi: theory HOL-Library.Log_Nat
Prime_Harmonic_Series: theory HOL-Algebra.Lattice
Akra_Bazzi: theory Landau_Symbols.Group_Sort
Prime_Harmonic_Series: theory HOL-Algebra.Complete_Lattice
Prime_Harmonic_Series: theory HOL-Algebra.Group
DiscretePricing: theory DiscretePricing.CRR_Model
Akra_Bazzi: theory Landau_Symbols.Landau_Real_Products
Prime_Harmonic_Series: theory HOL-Algebra.Coset
Prime_Harmonic_Series: theory HOL-Algebra.FiniteProduct
Akra_Bazzi: theory HOL-Library.Float
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1
Timing Applicative_Lifting (4 threads, 24.303s elapsed time, 76.648s cpu time, 4.860s GC time, factor 3.15)
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:03 elapsed time, 0:02:21 cpu time, factor 2.25)
Running Irrationality_J_Hancl ...
Prime_Harmonic_Series: theory HOL-Algebra.Ring
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis
Irrationality_J_Hancl: theory HOL-Library.Code_Abstract_Nat
Irrationality_J_Hancl: theory HOL-Library.Code_Target_Int
Irrationality_J_Hancl: theory HOL-Decision_Procs.Dense_Linear_Order
Irrationality_J_Hancl: theory HOL-Library.Lattice_Algebras
Irrationality_J_Hancl: theory HOL-Library.Code_Target_Nat
Prime_Harmonic_Series: theory HOL-Algebra.Generated_Groups
Irrationality_J_Hancl: theory HOL-Library.Log_Nat
Irrationality_J_Hancl: theory HOL-Library.Code_Target_Numeral
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis
Akra_Bazzi: theory Landau_Symbols.Landau_Simprocs
Akra_Bazzi: theory Landau_Symbols.Landau_More
Akra_Bazzi: theory HOL-Decision_Procs.Approximation_Bounds
Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Library
Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Asymptotics
Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Real
Prime_Harmonic_Series: theory HOL-Algebra.AbelCoset
Prime_Harmonic_Series: theory HOL-Algebra.Module
Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi
Akra_Bazzi: theory Akra_Bazzi.Master_Theorem
Irrationality_J_Hancl: theory HOL-Library.Float
Akra_Bazzi: theory HOL-Decision_Procs.Approximation
Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Method
Prime_Harmonic_Series: theory HOL-Algebra.Ideal
Irrationality_J_Hancl: theory HOL-Decision_Procs.Approximation_Bounds
Prime_Harmonic_Series: theory HOL-Algebra.RingHom
Prime_Harmonic_Series: theory HOL-Algebra.UnivPoly
Irrationality_J_Hancl: theory HOL-Decision_Procs.Approximation
Timing Ergodic_Theory (4 threads, 75.186s elapsed time, 255.236s cpu time, 5.324s 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:30 elapsed time, 0:04:39 cpu time, factor 3.10)
Running Stern_Brocot ...
Stern_Brocot: theory HOL-Library.BNF_Corec
Prime_Harmonic_Series: theory HOL-Algebra.Multiplicative_Group
Stern_Brocot: theory Stern_Brocot.Cotree
Prime_Harmonic_Series: theory HOL-Number_Theory.Residues
Prime_Harmonic_Series: theory HOL-Number_Theory.Euler_Criterion
Prime_Harmonic_Series: theory HOL-Number_Theory.Pocklington
Prime_Harmonic_Series: theory HOL-Number_Theory.Gauss
Prime_Harmonic_Series: theory HOL-Number_Theory.Residue_Primitive_Roots
Prime_Harmonic_Series: theory HOL-Number_Theory.Quadratic_Reciprocity
Prime_Harmonic_Series: theory HOL-Number_Theory.Number_Theory
Prime_Harmonic_Series: theory Prime_Harmonic_Series.Prime_Harmonic_Misc
Prime_Harmonic_Series: theory Prime_Harmonic_Series.Squarefree_Nat
Prime_Harmonic_Series: theory Prime_Harmonic_Series.Prime_Harmonic
Stern_Brocot: theory Stern_Brocot.Cotree_Algebra
Stern_Brocot: theory Stern_Brocot.Stern_Brocot_Tree
Timing MFMC_Countable (4 threads, 75.971s elapsed time, 233.440s cpu time, 6.712s GC time, factor 3.07)
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:25 elapsed time, 0:04:09 cpu time, factor 2.91)
Running Probabilistic_System_Zoo ...
Timing Green (4 threads, 77.891s elapsed time, 267.956s cpu time, 2.776s GC time, factor 3.44)
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:26 elapsed time, 0:04:48 cpu time, factor 3.34)
Running Treaps ...
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-Library.Cardinal_Notations
Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Extension
Probabilistic_System_Zoo: theory HOL-Cardinals.Wellfounded_More
Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Relation
Treaps: theory HOL-Data_Structures.Less_False
Treaps: theory HOL-Data_Structures.Cmp
Treaps: theory HOL-Library.Function_Algebras
Treaps: theory HOL-Library.Landau_Symbols
Treaps: theory HOL-Data_Structures.Sorted_Less
Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Embedding
Treaps: theory HOL-Data_Structures.List_Ins_Del
Treaps: theory Landau_Symbols.Group_Sort
Probabilistic_System_Zoo: theory HOL-Cardinals.Wellorder_Constructions
Treaps: theory List-Index.List_Index
Treaps: theory HOL-Data_Structures.Set_Specs
Treaps: theory HOL-Data_Structures.Tree_Set
Treaps: theory Comparison_Sort_Lower_Bound.Linorder_Relations
Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Order_Relation
Probabilistic_System_Zoo: theory HOL-Cardinals.Ordinal_Arithmetic
Timing DiscretePricing (4 threads, 72.730s elapsed time, 244.448s cpu time, 9.108s GC time, factor 3.36)
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:22 elapsed time, 0:04:20 cpu time, factor 3.15)
Running Prime_Distribution_Elementary ...
Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinal_Arithmetic
Probabilistic_System_Zoo: theory HOL-Cardinals.Cardinals
Treaps: theory Landau_Symbols.Landau_Real_Products
Probabilistic_System_Zoo: theory HOL-Cardinals.Bounded_Set
Akra_Bazzi: theory Akra_Bazzi.Akra_Bazzi_Approximation
Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Nonempty_Bounded_Set
Akra_Bazzi: theory Akra_Bazzi.Master_Theorem_Examples
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
Prime_Distribution_Elementary: theory Prime_Number_Theorem.Prime_Counting_Functions
Treaps: theory Landau_Symbols.Landau_Simprocs
Treaps: theory Landau_Symbols.Landau_More
Treaps: theory Quick_Sort_Cost.Randomised_Quick_Sort
Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Lcm_Nat_Upto
Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library
Prime_Distribution_Elementary: theory Prime_Number_Theorem.Mertens_Theorems
Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.More_Dirichlet_Misc
Treaps: theory Quick_Sort_Cost.Quick_Sort_Average_Case
Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Partial_Zeta_Bounds
Probabilistic_System_Zoo: theory HOL-Eisbach.Eisbach
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
Irrationality_J_Hancl: theory Irrationality_J_Hancl.Irrationality_J_Hancl
Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Probabilistic_Hierarchy
Treaps: theory Random_BSTs.Random_BSTs
Stern_Brocot: theory Stern_Brocot.Bird_Tree
Timing Prime_Harmonic_Series (4 threads, 78.515s elapsed time, 282.956s cpu time, 13.984s GC time, factor 3.60)
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:23 elapsed time, 0:04:52 cpu time, factor 3.52)
Timing Akra_Bazzi (4 threads, 73.360s elapsed time, 242.088s cpu time, 9.284s GC time, factor 3.30)
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:19 elapsed time, 0:04:14 cpu time, factor 3.19)
Building Randomised_Social_Choice ...
Running Monomorphic_Monad ...
Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Summatory_Divisor_Sigma_Bounds
Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Moebius_Mu_Sum
Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.Selberg_Asymptotic_Formula
Monomorphic_Monad: theory HOL-Library.Cardinal_Notations
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
Monomorphic_Monad: theory HOL-Library.Countable_Set_Type
Prime_Distribution_Elementary: theory Prime_Distribution_Elementary.PNT_Consequences
Randomised_Social_Choice: theory Randomised_Social_Choice.Order_Predicates
Treaps: theory Treaps.Treap
Treaps: theory Treaps.Probability_Misc
Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profiles
Treaps: theory Treaps.Random_List_Permutation
Monomorphic_Monad: theory Monomorphic_Monad.Monomorphic_Monad
Treaps: theory Treaps.Treap_Sort_and_BSTs
Randomised_Social_Choice: theory Randomised_Social_Choice.Elections
Randomised_Social_Choice: theory Randomised_Social_Choice.Utility_Functions
Randomised_Social_Choice: theory Randomised_Social_Choice.Preference_Profile_Cmd
Timing Stern_Brocot (4 threads, 45.616s elapsed time, 72.616s cpu time, 3.920s GC time, factor 1.59)
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.63)
Running Probabilistic_System_Zoo-Non_BNFs ...
Randomised_Social_Choice: theory Randomised_Social_Choice.Stochastic_Dominance
Timing Irrationality_J_Hancl (4 threads, 72.123s elapsed time, 159.048s cpu time, 5.980s GC time, factor 2.21)
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:17 elapsed time, 0:02:49 cpu time, factor 2.19)
Randomised_Social_Choice: theory Randomised_Social_Choice.SD_Efficiency
Building Quick_Sort_Cost ...
Randomised_Social_Choice: theory Randomised_Social_Choice.Social_Decision_Schemes
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Eisbach.Eisbach
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Fun_More
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Order_Relation_More
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Order_Union
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Library.Cardinal_Notations
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Wellorder_Extension
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Wellfounded_More
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Wellorder_Relation
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-Non_BNFs: theory HOL-Cardinals.Wellorder_Embedding
Treaps: theory Treaps.Random_Treap
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Wellorder_Constructions
Quick_Sort_Cost: theory Comparison_Sort_Lower_Bound.Linorder_Relations
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Cardinal_Order_Relation
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Ordinal_Arithmetic
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
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Cardinal_Arithmetic
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Cardinals
Quick_Sort_Cost: theory Landau_Symbols.Landau_Real_Products
Probabilistic_System_Zoo-Non_BNFs: theory HOL-Cardinals.Bounded_Set
Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Nonempty_Bounded_Set
Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Probabilistic_Hierarchy
Quick_Sort_Cost: theory Landau_Symbols.Landau_Simprocs
Quick_Sort_Cost: theory Landau_Symbols.Landau_More
Quick_Sort_Cost: theory Quick_Sort_Cost.Randomised_Quick_Sort
Probabilistic_System_Zoo: theory Probabilistic_System_Zoo.Vardi
Quick_Sort_Cost: theory Quick_Sort_Cost.Quick_Sort_Average_Case
Timing Constructive_Cryptography (4 threads, 330.117s elapsed time, 629.760s cpu time, 7.508s GC time, factor 1.91)
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:05:40 elapsed time, 0:10:47 cpu time, factor 1.90)
Running Game_Based_Crypto ...
Timing Treaps (4 threads, 37.685s elapsed time, 122.260s cpu time, 3.700s GC time, factor 3.24)
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:43 elapsed time, 0:02:12 cpu time, factor 3.08)
Running Prime_Number_Theorem ...
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
Monomorphic_Monad: theory Monomorphic_Monad.Interpreter
Game_Based_Crypto: theory Game_Based_Crypto.Unpredictable_Function
Monomorphic_Monad: theory Monomorphic_Monad.Just_Do_It_Examples
Monomorphic_Monad: theory Monomorphic_Monad.Monad_Overloading
Game_Based_Crypto: theory Game_Based_Crypto.RP_RF
Game_Based_Crypto: theory Game_Based_Crypto.IND_CCA2
Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem_Library
Prime_Number_Theorem: theory Stirling_Formula.Stirling_Formula
Timing Probabilistic_System_Zoo (4 threads, 41.318s elapsed time, 98.840s cpu time, 3.856s GC time, factor 2.39)
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
Finished Probabilistic_System_Zoo (0:00:45 elapsed time, 0:01:47 cpu time, factor 2.35)
Running Tarskis_Geometry ...
Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA
Game_Based_Crypto: theory Game_Based_Crypto.Elgamal
Tarskis_Geometry: theory HOL-Algebra.Congruence
Tarskis_Geometry: theory HOL-Library.Quadratic_Discriminant
Tarskis_Geometry: theory Tarskis_Geometry.Metric
Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Vardi
Tarskis_Geometry: theory Tarskis_Geometry.Miscellany
Prime_Number_Theorem: theory Prime_Number_Theorem.Newman_Ingham_Tauberian
Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Counting_Functions
Game_Based_Crypto: theory Game_Based_Crypto.PRF_IND_CPA
Tarskis_Geometry: theory Tarskis_Geometry.Linear_Algebra2
Tarskis_Geometry: theory Tarskis_Geometry.Tarski
Game_Based_Crypto: theory Game_Based_Crypto.IND_CPA_PK
Game_Based_Crypto: theory Game_Based_Crypto.PRF_UPF_IND_CCA
Tarskis_Geometry: theory Tarskis_Geometry.Euclid_Tarski
Tarskis_Geometry: theory HOL-Algebra.Order
Timing Prime_Distribution_Elementary (4 threads, 36.607s elapsed time, 138.704s cpu time, 3.108s GC time, factor 3.79)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Prime_Distribution_Elementary/outline.pdf
Finished Prime_Distribution_Elementary (0:00:44 elapsed time, 0:02:31 cpu time, factor 3.44)
Running UpDown_Scheme ...
Game_Based_Crypto: theory Game_Based_Crypto.SUF_CMA
Game_Based_Crypto: theory Game_Based_Crypto.Hashed_Elgamal
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
UpDown_Scheme: theory HOL-Library.Monad_Syntax
UpDown_Scheme: theory HOL-Imperative_HOL.Heap
Tarskis_Geometry: theory HOL-Algebra.Lattice
UpDown_Scheme: theory UpDown_Scheme.Grid_Point
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Syntax_Match
Prime_Number_Theorem: theory Prime_Number_Theorem.Prime_Number_Theorem
Prime_Number_Theorem: theory Prime_Number_Theorem.Mertens_Theorems
UpDown_Scheme: theory Automatic_Refinement.Misc
Tarskis_Geometry: theory HOL-Algebra.Complete_Lattice
Game_Based_Crypto: theory Game_Based_Crypto.Security_Spec
UpDown_Scheme: theory UpDown_Scheme.Grid
UpDown_Scheme: theory HOL-Imperative_HOL.Heap_Monad
Tarskis_Geometry: theory HOL-Algebra.Group
Game_Based_Crypto: theory Game_Based_Crypto.Cryptographic_Constructions
Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Finitely_Bounded_Set_Counterexample
Probabilistic_System_Zoo-Non_BNFs: theory Probabilistic_System_Zoo-Non_BNFs.Vardi_Counterexample
UpDown_Scheme: theory UpDown_Scheme.UpDown_Scheme
Timing Randomised_Social_Choice (4 threads, 12.879s elapsed time, 47.960s cpu time, 2.028s 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:39 elapsed time, 0:01:30 cpu time, factor 2.32)
Running SDS_Impossibility ...
UpDown_Scheme: theory UpDown_Scheme.Triangular_Function
Tarskis_Geometry: theory Tarskis_Geometry.Action
Tarskis_Geometry: theory Tarskis_Geometry.Projective
UpDown_Scheme: theory HOL-Imperative_HOL.Array
UpDown_Scheme: theory UpDown_Scheme.Down
UpDown_Scheme: theory UpDown_Scheme.Up
SDS_Impossibility: theory SDS_Impossibility.SDS_Impossibility
UpDown_Scheme: theory HOL-Imperative_HOL.Ref
UpDown_Scheme: theory UpDown_Scheme.Up_Down
UpDown_Scheme: theory HOL-Imperative_HOL.Imperative_HOL
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Run
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Assertions
Game_Based_Crypto: theory Game_Based_Crypto.Game_Based_Crypto
Timing Monomorphic_Monad (4 threads, 37.001s elapsed time, 65.080s cpu time, 2.872s GC time, factor 1.76)
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:44 elapsed time, 0:01:20 cpu time, factor 1.80)
Running Lp ...
Tarskis_Geometry: theory Tarskis_Geometry.Hyperbolic_Tarski
Lp: theory Ergodic_Theory.SG_Library_Complement
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Hoare_Triple
Timing Probabilistic_System_Zoo-Non_BNFs (4 threads, 36.867s elapsed time, 114.276s cpu time, 4.684s GC time, factor 3.10)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo-Non_BNFs/outline.pdf
Finished Probabilistic_System_Zoo-Non_BNFs (0:00:42 elapsed time, 0:02:04 cpu time, factor 2.95)
Building Stirling_Formula ...
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Automation
Lp: theory Lp.Functional_Spaces
Stirling_Formula: theory HOL-Library.Function_Algebras
Stirling_Formula: theory HOL-Library.Stirling
Stirling_Formula: theory Bernoulli.Bernoulli
Stirling_Formula: theory HOL-Library.Landau_Symbols
Stirling_Formula: theory Landau_Symbols.Group_Sort
UpDown_Scheme: theory Separation_Logic_Imperative_HOL.Sep_Main
UpDown_Scheme: theory UpDown_Scheme.Imperative
Stirling_Formula: theory Bernoulli.Periodic_Bernpoly
Stirling_Formula: theory Bernoulli.Bernoulli_FPS
Lp: theory Lp.Lp
Timing Quick_Sort_Cost (4 threads, 15.776s elapsed time, 58.192s cpu time, 2.172s GC time, factor 3.69)
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:44 elapsed time, 0:01:45 cpu time, factor 2.38)
Running Quaternions ...
Quaternions: theory Quaternions.Quaternions
Stirling_Formula: theory Landau_Symbols.Landau_Real_Products
Stirling_Formula: theory Landau_Symbols.Landau_Simprocs
Stirling_Formula: theory Landau_Symbols.Landau_More
Stirling_Formula: theory Stirling_Formula.Stirling_Formula
Stirling_Formula: theory Stirling_Formula.Ln_Gamma_Asymptotics
Timing Game_Based_Crypto (4 threads, 30.603s elapsed time, 115.368s cpu time, 2.956s GC time, factor 3.77)
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:00:40 elapsed time, 0:02:14 cpu time, factor 3.31)
Running pGCL ...
pGCL: theory pGCL.Misc
pGCL: theory pGCL.Expectations
Timing Prime_Number_Theorem (4 threads, 33.076s elapsed time, 104.032s cpu time, 2.740s GC time, factor 3.15)
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:40 elapsed time, 0:01:57 cpu time, factor 2.88)
Running HOL-Analysis-ex ...
pGCL: theory pGCL.Transformers
Timing UpDown_Scheme (4 threads, 30.975s elapsed time, 120.084s cpu time, 3.628s GC time, factor 3.88)
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:36 elapsed time, 0:02:10 cpu time, factor 3.57)
Running Kuratowski_Closure_Complement ...
HOL-Analysis-ex: theory HOL-Analysis-ex.Approximations
Timing Tarskis_Geometry (4 threads, 31.424s elapsed time, 111.856s cpu time, 3.604s GC time, factor 3.56)
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:40 elapsed time, 0:02:06 cpu time, factor 3.16)
Running Octonions ...
pGCL: theory pGCL.Induction
Kuratowski_Closure_Complement: theory Kuratowski_Closure_Complement.KuratowskiClosureComplementTheorem
pGCL: theory pGCL.Embedding
Octonions: theory Octonions.Cross_Product_7
pGCL: theory pGCL.Healthiness
pGCL: theory pGCL.Continuity
pGCL: theory pGCL.LoopInduction
pGCL: theory pGCL.Sublinearity
pGCL: theory pGCL.WellDefined
pGCL: theory pGCL.Algebra
pGCL: theory pGCL.Determinism
pGCL: theory pGCL.Loops
pGCL: theory pGCL.StructuredReasoning
Octonions: theory Octonions.Octonions
pGCL: theory pGCL.Automation
pGCL: theory pGCL.Termination
pGCL: theory pGCL.pGCL
Timing Lp (4 threads, 26.668s elapsed time, 87.336s cpu time, 1.412s GC time, factor 3.27)
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:33 elapsed time, 0:01:40 cpu time, factor 2.98)
Running Euler_MacLaurin ...
pGCL: theory pGCL.LoopExamples
pGCL: theory pGCL.Monty
pGCL: theory pGCL.Primitives
Euler_MacLaurin: theory HOL-Library.Function_Algebras
Euler_MacLaurin: theory HOL-Library.Stirling
Euler_MacLaurin: theory Bernoulli.Bernoulli
Euler_MacLaurin: theory HOL-Library.Landau_Symbols
Euler_MacLaurin: theory Landau_Symbols.Group_Sort
Euler_MacLaurin: theory Bernoulli.Periodic_Bernpoly
Euler_MacLaurin: theory Bernoulli.Bernoulli_FPS
Timing Quaternions (4 threads, 24.837s elapsed time, 34.644s cpu time, 0.724s GC time, factor 1.39)
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:30 elapsed time, 0:00:45 cpu time, factor 1.51)
Building Random_BSTs ...
Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin
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
Random_BSTs: theory HOL-Data_Structures.Set_Specs
Random_BSTs: theory HOL-Data_Structures.Tree_Set
Euler_MacLaurin: theory Landau_Symbols.Landau_Real_Products
Random_BSTs: theory Random_BSTs.Random_BSTs
Timing SDS_Impossibility (4 threads, 39.951s elapsed time, 92.972s cpu time, 1.580s GC time, factor 2.33)
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:46 elapsed time, 0:01:44 cpu time, factor 2.26)
Running Probabilistic_System_Zoo-BNFs ...
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Fun_More
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Order_Relation_More
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Order_Union
Probabilistic_System_Zoo-BNFs: theory HOL-Library.Cardinal_Notations
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Wellorder_Extension
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Wellfounded_More
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Wellorder_Relation
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Wellorder_Embedding
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Wellorder_Constructions
Euler_MacLaurin: theory Landau_Symbols.Landau_Simprocs
Euler_MacLaurin: theory Landau_Symbols.Landau_More
Euler_MacLaurin: theory Euler_MacLaurin.Euler_MacLaurin_Landau
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Cardinal_Order_Relation
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Ordinal_Arithmetic
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Cardinal_Arithmetic
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Cardinals
Probabilistic_System_Zoo-BNFs: theory HOL-Cardinals.Bounded_Set
Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Bool_Bounded_Set
Probabilistic_System_Zoo-BNFs: theory Probabilistic_System_Zoo-BNFs.Nonempty_Bounded_Set
Timing HOL-Analysis-ex (4 threads, 23.276s elapsed time, 58.772s cpu time, 0.268s GC time, factor 2.53)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Analysis-ex
Finished HOL-Analysis-ex (0:00:24 elapsed time, 0:01:00 cpu time, factor 2.42)
Running Cayley_Hamilton ...
Cayley_Hamilton: theory HOL-Library.More_List
Cayley_Hamilton: theory Cayley_Hamilton.Square_Matrix
Cayley_Hamilton: theory HOL-Computational_Algebra.Polynomial
Timing Octonions (4 threads, 20.002s elapsed time, 68.332s cpu time, 1.720s GC time, factor 3.42)
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:25 elapsed time, 0:01:18 cpu time, factor 3.12)
Running Neumann_Morgenstern_Utility ...
Timing Stirling_Formula (4 threads, 22.907s elapsed time, 75.672s cpu time, 2.500s GC time, factor 3.30)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stirling_Formula/outline.pdf
Finished Stirling_Formula (0:00:49 elapsed time, 0:02:01 cpu time, factor 2.44)
Running Catalan_Numbers ...
Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Syntax
Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.PMF_Composition
Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Preferences
Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Lotteries
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, 22.652s elapsed time, 72.212s cpu time, 1.832s GC time, factor 3.19)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Kuratowski_Closure_Complement/outline.pdf
Finished Kuratowski_Closure_Complement (0:00:28 elapsed time, 0:01:23 cpu time, factor 2.95)
Running Error_Function ...
Neumann_Morgenstern_Utility: theory First_Welfare_Theorem.Utility_Functions
Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem
Error_Function: theory HOL-Library.Function_Algebras
Error_Function: theory HOL-Library.Landau_Symbols
Error_Function: theory Landau_Symbols.Group_Sort
Timing pGCL (4 threads, 24.019s elapsed time, 91.320s cpu time, 1.744s GC time, factor 3.80)
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:33 elapsed time, 0:01:48 cpu time, factor 3.23)
Running HOL-Probability-ex ...
Catalan_Numbers: theory Landau_Symbols.Landau_Real_Products
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
Timing Euler_MacLaurin (4 threads, 18.121s elapsed time, 67.096s cpu time, 2.384s GC time, factor 3.70)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Euler_MacLaurin
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Euler_MacLaurin/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Euler_MacLaurin/outline.pdf
Finished Euler_MacLaurin (0:00:23 elapsed time, 0:01:18 cpu time, factor 3.28)
Running Bernoulli ...
Neumann_Morgenstern_Utility: theory Neumann_Morgenstern_Utility.Expected_Utility
HOL-Probability-ex: theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure
Bernoulli: theory HOL-Library.Stirling
Bernoulli: theory Bernoulli.Bernoulli
Error_Function: theory Error_Function.Error_Function
Error_Function: theory Landau_Symbols.Landau_Real_Products
Bernoulli: theory Bernoulli.Periodic_Bernpoly
Bernoulli: theory Bernoulli.Bernoulli_FPS
Cayley_Hamilton: theory Cayley_Hamilton.Cayley_Hamilton
Timing Probabilistic_System_Zoo-BNFs (4 threads, 14.453s elapsed time, 53.500s cpu time, 1.760s GC time, factor 3.70)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo-BNFs
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo-BNFs/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Probabilistic_System_Zoo-BNFs/outline.pdf
Finished Probabilistic_System_Zoo-BNFs (0:00:19 elapsed time, 0:01:03 cpu time, factor 3.25)
Running Random_Graph_Subgraph_Threshold ...
Bernoulli: theory Bernoulli.Bernoulli_Zeta
Catalan_Numbers: theory Landau_Symbols.Landau_Simprocs
Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Misc
Catalan_Numbers: theory Landau_Symbols.Landau_More
Catalan_Numbers: theory Catalan_Numbers.Catalan_Numbers
Error_Function: theory Landau_Symbols.Landau_Simprocs
Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Prob_Lemmas
Error_Function: theory Landau_Symbols.Landau_More
Error_Function: theory Error_Function.Error_Function_Asymptotics
Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Ugraph_Properties
Random_Graph_Subgraph_Threshold: theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold
Timing Cayley_Hamilton (4 threads, 12.955s elapsed time, 40.052s cpu time, 1.672s GC time, factor 3.09)
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:49 cpu time, factor 2.81)
Running Rank_Nullity_Theorem ...
Timing HOL-Probability-ex (4 threads, 9.833s elapsed time, 26.792s cpu time, 0.648s GC time, factor 2.72)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/HOL/HOL-Probability-ex
Finished HOL-Probability-ex (0:00:11 elapsed time, 0:00:28 cpu time, factor 2.42)
Running First_Welfare_Theorem ...
Rank_Nullity_Theorem: theory HOL-Library.Bit
Rank_Nullity_Theorem: theory HOL-Library.Function_Algebras
Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dual_Order
Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Mod_Type
Timing Random_BSTs (4 threads, 8.327s elapsed time, 16.688s cpu time, 0.892s GC time, factor 2.00)
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:56 cpu time, factor 1.74)
Running Randomised_BSTs ...
Timing Catalan_Numbers (4 threads, 12.245s elapsed time, 40.716s cpu time, 1.572s 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:16 elapsed time, 0:00:50 cpu time, factor 2.98)
Timing Neumann_Morgenstern_Utility (4 threads, 12.231s elapsed time, 40.588s cpu time, 0.840s GC time, factor 3.32)
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:51 cpu time, factor 2.87)
Running Comparison_Sort_Lower_Bound ...
First_Welfare_Theorem: theory First_Welfare_Theorem.Syntax
First_Welfare_Theorem: theory First_Welfare_Theorem.Argmax
Running Chord_Segments ...
First_Welfare_Theorem: theory First_Welfare_Theorem.Consumers
First_Welfare_Theorem: theory First_Welfare_Theorem.Preferences
Timing Error_Function (4 threads, 11.822s elapsed time, 42.232s cpu time, 1.504s GC time, factor 3.57)
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:51 cpu time, factor 3.11)
Running Lower_Semicontinuous ...
Randomised_BSTs: theory Monad_Normalisation.Monad_Normalisation
Chord_Segments: theory Triangle.Angles
Comparison_Sort_Lower_Bound: theory HOL-Library.Multiset_Permutations
Comparison_Sort_Lower_Bound: theory List-Index.List_Index
Randomised_BSTs: theory Randomised_BSTs.Randomised_BSTs
Chord_Segments: theory Triangle.Triangle
First_Welfare_Theorem: theory First_Welfare_Theorem.Utility_Functions
Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Miscellaneous
First_Welfare_Theorem: theory First_Welfare_Theorem.Common
Chord_Segments: theory Chord_Segments.Chord_Segments
Lower_Semicontinuous: theory Lower_Semicontinuous.Lower_Semicontinuous
First_Welfare_Theorem: theory First_Welfare_Theorem.Arrow_Debreu_Model
First_Welfare_Theorem: theory First_Welfare_Theorem.Exchange_Economy
Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Linorder_Relations
First_Welfare_Theorem: theory First_Welfare_Theorem.Private_Ownership_Economy
Timing Bernoulli (4 threads, 9.512s elapsed time, 25.400s cpu time, 0.408s GC time, factor 2.67)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Bernoulli/outline.pdf
Finished Bernoulli (0:00:14 elapsed time, 0:00:35 cpu time, factor 2.41)
Running Buffons_Needle ...
Comparison_Sort_Lower_Bound: theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound
Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Fundamental_Subspaces
Rank_Nullity_Theorem: theory Rank_Nullity_Theorem.Dim_Formula
Buffons_Needle: theory Buffons_Needle.Buffons_Needle
Timing Random_Graph_Subgraph_Threshold (4 threads, 7.505s elapsed time, 21.848s cpu time, 0.528s GC time, factor 2.91)
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:33 cpu time, factor 2.45)
Running Source_Coding_Theorem ...
Source_Coding_Theorem: theory Source_Coding_Theorem.Source_Coding_Theorem
Timing Chord_Segments (4 threads, 4.985s elapsed time, 10.140s cpu time, 0.124s GC time, factor 2.03)
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:09 elapsed time, 0:00:20 cpu time, factor 2.04)
Running Stewart_Apollonius ...
Timing Rank_Nullity_Theorem (4 threads, 8.086s elapsed time, 16.704s cpu time, 0.612s GC time, factor 2.07)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rank_Nullity_Theorem/outline.pdf
Finished Rank_Nullity_Theorem (0:00:13 elapsed time, 0:00:26 cpu time, factor 2.04)
Running Triangle ...
Timing Lower_Semicontinuous (4 threads, 4.990s elapsed time, 15.768s cpu time, 0.260s GC time, factor 3.16)
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:10 elapsed time, 0:00:25 cpu time, factor 2.53)
Running Fisher_Yates ...
Stewart_Apollonius: theory Triangle.Angles
Timing First_Welfare_Theorem (4 threads, 7.592s elapsed time, 26.180s cpu time, 0.556s GC time, factor 3.45)
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:36 cpu time, factor 2.86)
Running Ptolemys_Theorem ...
Stewart_Apollonius: theory Triangle.Triangle
Triangle: theory Triangle.Angles
Stewart_Apollonius: theory Stewart_Apollonius.Stewart_Apollonius
Timing Comparison_Sort_Lower_Bound (4 threads, 7.920s elapsed time, 21.020s cpu time, 0.748s GC time, factor 2.65)
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:30 cpu time, factor 2.42)
Timing Buffons_Needle (4 threads, 4.399s elapsed time, 14.304s cpu time, 0.088s GC time, factor 3.25)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Buffons_Needle/outline.pdf
Finished Buffons_Needle (0:00:09 elapsed time, 0:00:23 cpu time, factor 2.56)
Running Minkowskis_Theorem ...
Running Cartan_FP ...
Triangle: theory Triangle.Triangle
Fisher_Yates: theory Fisher_Yates.Fisher_Yates
Ptolemys_Theorem: theory Ptolemys_Theorem.Ptolemys_Theorem
Minkowskis_Theorem: theory Minkowskis_Theorem.Minkowskis_Theorem
Cartan_FP: theory Cartan_FP.Cartan
Timing Source_Coding_Theorem (4 threads, 4.203s elapsed time, 11.192s cpu time, 0.132s GC time, factor 2.66)
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:09 elapsed time, 0:00:21 cpu time, factor 2.30)
Timing Randomised_BSTs (4 threads, 9.371s elapsed time, 30.880s cpu time, 0.624s GC time, factor 3.30)
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:14 elapsed time, 0:00:40 cpu time, factor 2.79)
Running Monad_Normalisation ...
Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation
Monad_Normalisation: theory Monad_Normalisation.Monad_Normalisation_Test
Timing Cartan_FP (4 threads, 1.472s elapsed time, 4.616s cpu time, 0.076s GC time, factor 3.13)
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:05 elapsed time, 0:00:13 cpu time, factor 2.37)
Timing Stewart_Apollonius (4 threads, 3.938s elapsed time, 7.156s cpu time, 0.080s GC time, factor 1.82)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stewart_Apollonius/outline.pdf
Finished Stewart_Apollonius (0:00:08 elapsed time, 0:00:15 cpu time, factor 1.93)
Timing Ptolemys_Theorem (4 threads, 2.056s elapsed time, 4.780s cpu time, 0.068s GC time, factor 2.32)
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:06 elapsed time, 0:00:13 cpu time, factor 2.19)
Timing Minkowskis_Theorem (4 threads, 1.317s elapsed time, 4.544s cpu time, 0.092s GC time, factor 3.45)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Minkowskis_Theorem/outline.pdf
Finished Minkowskis_Theorem (0:00:05 elapsed time, 0:00:13 cpu time, factor 2.34)
Timing Triangle (4 threads, 3.566s elapsed time, 6.200s cpu time, 0.072s GC time, factor 1.74)
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:07 elapsed time, 0:00:14 cpu time, factor 1.90)
Timing Fisher_Yates (4 threads, 2.929s elapsed time, 8.284s cpu time, 0.072s GC time, factor 2.83)
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.35)
Timing Monad_Normalisation (4 threads, 1.017s elapsed time, 1.516s cpu time, 0.000s GC time, factor 1.49)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monad_Normalisation
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monad_Normalisation/document.pdf
Document at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Monad_Normalisation/outline.pdf
Finished Monad_Normalisation (0:00:05 elapsed time, 0:00:10 cpu time, factor 1.93)
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1
HOL-ODE-Numerics: theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform
*** Timeout
Smooth_Manifolds FAILED
(see also /media/data/jenkins/workspace/isabelle-all/heaps/polyml-5.8_x86_64-linux/log/Smooth_Manifolds)
*** Failed to finish proof (line 587 of "$AFP/Smooth_Manifolds/Analysis_More.thy"):
*** goal (1 subgoal):
*** 1. \U.
*** \U \ f ` topspace T;
*** openin T (f -` U \ topspace T)\
*** \ openin T {x \ topspace T. f x \ U}
*** At command "by" (line 587 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
*** Failed to finish proof (line 552 of "$AFP/Smooth_Manifolds/Analysis_More.thy"):
*** goal (1 subgoal):
*** 1. \openin Z V;
*** \x\topspace (Y i). g (f i x) \ topspace Z;
*** openin (Y i) {x \ topspace (Y i). g (f i x) \ V}\
*** \ openin (Y i)
*** ((g \ f i) -` V \ topspace (Y i))
*** At command "by" (line 552 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
*** Failed to finish proof (line 540 of "$AFP/Smooth_Manifolds/Analysis_More.thy"):
*** goal (1 subgoal):
*** 1. \U.
*** \\i. f i \ topspace (Y i) \ X;
*** U \ X;
*** \i. openin (Y i) (f i -` U \ topspace (Y i))\
*** \ openin (Y i)
*** {x \ topspace (Y i). f i x \ U}
*** At command "by" (line 540 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
*** Failed to finish proof (line 442 of "$AFP/Smooth_Manifolds/Analysis_More.thy"):
*** goal (2 subgoals):
*** 1. \X.
*** \\x\topspace T1. x \ topspace T2;
*** \U.
*** openin T2 U \
*** openin T1 {x \ topspace T1. x \ U};
*** openin T2 X\
*** \ openin T1 (X \ topspace T1)
*** 2. \U.
*** \\X.
*** openin T2 X \
*** openin T1 (X \ topspace T1);
*** topspace T1 \ topspace T2; openin T2 U\
*** \ openin T1 {x \ topspace T1. x \ U}
*** At command "by" (line 442 of "$AFP/Smooth_Manifolds/Analysis_More.thy")
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, 1725.168s elapsed time, 5617.184s cpu time, 1529.592s GC time, factor 3.26)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Numerics
Finished HOL-ODE-Numerics (0:30:23 elapsed time, 1:39:26 cpu time, factor 3.27)
Building Lorenz_Approximation ...
Running HOL-ODE-ARCH-COMP ...
Running HOL-ODE-Examples ...
Lorenz_Approximation: theory Lorenz_Approximation.Result_Elements
HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_One_Step_Method
HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Poincare_Map
HOL-ODE-Examples: theory HOL-ODE-Examples.Examples_Integral
HOL-ODE-ARCH-COMP: theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP
Lorenz_Approximation: theory Lorenz_Approximation.Result_File_Coarse
Lorenz_Approximation: theory Lorenz_Approximation.Lorenz_Approximation
HOL-ODE-Examples: theory HOL-ODE-Examples.ODE_Examples
Timing HOL-ODE-Examples (4 threads, 233.463s elapsed time, 764.668s cpu time, 10.748s GC time, factor 3.28)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-Examples
Finished HOL-ODE-Examples (0:03:56 elapsed time, 0:12:47 cpu time, factor 3.25)
Timing HOL-ODE-ARCH-COMP (4 threads, 266.761s elapsed time, 594.092s cpu time, 31.444s GC time, factor 2.23)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/HOL-ODE-ARCH-COMP
Finished HOL-ODE-ARCH-COMP (0:04:29 elapsed time, 0:09:56 cpu time, factor 2.22)
Timing Lorenz_Approximation (4 threads, 247.287s elapsed time, 510.024s cpu time, 49.960s GC time, factor 2.06)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_Approximation
Finished Lorenz_Approximation (0:04:41 elapsed time, 0:09:30 cpu time, factor 2.03)
Running Lorenz_C0 ...
Running Lorenz_C1 ...
Lorenz_C0: theory Lorenz_C0.Lorenz_C0
Lorenz_C1: theory Lorenz_C1.Lorenz_C1
Timing Lorenz_C1 (4 threads, 1.027s elapsed time, 1.760s 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.19)
Timing Lorenz_C0 (4 threads, 638.363s elapsed time, 2505.436s cpu time, 29.404s GC time, factor 3.92)
Browser info at /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Lorenz_C0
Finished Lorenz_C0 (0:10:40 elapsed time, 0:41:47 cpu time, factor 3.91)
Unfinished session(s): Functional_Ordered_Resolution_Prover, Higher_Order_Terms, Lambda_Free_EPO, Lambda_Free_KBOs, Lambda_Free_RPOs, Noninterference_Generic_Unwinding, Smooth_Manifolds
=== TIMING ===
Group AFP: 3:40:14 elapsed time, 10:15:00 cpu time, factor 2.79
Group main: 0:13:34 elapsed time, 0:42:31 cpu time, factor 3.13
Group doc: 0:00:00 elapsed time
Group timing: 0:13:46 elapsed time, 0:43:00 cpu time, factor 3.12
Group large: 0:14:40 elapsed time, 0:54:39 cpu time, factor 3.72
Group no_doc: 0:00:00 elapsed time
Overall: 1:01:54 elapsed time, 10:59:01 cpu time, factor 10.65
=== FAILED SESSIONS ===
Session Lambda_Free_KBOs: FAILED 2
Session Smooth_Manifolds: FAILED 1
Session Functional_Ordered_Resolution_Prover: FAILED 2
Session Higher_Order_Terms: FAILED 2
Session Noninterference_Generic_Unwinding: FAILED 2
Session Lambda_Free_EPO: FAILED 2
Session Lambda_Free_RPOs: FAILED 2
=== DEPENDENCIES ===
Generating dependencies file ...
Writing dependencies file ...
=== REPORT ===
Writing report file ...
=== SITEGEN ===
Writing status file ...
Running sitegen ...
[32mSuccess: Generated topics.html[0m
[32mSuccess: Generated index.html[0m
[32mSuccess: Generated html files for 466 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
[1m[32mChecked directory thys. Found 0 warnings.[0m
Packing tars ...
=== NOTIFICATIONS ===
Entry Noninterference_Generic_Unwinding: WARNING no maintainers specified
=== COMPLETED ===
Build step 'Execute shell' marked build as failure
Archiving artifacts
Started calculate disk usage of build
Finished Calculation of disk usage of build in 0 seconds
Started calculate disk usage of workspace
Finished Calculation of disk usage of workspace in 0 seconds
No emails were triggered.
Finished: FAILURE