Started by an SCM change
Running as SYSTEM
[EnvInject] - Loading node environment variables.
Building remotely on workermtahpc (mta_hpc) 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/
real URL is https://isabelle.in.tum.de/repos/isabelle/
no changes found
[isabelle-all] $ hg update --clean --rev default
0 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 33025e13dcdc08ee6ca7434ad5f3e310b52b0c60 --template exists\n
exists
[isabelle-all] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(33025e13dcdc08ee6ca7434ad5f3e310b52b0c60)" --encoding UTF-8 --encodingmode replace
[afp] $ hg showconfig paths.default
[afp] $ hg pull --rev default
pulling from https://foss.heptapod.net/isa-afp/afp-devel/
no changes found
[afp] $ hg update --clean --rev default
1440 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 da2bce68bc3122aa3656421828841d63ae0da4af --template exists\n
exists
[afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('default') and not ancestors(da2bce68bc3122aa3656421828841d63ae0da4af)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-all] $ /bin/sh -xe /tmp/jenkins3974874297834284511.sh
+ Admin/jenkins/run_build all
+ set -e
+ PROFILE=all
+ shift
+ bin/isabelle components -a
+ bin/isabelle jedit -bf
### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle.jar) ...
### Building graph browser (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_graphbrowser.jar) ...
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_admin.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
+ bin/isabelle ocaml_setup
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
       opam update

[NOTE] Package zarith is already installed (current version is 1.12).
+ 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.10.7
+ bin/isabelle ci_build all

=== CONFIGURATION ===

ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-bafe319bc3a6-1/x86_64_32-linux"
ML_SYSTEM="polyml-5.9"
ML_OPTIONS="-H 4000 --maxheap 8G"
jobs = 8, threads = 8, numa = true

=== BUILD ===

Build started at Fri, 25 Nov 2022 11:27:25 +0100
Isabelle id 33025e13dcdc
AFP id 65cec4220156

=== LOG ===

