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 070703d83cfe639d875f5f3099c0c8c8f1239502 --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(070703d83cfe639d875f5f3099c0c8c8f1239502)" --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
1501 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 1a1e92696b0dd99ca35b0b111bae56068a4f311f --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(1a1e92696b0dd99ca35b0b111bae56068a4f311f)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-all] $ /bin/sh -xe /tmp/jenkins7325917361640604309.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-a5d5fba90286/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 Tue, 23 May 2023 00:18:31 +0200
Isabelle id 070703d83cfe
AFP id e74d656c954e

=== 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/Boolos_Curious_Inference_Automated (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/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/Epistemic_Logic (AFP)
Session AFP/Public_Announcement_Logic (AFP)
Session AFP/Stalnaker_Logic (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/Birkhoff_Finite_Distributive_Lattices (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/Complete_Non_Orders (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/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/AOT (AFP)
Session AFP/Allen_Calculus (AFP)
Session AFP/Card_Partitions (AFP)
Session AFP/Bell_Numbers_Spivey (AFP)
Session AFP/Card_Equiv_Relations (AFP)
Session AFP/Equivalence_Relation_Enumeration (AFP)
Session AFP/Falling_Factorial_Sum (AFP)
Session AFP/Combinatorial_Enumeration_Algorithms (AFP)
Session AFP/Case_Labeling (AFP)
Session AFP/Clean (AFP)
Session AFP/Combinatorics_Words (AFP)
Session AFP/Combinatorics_Words_Graph_Lemma (AFP)
Session AFP/Cook_Levin (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/Turans_Graph_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/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/HoareForDivergence (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/Kneser_Cauchy_Davenport (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/PAPP_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/Multitape_To_Singletape_TM (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/Balog_Szemeredi_Gowers (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_Logic_Class (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/Sauer_Shelah_Lemma (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/StrictOmegaCategories (AFP)
Session AFP/Strong_Security (AFP)
Session Doc/Sugar (doc)
Session AFP/Sunflowers (AFP)
Session AFP/Clique_and_Monotone_Circuits (AFP)
Session AFP/Suppes_Theorem (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/Synthetic_Completeness (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/CHERI-C_Memory_Model (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/MDP-Algorithms (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/Quantifier_Elimination_Hybrid (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 Nominal2 on hpcisabelle/0 ...
Building Dependent_SIFUM_Type_Systems on hpcisabelle/1 ...
Building Launchbury on hpcisabelle/2 ...
Building Incompleteness on hpcisabelle/3 ...
Running MiniSail on hpcisabelle/4 ...
Running Goedel_HFSet_Semantic on hpcisabelle/5 ...
Running Goedel_HFSet_Semanticless on hpcisabelle/6 ...
Running Types_To_Sets_Extension on hpcisabelle/7 ...
Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Preliminaries
Nominal2: theory HOL-Library.Nat_Bijection
Nominal2: theory HOL-Library.Infinite_Set
Nominal2: theory HOL-Library.Cancellation
Nominal2: theory HOL-Library.Phantom_Type
Nominal2: theory HOL-Library.Old_Datatype
Nominal2: theory HOL-Library.Quotient_Syntax
Nominal2: theory HOL-Library.Quotient_Product
Nominal2: theory HOL-Library.Quotient_Option
Nominal2: theory HOL-Library.Quotient_Set
Launchbury: theory HOL-Library.Infinite_Set
Launchbury: theory HOL-Library.Cancellation
Launchbury: theory HOL-Library.AList
Launchbury: theory HOL-Library.LaTeXsugar
Launchbury: theory HOL-Library.Phantom_Type
Launchbury: theory HOL-Library.Quotient_Syntax
Launchbury: theory HOL-Library.FSet
Launchbury: theory Launchbury.HOLCF-Join
Launchbury: theory HOL-Library.Quotient_Option
Nominal2: theory HOL-Library.Quotient_List
Launchbury: theory HOL-Library.Quotient_Product
Launchbury: theory HOL-Library.Quotient_Set
Types_To_Sets_Extension: theory HOL-Eisbach.Eisbach
Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Tools
Types_To_Sets_Extension: theory HOL-Types_To_Sets.Types_To_Sets
Goedel_HFSet_Semantic: theory HOL-Library.Cancellation
Goedel_HFSet_Semantic: theory HOL-Library.Infinite_Set
Goedel_HFSet_Semantic: theory HOL-Library.Phantom_Type
Goedel_HFSet_Semantic: theory HOL-Library.Old_Datatype
Goedel_HFSet_Semantic: theory HOL-Library.Nat_Bijection
Goedel_HFSet_Semantic: theory HOL-Library.Quotient_Syntax
Goedel_HFSet_Semanticless: theory HOL-Library.Infinite_Set
Goedel_HFSet_Semanticless: theory HOL-Library.Cancellation
Goedel_HFSet_Semanticless: theory HOL-Library.Old_Datatype
Goedel_HFSet_Semanticless: theory HOL-Library.Nat_Bijection
Goedel_HFSet_Semanticless: theory HOL-Library.Quotient_Syntax
Goedel_HFSet_Semanticless: theory HOL-Library.Phantom_Type
Goedel_HFSet_Semantic: theory HOL-Library.Quotient_Option
Goedel_HFSet_Semantic: theory HOL-Library.Quotient_Product
Goedel_HFSet_Semanticless: theory HOL-Library.Quotient_Option
Goedel_HFSet_Semanticless: theory HOL-Library.Quotient_Set
Goedel_HFSet_Semanticless: theory HOL-Library.Quotient_Product
Goedel_HFSet_Semantic: theory HOL-Library.Quotient_Set
Incompleteness: theory FinFun.FinFun
MiniSail: theory FinFun.FinFun
MiniSail: theory HOL-Eisbach.Eisbach
Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Language
Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Security
Launchbury: theory Launchbury.HOLCF-Meet
Launchbury: theory HOL-Library.Quotient_List
Launchbury: theory Launchbury.HOLCF-Join-Classes
Goedel_HFSet_Semanticless: theory HOL-Library.Quotient_List
Goedel_HFSet_Semantic: theory HOL-Library.Quotient_List
Launchbury: theory Launchbury.Mono-Nat-Fun
Nominal2: theory HOL-Library.Countable
Launchbury: theory Launchbury.C
Nominal2: theory HOL-Library.Multiset
Nominal2: theory HOL-Library.Cardinality
Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Compositionality
Goedel_HFSet_Semantic: theory HereditarilyFinite.HF
Launchbury: theory Launchbury.Value
Goedel_HFSet_Semanticless: theory HereditarilyFinite.HF
Launchbury: theory HOL-Library.Multiset
Launchbury: theory Launchbury.Pointwise
Launchbury: theory HOL-Library.Cardinality
Launchbury: theory Launchbury.HOLCF-Utils
Launchbury: theory Launchbury.Env
Goedel_HFSet_Semanticless: theory HOL-Library.Countable
Goedel_HFSet_Semanticless: theory HOL-Library.Multiset
Incompleteness: theory Nominal2.Nominal2_Base
Nominal2: theory FinFun.FinFun
Goedel_HFSet_Semanticless: theory HOL-Library.Cardinality
Goedel_HFSet_Semantic: theory HOL-Library.Countable
Launchbury: theory Launchbury.CValue
Goedel_HFSet_Semantic: theory HOL-Library.Multiset
Launchbury: theory Launchbury.C-Meet
Goedel_HFSet_Semantic: theory HOL-Library.Cardinality
Launchbury: theory Launchbury.Env-HOLCF
Launchbury: theory Launchbury.AList-Utils
Nominal2: theory HOL-Library.FSet
Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS
Launchbury: theory FinFun.FinFun
Launchbury: theory Launchbury.C-restr
Launchbury: theory Launchbury.Iterative
Launchbury: theory Launchbury.ValueSimilarity
Goedel_HFSet_Semanticless: theory HereditarilyFinite.Ordinal
MiniSail: theory HOL-Eisbach.Eisbach_Tools
Goedel_HFSet_Semanticless: theory FinFun.FinFun
Goedel_HFSet_Semantic: theory HereditarilyFinite.Ordinal
Goedel_HFSet_Semantic: theory FinFun.FinFun
Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.TypeSystem
Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.LocallySoundModeUse
Goedel_HFSet_Semanticless: theory HereditarilyFinite.Rank
Goedel_HFSet_Semanticless: theory HOL-Library.FSet
Goedel_HFSet_Semantic: theory HereditarilyFinite.Rank
Goedel_HFSet_Semanticless: theory HereditarilyFinite.OrdArith
MiniSail: theory Nominal2.Nominal2_Base
Goedel_HFSet_Semantic: theory HereditarilyFinite.OrdArith
Goedel_HFSet_Semantic: theory HOL-Library.FSet
Incompleteness: theory Nominal2.Nominal2_Abs
Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Auxiliary
Types_To_Sets_Extension: theory Types_To_Sets_Extension.Manual_Prerequisites
Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Tests
Incompleteness: theory Nominal2.Nominal2_FCB
Incompleteness: theory Nominal2.Nominal2
Types_To_Sets_Extension: theory HOL-Library.Infinite_Set
Types_To_Sets_Extension: theory HOL-Library.FuncSet
Types_To_Sets_Extension: theory Types_To_Sets_Extension.FNDS_Auxiliary
Types_To_Sets_Extension: theory Types_To_Sets_Extension.Introduction
Types_To_Sets_Extension: theory HOL-Library.Nat_Bijection
Types_To_Sets_Extension: theory HOL-Library.Old_Datatype
Types_To_Sets_Extension: theory HOL-Library.Product_Plus
Types_To_Sets_Extension: theory Types_To_Sets_Extension.VS_Prerequisites
Types_To_Sets_Extension: theory Types_To_Sets_Extension.FNDS_Introduction
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Introduction
Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Introduction
Types_To_Sets_Extension: theory Types_To_Sets_Extension.FNDS_Definite_Description
Types_To_Sets_Extension: theory Types_To_Sets_Extension.VS_Groups
Types_To_Sets_Extension: theory HOL-Analysis.Product_Vector
Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Theory
Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Syntax
Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_Examples
Types_To_Sets_Extension: theory Types_To_Sets_Extension.Type_Simple_Orders
MiniSail: theory Nominal2.Nominal2_Abs
Types_To_Sets_Extension: theory Types_To_Sets_Extension.FNDS_Lifting_Set_Ext
Nominal2: theory Nominal2.Nominal2_Base
Types_To_Sets_Extension: theory Types_To_Sets_Extension.FNDS_Set_Ext
Types_To_Sets_Extension: theory Types_To_Sets_Extension.Lifting_Set_Ext
Types_To_Sets_Extension: theory Types_To_Sets_Extension.VS_Modules
MiniSail: theory Nominal2.Nominal2_FCB
Types_To_Sets_Extension: theory Types_To_Sets_Extension.Product_Type_Ext
MiniSail: theory Nominal2.Nominal2
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Relations
Launchbury: theory Nominal2.Nominal2_Base
Types_To_Sets_Extension: theory HOL-Library.Countable
Types_To_Sets_Extension: theory HOL-Library.Disjoint_Sets
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Semigroups
Types_To_Sets_Extension: theory Types_To_Sets_Extension.ETTS_CR
Types_To_Sets_Extension: theory Types_To_Sets_Extension.Set_Ext
Goedel_HFSet_Semanticless: theory Nominal2.Nominal2_Base
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Simple_Orders
Goedel_HFSet_Semantic: theory Nominal2.Nominal2_Base
Types_To_Sets_Extension: theory Types_To_Sets_Extension.Transfer_Ext
Types_To_Sets_Extension: theory Types_To_Sets_Extension.Type_Semigroups
Dependent_SIFUM_Type_Systems: theory HOL-Eisbach.Eisbach
Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Example
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Monoids
Types_To_Sets_Extension: theory Types_To_Sets_Extension.Set_Semigroups
Types_To_Sets_Extension: theory HOL-Library.Countable_Set
Launchbury: theory Nominal2.Nominal2_Abs
Nominal2: theory Nominal2.Atoms
Nominal2: theory Nominal2.Eqvt
Nominal2: theory Nominal2.Nominal2_Abs
Types_To_Sets_Extension: theory HOL-Library.Set_Idioms
Dependent_SIFUM_Type_Systems: theory HOL-Eisbach.Eisbach_Tools
Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.TypeSystemTactics
Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Example_Swap_Add
Dependent_SIFUM_Type_Systems: theory Dependent_SIFUM_Type_Systems.Example_TypeSystem
Incompleteness: theory Incompleteness.SyntaxN
Launchbury: theory Nominal2.Nominal2_FCB
Types_To_Sets_Extension: theory HOL-Analysis.Elementary_Topology
Launchbury: theory Nominal2.Nominal2
Nominal2: theory Nominal2.Nominal2_FCB
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Groups
Nominal2: theory Nominal2.Nominal2
Incompleteness: theory Incompleteness.Coding
Incompleteness: theory Incompleteness.Predicates
Incompleteness: theory Incompleteness.Sigma
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Semirings
Incompleteness: theory Incompleteness.Coding_Predicates
Goedel_HFSet_Semanticless: theory Nominal2.Nominal2_Abs
Types_To_Sets_Extension: theory Types_To_Sets_Extension.Set_Simple_Orders
MiniSail: theory MiniSail.Nominal-Utils
MiniSail: theory MiniSail.Syntax
Goedel_HFSet_Semantic: theory Nominal2.Nominal2_Abs
Goedel_HFSet_Semanticless: theory Nominal2.Nominal2_FCB
Goedel_HFSet_Semanticless: theory Nominal2.Nominal2
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Rings
Incompleteness: theory Incompleteness.Functions
Incompleteness: theory Incompleteness.Pf_Predicates
Goedel_HFSet_Semantic: theory Nominal2.Nominal2_FCB
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Semilattices
Incompleteness: theory Incompleteness.Goedel_I
Incompleteness: theory Incompleteness.II_Prelims
Goedel_HFSet_Semantic: theory Nominal2.Nominal2
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Lattices
Types_To_Sets_Extension: theory Types_To_Sets_Extension.VS_Vector_Spaces
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Linorders
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Topological_Space
Launchbury: theory Launchbury.Nominal-Utils
Launchbury: theory Launchbury.Vars
Launchbury: theory Launchbury.EvalHeap
MiniSail: theory MiniSail.BTVSubst
MiniSail: theory MiniSail.IVSubst
Preparing Dependent_SIFUM_Type_Systems/document ...
Launchbury: theory Launchbury.AList-Utils-Nominal
Launchbury: theory Launchbury.Nominal-HOLCF
Launchbury: theory Launchbury.Terms
Incompleteness: theory Incompleteness.Pseudo_Coding
Launchbury: theory Launchbury.CValue-Nominal
Launchbury: theory Launchbury.Env-Nominal
Launchbury: theory Launchbury.HasESem
Launchbury: theory Launchbury.Value-Nominal
Launchbury: theory Launchbury.HeapSemantics
Incompleteness: theory Incompleteness.Quote
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Complete_Lattices
Types_To_Sets_Extension: theory Types_To_Sets_Extension.FNDS_Conclusions
Incompleteness: theory Incompleteness.Goedel_II
MiniSail: theory MiniSail.Wellformed
MiniSail: theory MiniSail.SyntaxL
Preparing Nominal2/document ...
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Ordered_Topological_Spaces
Launchbury: theory Launchbury.Substitution
Launchbury: theory Launchbury.AbstractDenotational
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Product_Topology
Launchbury: theory Launchbury.Launchbury
Launchbury: theory Launchbury.Abstract-Denotational-Props
Launchbury: theory Launchbury.ResourcedDenotational
Launchbury: theory Launchbury.Denotational
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Topological_Space_Countability
Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.SyntaxN
Launchbury: theory Launchbury.CorrectnessOriginal
Launchbury: theory Launchbury.CorrectnessResourced
Launchbury: theory Launchbury.Denotational-Related
Launchbury: theory Launchbury.ResourcedAdequacy
Launchbury: theory Launchbury.Adequacy
Launchbury: theory Launchbury.EverythingAdequacy
Finished Dependent_SIFUM_Type_Systems/document (0:00:13 elapsed time)
Preparing Dependent_SIFUM_Type_Systems/outline ...
Types_To_Sets_Extension: theory Types_To_Sets_Extension.SML_Conclusions
Finished Nominal2/document (0:00:05 elapsed time)
Preparing Nominal2/outline ...
Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Coding
Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Predicates
Types_To_Sets_Extension: theory Types_To_Sets_Extension.VS_Conclusions
Goedel_HFSet_Semantic: theory Incompleteness.SyntaxN
Finished Nominal2/outline (0:00:03 elapsed time)
Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Sigma
Timing Nominal2 (8 threads, 21.597s elapsed time, 104.904s cpu time, 4.320s GC time, factor 4.86)
Finished Nominal2 (0:02:00 elapsed time, 0:02:12 cpu time, factor 1.10)
Running Modal_Logics_for_NTS on hpcisabelle/0 ...
Finished Dependent_SIFUM_Type_Systems/outline (0:00:06 elapsed time)
Timing Dependent_SIFUM_Type_Systems (8 threads, 68.827s elapsed time, 326.865s cpu time, 11.364s GC time, factor 4.75)
Finished Dependent_SIFUM_Type_Systems (0:01:51 elapsed time, 0:06:23 cpu time, factor 3.45)
Running Dependent_SIFUM_Refinement on hpcisabelle/1 ...
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FS_Set
Modal_Logics_for_NTS: theory HOL-Cardinals.Order_Union
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Nominal_Wellfounded
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Residual
Modal_Logics_for_NTS: theory HOL-Cardinals.Fun_More
Modal_Logics_for_NTS: theory HOL-Cardinals.Order_Relation_More
Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.CompositionalRefinement
Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Coding_Predicates
Modal_Logics_for_NTS: theory HOL-Cardinals.Wellorder_Extension
Goedel_HFSet_Semantic: theory Incompleteness.Coding
Goedel_HFSet_Semantic: theory Incompleteness.Predicates
Modal_Logics_for_NTS: theory HOL-Cardinals.Wellfounded_More
Modal_Logics_for_NTS: theory HOL-Cardinals.Wellorder_Relation
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Transition_System
Modal_Logics_for_NTS: theory HOL-Cardinals.Wellorder_Embedding
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Transition_System
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Transition_System
Modal_Logics_for_NTS: theory HOL-Cardinals.Wellorder_Constructions
Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Functions
Goedel_HFSet_Semantic: theory Incompleteness.Sigma
Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Pf_Predicates
Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.II_Prelims
Modal_Logics_for_NTS: theory HOL-Cardinals.Cardinal_Order_Relation
Modal_Logics_for_NTS: theory HOL-Cardinals.Ordinal_Arithmetic
Goedel_HFSet_Semantic: theory Incompleteness.Coding_Predicates
Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Goedel_I
Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Pseudo_Coding
Modal_Logics_for_NTS: theory HOL-Cardinals.Cardinal_Arithmetic
Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg2
Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.EgHighBranchRevC
Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1
Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Quote
Goedel_HFSet_Semantic: theory Incompleteness.Functions
Goedel_HFSet_Semantic: theory Incompleteness.Pf_Predicates
Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1Eg2
Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1RefinementTrivial
Preparing Types_To_Sets_Extension/document ...
Goedel_HFSet_Semantic: theory Incompleteness.Goedel_I
Goedel_HFSet_Semantic: theory Incompleteness.II_Prelims
Modal_Logics_for_NTS: theory HOL-Cardinals.Cardinals
Modal_Logics_for_NTS: theory HOL-Cardinals.Bounded_Set
Preparing Launchbury/document ...
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Nominal_Bounded_Set
Goedel_HFSet_Semanticless: theory Goedel_HFSet_Semanticless.Instance
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Formula
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Formula
Goedel_HFSet_Semantic: theory Incompleteness.Pseudo_Coding
Goedel_HFSet_Semantic: theory Incompleteness.Quote
Goedel_HFSet_Semantic: theory Goedel_HFSet_Semantic.Instance
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Validity
Dependent_SIFUM_Refinement: theory Dependent_SIFUM_Refinement.Eg1Eg2RefinementSimple
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Validity
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Disjunction
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Logical_Equivalence
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Formula
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Bisimilarity_Implies_Equivalence
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Equivalence_Implies_Bisimilarity
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Expressive_Completeness
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Logical_Equivalence
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Bisimilarity_Implies_Equivalence
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.FL_Equivalence_Implies_Bisimilarity
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Validity
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Logical_Equivalence
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.L_Transform
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Bisimilarity_Implies_Equivalence
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Equivalence_Implies_Bisimilarity
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.Weak_Expressive_Completeness
Modal_Logics_for_NTS: theory Modal_Logics_for_NTS.S_Transform
Finished Launchbury/document (0:00:14 elapsed time)
Preparing Launchbury/outline ...
MiniSail: theory MiniSail.RCLogic
MiniSail: theory MiniSail.WellformedL
Finished Launchbury/outline (0:00:09 elapsed time)
Timing Launchbury (8 threads, 136.572s elapsed time, 192.951s cpu time, 8.009s GC time, factor 1.41)
Finished Launchbury (0:02:34 elapsed time, 0:03:54 cpu time, factor 1.52)
Running LambdaAuth on hpcisabelle/2 ...
LambdaAuth: theory LambdaAuth.Nominal2_Lemmas
LambdaAuth: theory HOL-Library.Conditional_Parametricity
LambdaAuth: theory HOL-Library.AList
LambdaAuth: theory LambdaAuth.Syntax
LambdaAuth: theory HOL-Library.Finite_Map
Finished Types_To_Sets_Extension/document (0:00:43 elapsed time)
Preparing Types_To_Sets_Extension/outline ...
LambdaAuth: theory LambdaAuth.FMap_Lemmas
MiniSail: theory MiniSail.SubstMethods
LambdaAuth: theory LambdaAuth.Semantics
MiniSail: theory MiniSail.RCLogicL
MiniSail: theory MiniSail.Typing
LambdaAuth: theory LambdaAuth.Agreement
LambdaAuth: theory LambdaAuth.Results
Finished Types_To_Sets_Extension/outline (0:00:34 elapsed time)
Timing Types_To_Sets_Extension (8 threads, 148.475s elapsed time, 344.244s cpu time, 10.057s GC time, factor 2.32)
Finished Types_To_Sets_Extension (0:02:31 elapsed time, 0:05:50 cpu time, factor 2.32)
Running Call_Arity on hpcisabelle/7 ...
Call_Arity: theory Call_Arity.BalancedTraces
Call_Arity: theory Call_Arity.ConstOn
Call_Arity: theory Call_Arity.List-Interleavings
Call_Arity: theory Call_Arity.Set-Cpo
Call_Arity: theory Call_Arity.Arity
Call_Arity: theory Call_Arity.EtaExpansion
Call_Arity: theory Call_Arity.SestoftConf
Call_Arity: theory Call_Arity.AList-Utils-HOLCF
Call_Arity: theory Call_Arity.AnalBinds
Call_Arity: theory Call_Arity.Env-Set-Cpo
Call_Arity: theory Call_Arity.Cardinality-Domain
Call_Arity: theory Call_Arity.CoCallGraph
Call_Arity: theory Call_Arity.AEnv
Call_Arity: theory Call_Arity.Arity-Nominal
Call_Arity: theory Call_Arity.TTree
Call_Arity: theory Call_Arity.Cardinality-Domain-Lists
Call_Arity: theory Call_Arity.TransformTools
Call_Arity: theory Call_Arity.ArityAnalysisSig
Call_Arity: theory Call_Arity.AbstractTransform
Call_Arity: theory Call_Arity.ArityEtaExpansion
Call_Arity: theory Call_Arity.TTree-HOLCF
Call_Arity: theory Call_Arity.CoCallAnalysisSig
Call_Arity: theory Call_Arity.CoCallGraph-Nominal
Call_Arity: theory Call_Arity.ArityAnalysisAbinds
Call_Arity: theory Call_Arity.ArityStack
Call_Arity: theory Call_Arity.Sestoft
Call_Arity: theory Call_Arity.CardinalityAnalysisSig
Preparing LambdaAuth/document ...
Call_Arity: theory Call_Arity.ArityAnalysisStack
Call_Arity: theory Call_Arity.EtaExpansionSafe
Call_Arity: theory Call_Arity.SestoftGC
Call_Arity: theory Call_Arity.SestoftCorrect
Call_Arity: theory Call_Arity.ArityAnalysisSpec
Call_Arity: theory Call_Arity.ArityAnalysisFix
Call_Arity: theory Call_Arity.CoCallGraph-TTree
Call_Arity: theory Call_Arity.TTreeAnalysisSig
Call_Arity: theory Call_Arity.CoCallAritySig
Call_Arity: theory Call_Arity.CoCallAnalysisBinds
Call_Arity: theory Call_Arity.ArityAnalysisFixProps
Call_Arity: theory Call_Arity.CardinalityAnalysisSpec
Call_Arity: theory Call_Arity.ArityConsistent
Call_Arity: theory Call_Arity.CoCallAnalysisSpec
Call_Arity: theory Call_Arity.ArityEtaExpansionSafe
Call_Arity: theory Call_Arity.TrivialArityAnal
Call_Arity: theory Call_Arity.CoCallImplTTree
Call_Arity: theory Call_Arity.TTreeAnalysisSpec
Call_Arity: theory Call_Arity.TTreeImplCardinality
Call_Arity: theory Call_Arity.NoCardinalityAnalysis
Call_Arity: theory Call_Arity.ArityTransform
Call_Arity: theory Call_Arity.CoCallFix
Call_Arity: theory Call_Arity.CoCallImplTTreeSafe
Call_Arity: theory Call_Arity.ArityTransformSafe
Call_Arity: theory Call_Arity.CardArityTransformSafe
Call_Arity: theory Call_Arity.ArityAnalysisCorrDenotational
Call_Arity: theory Call_Arity.TTreeImplCardinalitySafe
Call_Arity: theory Call_Arity.CoCallAnalysisImpl
Finished LambdaAuth/document (0:00:06 elapsed time)
Preparing LambdaAuth/outline ...
Call_Arity: theory Call_Arity.CallArityEnd2End
Call_Arity: theory Call_Arity.CoCallImplSafe
Call_Arity: theory Call_Arity.CallArityEnd2EndSafe
Preparing Dependent_SIFUM_Refinement/document ...
Finished LambdaAuth/outline (0:00:04 elapsed time)
Timing LambdaAuth (8 threads, 53.321s elapsed time, 184.265s cpu time, 3.669s GC time, factor 3.46)
Finished LambdaAuth (0:00:55 elapsed time, 0:03:08 cpu time, factor 3.41)
Running Rewriting_Z on hpcisabelle/2 ...
Rewriting_Z: theory HOL-Eisbach.Eisbach
Rewriting_Z: theory Abstract-Rewriting.Seq
Rewriting_Z: theory HOL-Library.While_Combinator
Rewriting_Z: theory Regular-Sets.Regular_Set
Finished Dependent_SIFUM_Refinement/document (0:00:06 elapsed time)
Preparing Dependent_SIFUM_Refinement/outline ...
Rewriting_Z: theory Regular-Sets.Regular_Exp
Finished Dependent_SIFUM_Refinement/outline (0:00:04 elapsed time)
Timing Dependent_SIFUM_Refinement (8 threads, 111.095s elapsed time, 412.146s cpu time, 17.810s GC time, factor 3.71)
Finished Dependent_SIFUM_Refinement (0:01:53 elapsed time, 0:07:00 cpu time, factor 3.69)
Running Certification_Monads on hpcisabelle/1 ...
Rewriting_Z: theory Regular-Sets.NDerivative
Rewriting_Z: theory Regular-Sets.Relation_Interpretation
Certification_Monads: theory Deriving.Derive_Manager
Certification_Monads: theory Deriving.Generator_Aux
Certification_Monads: theory Certification_Monads.Misc
Certification_Monads: theory HOL-Library.Adhoc_Overloading
Certification_Monads: theory Partial_Function_MR.Partial_Function_MR
Certification_Monads: theory Certification_Monads.Error_Syntax
Certification_Monads: theory HOL-Library.Monad_Syntax
Certification_Monads: theory Show.Show
Certification_Monads: theory Certification_Monads.Error_Monad
Certification_Monads: theory Certification_Monads.Strict_Sum
Certification_Monads: theory Certification_Monads.Check_Monad
Certification_Monads: theory Certification_Monads.Parser_Monad
Rewriting_Z: theory Regular-Sets.Equivalence_Checking
Rewriting_Z: theory Regular-Sets.Regexp_Method
Rewriting_Z: theory Abstract-Rewriting.Abstract_Rewriting
Preparing Certification_Monads/document ...
Rewriting_Z: theory Rewriting_Z.Z
Rewriting_Z: theory Rewriting_Z.CL_Z
Rewriting_Z: theory Rewriting_Z.Lambda_Z
Finished Certification_Monads/document (0:00:02 elapsed time)
Preparing Certification_Monads/outline ...
Preparing Call_Arity/document ...
Finished Certification_Monads/outline (0:00:02 elapsed time)
Timing Certification_Monads (8 threads, 4.190s elapsed time, 14.838s cpu time, 0.267s GC time, factor 3.54)
Finished Certification_Monads (0:00:06 elapsed time, 0:00:19 cpu time, factor 3.07)
Running Isabelle_C on hpcisabelle/1 ...
Isabelle_C: theory HOL-ex.Cartouche_Examples
Isabelle_C: theory Isabelle_C.C_Ast
Isabelle_C: theory Isabelle_C.C_Lexer_Language
Preparing Modal_Logics_for_NTS/document ...
Preparing Rewriting_Z/document ...
Isabelle_C: theory Isabelle_C.C_Lexer_Annotation
Finished Rewriting_Z/document (0:00:02 elapsed time)
Preparing Rewriting_Z/outline ...
Finished Rewriting_Z/outline (0:00:03 elapsed time)
Timing Rewriting_Z (8 threads, 22.052s elapsed time, 70.496s cpu time, 2.148s GC time, factor 3.20)
Finished Rewriting_Z (0:00:24 elapsed time, 0:01:14 cpu time, factor 3.08)
Running Robinson_Arithmetic on hpcisabelle/2 ...
Robinson_Arithmetic: theory HOL-Library.Cancellation
Robinson_Arithmetic: theory HOL-Library.Infinite_Set
Robinson_Arithmetic: theory HOL-Library.Nat_Bijection
Robinson_Arithmetic: theory HOL-Library.Phantom_Type
Robinson_Arithmetic: theory HOL-Library.Old_Datatype
Robinson_Arithmetic: theory HOL-Library.Quotient_Syntax
Robinson_Arithmetic: theory HOL-Library.Quotient_Option
Robinson_Arithmetic: theory HOL-Library.Quotient_Set
Robinson_Arithmetic: theory HOL-Library.Quotient_Product
Robinson_Arithmetic: theory HOL-Library.Quotient_List
Robinson_Arithmetic: theory HOL-Library.Countable
Robinson_Arithmetic: theory HOL-Library.Multiset
Robinson_Arithmetic: theory HOL-Library.Cardinality
Robinson_Arithmetic: theory FinFun.FinFun
Robinson_Arithmetic: theory HOL-Library.FSet
Finished Call_Arity/document (0:00:16 elapsed time)
Preparing Call_Arity/outline ...
Finished Modal_Logics_for_NTS/document (0:00:13 elapsed time)
Preparing Modal_Logics_for_NTS/outline ...
Robinson_Arithmetic: theory Nominal2.Nominal2_Base
Finished Modal_Logics_for_NTS/outline (0:00:05 elapsed time)
Timing Modal_Logics_for_NTS (8 threads, 136.566s elapsed time, 572.267s cpu time, 44.184s GC time, factor 4.19)
Finished Modal_Logics_for_NTS (0:02:19 elapsed time, 0:09:41 cpu time, factor 4.16)
Running XML on hpcisabelle/0 ...
XML: theory Deriving.Derive_Manager
XML: theory Certification_Monads.Error_Syntax
XML: theory Deriving.Generator_Aux
XML: theory Partial_Function_MR.Partial_Function_MR
XML: theory Certification_Monads.Error_Monad
Robinson_Arithmetic: theory Nominal2.Nominal2_Abs
XML: theory Certification_Monads.Strict_Sum
XML: theory Show.Show
Finished Call_Arity/outline (0:00:09 elapsed time)
Timing Call_Arity (8 threads, 33.455s elapsed time, 205.733s cpu time, 12.851s GC time, factor 6.15)
Finished Call_Arity (0:00:35 elapsed time, 0:03:31 cpu time, factor 5.88)
Running Partial_Function_MR on hpcisabelle/7 ...
XML: theory Certification_Monads.Parser_Monad
Robinson_Arithmetic: theory Nominal2.Nominal2_FCB
Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR
Partial_Function_MR: theory HOL-Library.Adhoc_Overloading
Robinson_Arithmetic: theory Nominal2.Nominal2
Partial_Function_MR: theory HOL-Library.Monad_Syntax
Partial_Function_MR: theory Partial_Function_MR.Partial_Function_MR_Examples
XML: theory XML.Xml
Robinson_Arithmetic: theory Robinson_Arithmetic.Robinson_Arithmetic
XML: theory XML.Xmlt
Preparing Partial_Function_MR/document ...
Finished Partial_Function_MR/document (0:00:03 elapsed time)
Preparing Partial_Function_MR/outline ...
Robinson_Arithmetic: theory Robinson_Arithmetic.Instance
Finished Partial_Function_MR/outline (0:00:03 elapsed time)
Timing Partial_Function_MR (8 threads, 6.846s elapsed time, 11.252s cpu time, 0.317s GC time, factor 1.64)
Finished Partial_Function_MR (0:00:08 elapsed time, 0:00:14 cpu time, factor 1.68)
Preparing XML/document ...
Finished XML/document (0:00:02 elapsed time)
Preparing XML/outline ...
Preparing Robinson_Arithmetic/document ...
Finished XML/outline (0:00:02 elapsed time)
Timing XML (8 threads, 21.177s elapsed time, 48.993s cpu time, 2.816s GC time, factor 2.31)
Finished XML (0:00:23 elapsed time, 0:00:53 cpu time, factor 2.24)
Isabelle_C: theory Isabelle_C.C_Environment
Isabelle_C: theory Isabelle_C.C_Parser_Language
Isabelle_C: theory Isabelle_C.C_Parser_Annotation
Finished Robinson_Arithmetic/document (0:00:02 elapsed time)
Preparing Robinson_Arithmetic/outline ...
Finished Robinson_Arithmetic/outline (0:00:02 elapsed time)
Timing Robinson_Arithmetic (8 threads, 37.366s elapsed time, 163.955s cpu time, 5.015s GC time, factor 4.39)
Finished Robinson_Arithmetic (0:00:39 elapsed time, 0:02:49 cpu time, factor 4.28)
Isabelle_C: theory Isabelle_C.C_Eval
Isabelle_C: theory Isabelle_C.C_Command
Isabelle_C: theory Isabelle_C.C_Document
Isabelle_C: theory Isabelle_C.C_Main
Isabelle_C: theory Isabelle_C.C0
Isabelle_C: theory Isabelle_C.C2
Isabelle_C: theory Isabelle_C.C_paper
Isabelle_C: theory Isabelle_C.C1
Isabelle_C: theory Isar_Ref.Base
Isabelle_C: theory Isabelle_C.README
Isabelle_C: theory Isabelle_C.C_Appendices
### Ignored report message: int
### Ignored report message: array\ int
### Ignored report message: int
Preparing Isabelle_C/document ...
MiniSail: theory MiniSail.Operational
MiniSail: theory MiniSail.TypingL
MiniSail: theory MiniSail.ContextSubtypingL
Finished Isabelle_C/document (0:00:22 elapsed time)
Preparing Isabelle_C/outline ...
MiniSail: theory MiniSail.BTVSubstTypingL
MiniSail: theory MiniSail.IVSubstTypingL
MiniSail: theory MiniSail.Safety
MiniSail: theory MiniSail.MiniSail
Preparing Goedel_HFSet_Semantic/document ...
Finished Goedel_HFSet_Semantic/document (0:00:01 elapsed time)
Preparing Goedel_HFSet_Semantic/outline ...
Finished Goedel_HFSet_Semantic/outline (0:00:01 elapsed time)
Timing Goedel_HFSet_Semantic (8 threads, 369.305s elapsed time, 1527.496s cpu time, 25.762s GC time, factor 4.14)
Finished Goedel_HFSet_Semantic (0:06:12 elapsed time, 0:25:37 cpu time, factor 4.13)
Finished Isabelle_C/outline (0:00:22 elapsed time)
Timing Isabelle_C (8 threads, 63.792s elapsed time, 76.571s cpu time, 16.774s GC time, factor 1.20)
Finished Isabelle_C (0:01:05 elapsed time, 0:01:19 cpu time, factor 1.22)
Preparing Incompleteness/document ...
Finished Incompleteness/document (0:00:19 elapsed time)
Preparing Incompleteness/outline ...
Finished Incompleteness/outline (0:00:10 elapsed time)
Timing Incompleteness (8 threads, 355.424s elapsed time, 1384.055s cpu time, 18.755s GC time, factor 3.89)
Finished Incompleteness (0:06:24 elapsed time, 0:24:09 cpu time, factor 3.77)
Running Surprise_Paradox on hpcisabelle/0 ...
Surprise_Paradox: theory Surprise_Paradox.Surprise_Paradox
Preparing Surprise_Paradox/document ...
Finished Surprise_Paradox/document (0:00:02 elapsed time)
Preparing Surprise_Paradox/outline ...
Finished Surprise_Paradox/outline (0:00:02 elapsed time)
Timing Surprise_Paradox (8 threads, 2.382s elapsed time, 4.998s cpu time, 0.000s GC time, factor 2.10)
Finished Surprise_Paradox (0:00:04 elapsed time, 0:00:08 cpu time, factor 1.70)
Preparing Goedel_HFSet_Semanticless/document ...
Finished Goedel_HFSet_Semanticless/document (0:00:09 elapsed time)
Preparing Goedel_HFSet_Semanticless/outline ...
Finished Goedel_HFSet_Semanticless/outline (0:00:04 elapsed time)
Timing Goedel_HFSet_Semanticless (8 threads, 428.676s elapsed time, 1817.577s cpu time, 28.782s GC time, factor 4.24)
Finished Goedel_HFSet_Semanticless (0:07:11 elapsed time, 0:30:27 cpu time, factor 4.23)
Preparing MiniSail/document ...
Finished MiniSail/document (0:00:33 elapsed time)
Preparing MiniSail/outline ...
Finished MiniSail/outline (0:00:12 elapsed time)
Timing MiniSail (8 threads, 677.948s elapsed time, 3564.474s cpu time, 233.760s GC time, factor 5.26)
Finished MiniSail (0:11:22 elapsed time, 0:59:37 cpu time, factor 5.25)
Presentation in "/media/data/jenkins/workspace/isabelle-all/browser_info"
Presenting Certification_Monads in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Certification_Monads" ...
Presenting Launchbury in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Launchbury" ...
Presenting Dependent_SIFUM_Refinement in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dependent_SIFUM_Refinement" ...
Presenting Types_To_Sets_Extension in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Types_To_Sets_Extension" ...
Presenting Incompleteness in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Incompleteness" ...
Presenting MiniSail in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/MiniSail" ...
Presenting Dependent_SIFUM_Type_Systems in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Dependent_SIFUM_Type_Systems" ...
Presenting XML in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/XML" ...
Presenting Surprise_Paradox in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Surprise_Paradox" ...
Presenting document Dependent_SIFUM_Refinement/document
Presenting document Certification_Monads/document
Presenting document Surprise_Paradox/document
Presenting document Surprise_Paradox/outline
Presenting document XML/document
Presenting document Dependent_SIFUM_Refinement/outline
Presenting document Certification_Monads/outline
Presenting document XML/outline
Presenting document Dependent_SIFUM_Type_Systems/document
Presenting document Incompleteness/document
Presenting document Dependent_SIFUM_Type_Systems/outline
Presenting document Incompleteness/outline
Presenting document MiniSail/document
Presenting document MiniSail/outline
Presenting theory "Certification_Monads.Error_Syntax"
Presenting document Launchbury/document
Presenting document Launchbury/outline
Presenting document Types_To_Sets_Extension/document
Presenting document Types_To_Sets_Extension/outline
Presenting theory "Dependent_SIFUM_Type_Systems.Preliminaries"
Presenting theory "Surprise_Paradox.Surprise_Paradox"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "Certification_Monads.Error_Syntax"
Presenting Call_Arity in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Call_Arity" ...
Presenting document Call_Arity/document
Presenting document Call_Arity/outline
Presenting theory "Certification_Monads.Error_Monad"
Presenting theory "Call_Arity.BalancedTraces"
Presenting theory "Certification_Monads.Error_Monad"
Presenting theory "Types_To_Sets_Extension.ETTS_Tools"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Library.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Term.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Logic.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Tactical.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Simplifier.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_HOLogic.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Tools/More_Transfer.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Tools/ETTS_Writer.ML"
Presenting theory "Dependent_SIFUM_Type_Systems.Security"
Presenting theory "Call_Arity.SestoftConf"
Presenting theory "Certification_Monads.Check_Monad"
Presenting theory "Deriving.Generator_Aux"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
Presenting theory "HOL-Types_To_Sets.Types_To_Sets"
Presenting file "~~/src/HOL/Types_To_Sets/local_typedef.ML"
Presenting file "~~/src/HOL/Types_To_Sets/unoverloading.ML"
Presenting file "~~/src/HOL/Types_To_Sets/internalize_sort.ML"
Presenting file "~~/src/HOL/Types_To_Sets/unoverload_type.ML"
Presenting file "~~/src/HOL/Types_To_Sets/unoverload_def.ML"
Presenting theory "HOL-Library.AList"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "Call_Arity.Sestoft"
Presenting theory "Launchbury.AList-Utils"
Presenting theory "FinFun.FinFun"
Presenting theory "Partial_Function_MR.Partial_Function_MR"
Presenting file "$AFP/Partial_Function_MR/partial_function_mr.ML"
Presenting theory "Launchbury.HOLCF-Join"
Presenting theory "Call_Arity.SestoftCorrect"
Presenting theory "FinFun.FinFun"
Presenting theory "Call_Arity.Arity"
Presenting theory "Call_Arity.AEnv"
Presenting theory "Call_Arity.Arity-Nominal"
Presenting theory "Launchbury.HOLCF-Join-Classes"
Presenting theory "Call_Arity.ArityAnalysisSig"
Presenting theory "Launchbury.Env"
Presenting theory "Certification_Monads.Strict_Sum"
Presenting theory "Call_Arity.ArityAnalysisAbinds"
Presenting theory "Call_Arity.ArityAnalysisSpec"
Presenting theory "Dependent_SIFUM_Refinement.CompositionalRefinement"
Presenting theory "Call_Arity.TrivialArityAnal"
Presenting theory "Call_Arity.Cardinality-Domain"
Presenting theory "Call_Arity.CardinalityAnalysisSig"
Presenting theory "Call_Arity.ConstOn"
Presenting theory "Dependent_SIFUM_Refinement.Eg1"
Presenting theory "Call_Arity.CardinalityAnalysisSpec"
Presenting theory "Call_Arity.ArityAnalysisStack"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "Dependent_SIFUM_Refinement.Eg1RefinementTrivial"
Presenting theory "Dependent_SIFUM_Refinement.Eg2"
Presenting theory "Show.Show"
Presenting file "$AFP/Show/show_generator.ML"
Presenting theory "Dependent_SIFUM_Refinement.Eg1Eg2"
Presenting theory "Call_Arity.NoCardinalityAnalysis"
Presenting theory "Deriving.Generator_Aux"
Presenting theory "HOL-Library.Cancellation"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
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 "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "Call_Arity.TransformTools"
Presenting theory "Call_Arity.AbstractTransform"
Presenting theory "Certification_Monads.Parser_Monad"
Presenting theory "Dependent_SIFUM_Refinement.Eg1Eg2RefinementSimple"
Presenting theory "Call_Arity.EtaExpansion"
Presenting theory "Show.Show"
Presenting file "$AFP/Show/show_generator.ML"
Presenting theory "Call_Arity.EtaExpansionSafe"
Presenting theory "Call_Arity.ArityStack"
Presenting theory "Call_Arity.ArityEtaExpansion"
Presenting theory "Call_Arity.ArityEtaExpansionSafe"
Presenting theory "Call_Arity.ArityTransform"
Presenting theory "Certification_Monads.Parser_Monad"
Presenting theory "Certification_Monads.Misc"
Presenting theory "XML.Xml"
Presenting theory "Dependent_SIFUM_Type_Systems.Compositionality"
Presenting theory "Nominal2.Nominal2_Base"
Presenting file "$AFP/Nominal2/nominal_basics.ML"
Presenting file "$AFP/Nominal2/nominal_thmdecls.ML"
Presenting file "$AFP/Nominal2/nominal_permeq.ML"
Presenting file "$AFP/Nominal2/nominal_library.ML"
Presenting file "$AFP/Nominal2/nominal_atoms.ML"
Presenting file "$AFP/Nominal2/nominal_eqvt.ML"
Presenting theory "Nominal2.Nominal2_Base"
Presenting theory "Call_Arity.ArityConsistent"
Presenting theory "Partial_Function_MR.Partial_Function_MR"
Presenting file "$AFP/Partial_Function_MR/partial_function_mr.ML"
Presenting file "$AFP/Nominal2/nominal_basics.ML"
Presenting file "$AFP/Nominal2/nominal_thmdecls.ML"
Presenting file "$AFP/Nominal2/nominal_permeq.ML"
Presenting file "$AFP/Nominal2/nominal_library.ML"
Presenting file "$AFP/Nominal2/nominal_atoms.ML"
Presenting file "$AFP/Nominal2/nominal_eqvt.ML"
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 "Dependent_SIFUM_Type_Systems.Language"
Presenting theory "Certification_Monads.Strict_Sum"
Presenting theory "Call_Arity.ArityTransformSafe"
Presenting theory "Call_Arity.Set-Cpo"
Presenting theory "Call_Arity.Env-Set-Cpo"
Presenting theory "Call_Arity.CoCallGraph"
Presenting theory "Nominal2.Nominal2_Abs"
Presenting theory "Call_Arity.CoCallAnalysisSig"
Presenting theory "Call_Arity.AList-Utils-HOLCF"
Presenting theory "Call_Arity.CoCallGraph-Nominal"
Presenting theory "XML.Xmlt"
Presenting Isabelle_C in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Isabelle_C" ...
Presenting document Isabelle_C/document
Presenting document Isabelle_C/outline
Presenting theory "Call_Arity.CoCallAnalysisBinds"
Presenting theory "Nominal2.Nominal2_Abs"
Presenting theory "Call_Arity.ArityAnalysisFix"
Presenting theory "Nominal2.Nominal2_FCB"
Presenting theory "HOL-ex.Cartouche_Examples"
Presenting theory "Nominal2.Nominal2_FCB"
Presenting theory "HOL-Library.Multiset"
Presenting theory "Call_Arity.CoCallFix"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "Call_Arity.CoCallAnalysisImpl"
Presenting theory "Call_Arity.CallArityEnd2End"
Presenting theory "Isabelle_C.C_Lexer_Language"
Presenting theory "Dependent_SIFUM_Refinement.EgHighBranchRevC"
Presenting theory "Call_Arity.SestoftGC"
Presenting theory "HOL-Library.FSet"
Presenting Nominal2 in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Nominal2" ...
Presenting document Nominal2/document
Presenting document Nominal2/outline
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "HOL-Library.Infinite_Set"
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 "HOL-Library.Cardinality"
Presenting theory "Call_Arity.CardArityTransformSafe"
Presenting theory "Call_Arity.CoCallAritySig"
Presenting theory "Call_Arity.CoCallAnalysisSpec"
Presenting theory "Call_Arity.ArityAnalysisFixProps"
Presenting theory "Call_Arity.CoCallImplSafe"
Presenting theory "Types_To_Sets_Extension.ETTS"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Tactics.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Utilities.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_RI.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Substitution.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Context.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Algorithm.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Active.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Lemma.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/ETTS_Lemmas.ML"
Presenting theory "FinFun.FinFun"
Presenting theory "Call_Arity.List-Interleavings"
Presenting theory "Types_To_Sets_Extension.ETTS_Auxiliary"
Presenting theory "HOL-Library.Multiset"
Presenting theory "Types_To_Sets_Extension.Manual_Prerequisites"
Presenting file "~~/src/Doc/antiquote_setup.ML"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Library.FSet"
Presenting theory "Dependent_SIFUM_Type_Systems.TypeSystem"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "Types_To_Sets_Extension.ETTS_Tests"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_AMEND_CTXT_DATA.ML"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_ALGORITHM.ML"
Presenting theory "Call_Arity.TTree"
Presenting file "$AFP/Types_To_Sets_Extension/ETTS/Tests/ETTS_TEST_TTS_REGISTER_SBTS.ML"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "Types_To_Sets_Extension.ETTS_Introduction"
Presenting theory "Types_To_Sets_Extension.ETTS_Theory"
Presenting theory "Types_To_Sets_Extension.ETTS_Syntax"
Presenting theory "Types_To_Sets_Extension.ETTS_Examples"
Presenting theory "Types_To_Sets_Extension.ETTS_CR"
Presenting theory "Types_To_Sets_Extension.Introduction"
Presenting theory "Types_To_Sets_Extension.SML_Introduction"
Presenting theory "Call_Arity.TTree-HOLCF"
Presenting theory "Types_To_Sets_Extension.Set_Ext"
Presenting theory "Call_Arity.AnalBinds"
Presenting theory "Call_Arity.TTreeAnalysisSig"
Presenting theory "Dependent_SIFUM_Type_Systems.LocallySoundModeUse"
Presenting theory "Types_To_Sets_Extension.Lifting_Set_Ext"
Presenting theory "Types_To_Sets_Extension.Product_Type_Ext"
Presenting theory "Nominal2.Nominal2"
Presenting file "$AFP/Nominal2/nominal_dt_data.ML"
Presenting file "$AFP/Nominal2/nominal_dt_rawfuns.ML"
Presenting file "$AFP/Nominal2/nominal_dt_alpha.ML"
Presenting file "$AFP/Nominal2/nominal_dt_quot.ML"
Presenting file "$AFP/Nominal2/nominal_induct.ML"
Presenting file "$AFP/Nominal2/nominal_inductive.ML"
Presenting file "$AFP/Nominal2/nominal_function_common.ML"
Presenting file "$AFP/Nominal2/nominal_function_core.ML"
Presenting file "$AFP/Nominal2/nominal_mutual.ML"
Presenting file "$AFP/Nominal2/nominal_function.ML"
Presenting file "$AFP/Nominal2/nominal_termination.ML"
Presenting theory "Types_To_Sets_Extension.Transfer_Ext"
Presenting theory "FinFun.FinFun"
Presenting theory "MiniSail.Nominal-Utils"
Presenting theory "Call_Arity.CoCallGraph-TTree"
Presenting theory "Types_To_Sets_Extension.SML_Relations"
Presenting theory "Call_Arity.CoCallImplTTree"
Presenting theory "Dependent_SIFUM_Type_Systems.Example"
Presenting theory "Call_Arity.Cardinality-Domain-Lists"
Presenting theory "Call_Arity.TTreeAnalysisSpec"
Presenting theory "Nominal2.Nominal2_Base"
Presenting theory "MiniSail.Syntax"
Presenting file "$AFP/Nominal2/nominal_basics.ML"
Presenting file "$AFP/Nominal2/nominal_thmdecls.ML"
Presenting file "$AFP/Nominal2/nominal_permeq.ML"
Presenting file "$AFP/Nominal2/nominal_library.ML"
Presenting file "$AFP/Nominal2/nominal_atoms.ML"
Presenting file "$AFP/Nominal2/nominal_eqvt.ML"
Presenting theory "HOL-Library.Quotient_Syntax"
Presenting theory "HOL-Library.Quotient_Set"
Presenting theory "Types_To_Sets_Extension.SML_Simple_Orders"
Presenting theory "Call_Arity.CoCallImplTTreeSafe"
Presenting theory "HOL-Library.Quotient_Product"
Presenting theory "Call_Arity.TTreeImplCardinality"
Presenting theory "HOL-Library.Quotient_Option"
Presenting theory "Types_To_Sets_Extension.SML_Semigroups"
Presenting theory "HOL-Library.Quotient_List"
Presenting theory "Types_To_Sets_Extension.SML_Monoids"
Presenting theory "Types_To_Sets_Extension.SML_Groups"
Presenting theory "MiniSail.IVSubst"
Presenting theory "Call_Arity.TTreeImplCardinalitySafe"
Presenting theory "Call_Arity.CallArityEnd2EndSafe"
Presenting theory "Types_To_Sets_Extension.SML_Semirings"
Presenting theory "Types_To_Sets_Extension.SML_Rings"
Presenting theory "MiniSail.BTVSubst"
Presenting theory "Types_To_Sets_Extension.SML_Semilattices"
Presenting theory "Call_Arity.ArityAnalysisCorrDenotational"
Presenting LambdaAuth in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/LambdaAuth" ...
Presenting document LambdaAuth/document
Presenting document LambdaAuth/outline
Presenting theory "LambdaAuth.Nominal2_Lemmas"
Presenting theory "Nominal2.Nominal2_Abs"
Presenting theory "Types_To_Sets_Extension.SML_Lattices"
Presenting theory "Nominal2.Nominal2_FCB"
Presenting theory "MiniSail.Wellformed"
Presenting theory "HOL-Library.AList"
Presenting theory "Nominal2.Nominal2"
Presenting file "$AFP/Nominal2/nominal_dt_data.ML"
Presenting file "$AFP/Nominal2/nominal_dt_rawfuns.ML"
Presenting file "$AFP/Nominal2/nominal_dt_alpha.ML"
Presenting file "$AFP/Nominal2/nominal_dt_quot.ML"
Presenting file "$AFP/Nominal2/nominal_induct.ML"
Presenting file "$AFP/Nominal2/nominal_inductive.ML"
Presenting file "$AFP/Nominal2/nominal_function_common.ML"
Presenting file "$AFP/Nominal2/nominal_function_core.ML"
Presenting file "$AFP/Nominal2/nominal_mutual.ML"
Presenting file "$AFP/Nominal2/nominal_function.ML"
Presenting theory "MiniSail.RCLogic"
Presenting file "$AFP/Nominal2/nominal_termination.ML"
Presenting theory "MiniSail.SyntaxL"
Presenting theory "HOL-Eisbach.Eisbach"
Presenting theory "Types_To_Sets_Extension.SML_Complete_Lattices"
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 "Nominal2.Nominal2_Base"
Presenting theory "HOL-Library.Conditional_Parametricity"
Presenting file "~~/src/HOL/Library/conditional_parametricity.ML"
Presenting theory "Dependent_SIFUM_Type_Systems.TypeSystemTactics"
Presenting file "$AFP/Nominal2/nominal_basics.ML"
Presenting file "$AFP/Nominal2/nominal_thmdecls.ML"
Presenting file "$AFP/Nominal2/nominal_permeq.ML"
Presenting file "$AFP/Nominal2/nominal_library.ML"
Presenting file "$AFP/Nominal2/nominal_atoms.ML"
Presenting file "$AFP/Nominal2/nominal_eqvt.ML"
Presenting theory "HOL-Library.Quotient_Syntax"
Presenting theory "HOL-Library.Quotient_Set"
Presenting theory "Types_To_Sets_Extension.SML_Linorders"
Presenting theory "Dependent_SIFUM_Type_Systems.Example_TypeSystem"
Presenting theory "HOL-Library.Quotient_Product"
Presenting theory "HOL-Library.Quotient_Option"
Presenting theory "Dependent_SIFUM_Type_Systems.Example_Swap_Add"
Presenting Modal_Logics_for_NTS in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Modal_Logics_for_NTS" ...
Presenting document Modal_Logics_for_NTS/document
Presenting document Modal_Logics_for_NTS/outline
Presenting theory "HOL-Library.Quotient_List"
Presenting theory "HOL-Cardinals.Fun_More"
Presenting theory "Incompleteness.SyntaxN"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "HOL-Library.Finite_Map"
Presenting theory "HOL-Cardinals.Order_Relation_More"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "HOL-Cardinals.Wellfounded_More"
Presenting theory "LambdaAuth.FMap_Lemmas"
Presenting theory "LambdaAuth.Syntax"
Presenting theory "Incompleteness.Coding"
Presenting theory "HOL-Cardinals.Wellorder_Relation"
Presenting theory "HOL-Cardinals.Wellorder_Embedding"
Presenting theory "Nominal2.Nominal2_Abs"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Cardinals.Order_Union"
Presenting theory "LambdaAuth.Semantics"
Presenting theory "Incompleteness.Predicates"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "Nominal2.Nominal2_FCB"
Presenting theory "LambdaAuth.Agreement"
Presenting theory "HOL-Cardinals.Wellorder_Constructions"
Presenting theory "Incompleteness.Sigma"
Presenting theory "MiniSail.WellformedL"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "LambdaAuth.Results"
Presenting Rewriting_Z in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Rewriting_Z" ...
Presenting document Rewriting_Z/document
Presenting document Rewriting_Z/outline
Presenting theory "HOL-Library.Set_Idioms"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "MiniSail.Typing"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "MiniSail.Operational"
Presenting theory "Incompleteness.Coding_Predicates"
Presenting theory "HOL-Library.While_Combinator"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "HOL-Library.FuncSet"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Incompleteness.Pf_Predicates"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "HOL-Cardinals.Ordinal_Arithmetic"
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 "MiniSail.SubstMethods"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "HOL-Library.Disjoint_Sets"
Presenting theory "HOL-Library.Product_Plus"
Presenting theory "Incompleteness.Functions"
Presenting theory "HOL-Cardinals.Cardinal_Order_Relation"
Presenting theory "Nominal2.Nominal2"
Presenting file "$AFP/Nominal2/nominal_dt_data.ML"
Presenting file "$AFP/Nominal2/nominal_dt_rawfuns.ML"
Presenting file "$AFP/Nominal2/nominal_dt_alpha.ML"
Presenting file "$AFP/Nominal2/nominal_dt_quot.ML"
Presenting file "$AFP/Nominal2/nominal_induct.ML"
Presenting file "$AFP/Nominal2/nominal_inductive.ML"
Presenting file "$AFP/Nominal2/nominal_function_common.ML"
Presenting file "$AFP/Nominal2/nominal_function_core.ML"
Presenting file "$AFP/Nominal2/nominal_mutual.ML"
Presenting file "$AFP/Nominal2/nominal_function.ML"
Presenting file "$AFP/Nominal2/nominal_termination.ML"
Presenting theory "Launchbury.Pointwise"
Presenting theory "Incompleteness.Goedel_I"
Presenting theory "HOL-Analysis.Product_Vector"
Presenting theory "Launchbury.HOLCF-Utils"
Presenting theory "Launchbury.EvalHeap"
Presenting theory "HOL-Cardinals.Cardinal_Arithmetic"
Presenting theory "Launchbury.Nominal-Utils"
Presenting theory "Launchbury.AList-Utils-Nominal"
Presenting theory "HOL-Cardinals.Wellorder_Extension"
Presenting theory "MiniSail.RCLogicL"
Presenting theory "HOL-Cardinals.Cardinals"
Presenting theory "Launchbury.Nominal-HOLCF"
Presenting theory "Launchbury.Env-HOLCF"
Presenting theory "Launchbury.HasESem"
Presenting theory "Launchbury.Iterative"
Presenting theory "Launchbury.Env-Nominal"
Presenting theory "HOL-Cardinals.Bounded_Set"
Presenting theory "Modal_Logics_for_NTS.Nominal_Bounded_Set"
Presenting theory "Modal_Logics_for_NTS.Nominal_Wellfounded"
Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
Presenting theory "Modal_Logics_for_NTS.Residual"
Presenting theory "Launchbury.HeapSemantics"
Presenting theory "Rewriting_Z.Z"
Presenting theory "Launchbury.Vars"
Presenting theory "Modal_Logics_for_NTS.Transition_System"
Presenting theory "Launchbury.Terms"
Presenting theory "Launchbury.AbstractDenotational"
Presenting theory "Launchbury.Substitution"
Presenting theory "Launchbury.Abstract-Denotational-Props"
Presenting theory "Launchbury.Value"
Presenting theory "Modal_Logics_for_NTS.Formula"
Presenting theory "Launchbury.Value-Nominal"
Presenting theory "Launchbury.Denotational"
Presenting theory "Modal_Logics_for_NTS.Validity"
Presenting theory "Modal_Logics_for_NTS.Logical_Equivalence"
Presenting theory "Modal_Logics_for_NTS.Bisimilarity_Implies_Equivalence"
Presenting theory "Modal_Logics_for_NTS.Equivalence_Implies_Bisimilarity"
Presenting theory "Modal_Logics_for_NTS.Disjunction"
Presenting theory "Launchbury.Launchbury"
Presenting theory "Nominal2.Nominal2"
Presenting file "$AFP/Nominal2/nominal_dt_data.ML"
Presenting file "$AFP/Nominal2/nominal_dt_rawfuns.ML"
Presenting file "$AFP/Nominal2/nominal_dt_alpha.ML"
Presenting file "$AFP/Nominal2/nominal_dt_quot.ML"
Presenting file "$AFP/Nominal2/nominal_induct.ML"
Presenting file "$AFP/Nominal2/nominal_inductive.ML"
Presenting theory "Modal_Logics_for_NTS.Expressive_Completeness"
Presenting file "$AFP/Nominal2/nominal_function_common.ML"
Presenting file "$AFP/Nominal2/nominal_function_core.ML"
Presenting file "$AFP/Nominal2/nominal_mutual.ML"
Presenting theory "Modal_Logics_for_NTS.FS_Set"
Presenting file "$AFP/Nominal2/nominal_function.ML"
Presenting theory "HOL-Analysis.Elementary_Topology"
Presenting file "$AFP/Nominal2/nominal_termination.ML"
Presenting theory "Nominal2.Atoms"
Presenting theory "Launchbury.CorrectnessOriginal"
Presenting theory "Launchbury.Mono-Nat-Fun"
Presenting theory "Nominal2.Eqvt"
Presenting theory "Launchbury.C"
Presenting Partial_Function_MR in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Partial_Function_MR" ...
Presenting document Partial_Function_MR/document
Presenting document Partial_Function_MR/outline
Presenting theory "Modal_Logics_for_NTS.FL_Transition_System"
Presenting theory "Launchbury.CValue"
Presenting theory "Launchbury.CValue-Nominal"
Presenting theory "Incompleteness.II_Prelims"
Presenting theory "Launchbury.HOLCF-Meet"
Presenting theory "Launchbury.C-Meet"
Presenting theory "Partial_Function_MR.Partial_Function_MR"
Presenting file "$AFP/Partial_Function_MR/partial_function_mr.ML"
Presenting theory "HOL-Library.Adhoc_Overloading"
Presenting file "~~/src/HOL/Library/adhoc_overloading.ML"
Presenting theory "Launchbury.C-restr"
Presenting theory "HOL-Library.Monad_Syntax"
Presenting theory "Incompleteness.Pseudo_Coding"
Presenting theory "Launchbury.ResourcedDenotational"
Presenting theory "Partial_Function_MR.Partial_Function_MR_Examples"
Presenting Goedel_HFSet_Semantic in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Goedel_HFSet_Semantic" ...
Presenting document Goedel_HFSet_Semantic/document
Presenting document Goedel_HFSet_Semantic/outline
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 "Rewriting_Z.Lambda_Z"
Presenting theory "Launchbury.CorrectnessResourced"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "Rewriting_Z.CL_Z"
Presenting Goedel_HFSet_Semanticless in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Goedel_HFSet_Semanticless" ...
Presenting document Goedel_HFSet_Semanticless/document
Presenting document Goedel_HFSet_Semanticless/outline
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 "Launchbury.ResourcedAdequacy"
Presenting theory "Types_To_Sets_Extension.SML_Topological_Space"
Presenting theory "Types_To_Sets_Extension.SML_Topological_Space_Countability"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "Launchbury.ValueSimilarity"
Presenting theory "Launchbury.Denotational-Related"
Presenting theory "HOL-Library.Cancellation"
Presenting file "~~/src/HOL/Library/Cancellation/cancel.ML"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_data.ML"
Presenting theory "Launchbury.Adequacy"
Presenting file "~~/src/HOL/Library/Cancellation/cancel_simprocs.ML"
Presenting theory "Types_To_Sets_Extension.SML_Ordered_Topological_Spaces"
Presenting theory "HOL-Library.LaTeXsugar"
Presenting theory "Launchbury.EverythingAdequacy"
Presenting Robinson_Arithmetic in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Robinson_Arithmetic" ...
Presenting document Robinson_Arithmetic/document
Presenting document Robinson_Arithmetic/outline
Presenting theory "Incompleteness.Quote"
Presenting theory "Types_To_Sets_Extension.SML_Product_Topology"
Presenting theory "Types_To_Sets_Extension.SML_Conclusions"
Presenting theory "Incompleteness.Goedel_II"
Presenting theory "Types_To_Sets_Extension.VS_Prerequisites"
Presenting theory "MiniSail.TypingL"
Presenting theory "HOL-Library.Infinite_Set"
Presenting theory "HOL-Library.Multiset"
Presenting theory "Modal_Logics_for_NTS.FL_Formula"
Presenting theory "Types_To_Sets_Extension.VS_Groups"
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 file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "Modal_Logics_for_NTS.FL_Validity"
Presenting theory "Modal_Logics_for_NTS.FL_Logical_Equivalence"
Presenting theory "Modal_Logics_for_NTS.FL_Bisimilarity_Implies_Equivalence"
Presenting theory "Types_To_Sets_Extension.VS_Modules"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "Modal_Logics_for_NTS.FL_Equivalence_Implies_Bisimilarity"
Presenting theory "HOL-Library.FSet"
Presenting theory "HOL-Library.Multiset"
Presenting theory "HOL-Library.Phantom_Type"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "HOL-Library.Multiset"
Presenting theory "Modal_Logics_for_NTS.L_Transform"
Presenting file "~~/src/HOL/Library/multiset_simprocs.ML"
Presenting theory "Types_To_Sets_Extension.VS_Vector_Spaces"
Presenting theory "Types_To_Sets_Extension.VS_Conclusions"
Presenting theory "Types_To_Sets_Extension.FNDS_Introduction"
Presenting theory "Types_To_Sets_Extension.FNDS_Set_Ext"
Presenting theory "MiniSail.ContextSubtypingL"
Presenting theory "Modal_Logics_for_NTS.Weak_Transition_System"
Presenting theory "Types_To_Sets_Extension.FNDS_Definite_Description"
Presenting theory "Types_To_Sets_Extension.FNDS_Auxiliary"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "Modal_Logics_for_NTS.Weak_Formula"
Presenting theory "Types_To_Sets_Extension.Type_Simple_Orders"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "Modal_Logics_for_NTS.Weak_Validity"
Presenting theory "Modal_Logics_for_NTS.Weak_Logical_Equivalence"
Presenting theory "Modal_Logics_for_NTS.Weak_Bisimilarity_Implies_Equivalence"
Presenting theory "HOL-Library.Old_Datatype"
Presenting file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
Presenting theory "FinFun.FinFun"
Presenting theory "Types_To_Sets_Extension.Set_Simple_Orders"
Presenting theory "Modal_Logics_for_NTS.Weak_Equivalence_Implies_Bisimilarity"
Presenting theory "HOL-Library.Nat_Bijection"
Presenting theory "Types_To_Sets_Extension.Type_Semigroups"
Presenting theory "Types_To_Sets_Extension.FNDS_Lifting_Set_Ext"
Presenting theory "Types_To_Sets_Extension.Set_Semigroups"
Presenting theory "Types_To_Sets_Extension.FNDS_Conclusions"
Presenting theory "HOL-Library.FSet"
Presenting theory "Modal_Logics_for_NTS.Weak_Expressive_Completeness"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "HOL-Library.Countable"
Presenting file "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "Modal_Logics_for_NTS.S_Transform"
Presenting theory "HOL-Library.FSet"
Presenting theory "HOL-Library.Phantom_Type"
Presenting theory "FinFun.FinFun"
Presenting theory "HOL-Library.Cardinality"
Presenting theory "Nominal2.Nominal2_Base"
Presenting file "$AFP/Nominal2/nominal_basics.ML"
Presenting file "$AFP/Nominal2/nominal_thmdecls.ML"
Presenting file "$AFP/Nominal2/nominal_permeq.ML"
Presenting file "$AFP/Nominal2/nominal_library.ML"
Presenting file "$AFP/Nominal2/nominal_atoms.ML"
Presenting file "$AFP/Nominal2/nominal_eqvt.ML"
Presenting theory "HOL-Library.Quotient_Syntax"
Presenting theory "HOL-Library.Quotient_Set"
Presenting theory "HOL-Library.Quotient_Product"
Presenting theory "HOL-Library.Quotient_Option"
Presenting theory "HOL-Library.Quotient_List"
Presenting theory "FinFun.FinFun"
Presenting theory "MiniSail.IVSubstTypingL"
Presenting theory "Nominal2.Nominal2_Abs"
Presenting theory "Nominal2.Nominal2_Base"
Presenting theory "Nominal2.Nominal2_FCB"
Presenting file "$AFP/Nominal2/nominal_basics.ML"
Presenting file "$AFP/Nominal2/nominal_thmdecls.ML"
Presenting file "$AFP/Nominal2/nominal_permeq.ML"
Presenting file "$AFP/Nominal2/nominal_library.ML"
Presenting file "$AFP/Nominal2/nominal_atoms.ML"
Presenting file "$AFP/Nominal2/nominal_eqvt.ML"
Presenting theory "HOL-Library.Quotient_Syntax"
Presenting theory "HOL-Library.Quotient_Set"
Presenting theory "HOL-Library.Quotient_Product"
Presenting theory "HOL-Library.Quotient_Option"
Presenting theory "MiniSail.BTVSubstTypingL"
Presenting theory "HOL-Library.Quotient_List"
Presenting theory "Nominal2.Nominal2_Abs"
Presenting theory "Nominal2.Nominal2_Base"
Presenting theory "Nominal2.Nominal2_FCB"
Presenting file "$AFP/Nominal2/nominal_basics.ML"
Presenting file "$AFP/Nominal2/nominal_thmdecls.ML"
Presenting file "$AFP/Nominal2/nominal_permeq.ML"
Presenting file "$AFP/Nominal2/nominal_library.ML"
Presenting file "$AFP/Nominal2/nominal_atoms.ML"
Presenting file "$AFP/Nominal2/nominal_eqvt.ML"
Presenting theory "HOL-Library.Quotient_Syntax"
Presenting theory "HOL-Library.Quotient_Set"
Presenting theory "HOL-Library.Quotient_Product"
Presenting theory "HOL-Library.Quotient_Option"
Presenting theory "HOL-Library.Quotient_List"
Presenting theory "Nominal2.Nominal2_Abs"
Presenting theory "Nominal2.Nominal2_FCB"
Presenting theory "MiniSail.Safety"
Presenting theory "MiniSail.MiniSail"
Presenting theory "Nominal2.Nominal2"
Presenting file "$AFP/Nominal2/nominal_dt_data.ML"
Presenting file "$AFP/Nominal2/nominal_dt_rawfuns.ML"
Presenting file "$AFP/Nominal2/nominal_dt_alpha.ML"
Presenting file "$AFP/Nominal2/nominal_dt_quot.ML"
Presenting file "$AFP/Nominal2/nominal_induct.ML"
Presenting file "$AFP/Nominal2/nominal_inductive.ML"
Presenting file "$AFP/Nominal2/nominal_function_common.ML"
Presenting file "$AFP/Nominal2/nominal_function_core.ML"
Presenting file "$AFP/Nominal2/nominal_mutual.ML"
Presenting file "$AFP/Nominal2/nominal_function.ML"
Presenting file "$AFP/Nominal2/nominal_termination.ML"
Presenting theory "HereditarilyFinite.HF"
Presenting theory "HereditarilyFinite.Ordinal"
Presenting theory "Isabelle_C.C_Ast"
Presenting theory "HereditarilyFinite.Rank"
Presenting theory "HereditarilyFinite.OrdArith"
Presenting theory "Nominal2.Nominal2"
Presenting file "$AFP/Nominal2/nominal_dt_data.ML"
Presenting file "$AFP/Nominal2/nominal_dt_rawfuns.ML"
Presenting file "$AFP/Nominal2/nominal_dt_alpha.ML"
Presenting file "$AFP/Nominal2/nominal_dt_quot.ML"
Presenting file "$AFP/Nominal2/nominal_induct.ML"
Presenting file "$AFP/Nominal2/nominal_inductive.ML"
Presenting file "$AFP/Nominal2/nominal_function_common.ML"
Presenting file "$AFP/Nominal2/nominal_function_core.ML"
Presenting file "$AFP/Nominal2/nominal_mutual.ML"
Presenting file "$AFP/Nominal2/nominal_function.ML"
Presenting file "$AFP/Nominal2/nominal_termination.ML"
Presenting file "$AFP/Isabelle_C/C11-FrontEnd/generated/c_ast.ML"
Presenting theory "Incompleteness.SyntaxN"
Presenting theory "Robinson_Arithmetic.Robinson_Arithmetic"
Presenting theory "Nominal2.Nominal2"
Presenting file "$AFP/Nominal2/nominal_dt_data.ML"
Presenting file "$AFP/Nominal2/nominal_dt_rawfuns.ML"
Presenting file "$AFP/Nominal2/nominal_dt_alpha.ML"
Presenting theory "Incompleteness.Coding"
Presenting file "$AFP/Nominal2/nominal_dt_quot.ML"
Presenting file "$AFP/Nominal2/nominal_induct.ML"
Presenting file "$AFP/Nominal2/nominal_inductive.ML"
Presenting file "$AFP/Nominal2/nominal_function_common.ML"
Presenting file "$AFP/Nominal2/nominal_function_core.ML"
Presenting theory "Robinson_Arithmetic.Instance"
Presenting file "$AFP/Nominal2/nominal_mutual.ML"
Presenting file "$AFP/Nominal2/nominal_function.ML"
Presenting file "$AFP/Nominal2/nominal_termination.ML"
Presenting theory "HereditarilyFinite.HF"
Presenting theory "Incompleteness.Predicates"
Presenting theory "HereditarilyFinite.Ordinal"
Presenting theory "HereditarilyFinite.Rank"
Presenting theory "HereditarilyFinite.OrdArith"
Presenting theory "Incompleteness.Sigma"
Presenting theory "Incompleteness.Coding_Predicates"
Presenting theory "Goedel_HFSet_Semanticless.SyntaxN"
Presenting theory "Isabelle_C.C_Environment"
Presenting theory "Goedel_HFSet_Semanticless.Coding"
Presenting theory "Incompleteness.Pf_Predicates"
Presenting theory "Goedel_HFSet_Semanticless.Predicates"
Presenting theory "Goedel_HFSet_Semanticless.Sigma"
Presenting theory "Goedel_HFSet_Semanticless.Coding_Predicates"
Presenting theory "Goedel_HFSet_Semanticless.Pf_Predicates"
Presenting theory "Incompleteness.II_Prelims"
Presenting theory "Incompleteness.Pseudo_Coding"
Presenting theory "Incompleteness.Quote"
Presenting theory "Incompleteness.Functions"
Presenting theory "Incompleteness.Goedel_I"
Presenting theory "Goedel_HFSet_Semanticless.II_Prelims"
Presenting theory "Goedel_HFSet_Semantic.Instance"
Presenting theory "Goedel_HFSet_Semanticless.Pseudo_Coding"
Presenting theory "Goedel_HFSet_Semanticless.Quote"
Presenting theory "Isabelle_C.C_Parser_Language"
Presenting theory "Goedel_HFSet_Semanticless.Functions"
Presenting file "$AFP/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/base.sig"
Presenting file "$AFP/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/join.sml"
Presenting file "$AFP/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/lrtable.sml"
Presenting file "$AFP/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/stream.sml"
Presenting file "$AFP/Isabelle_C/src_ext/mlton/lib/mlyacc-lib/parser1.sml"
Presenting file "$AFP/Isabelle_C/C11-FrontEnd/generated/c_grammar_fun.grm.sig"
Presenting theory "Goedel_HFSet_Semanticless.Goedel_I"
Presenting file "$AFP/Isabelle_C/C11-FrontEnd/generated/c_grammar_fun.grm.sml"
Presenting theory "Goedel_HFSet_Semanticless.Instance"
Presenting theory "Isabelle_C.C_Lexer_Annotation"
Presenting theory "Isabelle_C.C_Parser_Annotation"
Presenting theory "Isabelle_C.C_Eval"
Presenting theory "Isabelle_C.C_Command"
Presenting theory "Isabelle_C.C_Document"
Presenting theory "Isabelle_C.C_Main"
Presenting theory "Isabelle_C.C0"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/argument_scope.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/atomic_parenthesis.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/bitfield_declaration_ambiguity.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/bitfield_declaration_ambiguity.ok.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/block_scope.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/char-literal-printing.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/c-namespace.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/control-scope.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/dangling_else.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/declarators.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/designator.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/enum.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/enum_constant_visibility.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/enum_shadows_typedef.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/enum-trick.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/expressions.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/function-decls.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/local_scope.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/local_typedef.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/long-long-struct.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/namespaces.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/no_local_scope.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/parameter_declaration_ambiguity.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/parameter_declaration_ambiguity.test.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/statements.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/struct-recursion.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/typedef_star.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/types.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/variable_star.c"
Presenting file "$AFP/Isabelle_C/src_ext/parser_menhir/tests/bitfield_declaration_ambiguity.fail.c"
Presenting theory "Isabelle_C.C1"
Presenting theory "Isabelle_C.C2"
Presenting theory "Isabelle_C.C_paper"
Presenting theory "Isar_Ref.Base"
Presenting file "~~/src/Doc/antiquote_setup.ML"
Presenting theory "Isabelle_C.C_Appendices"
Presenting theory "Isabelle_C.README"

=== TIMING ===

Group AFP: 0:48:46 elapsed time, 3:08:36 cpu time, factor 3.87
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:16:26 elapsed time, 3:08:36 cpu time, factor 11.47

=== 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