Session Pure/Pure
Session Misc/CTT
Session Misc/Cube
Session FOL/FOL
Session FOL/CCL
Session FOL/FOL-ex
Session FOL/FOLP
Session FOL/FOLP-ex
Session Doc/Intro (doc)
Session FOL/LCF
Session Doc/Logics (doc)
Session Doc/Nitpick (doc)
Session Pure/Pure-Examples
Session Pure/Pure-ex
Session Misc/SML
Session Misc/Sequents
Session Doc/Sledgehammer (doc)
Session AFP/SpecCheck (AFP)
Session Misc/Tools
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/Ackermanns_not_PR (AFP)
Session AFP/AnselmGod (AFP)
Session AFP/Aristotles_Assertoric_Syllogistic (AFP)
Session AFP/Attack_Trees (AFP)
Session AFP/AxiomaticCategoryTheory (AFP)
Session AFP/Belief_Revision (AFP)
Session AFP/BinarySearchTree (AFP)
Session AFP/Binomial-Queues (AFP)
Session AFP/Bondy (AFP)
Session AFP/Boolos_Curious_Inference (AFP)
Session AFP/BytecodeLogicJmlTypes (AFP)
Session AFP/C2KA_DistributedSystems (AFP)
Session AFP/CISC-Kernel (AFP)
Session AFP/CYK (AFP)
Session AFP/Cauchy (AFP)
Session AFP/Sqrt_Babylonian (AFP)
Session Doc/Classes (doc)
Session AFP/ClockSynchInst (AFP)
Session AFP/Compiling-Exceptions-Correctly (AFP)
Session AFP/Complete_Non_Orders (AFP)
Session AFP/ComponentDependencies (AFP)
Session AFP/Concurrent_Revisions (AFP)
Session AFP/Constructor_Funs (AFP)
Session AFP/CryptoBasedCompositionalProperties (AFP)
Session AFP/DPT-SAT-Solver (AFP)
Session AFP/Dedekind_Real (AFP)
Session Doc/Demo_EPTCS (doc)
Session Doc/Demo_Easychair (doc)
Session Doc/Demo_FoilTeX (doc)
Session Doc/Demo_LIPIcs (doc)
Session Doc/Demo_LLNCS (doc)
Session AFP/Depth-First-Search (AFP)
Session AFP/Digit_Expansions (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/Foundation_of_geometry (AFP)
Session AFP/Free-Boolean-Algebra (AFP)
Session AFP/Fresh_Identifiers (AFP)
Session AFP/FunWithFunctions (AFP)
Session AFP/FunWithTilings (AFP)
Session Doc/Functions (doc)
Session AFP/GPU_Kernel_PL (AFP)
Session AFP/GenClock (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/Generic_Deriving (AFP)
Session AFP/GewirthPGCProof (AFP)
Session AFP/GoedelGod (AFP)
Session AFP/Goodstein_Lambda (AFP)
Session HOL/HOL-Cardinals (timing)
Session AFP/Binding_Syntax_Theory (AFP)
Session AFP/Ordinals_and_Cardinals (AFP)
Session AFP/Risk_Free_Lending (AFP)
Session HOL/HOL-Hoare
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/ADS_Functor (AFP)
Session AFP/Approximation_Algorithms (AFP)
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/Bounded_Deducibility_Security (AFP)
Session AFP/BD_Security_Compositional (AFP)
Session AFP/CoSMeDis (AFP)
Session AFP/CoCon (AFP)
Session AFP/CoSMed (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 Doc/Codegen (doc)
Session AFP/CofGroups (AFP)
Session AFP/Completeness (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/Concurrent_Ref_Alg (AFP)
Session AFP/Conditional_Simplification (AFP)
Session AFP/Conditional_Transfer_Rule (AFP)
Session AFP/CoreC++ (AFP)
Session AFP/Core_DOM (AFP)
Session AFP/Shadow_DOM (AFP)
Session AFP/DOM_Components (AFP)
Session AFP/Core_SC_DOM (AFP)
Session AFP/Shadow_SC_DOM (AFP)
Session AFP/SC_DOM_Components (AFP)
Session Doc/Datatypes (doc)
Session Doc/Corec (doc)
Session AFP/Decl_Sem_Fun_PL (AFP)
Session AFP/Encodability_Process_Calculi (AFP)
Session AFP/Epistemic_Logic (AFP)
Session AFP/Public_Announcement_Logic (AFP)
Session AFP/Stalnaker_Logic (AFP)
Session AFP/Euler_Partition (AFP)
Session AFP/FOL-Fitting (AFP)
Session AFP/FOL_Seq_Calc1 (AFP)
Session AFP/FOL_Axiomatic (AFP)
Session AFP/FOL_Harrison (AFP)
Session AFP/Factored_Transition_System_Bounding (AFP)
Session AFP/FinFun (AFP)
Session AFP/Extended_Finite_State_Machines (AFP)
Session AFP/Extended_Finite_State_Machine_Inference (AFP)
Session AFP/Finger-Trees (AFP)
Session AFP/Finite-Map-Extras (AFP)
Session AFP/Generalized_Counting_Sort (AFP)
Session AFP/Graph_Saturation (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-Combinatorics (main timing)
Session AFP/Blue_Eyes (AFP)
Session AFP/Derangements (AFP)
Session AFP/Discrete_Summation (AFP)
Session AFP/Gauss-Jordan-Elim-Fun (AFP)
Session AFP/Graph_Theory (AFP)
Session AFP/ShortestPath (AFP)
Session HOL/HOL-Computational_Algebra (main timing)
Session AFP/Descartes_Sign_Rule (AFP)
Session HOL/HOL-Algebra (main timing)
Session AFP/Finitely_Generated_Abelian_Groups (AFP)
Session HOL/HOL-Decision_Procs (timing)
Session HOL/HOL-Quotient_Examples (timing)
Session AFP/Interpolation_Polynomials_HOL_Algebra (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/Actuarial_Mathematics (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/Complex_Geometry (AFP)
Session AFP/Poincare_Disc (AFP)
Session AFP/Differential_Game_Logic (AFP)
Session AFP/First_Welfare_Theorem (AFP)
Session AFP/Green (AFP)
Session HOL/HOL-Analysis-ex
Session HOL/HOL-Complex_Analysis (main timing)
Session AFP/Cartan_FP (AFP)
Session HOL/HOL-Eisbach
Session AFP/Allen_Calculus (AFP)
Session AFP/Card_Partitions (AFP)
Session AFP/Bell_Numbers_Spivey (AFP)
Session AFP/Card_Equiv_Relations (AFP)
Session AFP/Equivalence_Relation_Enumeration (AFP)
Session AFP/Falling_Factorial_Sum (AFP)
Session AFP/Case_Labeling (AFP)
Session AFP/Clean (AFP)
Session AFP/Combinatorics_Words (AFP)
Session AFP/Combinatorics_Words_Graph_Lemma (AFP)
Session AFP/Dependent_SIFUM_Type_Systems (AFP)
Session AFP/Dependent_SIFUM_Refinement (AFP)
Session Doc/Eisbach (doc)
Session HOL/HOL-Hahn_Banach
Session HOL/HOL-Homology (timing)
Session HOL/HOL-Probability (main timing)
Session AFP/Buffons_Needle (AFP)
Session AFP/Density_Compiler (AFP)
Session AFP/DiscretePricing (AFP)
Session AFP/Ergodic_Theory (AFP)
Session AFP/Gromov_Hyperbolicity (AFP)
Session AFP/Laws_of_Large_Numbers (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/Hahn_Jordan_Decomposition (AFP)
Session AFP/Lp (AFP)
Session AFP/MDP-Rewards (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/Quasi_Borel_Spaces (AFP)
Session AFP/Skip_Lists (AFP)
Session AFP/Source_Coding_Theorem (AFP)
Session AFP/Hyperdual (AFP)
Session AFP/Irrationality_J_Hancl (AFP)
Session AFP/Kuratowski_Closure_Complement (AFP)
Session AFP/Laplace_Transform (AFP)
Session AFP/Lower_Semicontinuous (AFP)
Session AFP/Minkowskis_Theorem (AFP)
Session AFP/Octonions (AFP)
Session AFP/Ptolemys_Theorem (AFP)
Session AFP/Quaternions (AFP)
Session AFP/Rank_Nullity_Theorem (AFP)
Session AFP/Gauss_Jordan (AFP)
Session AFP/Echelon_Form (AFP)
Session AFP/Hermite (AFP)
Session AFP/MDP-Algorithms (AFP)
Session AFP/Tarskis_Geometry (AFP)
Session AFP/Triangle (AFP)
Session AFP/Chord_Segments (AFP)
Session AFP/Stewart_Apollonius (AFP)
Session AFP/Youngs_Inequality (AFP)
Session AFP/pGCL (AFP)
Session HOL/HOL-Examples
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/Arith_Prog_Rel_Primes (AFP)
Session AFP/Bernoulli (AFP)
Session AFP/E_Transcendental (AFP)
Session AFP/Elliptic_Curves_Group_Law (AFP)
Session AFP/Fermat3_4 (AFP)
Session HOL/HOL-Data_Structures (timing)
Session AFP/Efficient-Mergesort (AFP)
Session HOL/HOL-Codegenerator_Test
Session AFP/Query_Optimization (AFP)
Session HOL/HOL-ex (timing)
Session AFP/Automatic_Refinement (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Lehmer (AFP)
Session AFP/Lifting_the_Exponent (AFP)
Session AFP/Padic_Ints (AFP)
Session AFP/Padic_Field (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/Lucas_Theorem (AFP)
Session AFP/DPRM_Theorem (AFP)
Session AFP/Mason_Stothers (AFP)
Session AFP/Polynomial_Interpolation (AFP)
Session AFP/Formal_Puiseux_Series (AFP)
Session AFP/Probabilistic_Prime_Tests (AFP)
Session AFP/Rep_Fin_Groups (AFP)
Session AFP/Sturm_Sequences (AFP)
Session AFP/Safe_Distance (AFP)
Session AFP/Special_Function_Bounds (AFP)
Session AFP/Sturm_Tarski (AFP)
Session AFP/Budan_Fourier (AFP)
Session AFP/Three_Circles (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-IMP (timing)
Session AFP/Abs_Int_ITP2012 (AFP)
Session AFP/Relational-Incorrectness-Logic (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-Metis_Examples (timing)
Session HOL/HOL-Proofs (timing)
Session HOL/HOL-Proofs-Extraction (timing)
Session HOL/HOL-Proofs-ex
Session HOL/HOL-Proofs-Lambda (timing)
Session AFP/Applicative_Lifting (AFP)
Session AFP/Free-Groups (AFP)
Session AFP/Stern_Brocot (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/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/LightweightJava (AFP)
Session AFP/LinearQuantifierElim (AFP)
Session AFP/List-Infinite (AFP)
Session AFP/Nat-Interval-Logic (AFP)
Session AFP/AutoFocus-Stream (AFP)
Session AFP/Median_Method (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/Prefix_Free_Code_Combinators (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/Stateful_Protocol_Composition_and_Typing (AFP)
Session AFP/Automated_Stateful_Protocol_Verification (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/ResiduatedTransitionSystem (AFP)
Session AFP/Ribbon_Proofs (AFP)
Session AFP/SATSolverVerification (AFP)
Session AFP/Safe_OCL (AFP)
Session AFP/Schutz_Spacetime (AFP)
Session AFP/Selection_Heap_Sort (AFP)
Session AFP/Simplex (AFP)
Session AFP/Skew_Heap (AFP)
Session AFP/Solidity (AFP)
Session AFP/Sort_Encodings (AFP)
Session AFP/Splay_Tree (AFP)
Session AFP/Amortized_Complexity (AFP)
Session AFP/Dynamic_Tables (AFP)
Session AFP/Root_Balanced_Tree (AFP)
Session AFP/Closest_Pair_Points (AFP)
Session AFP/Stable_Matching (AFP)
Session AFP/SuperCalc (AFP)
Session Doc/System (doc)
Session AFP/Szemeredi_Regularity (AFP)
Session AFP/Roth_Arithmetic_Progressions (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-Matrix_LP
Session HOL/HOL-MicroJava (timing)
Session HOL/HOL-Mirabelle-ex
Session HOL/HOL-Mutabelle
Session HOL/HOL-NanoJava
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-Prolog
Session HOL/HOL-Quickcheck_Examples (timing)
Session HOL/HOL-Real_Asymp
Session AFP/Cotangent_PFD_Formula (AFP)
Session AFP/Fourier (AFP)
Session AFP/Furstenberg_Topology (AFP)
Session HOL/HOL-Real_Asymp-Manual
Session AFP/Sophomores_Dream (AFP)
Session AFP/Stirling_Formula (AFP)
Session AFP/Irrationals_From_THEBOOK (AFP)
Session AFP/Lambert_W (AFP)
Session HOL/HOL-SET_Protocol (timing)
Session HOL/HOL-SMT_Examples (timing)
Session HOL/HOL-SPARK
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session HOL/HOL-SPARK-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-TPTP
Session HOL/HOL-Types_To_Sets
Session AFP/Banach_Steinhaus (AFP)
Session AFP/Smooth_Manifolds (AFP)
Session AFP/Types_To_Sets_Extension (AFP)
Session HOL/HOL-Unix
Session HOL/HOL-ZF
Session AFP/Category2 (AFP)
Session HOL/HOLCF (main timing)
Session AFP/Circus (AFP)
Session AFP/HOL-CSP (AFP)
Session HOL/HOLCF-IMP
Session HOL/HOLCF-Library
Session AFP/CSP_RefTK (AFP)
Session HOL/HOLCF-FOCUS
Session HOL/HOLCF-ex
Session AFP/PCF (AFP)
Session AFP/HOLCF-Prelude (AFP)
Session AFP/BirdKMP (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/Hales_Jewett (AFP)
Session Misc/Haskell
Session AFP/Heard_Of (AFP)
Session AFP/Consensus_Refined (AFP)
Session AFP/Hello_World (AFP)
Session AFP/Hood_Melville_Queue (AFP)
Session AFP/HotelKeyCards (AFP)
Session Doc/How_to_Prove_it (no_doc)
Session AFP/Huffman (AFP)
Session AFP/Hybrid_Logic (AFP)
Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
Session AFP/IFC_Tracking (AFP)
Session AFP/IMP2 (AFP)
Session AFP/IMP2_Binary_Heap (AFP)
Session AFP/IMP_Compiler (AFP)
Session AFP/IMP_Compiler_Reuse (AFP)
Session Doc/Implementation (doc)
Session AFP/Implicational_Logic (AFP)
Session AFP/Impossible_Geometry (AFP)
Session AFP/Inductive_Confidentiality (AFP)
Session AFP/Inductive_Inference (AFP)
Session AFP/InfPathElimination (AFP)
Session AFP/Intro_Dest_Elim (AFP)
Session AFP/Involutions2Squares (AFP)
Session AFP/IsaGeoCoq (AFP)
Session AFP/IsaNet (AFP)
Session Doc/Isar_Ref (doc)
Session AFP/Isabelle_C (AFP)
Session Doc/JEdit (doc)
Session AFP/Jacobson_Basic_Algebra (AFP)
Session AFP/Grothendieck_Schemes (AFP)
Session AFP/Pluennecke_Ruzsa_Inequality (AFP)
Session AFP/Khovanskii_Theorem (AFP)
Session AFP/JiveDataStoreModel (AFP)
Session AFP/Key_Agreement_Strong_Adversaries (AFP)
Session AFP/Kleene_Algebra (AFP)
Session AFP/KAD (AFP)
Session AFP/KAT_and_DRA (AFP)
Session AFP/Algebraic_VCs (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/Relational_Paths (AFP)
Session AFP/Residuated_Lattices (AFP)
Session AFP/Knights_Tour (AFP)
Session AFP/LambdaMu (AFP)
Session AFP/LatticeProperties (AFP)
Session AFP/DataRefinementIBP (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Lazy_Case (AFP)
Session AFP/Lifting_Definition_Option (AFP)
Session AFP/List-Index (AFP)
Session AFP/Comparison_Sort_Lower_Bound (AFP)
Session AFP/Jinja (AFP)
Session AFP/Dominance_CHK (AFP)
Session AFP/HRB-Slicing (AFP)
Session AFP/InformationFlowSlicing_Inter (AFP)
Session AFP/Slicing (AFP)
Session AFP/InformationFlowSlicing (AFP)
Session AFP/JinjaDCI (AFP)
Session AFP/Regression_Test_Selection (AFP)
Session AFP/List_Update (AFP)
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/List_Interleaving (AFP)
Session AFP/List_Inversions (AFP)
Session AFP/LocalLexing (AFP)
Session Doc/Locales (doc)
Session AFP/Locally-Nameless-Sigma (AFP)
Session AFP/Logging_Independent_Anonymity (AFP)
Session AFP/Lowe_Ontological_Argument (AFP)
Session Doc/Main (doc)
Session AFP/Marriage (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Matroids (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/Maximum_Segment_Sum (AFP)
Session AFP/Median_Of_Medians_Selection (AFP)
Session AFP/KD_Tree (AFP)
Session AFP/Menger (AFP)
Session AFP/Mereology (AFP)
Session AFP/Metalogic_ProofChecker (AFP)
Session AFP/MiniML (AFP)
Session AFP/Modular_Assembly_Kit_Security (AFP)
Session AFP/MonoBoolTranAlgebra (AFP)
Session AFP/Name_Carrying_Type_Inference (AFP)
Session AFP/Nano_JSON (AFP)
Session AFP/Nash_Williams (AFP)
Session AFP/No_FTL_observers (AFP)
Session AFP/Nominal2 (AFP)
Session AFP/Incompleteness (AFP)
Session AFP/Surprise_Paradox (AFP)
Session AFP/LambdaAuth (AFP)
Session AFP/Launchbury (AFP)
Session AFP/Call_Arity (AFP)
Session AFP/Modal_Logics_for_NTS (AFP)
Session AFP/Rewriting_Z (AFP)
Session AFP/Noninterference_CSP (AFP)
Session AFP/Noninterference_Ipurge_Unwinding (AFP)
Session AFP/Noninterference_Generic_Unwinding (AFP)
Session AFP/Noninterference_Inductive_Unwinding (AFP)
Session AFP/Noninterference_Sequential_Composition (AFP)
Session AFP/Noninterference_Concurrent_Composition (AFP)
Session AFP/NormByEval (AFP)
Session AFP/OpSets (AFP)
Session AFP/Open_Induction (AFP)
Session AFP/Well_Quasi_Orders (AFP)
Session AFP/Decreasing-Diagrams-II (AFP)
Session AFP/Myhill-Nerode (AFP)
Session AFP/Ordinal (AFP)
Session AFP/Nested_Multisets_Ordinals (AFP)
Session AFP/Design_Theory (AFP)
Session AFP/Undirected_Graph_Theory (AFP)
Session AFP/Lambda_Free_RPOs (AFP)
Session AFP/Lambda_Free_EPO (AFP)
Session AFP/Ordered_Resolution_Prover (AFP)
Session AFP/Chandy_Lamport (AFP)
Session AFP/Saturation_Framework (AFP)
Session AFP/Saturation_Framework_Extensions (AFP)
Session AFP/Progress_Tracking (AFP)
Session AFP/PAL (AFP)
Session AFP/PLM (AFP)
Session AFP/PSemigroupsConvolution (AFP)
Session AFP/Package_logic (AFP)
Session AFP/Combinable_Wands (AFP)
Session AFP/Paraconsistency (AFP)
Session AFP/Parity_Game (AFP)
Session AFP/GaleStewart_Games (AFP)
Session AFP/Partial_Function_MR (AFP)
Session AFP/Physical_Quantities (AFP)
Session AFP/Pop_Refinement (AFP)
Session AFP/Possibilistic_Noninterference (AFP)
Session AFP/Priority_Search_Trees (AFP)
Session AFP/Prim_Dijkstra_Simple (AFP)
Session Doc/Prog_Prove (doc)
Session AFP/Projective_Geometry (AFP)
Session AFP/Proof_Strategy_Language (AFP)
Session AFP/PropResPI (AFP)
Session AFP/Propositional_Proof_Systems (AFP)
Session AFP/PseudoHoops (AFP)
Session AFP/Ramsey-Infinite (AFP)
Session AFP/Real_Power (AFP)
Session AFP/Real_Time_Deque (AFP)
Session AFP/Recursion-Theory-I (AFP)
Session AFP/Minsky_Machines (AFP)
Session AFP/RefinementReactive (AFP)
Session AFP/Regex_Equivalence (AFP)
Session AFP/Relational_Method (AFP)
Session AFP/Resolution_FOL (AFP)
Session AFP/Robbins-Conjecture (AFP)
Session AFP/Roy_Floyd_Warshall (AFP)
Session AFP/SCC_Bloemen_Sequential (AFP)
Session AFP/SIFPL (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/Security_Protocol_Refinement (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/Hoare_Time (AFP)
Session AFP/Separata (AFP)
Session AFP/Separation_Logic_Unbounded (AFP)
Session AFP/Simpl (AFP)
Session AFP/BDD (AFP)
Session AFP/SimplifiedOntologicalArgument (AFP)
Session AFP/Sliding_Window_Algorithm (AFP)
Session AFP/Statecharts (AFP)
Session AFP/Stellar_Quorums (AFP)
Session AFP/Stone_Algebras (AFP)
Session AFP/Stone_Relation_Algebras (AFP)
Session AFP/Stone_Kleene_Relation_Algebras (AFP)
Session AFP/Aggregation_Algebras (AFP)
Session AFP/Relational_Disjoint_Set_Forests (AFP)
Session AFP/Relational_Minimum_Spanning_Trees (AFP)
Session AFP/Relational_Forests (AFP)
Session AFP/Subset_Boolean_Algebras (AFP)
Session AFP/Correctness_Algebras (AFP)
Session AFP/Store_Buffer_Reduction (AFP)
Session AFP/Strong_Security (AFP)
Session Doc/Sugar (doc)
Session AFP/Sunflowers (AFP)
Session AFP/Clique_and_Monotone_Circuits (AFP)
Session AFP/Syntax_Independent_Logic (AFP)
Session AFP/Goedel_Incompleteness (AFP)
Session AFP/Goedel_HFSet_Semantic (AFP)
Session AFP/Goedel_HFSet_Semanticless (AFP)
Session AFP/Robinson_Arithmetic (AFP)
Session AFP/Szpilrajn (AFP)
Session AFP/Combinatorics_Words_Lyndon (AFP)
Session AFP/TESL_Language (AFP)
Session AFP/TLA (AFP)
Session AFP/Timed_Automata (AFP)
Session AFP/Probabilistic_Timed_Automata (AFP)
Session AFP/Topological_Semantics (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/Van_der_Waerden (AFP)
Session AFP/VeriComp (AFP)
Session AFP/Interpreter_Optimizations (AFP)
Session AFP/Verified-Prover (AFP)
Session AFP/VolpanoSmith (AFP)
Session AFP/WHATandWHERE_Security (AFP)
Session AFP/Weight_Balanced_Trees (AFP)
Session AFP/Weighted_Arithmetic_Geometric_Mean (AFP)
Session AFP/Word_Lib (AFP)
Session AFP/Complx (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Routing (AFP)
Session AFP/Interval_Arithmetic_Word32 (AFP)
Session AFP/LEM (AFP)
Session AFP/Native_Word (AFP)
Session AFP/Collections (AFP)
Session AFP/Abstract_Completeness (AFP)
Session AFP/Abstract_Soundness (AFP)
Session AFP/FOL_Seq_Calc3 (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/Eval_FO (AFP)
Session AFP/MFOTL_Monitor (AFP)
Session AFP/Generic_Join (AFP)
Session AFP/MFODL_Monitor_Optimized (AFP)
Session AFP/VYDRA_MDL (AFP)
Session AFP/Formula_Derivatives (AFP)
Session AFP/MSO_Regex_Equivalence (AFP)
Session AFP/Show (AFP)
Session AFP/Affine_Arithmetic (AFP)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/Differential_Dynamic_Logic (AFP)
Session AFP/Hybrid_Systems_VCs (AFP)
Session AFP/Matrices_for_ODEs (AFP)
Session AFP/Taylor_Models (AFP)
Session AFP/CakeML (AFP)
Session AFP/Certification_Monads (AFP)
Session AFP/AI_Planning_Languages_Semantics (AFP)
Session AFP/Verified_SAT_Based_AI_Planning (AFP)
Session AFP/Dict_Construction (AFP)
Session AFP/Formula_Derivatives-Examples (AFP)
Session AFP/Monad_Memo_DP (AFP)
Session AFP/Hidden_Markov_Models (AFP)
Session AFP/Optimal_BST (AFP)
Session AFP/Polynomial_Factorization (AFP)
Session AFP/Amicable_Numbers (AFP)
Session AFP/Dirichlet_Series (AFP)
Session AFP/Finite_Fields (AFP)
Session AFP/Universal_Hash_Families (AFP)
Session AFP/Frequency_Moments (AFP)
Session AFP/Zeta_Function (AFP)
Session AFP/Dirichlet_L (AFP)
Session AFP/Gauss_Sums (AFP)
Session AFP/Prime_Number_Theorem (AFP)
Session AFP/Prime_Distribution_Elementary (AFP)
Session AFP/IMO2019 (AFP)
Session AFP/Irrational_Series_Erdos_Straus (AFP)
Session AFP/Transcendence_Series_Hancl_Rucki (AFP)
Session AFP/Zeta_3_Irrational (AFP)
Session AFP/Gaussian_Integers (AFP)
Session AFP/Jordan_Normal_Form (AFP)
Session AFP/Farkas (AFP)
Session AFP/Isabelle_Marries_Dirac (AFP)
Session AFP/Knuth_Bendix_Order (AFP)
Session AFP/Functional_Ordered_Resolution_Prover (AFP)
Session AFP/Regular_Tree_Relations (AFP)
Session AFP/FO_Theory_Rewriting (AFP)
Session AFP/Rewrite_Properties_Reduction (AFP)
Session AFP/Weighted_Path_Order (AFP)
Session AFP/Multiset_Ordering_NPC (AFP)
Session AFP/Linear_Recurrences (AFP)
Session AFP/Perron_Frobenius (AFP)
Session AFP/Stochastic_Matrices (AFP)
Session AFP/Subresultants (AFP)
Session AFP/Berlekamp_Zassenhaus (AFP)
Session AFP/Algebraic_Numbers (AFP)
Session AFP/BenOr_Kozen_Reif (AFP)
Session AFP/LLL_Basis_Reduction (AFP)
Session AFP/LLL_Factorization (AFP)
Session AFP/Linear_Inequalities (AFP)
Session AFP/LP_Duality (AFP)
Session AFP/Linear_Programming (AFP)
Session AFP/Number_Theoretic_Transform (AFP)
Session AFP/CRYSTALS-Kyber (AFP)
Session AFP/Smith_Normal_Form (AFP)
Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP)
Session AFP/Polynomials (AFP)
Session AFP/Deep_Learning (AFP)
Session AFP/QHLProver (AFP)
Session AFP/Projective_Measurements (AFP)
Session AFP/Commuting_Hermitian (AFP)
Session AFP/Groebner_Bases (AFP)
Session AFP/Fishers_Inequality (AFP)
Session AFP/Groebner_Macaulay (AFP)
Session AFP/Nullstellensatz (AFP)
Session AFP/Signature_Groebner (AFP)
Session AFP/Lambda_Free_KBOs (AFP)
Session AFP/Symmetric_Polynomials (AFP)
Session AFP/Pi_Transcendental (AFP)
Session AFP/Power_Sum_Polynomials (AFP)
Session AFP/Hermite_Lindemann (AFP)
Session AFP/Factor_Algebraic_Polynomial (AFP)
Session AFP/Cubic_Quartic_Equations (AFP)
Session AFP/Linear_Recurrences_Solver (AFP)
Session AFP/Virtual_Substitution (AFP)
Session AFP/Real_Impl (AFP)
Session AFP/Complex_Bounded_Operators (AFP)
Session AFP/Registers (AFP)
Session AFP/QR_Decomposition (AFP)
Session AFP/XML (AFP)
Session AFP/Van_Emde_Boas_Trees (AFP)
Session AFP/Dijkstra_Shortest_Path (AFP)
Session AFP/Koenigsberg_Friendship (AFP)
Session AFP/FOL_Seq_Calc2 (AFP)
Session AFP/Formal_SSA (AFP)
Session AFP/Minimal_SSA (AFP)
Session AFP/Gale_Shapley (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/Poincare_Bendixson (AFP)
Session AFP/Safe_Range_RC (AFP)
Session AFP/Transition_Systems_and_Automata (AFP)
Session AFP/Adaptive_State_Counting (AFP)
Session AFP/Buchi_Complementation (AFP)
Session AFP/LTL_Master_Theorem (AFP)
Session AFP/LTL_Normal_Form (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/LTL_to_DRA (AFP)
Session AFP/Network_Security_Policy_Verification (AFP)
Session AFP/Planarity_Certificates (AFP)
Session AFP/Tree-Automata (AFP)
Session AFP/Datatype_Order_Generator (AFP)
Session AFP/Higher_Order_Terms (AFP)
Session AFP/CakeML_Codegen (AFP)
Session AFP/Old_Datatype_Show (AFP)
Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
Session AFP/FSM_Tests (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/LOFT (AFP)
Session AFP/Mersenne_Primes (AFP)
Session AFP/MiniSail (AFP)
Session AFP/Separation_Logic_Imperative_HOL (AFP)
Session AFP/Sepref_Prereq (AFP)
Session AFP/ROBDD (AFP)
Session AFP/Refine_Imperative_HOL (AFP)
Session AFP/BTree (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/Probabilistic_While (AFP)
Session AFP/CryptHOL (AFP)
Session AFP/Constructive_Cryptography (AFP)
Session AFP/Game_Based_Crypto (AFP)
Session AFP/Multi_Party_Computation (AFP)
Session AFP/Sigma_Commit_Crypto (AFP)
Session AFP/Constructive_Cryptography_CM (AFP)
Session AFP/Prpu_Maxflow (AFP)
Session AFP/Knuth_Morris_Pratt (AFP)
Session AFP/Kruskal (AFP)
Session AFP/PAC_Checker (AFP)
Session AFP/VerifyThis2018 (AFP)
Session AFP/VerifyThis2019 (AFP)
Session AFP/Simplicial_complexes_and_boolean_functions (AFP)
Session AFP/UpDown_Scheme (AFP)
Session AFP/WebAssembly (AFP)
Session AFP/SPARCv8 (AFP)
Session AFP/X86_Semantics (AFP)
Session AFP/ZFC_in_HOL (AFP)
Session AFP/CZH_Foundations (AFP)
Session AFP/CZH_Elementary_Categories (AFP)
Session AFP/CZH_Universal_Constructions (AFP)
Session AFP/Category3 (AFP)
Session AFP/MonoidalCategory (AFP)
Session AFP/Ordinal_Partitions (AFP)
Session AFP/Wetzels_Problem (AFP)
Session FOL/ZF (main timing)
Session Doc/Logics_ZF (doc)
Session AFP/Recursion-Addition (AFP)
Session FOL/ZF-AC
Session FOL/ZF-Coind
Session FOL/ZF-Constructible
Session AFP/Delta_System_Lemma (AFP)
Session AFP/Transitive_Models (AFP)
Session AFP/Independence_CH (AFP)
Session AFP/Forcing (AFP)
Session FOL/ZF-IMP
Session FOL/ZF-Induct
Session FOL/ZF-UNITY (timing)
Session FOL/ZF-Resid
Session FOL/ZF-ex
Building First_Order_Terms ...
Running Functional_Ordered_Resolution_Prover ...
Running FO_Theory_Rewriting ...
Running Regular_Tree_Relations ...
Running Resolution_FOL ...
Running Rewrite_Properties_Reduction ...
First_Order_Terms: theory First_Order_Terms.Transitive_Closure_More
First_Order_Terms: theory First_Order_Terms.Fun_More
First_Order_Terms: theory First_Order_Terms.Option_Monad
First_Order_Terms: theory First_Order_Terms.Seq_More
Resolution_FOL: theory First_Order_Terms.Term
Resolution_FOL: theory HOL-Library.Adhoc_Overloading
Resolution_FOL: theory HOL-Library.Cancellation
Resolution_FOL: theory HOL-Library.Infinite_Set
Resolution_FOL: theory HOL-Library.Nat_Bijection
Resolution_FOL: theory HOL-Library.Old_Datatype
Resolution_FOL: theory HOL-Library.While_Combinator
Resolution_FOL: theory Regular-Sets.Regular_Set
Resolution_FOL: theory HOL-Library.Monad_Syntax
First_Order_Terms: theory First_Order_Terms.Term
Resolution_FOL: theory First_Order_Terms.Option_Monad
FO_Theory_Rewriting: theory Containers.Equal
FO_Theory_Rewriting: theory Containers.Extend_Partial_Order
FO_Theory_Rewriting: theory Containers.List_Fusion
FO_Theory_Rewriting: theory Deriving.Derive_Manager
FO_Theory_Rewriting: theory Deriving.Comparator
FO_Theory_Rewriting: theory Deriving.Generator_Aux
FO_Theory_Rewriting: theory FO_Theory_Rewriting.Saturation
FO_Theory_Rewriting: theory First_Order_Terms.Term
FO_Theory_Rewriting: theory Containers.Closure_Set
Regular_Tree_Relations: theory Abstract-Rewriting.Seq
Regular_Tree_Relations: theory Matrix.Utility
Regular_Tree_Relations: theory First_Order_Terms.Term
Regular_Tree_Relations: theory Regular-Sets.Regular_Set
FO_Theory_Rewriting: theory Containers.AssocList
Rewrite_Properties_Reduction: theory Regular-Sets.Regular_Set
Rewrite_Properties_Reduction: theory First_Order_Terms.Term
Rewrite_Properties_Reduction: theory Abstract-Rewriting.Seq
Rewrite_Properties_Reduction: theory Matrix.Utility
FO_Theory_Rewriting: theory Containers.Containers_Auxiliary
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Transitive_Closure_More
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term
Functional_Ordered_Resolution_Prover: theory Deriving.Generator_Aux
Functional_Ordered_Resolution_Prover: theory Deriving.Derive_Manager
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Fun_More
Functional_Ordered_Resolution_Prover: theory Deriving.Comparator
Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Order_Union
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Option_Monad
Resolution_FOL: theory Resolution_FOL.Tree
Resolution_FOL: theory Abstract-Rewriting.Seq
Regular_Tree_Relations: theory Polynomial_Factorization.Missing_List
FO_Theory_Rewriting: theory First_Order_Terms.Option_Monad
Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Seq
Functional_Ordered_Resolution_Prover: theory Word_Lib.Bit_Comprehension
Rewrite_Properties_Reduction: theory Polynomial_Factorization.Missing_List
Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Wellorder_Extension
Functional_Ordered_Resolution_Prover: theory Word_Lib.More_Divides
First_Order_Terms: theory First_Order_Terms.Unifiers
First_Order_Terms: theory First_Order_Terms.Term_Pair_Multiset
First_Order_Terms: theory First_Order_Terms.Subsumption
Functional_Ordered_Resolution_Prover: theory Word_Lib.Signed_Division_Word
Resolution_FOL: theory HOL-Library.Countable
Resolution_FOL: theory HOL-Library.Multiset
FO_Theory_Rewriting: theory Deriving.Equality_Generator
FO_Theory_Rewriting: theory Abstract-Rewriting.Seq
Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Generator
First_Order_Terms: theory First_Order_Terms.Abstract_Unification
First_Order_Terms: theory First_Order_Terms.Abstract_Matching
Functional_Ordered_Resolution_Prover: theory Deriving.Countable_Generator
Functional_Ordered_Resolution_Prover: theory Lambda_Free_RPOs.Lambda_Free_Util
FO_Theory_Rewriting: theory Containers.Containers_Generator
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Seq_More
FO_Theory_Rewriting: theory FOL-Fitting.FOL_Fitting
Functional_Ordered_Resolution_Prover: theory Matrix.Utility
Functional_Ordered_Resolution_Prover: theory Native_Word.Code_Int_Integer_Conversion
Resolution_FOL: theory First_Order_Terms.Unifiers
Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Instances
Functional_Ordered_Resolution_Prover: theory Open_Induction.Restricted_Predicates
FO_Theory_Rewriting: theory Deriving.Equality_Instances
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover
FO_Theory_Rewriting: theory Matrix.Utility
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Set
FO_Theory_Rewriting: theory Regular-Sets.Regular_Set
First_Order_Terms: theory First_Order_Terms.Unification
FO_Theory_Rewriting: theory Deriving.Compare
FO_Theory_Rewriting: theory Deriving.Comparator_Generator
Functional_Ordered_Resolution_Prover: theory Deriving.Compare
Functional_Ordered_Resolution_Prover: theory Deriving.Comparator_Generator
FO_Theory_Rewriting: theory Containers.Collection_Enum
FO_Theory_Rewriting: theory Containers.Lexicographic_Order
FO_Theory_Rewriting: theory Containers.Collection_Eq
Functional_Ordered_Resolution_Prover: theory Polynomial_Factorization.Missing_List
Functional_Ordered_Resolution_Prover: theory Show.Show
First_Order_Terms: theory First_Order_Terms.Matching
Resolution_FOL: theory HOL-Library.Countable_Set
FO_Theory_Rewriting: theory Containers.RBT_ext
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unifiers
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term_Pair_Multiset
FO_Theory_Rewriting: theory Containers.Set_Linorder
Regular_Tree_Relations: theory Regular-Sets.Regular_Exp
FO_Theory_Rewriting: theory Deriving.RBT_Comparator_Impl
Rewrite_Properties_Reduction: theory Regular-Sets.Regular_Exp
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Subsumption
Resolution_FOL: theory Resolution_FOL.TermsAndLiterals
Functional_Ordered_Resolution_Prover: theory Word_Lib.More_Arithmetic
FO_Theory_Rewriting: theory Deriving.Compare_Generator
FO_Theory_Rewriting: theory Polynomial_Factorization.Missing_List
FO_Theory_Rewriting: theory Containers.DList_Set
Regular_Tree_Relations: theory Regular-Sets.NDerivative
Regular_Tree_Relations: theory Regular-Sets.Relation_Interpretation
FO_Theory_Rewriting: theory Deriving.Compare_Instances
Rewrite_Properties_Reduction: theory Regular-Sets.NDerivative
Rewrite_Properties_Reduction: theory Regular-Sets.Relation_Interpretation
Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Generator
Functional_Ordered_Resolution_Prover: theory Word_Lib.More_Word
FO_Theory_Rewriting: theory Regular_Tree_Relations.Horn_Inference
Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Instances
Functional_Ordered_Resolution_Prover: theory Show.Show_Instances
Regular_Tree_Relations: theory Regular-Sets.Equivalence_Checking
Rewrite_Properties_Reduction: theory Regular-Sets.Equivalence_Checking
Resolution_FOL: theory Resolution_FOL.Resolution
Regular_Tree_Relations: theory Regular-Sets.Regexp_Method
Rewrite_Properties_Reduction: theory Regular-Sets.Regexp_Method
Regular_Tree_Relations: theory Abstract-Rewriting.Abstract_Rewriting
Rewrite_Properties_Reduction: theory Abstract-Rewriting.Abstract_Rewriting
Resolution_FOL: theory First_Order_Terms.Term_Pair_Multiset
Resolution_FOL: theory Resolution_FOL.Completeness
Resolution_FOL: theory Resolution_FOL.Examples
Functional_Ordered_Resolution_Prover: theory Native_Word.Code_Target_Word_Base
Functional_Ordered_Resolution_Prover: theory Word_Lib.Bit_Shifts_Infix_Syntax
Functional_Ordered_Resolution_Prover: theory Word_Lib.Least_significant_bit
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover
Regular_Tree_Relations: theory Knuth_Bendix_Order.Subterm_and_Context
Functional_Ordered_Resolution_Prover: theory Word_Lib.Most_significant_bit
Functional_Ordered_Resolution_Prover: theory Word_Lib.Generic_set_bit
Preparing First_Order_Terms/document ...
Functional_Ordered_Resolution_Prover: theory Native_Word.Code_Target_Integer_Bit
Functional_Ordered_Resolution_Prover: theory Native_Word.Word_Type_Copies
Rewrite_Properties_Reduction: theory Knuth_Bendix_Order.Subterm_and_Context
Resolution_FOL: theory Regular-Sets.Regular_Exp
Rewrite_Properties_Reduction: theory Regular_Tree_Relations.Term_Context
Resolution_FOL: theory Regular-Sets.NDerivative
Resolution_FOL: theory Regular-Sets.Relation_Interpretation
Regular_Tree_Relations: theory Regular_Tree_Relations.Term_Context
Rewrite_Properties_Reduction: theory Regular_Tree_Relations.Basic_Utils
Resolution_FOL: theory Regular-Sets.Equivalence_Checking
Rewrite_Properties_Reduction: theory Regular_Tree_Relations.Ground_Terms
Finished First_Order_Terms/document (0:00:06 elapsed time)
Preparing First_Order_Terms/outline ...
Regular_Tree_Relations: theory Regular_Tree_Relations.Basic_Utils
Resolution_FOL: theory Regular-Sets.Regexp_Method
Resolution_FOL: theory Abstract-Rewriting.Abstract_Rewriting
Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Terms_Positions
Regular_Tree_Relations: theory Regular_Tree_Relations.Ground_Terms
Regular_Tree_Relations: theory Regular_Tree_Relations.FSet_Utils
Regular_Tree_Relations: theory Regular_Tree_Relations.Ground_Closure
Regular_Tree_Relations: theory Regular_Tree_Relations.Ground_Ctxt
Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Rewriting
Finished First_Order_Terms/outline (0:00:04 elapsed time)
FO_Theory_Rewriting: theory Containers.Collection_Order
Timing First_Order_Terms (8 threads, 6.760s elapsed time, 30.840s cpu time, 1.302s GC time, factor 4.56)
Finished First_Order_Terms (0:00:39 elapsed time, 0:01:10 cpu time, factor 1.81)
Building Stateful_Protocol_Composition_and_Typing ...
Building Knuth_Bendix_Order ...
Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Replace_Constant
Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Rewriting_GTRS
Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Rewriting_LLRG_LV_Mondaic
Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Rewriting_Properties
Regular_Tree_Relations: theory Regular_Tree_Relations.Horn_Inference
Knuth_Bendix_Order: theory Matrix.Utility
Knuth_Bendix_Order: theory Knuth_Bendix_Order.Order_Pair
Knuth_Bendix_Order: theory Knuth_Bendix_Order.Subterm_and_Context
FO_Theory_Rewriting: theory Containers.RBT_Mapping2
Regular_Tree_Relations: theory Regular_Tree_Relations.Horn_List
Regular_Tree_Relations: theory Regular_Tree_Relations.Horn_Fset
Regular_Tree_Relations: theory Regular_Tree_Relations.Tree_Automata
Resolution_FOL: theory First_Order_Terms.Abstract_Unification
Knuth_Bendix_Order: theory Polynomial_Factorization.Missing_List
Knuth_Bendix_Order: theory Knuth_Bendix_Order.Lexicographic_Extension
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Miscellaneous
FO_Theory_Rewriting: theory Containers.RBT_Set2
Resolution_FOL: theory First_Order_Terms.Unification
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Messages
Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Ground_Reduction_on_LLRG
Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Ground_Reduction_on_GTRS
Rewrite_Properties_Reduction: theory Rewrite_Properties_Reduction.Ground_Reduction_on_LV
Resolution_FOL: theory Resolution_FOL.Unification_Theorem
FO_Theory_Rewriting: theory Containers.Set_Impl
Regular_Tree_Relations: theory Regular_Tree_Relations.Tree_Automata_Det
Regular_Tree_Relations: theory Regular_Tree_Relations.Tree_Automata_Pumping
Regular_Tree_Relations: theory Regular_Tree_Relations.Myhill_Nerode
Regular_Tree_Relations: theory Regular_Tree_Relations.Tree_Automata_Complement
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.More_Unification
Resolution_FOL: theory Resolution_FOL.Completeness_Instance
Knuth_Bendix_Order: theory Knuth_Bendix_Order.Term_Aux
Knuth_Bendix_Order: theory Knuth_Bendix_Order.KBO
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Exp
Functional_Ordered_Resolution_Prover: theory Regular-Sets.NDerivative
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Relation_Interpretation
Regular_Tree_Relations: theory Regular_Tree_Relations.GTT
Regular_Tree_Relations: theory Regular_Tree_Relations.RRn_Automata
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Equivalence_Checking
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regexp_Method
Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Abstract_Rewriting
Regular_Tree_Relations: theory Regular_Tree_Relations.GTT_Compose
Preparing Rewrite_Properties_Reduction/document ...
Regular_Tree_Relations: theory Regular_Tree_Relations.GTT_Transitive_Closure
Regular_Tree_Relations: theory Regular_Tree_Relations.Pair_Automaton
Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Relative_Rewriting
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Matching
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Unification
Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.Subterm_and_Context
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Intruder_Deduction
Regular_Tree_Relations: theory Regular_Tree_Relations.RR2_Infinite
Regular_Tree_Relations: theory Regular_Tree_Relations.AGTT
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Strands_and_Constraints
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unification
Finished Rewrite_Properties_Reduction/document (0:00:07 elapsed time)
Preparing Rewrite_Properties_Reduction/outline ...
FO_Theory_Rewriting: theory Containers.Mapping_Impl
FO_Theory_Rewriting: theory Containers.Map_To_Mapping
FO_Theory_Rewriting: theory Containers.Containers
FO_Theory_Rewriting: theory Regular-Sets.Regular_Exp
Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.Order_Pair
FO_Theory_Rewriting: theory Regular-Sets.NDerivative
FO_Theory_Rewriting: theory Regular-Sets.Relation_Interpretation
FO_Theory_Rewriting: theory Regular-Sets.Equivalence_Checking
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Matching
Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.Lexicographic_Extension
FO_Theory_Rewriting: theory Regular-Sets.Regexp_Method
FO_Theory_Rewriting: theory Abstract-Rewriting.Abstract_Rewriting
Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.Term_Aux
Finished Rewrite_Properties_Reduction/outline (0:00:04 elapsed time)
Timing Rewrite_Properties_Reduction (8 threads, 54.108s elapsed time, 198.842s cpu time, 7.554s GC time, factor 3.67)
Finished Rewrite_Properties_Reduction (0:01:12 elapsed time, 0:03:22 cpu time, factor 2.80)
Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.KBO
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Labeled_Strands
FO_Theory_Rewriting: theory Knuth_Bendix_Order.Subterm_and_Context
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Lazy_Intruder
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Typed_Model
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Strands
FO_Theory_Rewriting: theory Regular_Tree_Relations.Term_Context
FO_Theory_Rewriting: theory Regular_Tree_Relations.Basic_Utils
FO_Theory_Rewriting: theory Regular_Tree_Relations.Ground_Terms
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Example_TLS
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Typing_Result
FO_Theory_Rewriting: theory Regular_Tree_Relations.FSet_Utils
FO_Theory_Rewriting: theory Regular_Tree_Relations.Ground_Closure
FO_Theory_Rewriting: theory Regular_Tree_Relations.Ground_Ctxt
FO_Theory_Rewriting: theory FO_Theory_Rewriting.Utils
FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata
FO_Theory_Rewriting: theory Regular_Tree_Relations.Horn_Fset
FO_Theory_Rewriting: theory FO_Theory_Rewriting.Bot_Terms
FO_Theory_Rewriting: theory FO_Theory_Rewriting.Rewriting
FO_Theory_Rewriting: theory FO_Theory_Rewriting.Multihole_Context
Preparing Knuth_Bendix_Order/document ...
FO_Theory_Rewriting: theory FO_Theory_Rewriting.FOR_Certificate
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Labeled_Stateful_Strands
FO_Theory_Rewriting: theory FO_Theory_Rewriting.Ground_MCtxt
FO_Theory_Rewriting: theory FO_Theory_Rewriting.NF
FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl
FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Det
FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Pumping
FO_Theory_Rewriting: theory Regular_Tree_Relations.GTT
FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Complement
FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Abstract_Impl
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Parallel_Compositionality
Preparing Resolution_FOL/document ...
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Typing
FO_Theory_Rewriting: theory Regular_Tree_Relations.RRn_Automata
FO_Theory_Rewriting: theory Regular_Tree_Relations.GTT_Compose
FO_Theory_Rewriting: theory Regular_Tree_Relations.GTT_Transitive_Closure
FO_Theory_Rewriting: theory Regular_Tree_Relations.Pair_Automaton
Finished Knuth_Bendix_Order/document (0:00:05 elapsed time)
Preparing Knuth_Bendix_Order/outline ...
FO_Theory_Rewriting: theory Regular_Tree_Relations.Tree_Automata_Impl
FO_Theory_Rewriting: theory FO_Theory_Rewriting.LV_to_GTT
FO_Theory_Rewriting: theory Regular_Tree_Relations.AGTT
FO_Theory_Rewriting: theory Regular_Tree_Relations.RR2_Infinite
Functional_Ordered_Resolution_Prover: theory Native_Word.Uint32
FO_Theory_Rewriting: theory Regular_Tree_Relations.RR2_Infinite_Q_infinity
Finished Knuth_Bendix_Order/outline (0:00:03 elapsed time)
FO_Theory_Rewriting: theory FO_Theory_Rewriting.Context_Extensions
FO_Theory_Rewriting: theory FO_Theory_Rewriting.Tree_Automata_Derivation_Split
Timing Knuth_Bendix_Order (8 threads, 7.084s elapsed time, 48.304s cpu time, 2.412s GC time, factor 6.82)
Finished Knuth_Bendix_Order (0:00:45 elapsed time, 0:01:27 cpu time, factor 1.94)
Building Weighted_Path_Order ...
Functional_Ordered_Resolution_Prover: theory Collections.HashCode
Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Generator
FO_Theory_Rewriting: theory Regular_Tree_Relations.Regular_Relation_Abstract_Impl
FO_Theory_Rewriting: theory FO_Theory_Rewriting.TA_Clousure_Const
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Stateful_Compositionality
Finished Resolution_FOL/document (0:00:06 elapsed time)
Preparing Resolution_FOL/outline ...
FO_Theory_Rewriting: theory FO_Theory_Rewriting.Context_RR2
Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Instances
Functional_Ordered_Resolution_Prover: theory Deriving.Derive
FO_Theory_Rewriting: theory Regular_Tree_Relations.Regular_Relation_Impl
FO_Theory_Rewriting: theory FO_Theory_Rewriting.Type_Instances_Impl
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.IsaFoR_Term
FO_Theory_Rewriting: theory FO_Theory_Rewriting.FOL_Extra
FO_Theory_Rewriting: theory FO_Theory_Rewriting.NF_Impl
Weighted_Path_Order: theory Weighted_Path_Order.Status
Weighted_Path_Order: theory Weighted_Path_Order.List_Order
Weighted_Path_Order: theory Weighted_Path_Order.Precedence
Weighted_Path_Order: theory Weighted_Path_Order.Relations
Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension_Pair
FO_Theory_Rewriting: theory FO_Theory_Rewriting.Lift_Root_Step
Finished Resolution_FOL/outline (0:00:04 elapsed time)
Timing Resolution_FOL (8 threads, 95.963s elapsed time, 219.892s cpu time, 7.316s GC time, factor 2.29)
Finished Resolution_FOL (0:01:38 elapsed time, 0:03:41 cpu time, factor 2.26)
Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension2
Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension_Pair_Impl
FO_Theory_Rewriting: theory FO_Theory_Rewriting.FOR_Semantics
FO_Theory_Rewriting: theory FO_Theory_Rewriting.GTT_RRn
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Executable_Subsumption
Weighted_Path_Order: theory Weighted_Path_Order.Multiset_Extension2_Impl
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Executable_FO_Ordered_Resolution_Prover
Weighted_Path_Order: theory Weighted_Path_Order.WPO
Regular_Tree_Relations: theory Containers.Equal
Regular_Tree_Relations: theory Containers.List_Fusion
Regular_Tree_Relations: theory Containers.Extend_Partial_Order
Regular_Tree_Relations: theory Deriving.Generator_Aux
Regular_Tree_Relations: theory Deriving.Derive_Manager
Regular_Tree_Relations: theory Deriving.Comparator
Regular_Tree_Relations: theory Containers.AssocList
Regular_Tree_Relations: theory Containers.Containers_Auxiliary
Regular_Tree_Relations: theory Containers.Closure_Set
Regular_Tree_Relations: theory Regular_Tree_Relations.RR2_Infinite_Q_infinity
Regular_Tree_Relations: theory Regular_Tree_Relations.Tree_Automata_Abstract_Impl
FO_Theory_Rewriting: theory FO_Theory_Rewriting.FOR_Check
Weighted_Path_Order: theory Weighted_Path_Order.KBO_Transformation
Weighted_Path_Order: theory Weighted_Path_Order.LPO
Weighted_Path_Order: theory Weighted_Path_Order.RPO
Regular_Tree_Relations: theory Deriving.Equality_Generator
Regular_Tree_Relations: theory Containers.Containers_Generator
Weighted_Path_Order: theory Weighted_Path_Order.KBO_as_WPO
Weighted_Path_Order: theory Weighted_Path_Order.Executable_Orders
Regular_Tree_Relations: theory Deriving.Equality_Instances
Regular_Tree_Relations: theory Containers.Collection_Enum
Regular_Tree_Relations: theory Containers.Collection_Eq
Regular_Tree_Relations: theory Regular_Tree_Relations.Regular_Relation_Abstract_Impl
Regular_Tree_Relations: theory Deriving.Compare
Regular_Tree_Relations: theory Deriving.Comparator_Generator
Regular_Tree_Relations: theory Containers.Lexicographic_Order
Regular_Tree_Relations: theory Containers.RBT_ext
Regular_Tree_Relations: theory Containers.DList_Set
Regular_Tree_Relations: theory Deriving.RBT_Comparator_Impl
Regular_Tree_Relations: theory Containers.Set_Linorder
Regular_Tree_Relations: theory Deriving.Compare_Generator
Regular_Tree_Relations: theory Deriving.Compare_Instances
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Example_Keyserver
Regular_Tree_Relations: theory Containers.Collection_Order
Regular_Tree_Relations: theory Containers.RBT_Mapping2
FO_Theory_Rewriting: theory FO_Theory_Rewriting.FOR_Check_Impl
Regular_Tree_Relations: theory Containers.RBT_Set2
Regular_Tree_Relations: theory Containers.Set_Impl
Stateful_Protocol_Composition_and_Typing: theory Stateful_Protocol_Composition_and_Typing.Examples
Regular_Tree_Relations: theory Containers.Mapping_Impl
Regular_Tree_Relations: theory Containers.Map_To_Mapping
Regular_Tree_Relations: theory Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl
Regular_Tree_Relations: theory Containers.Containers
Preparing Weighted_Path_Order/document ...
Regular_Tree_Relations: theory Regular_Tree_Relations.Tree_Automata_Impl
Regular_Tree_Relations: theory Regular_Tree_Relations.Regular_Relation_Impl
Finished Weighted_Path_Order/document (0:00:11 elapsed time)
Preparing Weighted_Path_Order/outline ...
Preparing Regular_Tree_Relations/document ...
Finished Weighted_Path_Order/outline (0:00:05 elapsed time)
Timing Weighted_Path_Order (8 threads, 36.670s elapsed time, 102.574s cpu time, 2.888s GC time, factor 2.80)
Finished Weighted_Path_Order (0:00:59 elapsed time, 0:02:27 cpu time, factor 2.47)
Running Multiset_Ordering_NPC ...
Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.Propositional_Formula
Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.Multiset_Ordering_More
Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.Multiset_Ordering_in_NP
Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.Multiset_Ordering_NP_Hard
Preparing FO_Theory_Rewriting/document ...
Multiset_Ordering_NPC: theory Multiset_Ordering_NPC.RPO_NP_Hard
Finished Regular_Tree_Relations/document (0:00:22 elapsed time)
Preparing Regular_Tree_Relations/outline ...
Finished Regular_Tree_Relations/outline (0:00:11 elapsed time)
Timing Regular_Tree_Relations (8 threads, 171.055s elapsed time, 675.372s cpu time, 61.186s GC time, factor 3.95)
Finished Regular_Tree_Relations (0:02:54 elapsed time, 0:11:18 cpu time, factor 3.89)
Preparing Multiset_Ordering_NPC/document ...
Finished FO_Theory_Rewriting/document (0:00:21 elapsed time)
Preparing FO_Theory_Rewriting/outline ...
Preparing Functional_Ordered_Resolution_Prover/document ...
Finished Multiset_Ordering_NPC/document (0:00:06 elapsed time)
Preparing Multiset_Ordering_NPC/outline ...
Finished Functional_Ordered_Resolution_Prover/document (0:00:03 elapsed time)
Preparing Functional_Ordered_Resolution_Prover/outline ...
Finished Multiset_Ordering_NPC/outline (0:00:03 elapsed time)
Timing Multiset_Ordering_NPC (8 threads, 26.950s elapsed time, 71.713s cpu time, 1.960s GC time, factor 2.66)
Finished Multiset_Ordering_NPC (0:00:30 elapsed time, 0:01:15 cpu time, factor 2.46)
Finished Functional_Ordered_Resolution_Prover/outline (0:00:02 elapsed time)
Timing Functional_Ordered_Resolution_Prover (8 threads, 211.455s elapsed time, 435.968s cpu time, 26.193s GC time, factor 2.06)
Finished Functional_Ordered_Resolution_Prover (0:03:34 elapsed time, 0:07:19 cpu time, factor 2.04)
Finished FO_Theory_Rewriting/outline (0:00:11 elapsed time)
Timing FO_Theory_Rewriting (8 threads, 189.071s elapsed time, 1216.043s cpu time, 121.678s GC time, factor 6.43)
Finished FO_Theory_Rewriting (0:03:12 elapsed time, 0:20:19 cpu time, factor 6.34)
Preparing Stateful_Protocol_Composition_and_Typing/document ...
Finished Stateful_Protocol_Composition_and_Typing/document (0:00:36 elapsed time)
Preparing Stateful_Protocol_Composition_and_Typing/outline ...
Finished Stateful_Protocol_Composition_and_Typing/outline (0:00:15 elapsed time)
Timing Stateful_Protocol_Composition_and_Typing (8 threads, 180.849s elapsed time, 1085.173s cpu time, 55.672s GC time, factor 6.00)
Finished Stateful_Protocol_Composition_and_Typing (0:04:01 elapsed time, 0:20:29 cpu time, factor 5.10)
Running Automated_Stateful_Protocol_Verification ...
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.ml_yacc_lib
Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Variants
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Transactions
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_term
Automated_Stateful_Protocol_Verification: theory HOL-Eisbach.Eisbach_Tools
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Eisbach_Protocol_Verification
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_fp_parser
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac_protocol_parser
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.trac
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Abstraction
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Model
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Term_Implication
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Verification
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PSPSP
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver2
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Keyserver_Composition
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model03
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model07
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.introduction
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.PKCS_Model09
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.KeyserverEx
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.Examples
Automated_Stateful_Protocol_Verification: theory Automated_Stateful_Protocol_Verification.manual
Preparing Automated_Stateful_Protocol_Verification/document ...
Finished Automated_Stateful_Protocol_Verification/document (0:00:30 elapsed time)
Preparing Automated_Stateful_Protocol_Verification/outline ...
Finished Automated_Stateful_Protocol_Verification/outline (0:00:16 elapsed time)
Timing Automated_Stateful_Protocol_Verification (8 threads, 722.503s elapsed time, 2915.393s cpu time, 1343.818s GC time, factor 4.04)
Finished Automated_Stateful_Protocol_Verification (0:12:06 elapsed time, 0:48:39 cpu time, factor 4.02)
Presentation in "/media/data/jenkins/workspace/isabelle-all/browser_info"
Presenting Automated_Stateful_Protocol_Verification in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Automated_Stateful_Protocol_Verification" ...
Presenting FO_Theory_Rewriting in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/FO_Theory_Rewriting" ...
Presenting Weighted_Path_Order in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Weighted_Path_Order" ...
Presenting Multiset_Ordering_NPC in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Multiset_Ordering_NPC" ...
Presenting Functional_Ordered_Resolution_Prover in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover" ...
Presenting First_Order_Terms in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/First_Order_Terms" ...
Presenting Stateful_Protocol_Composition_and_Typing in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Stateful_Protocol_Composition_and_Typing" ...
Presenting Knuth_Bendix_Order in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Knuth_Bendix_Order" ...
Presenting Regular_Tree_Relations in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Regular_Tree_Relations" ...
Presenting document Knuth_Bendix_Order/document
Presenting document First_Order_Terms/document
Presenting document Multiset_Ordering_NPC/document
Presenting document Weighted_Path_Order/document
Presenting document Multiset_Ordering_NPC/outline
Presenting document First_Order_Terms/outline
Presenting document Weighted_Path_Order/outline
Presenting document Knuth_Bendix_Order/outline
Presenting document Functional_Ordered_Resolution_Prover/document
Presenting document Functional_Ordered_Resolution_Prover/outline
Presenting document Stateful_Protocol_Composition_and_Typing/document
Presenting document Stateful_Protocol_Composition_and_Typing/outline
Presenting document Automated_Stateful_Protocol_Verification/document
Presenting document Automated_Stateful_Protocol_Verification/outline
Presenting document Regular_Tree_Relations/document
Presenting theory "First_Order_Terms.Transitive_Closure_More"
Presenting document FO_Theory_Rewriting/document
Presenting document Regular_Tree_Relations/outline
Presenting document FO_Theory_Rewriting/outline
Presenting theory "Weighted_Path_Order.Status"
Presenting theory "First_Order_Terms.Seq_More"
Presenting theory "Weighted_Path_Order.Precedence"
Presenting theory "First_Order_Terms.Fun_More"
Presenting theory "Matrix.Utility"
Presenting theory "Matrix.Utility"
Presenting theory "Weighted_Path_Order.Relations"
Presenting theory "First_Order_Terms.Option_Monad"
Presenting theory "Multiset_Ordering_NPC.Multiset_Ordering_More"
Presenting theory "Weighted_Path_Order.List_Order"
Presenting theory "Knuth_Bendix_Order.Order_Pair"
Presenting theory "Multiset_Ordering_NPC.Propositional_Formula"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Miscellaneous"
Presenting theory "First_Order_Terms.Term"
Presenting theory "First_Order_Terms.Term"
Presenting theory "First_Order_Terms.Term"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Messages"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "First_Order_Terms.Term_Pair_Multiset"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Polynomial_Factorization.Missing_List"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "Weighted_Path_Order.Multiset_Extension_Pair"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "First_Order_Terms.Abstract_Matching"
Presenting theory "Weighted_Path_Order.Multiset_Extension_Pair_Impl"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "Multiset_Ordering_NPC.Multiset_Ordering_in_NP"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "Knuth_Bendix_Order.Lexicographic_Extension"
Presenting theory "First_Order_Terms.Unifiers"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "First_Order_Terms.Abstract_Unification"
Presenting theory "Multiset_Ordering_NPC.Multiset_Ordering_NP_Hard"
Presenting theory "Knuth_Bendix_Order.Subterm_and_Context"
Presenting theory "Knuth_Bendix_Order.Term_Aux"
Presenting theory "Automated_Stateful_Protocol_Verification.Transactions"
Presenting theory "Multiset_Ordering_NPC.RPO_NP_Hard"
Presenting Rewrite_Properties_Reduction in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rewrite_Properties_Reduction" ...
Presenting document Rewrite_Properties_Reduction/document
Presenting document Rewrite_Properties_Reduction/outline
Presenting theory "First_Order_Terms.Unification"
Presenting theory "Automated_Stateful_Protocol_Verification.Term_Abstraction"
Presenting theory "First_Order_Terms.Term"
Presenting theory "Weighted_Path_Order.Multiset_Extension2"
Presenting theory "First_Order_Terms.Matching"
Presenting theory "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "First_Order_Terms.Subsumption"
Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Weighted_Path_Order.Multiset_Extension2_Impl"
Presenting theory "Lambda_Free_RPOs.Lambda_Free_Util"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
Presenting theory "Knuth_Bendix_Order.Subterm_and_Context"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Matrix.Utility"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Stateful_Protocol_Composition_and_Typing.More_Unification"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "Knuth_Bendix_Order.Subterm_and_Context"
Presenting theory "Polynomial_Factorization.Missing_List"
Presenting theory "Matrix.Utility"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "Polynomial_Factorization.Missing_List"
Presenting theory "Regular_Tree_Relations.Term_Context"
Presenting theory "Regular_Tree_Relations.Basic_Utils"
Presenting theory "Regular_Tree_Relations.Ground_Terms"
Presenting theory "Polynomial_Factorization.Missing_List"
Presenting theory "Regular_Tree_Relations.FSet_Utils"
Presenting theory "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Intruder_Deduction"
Presenting theory "Regular_Tree_Relations.Term_Context"
Presenting theory "FO_Theory_Rewriting.Utils"
Presenting theory "Regular_Tree_Relations.Basic_Utils"
Presenting theory "Regular_Tree_Relations.Ground_Terms"
Presenting theory "Regular_Tree_Relations.FSet_Utils"
Presenting theory "Regular_Tree_Relations.Ground_Ctxt"
Presenting theory "FO_Theory_Rewriting.Multihole_Context"
Presenting theory "Regular_Tree_Relations.Ground_Closure"
Presenting theory "Regular_Tree_Relations.Horn_Inference"
Presenting theory "Regular_Tree_Relations.Horn_List"
Presenting theory "Regular_Tree_Relations.Horn_Fset"
Presenting theory "Regular_Tree_Relations.Ground_Ctxt"
Presenting theory "Knuth_Bendix_Order.KBO"
Presenting theory "Deriving.Generator_Aux"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting Resolution_FOL in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Resolution_FOL" ...
Presenting document Resolution_FOL/document
Presenting document Resolution_FOL/outline
Presenting theory "Deriving.Comparator"
Presenting theory "FO_Theory_Rewriting.Ground_MCtxt"
Presenting theory "FO_Theory_Rewriting.Bot_Terms"
Presenting theory "Weighted_Path_Order.WPO"
Presenting theory "HOL-Library.Old_Datatype"
Presenting theory "Deriving.Comparator_Generator"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting file "$AFP/Deriving/Comparator_Generator/comparator_generator.ML"
Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
Presenting theory "FO_Theory_Rewriting.Saturation"
Presenting theory "Deriving.Compare"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_code.ML"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "Deriving.Compare_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_generator.ML"
Presenting theory "FO_Theory_Rewriting.Rewriting"
Presenting theory "Deriving.Compare_Instances"
Presenting theory "Weighted_Path_Order.RPO"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "Deriving.Equality_Generator"
Presenting file "$AFP/Deriving/Equality_Generator/equality_generator.ML"
Presenting theory "Knuth_Bendix_Order.Subterm_and_Context"
Presenting theory "Deriving.Equality_Instances"
Presenting theory "Weighted_Path_Order.LPO"
Presenting theory "Word_Lib.More_Arithmetic"
Presenting theory "Matrix.Utility"
Presenting theory "Word_Lib.More_Divides"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "Weighted_Path_Order.KBO_Transformation"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Strands_and_Constraints"
Presenting theory "Resolution_FOL.TermsAndLiterals"
Presenting theory "Regular_Tree_Relations.Tree_Automata"
Presenting theory "Regular_Tree_Relations.Tree_Automata"
Presenting theory "Word_Lib.More_Word"
Presenting theory "Regular_Tree_Relations.Tree_Automata_Det"
Presenting theory "Weighted_Path_Order.KBO_as_WPO"
Presenting theory "Regular_Tree_Relations.Tree_Automata_Complement"
Presenting theory "Polynomial_Factorization.Missing_List"
Presenting theory "Weighted_Path_Order.Executable_Orders"
Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"
Presenting theory "Regular_Tree_Relations.Ground_Closure"
Presenting theory "Regular_Tree_Relations.Tree_Automata_Det"
Presenting theory "Word_Lib.Most_significant_bit"
Presenting theory "Resolution_FOL.Tree"
Presenting theory "Word_Lib.Least_significant_bit"
Presenting theory "Regular_Tree_Relations.GTT"
Presenting theory "Word_Lib.Generic_set_bit"
Presenting theory "Regular_Tree_Relations.Tree_Automata_Complement"
Presenting theory "Word_Lib.Bit_Comprehension"
Presenting theory "Word_Lib.Signed_Division_Word"
Presenting theory "Regular_Tree_Relations.Term_Context"
Presenting theory "Native_Word.Code_Target_Word_Base"
Presenting theory "Regular_Tree_Relations.GTT_Compose"
Presenting theory "Regular_Tree_Relations.Tree_Automata_Pumping"
Presenting theory "Regular_Tree_Relations.Myhill_Nerode"
Presenting theory "Native_Word.Word_Type_Copies"
Presenting theory "Native_Word.Code_Int_Integer_Conversion"
Presenting theory "Regular_Tree_Relations.Pair_Automaton"
Presenting theory "Regular_Tree_Relations.Basic_Utils"
Presenting theory "Native_Word.Code_Target_Integer_Bit"
Presenting theory "Regular_Tree_Relations.GTT"
Presenting theory "FO_Theory_Rewriting.LV_to_GTT"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Lazy_Intruder"
Presenting theory "Native_Word.Uint32"
Presenting theory "Collections.HashCode"
Presenting theory "FO_Theory_Rewriting.NF"
Presenting theory "Regular_Tree_Relations.Ground_Terms"
Presenting theory "FO_Theory_Rewriting.Tree_Automata_Derivation_Split"
Presenting theory "Deriving.Hash_Generator"
Presenting file "$AFP/Deriving/Hash_Generator/hash_generator.ML"
Presenting theory "Deriving.Hash_Instances"
Presenting theory "Deriving.Countable_Generator"
Presenting theory "Deriving.Derive"
Presenting theory "Resolution_FOL.Resolution"
Presenting theory "Regular_Tree_Relations.GTT_Compose"
Presenting theory "FO_Theory_Rewriting.TA_Clousure_Const"
Presenting theory "Rewrite_Properties_Reduction.Terms_Positions"
Presenting theory "First_Order_Terms.Term"
Presenting theory "Deriving.Generator_Aux"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
Presenting theory "Regular_Tree_Relations.GTT_Transitive_Closure"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "Deriving.Comparator"
Presenting theory "Resolution_FOL.Completeness"
Presenting theory "Resolution_FOL.Examples"
Presenting theory "First_Order_Terms.Unifiers"
Presenting theory "Deriving.Comparator_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/comparator_generator.ML"
Presenting theory "Deriving.Compare"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_code.ML"
Presenting theory "Regular_Tree_Relations.Pair_Automaton"
Presenting theory "First_Order_Terms.Term_Pair_Multiset"
Presenting theory "Deriving.Compare_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_generator.ML"
Presenting theory "Deriving.Compare_Instances"
Presenting theory "Containers.Containers_Auxiliary"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "First_Order_Terms.Term"
Presenting theory "Rewrite_Properties_Reduction.Rewriting"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Regular_Tree_Relations.AGTT"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Containers.List_Fusion"
Presenting theory "Containers.Lexicographic_Order"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "First_Order_Terms.Unifiers"
Presenting theory "Containers.Extend_Partial_Order"
Presenting theory "HOL-Library.Cancellation"
Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "Rewrite_Properties_Reduction.Replace_Constant"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Typed_Model"
Presenting theory "Containers.Set_Linorder"
Presenting theory "Containers.Containers_Generator"
Presenting file "$AFP/Containers/containers_generator.ML"
Presenting theory "Rewrite_Properties_Reduction.Rewriting_Properties"
Presenting theory "Containers.Collection_Order"
Presenting file "$AFP/Containers/ccompare_generator.ML"
Presenting theory "Deriving.Equality_Generator"
Presenting file "$AFP/Deriving/Equality_Generator/equality_generator.ML"
Presenting theory "Deriving.Equality_Instances"
Presenting theory "Containers.Collection_Eq"
Presenting file "$AFP/Containers/ceq_generator.ML"
Presenting theory "Containers.Collection_Enum"
Presenting file "$AFP/Containers/cenum_generator.ML"
Presenting theory "Containers.Equal"
Presenting theory "Rewrite_Properties_Reduction.Rewriting_LLRG_LV_Mondaic"
Presenting theory "Containers.DList_Set"
Presenting theory "Rewrite_Properties_Reduction.Rewriting_GTRS"
Presenting theory "Containers.RBT_ext"
Presenting theory "Deriving.RBT_Comparator_Impl"
Presenting theory "Regular_Tree_Relations.RRn_Automata"
Presenting theory "Containers.RBT_Mapping2"
Presenting theory "HOL-Library.Multiset"
Presenting theory "Containers.RBT_Set2"
Presenting theory "Containers.Closure_Set"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
Presenting theory "Rewrite_Properties_Reduction.Ground_Reduction_on_LLRG"
Presenting theory "First_Order_Terms.Term_Pair_Multiset"
Presenting theory "Regular_Tree_Relations.RR2_Infinite"
Presenting theory "First_Order_Terms.Abstract_Unification"
Presenting theory "Rewrite_Properties_Reduction.Ground_Reduction_on_GTRS"
Presenting theory "First_Order_Terms.Option_Monad"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "Regular_Tree_Relations.Tree_Automata_Abstract_Impl"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Containers.Set_Impl"
Presenting file "$AFP/Containers/set_impl_generator.ML"
Presenting theory "Rewrite_Properties_Reduction.Ground_Reduction_on_LV"
Presenting theory "Containers.AssocList"
Presenting theory "Containers.Mapping_Impl"
Presenting file "$AFP/Containers/mapping_impl_generator.ML"
Presenting theory "Deriving.Generator_Aux"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
Presenting theory "First_Order_Terms.Unification"
Presenting theory "Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl"
Presenting theory "HOL-Library.While_Combinator"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "FO_Theory_Rewriting.Type_Instances_Impl"
Presenting theory "FO_Theory_Rewriting.NF_Impl"
Presenting theory "First_Order_Terms.Fun_More"
Presenting theory "Deriving.Comparator"
Presenting theory "First_Order_Terms.Transitive_Closure_More"
Presenting theory "First_Order_Terms.Seq_More"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "First_Order_Terms.Subsumption"
Presenting theory "FO_Theory_Rewriting.Context_Extensions"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "FO_Theory_Rewriting.FOR_Certificate"
Presenting theory "HOL-Cardinals.Order_Union"
Presenting theory "Deriving.Comparator_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/comparator_generator.ML"
Presenting theory "FO_Theory_Rewriting.Lift_Root_Step"
Presenting theory "Deriving.Compare"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_code.ML"
Presenting theory "HOL-Cardinals.Wellorder_Extension"
Presenting theory "Deriving.Compare_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_generator.ML"
Presenting theory "Deriving.Compare_Instances"
Presenting theory "Containers.Containers_Auxiliary"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Regular_Tree_Relations.RRn_Automata"
Presenting theory "Containers.List_Fusion"
Presenting theory "Containers.Lexicographic_Order"
Presenting theory "FO_Theory_Rewriting.Context_RR2"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Typing_Result"
Presenting theory "FO_Theory_Rewriting.GTT_RRn"
Presenting theory "Containers.Extend_Partial_Order"
Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
Presenting theory "Abstract-Rewriting.Relative_Rewriting"
Presenting theory "First_Order_Terms.Abstract_Unification"
Presenting theory "Knuth_Bendix_Order.Order_Pair"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "Containers.Set_Linorder"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "First_Order_Terms.Option_Monad"
Presenting theory "Containers.Containers_Generator"
Presenting file "$AFP/Containers/containers_generator.ML"
Presenting theory "FOL-Fitting.FOL_Fitting"
Presenting theory "Containers.Collection_Order"
Presenting file "$AFP/Containers/ccompare_generator.ML"
Presenting theory "Knuth_Bendix_Order.Lexicographic_Extension"
Presenting theory "FO_Theory_Rewriting.FOL_Extra"
Presenting theory "Deriving.Equality_Generator"
Presenting file "$AFP/Deriving/Equality_Generator/equality_generator.ML"
Presenting theory "Deriving.Equality_Instances"
Presenting theory "FO_Theory_Rewriting.FOR_Semantics"
Presenting theory "First_Order_Terms.Unification"
Presenting theory "Containers.Collection_Eq"
Presenting theory "First_Order_Terms.Option_Monad"
Presenting file "$AFP/Containers/ceq_generator.ML"
Presenting theory "Regular_Tree_Relations.GTT_Transitive_Closure"
Presenting theory "Knuth_Bendix_Order.Subterm_and_Context"
Presenting theory "Knuth_Bendix_Order.Term_Aux"
Presenting theory "Regular_Tree_Relations.AGTT"
Presenting theory "Containers.Collection_Enum"
Presenting file "$AFP/Containers/cenum_generator.ML"
Presenting theory "Resolution_FOL.Unification_Theorem"
Presenting theory "Containers.Equal"
Presenting theory "Resolution_FOL.Completeness_Instance"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Stateful_Strands"
Presenting theory "Regular_Tree_Relations.Tree_Automata_Pumping"
Presenting theory "Containers.DList_Set"
Presenting theory "Regular_Tree_Relations.RR2_Infinite"
Presenting theory "Containers.RBT_ext"
Presenting theory "Regular_Tree_Relations.RR2_Infinite_Q_infinity"
Presenting theory "Deriving.RBT_Comparator_Impl"
Presenting theory "Knuth_Bendix_Order.KBO"
Presenting theory "Containers.RBT_Mapping2"
Presenting theory "Containers.RBT_Set2"
Presenting theory "Containers.Closure_Set"
Presenting theory "FO_Theory_Rewriting.FOR_Check"
Presenting theory "Functional_Ordered_Resolution_Prover.IsaFoR_Term"
Presenting theory "Regular_Tree_Relations.Horn_Inference"
Presenting theory "Regular_Tree_Relations.Horn_Fset"
Presenting theory "Regular_Tree_Relations.Tree_Automata_Abstract_Impl"
Presenting theory "Containers.Map_To_Mapping"
Presenting theory "Containers.Containers"
Presenting theory "Regular_Tree_Relations.Tree_Automata_Impl"
Presenting theory "First_Order_Terms.Abstract_Matching"
Presenting theory "Regular_Tree_Relations.Regular_Relation_Abstract_Impl"
Presenting theory "Regular_Tree_Relations.Regular_Relation_Impl"
Presenting theory "First_Order_Terms.Matching"
Presenting theory "Functional_Ordered_Resolution_Prover.Executable_Subsumption"
Presenting theory "FO_Theory_Rewriting.FOR_Check_Impl"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Stateful_Typing"
Presenting theory "Containers.Set_Impl"
Presenting theory "Show.Show"
Presenting file "$AFP/Show/show_generator.ML"
Presenting file "$AFP/Containers/set_impl_generator.ML"
Presenting theory "Containers.AssocList"
Presenting theory "Show.Show_Instances"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Labeled_Strands"
Presenting theory "Containers.Mapping_Impl"
Presenting file "$AFP/Containers/mapping_impl_generator.ML"
Presenting theory "Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl"
Presenting theory "Functional_Ordered_Resolution_Prover.Executable_FO_Ordered_Resolution_Prover"
Presenting theory "Containers.Map_To_Mapping"
Presenting theory "Containers.Containers"
Presenting theory "Regular_Tree_Relations.Tree_Automata_Impl"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Parallel_Compositionality"
Presenting theory "Regular_Tree_Relations.RR2_Infinite_Q_infinity"
Presenting theory "Regular_Tree_Relations.Regular_Relation_Abstract_Impl"
Presenting theory "Automated_Stateful_Protocol_Verification.Stateful_Protocol_Model"
Presenting theory "Regular_Tree_Relations.Regular_Relation_Impl"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Labeled_Stateful_Strands"
Presenting theory "Automated_Stateful_Protocol_Verification.Term_Variants"
Presenting theory "Automated_Stateful_Protocol_Verification.Term_Implication"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Stateful_Compositionality"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Example_Keyserver"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Example_TLS"
Presenting theory "Stateful_Protocol_Composition_and_Typing.Examples"
Presenting theory "Automated_Stateful_Protocol_Verification.Stateful_Protocol_Verification"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting file "~~/src/HOL/Eisbach/parse_tools.ML"
Presenting file "~~/src/HOL/Eisbach/method_closure.ML"
Presenting file "~~/src/HOL/Eisbach/eisbach_rule_insts.ML"
Presenting file "~~/src/HOL/Eisbach/match_method.ML"
Presenting theory "HOL-Eisbach.Eisbach_Tools"
Presenting theory "Automated_Stateful_Protocol_Verification.Eisbach_Protocol_Verification"
Presenting theory "Automated_Stateful_Protocol_Verification.ml_yacc_lib"
Presenting file "$AFP/Automated_Stateful_Protocol_Verification/trac/ml-yacc-lib/base.sig"
Presenting file "$AFP/Automated_Stateful_Protocol_Verification/trac/ml-yacc-lib/join.sml"
Presenting file "$AFP/Automated_Stateful_Protocol_Verification/trac/ml-yacc-lib/lrtable.sml"
Presenting file "$AFP/Automated_Stateful_Protocol_Verification/trac/ml-yacc-lib/stream.sml"
Presenting file "$AFP/Automated_Stateful_Protocol_Verification/trac/ml-yacc-lib/parser2.sml"
Presenting theory "Automated_Stateful_Protocol_Verification.trac_term"
Presenting theory "Automated_Stateful_Protocol_Verification.trac_fp_parser"
Presenting file "$AFP/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.grm.sig"
Presenting file "$AFP/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.lex.sml"
Presenting file "$AFP/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.grm.sml"
Presenting theory "Automated_Stateful_Protocol_Verification.trac_protocol_parser"
Presenting file "$AFP/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.grm.sig"
Presenting file "$AFP/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.lex.sml"
Presenting file "$AFP/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.grm.sml"
Presenting theory "Automated_Stateful_Protocol_Verification.trac"
Presenting theory "Automated_Stateful_Protocol_Verification.PSPSP"
Presenting theory "Automated_Stateful_Protocol_Verification.introduction"
Presenting theory "Automated_Stateful_Protocol_Verification.KeyserverEx"
Presenting theory "Automated_Stateful_Protocol_Verification.manual"
Presenting theory "Automated_Stateful_Protocol_Verification.Keyserver"
Presenting theory "Automated_Stateful_Protocol_Verification.Keyserver2"
Presenting theory "Automated_Stateful_Protocol_Verification.Keyserver_Composition"
Presenting theory "Automated_Stateful_Protocol_Verification.PKCS_Model03"
Presenting theory "Automated_Stateful_Protocol_Verification.PKCS_Model07"
Presenting theory "Automated_Stateful_Protocol_Verification.PKCS_Model09"
Presenting theory "Automated_Stateful_Protocol_Verification.Examples"

=== TIMING ===

Group AFP: 0:31:34 elapsed time, 2:01:30 cpu time, factor 3.85
Group main: 0:00:00 elapsed time
Group large: 0:00:00 elapsed time
Group no_doc: 0:00:00 elapsed time
Group doc: 0:00:00 elapsed time
Group timing: 0:00:00 elapsed time
Overall: 0:21:32 elapsed time, 2:01:30 cpu time, factor 5.64

=== DEPENDENCIES ===

Generating dependencies file ...
Writing dependencies file ...

=== REPORT ===

Writing report file ...

=== SITEGEN ===

Writing status file ...
Running sitegen ...
using [/media/data/jenkins/workspace/isabelle-all/bin/isabelle]
Preparing site generation in out/hugo
Cleaning up generated files...
Preparing topics...
Preparing licenses...
Preparing releases...
Preparing authors...
Extracting keywords...
Preparing entries...
Preparing statistics...
Preparing project files
Preparing devel version...
Finished sitegen preparation.
Cleaning output dir...
Building site...
Build in /media/data/jenkins/workspace/isabelle-all/afp/web/index.html
Packing tars ...

=== COMPLETED ===

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: SUCCESS