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 41c92fcb8805d6284e514670d8d9bcf1c4a4a41b --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(41c92fcb8805d6284e514670d8d9bcf1c4a4a41b)" --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
1446 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 12867ed914b04c8252a649c295153ce0f7bf987f --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(12867ed914b04c8252a649c295153ce0f7bf987f)" --encoding UTF-8 --encodingmode replace
No emails were triggered.
[isabelle-all] $ /bin/sh -xe /tmp/jenkins379689937063665897.sh
+ Admin/jenkins/run_build all
+ set -e
+ PROFILE=all
+ shift
+ bin/isabelle components -a
+ bin/isabelle jedit -bf
### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle.jar) ...
### Building graph browser (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_graphbrowser.jar) ...
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-all/lib/classes/isabelle_admin.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
### Building AFP/Tools (/media/data/jenkins/workspace/isabelle-all/afp/admin/jenkins/../../tools/lib/classes/afp_tools.jar) ...
+ bin/isabelle ocaml_setup
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
       opam update

[NOTE] Package zarith is already installed (current version is 1.12).
+ bin/isabelle ghc_setup
stack will use a sandboxed GHC it installed
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
The Glorious Glasgow Haskell Compilation System, version 8.10.7
+ bin/isabelle ci_build all

=== CONFIGURATION ===

ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-linux"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-bafe319bc3a6-1/x86_64_32-linux"
ML_SYSTEM="polyml-5.9"
ML_OPTIONS="-H 4000 --maxheap 8G"
jobs = 8, threads = 8, numa = true

=== BUILD ===

Build started at Tue, 22 Nov 2022 20:03:27 +0100
Isabelle id 41c92fcb8805
AFP id da2bce68bc31

=== LOG ===

Session Pure/Pure
Session Misc/CTT
Session Misc/Cube
Session FOL/FOL
Session FOL/CCL
Session FOL/FOL-ex
Session FOL/FOLP
Session FOL/FOLP-ex
Session Doc/Intro (doc)
Session FOL/LCF
Session Doc/Logics (doc)
Session Doc/Nitpick (doc)
Session Pure/Pure-Examples
Session Pure/Pure-ex
Session Misc/SML
Session Misc/Sequents
Session Doc/Sledgehammer (doc)
Session AFP/SpecCheck (AFP)
Session Misc/Tools
Session HOL/HOL (main)
Session AFP/AVL-Trees (AFP)
Session AFP/AWN (AFP)
Session AFP/Abortable_Linearizable_Modules (AFP)
Session AFP/Abstract-Hoare-Logics (AFP)
Session AFP/Ackermanns_not_PR (AFP)
Session AFP/AnselmGod (AFP)
Session AFP/Aristotles_Assertoric_Syllogistic (AFP)
Session AFP/Attack_Trees (AFP)
Session AFP/AxiomaticCategoryTheory (AFP)
Session AFP/Belief_Revision (AFP)
Session AFP/BinarySearchTree (AFP)
Session AFP/Binomial-Queues (AFP)
Session AFP/Bondy (AFP)
Session AFP/Boolos_Curious_Inference (AFP)
Session AFP/BytecodeLogicJmlTypes (AFP)
Session AFP/C2KA_DistributedSystems (AFP)
Session AFP/CISC-Kernel (AFP)
Session AFP/CYK (AFP)
Session AFP/Cauchy (AFP)
Session AFP/Sqrt_Babylonian (AFP)
Session Doc/Classes (doc)
Session AFP/ClockSynchInst (AFP)
Session AFP/Compiling-Exceptions-Correctly (AFP)
Session AFP/Complete_Non_Orders (AFP)
Session AFP/ComponentDependencies (AFP)
Session AFP/Concurrent_Revisions (AFP)
Session AFP/Constructor_Funs (AFP)
Session AFP/CryptoBasedCompositionalProperties (AFP)
Session AFP/DPT-SAT-Solver (AFP)
Session AFP/Dedekind_Real (AFP)
Session Doc/Demo_EPTCS (doc)
Session Doc/Demo_Easychair (doc)
Session Doc/Demo_FoilTeX (doc)
Session Doc/Demo_LIPIcs (doc)
Session Doc/Demo_LLNCS (doc)
Session AFP/Depth-First-Search (AFP)
Session AFP/Digit_Expansions (AFP)
Session AFP/Diophantine_Eqns_Lin_Hom (AFP)
Session AFP/DiskPaxos (AFP)
Session AFP/Example-Submission (AFP)
Session AFP/FFT (AFP)
Session AFP/FLP (AFP)
Session AFP/FeatherweightJava (AFP)
Session AFP/Featherweight_OCL (AFP)
Session AFP/FileRefinement (AFP)
Session AFP/FocusStreamsCaseStudies (AFP)
Session AFP/Foundation_of_geometry (AFP)
Session AFP/Free-Boolean-Algebra (AFP)
Session AFP/Fresh_Identifiers (AFP)
Session AFP/FunWithFunctions (AFP)
Session AFP/FunWithTilings (AFP)
Session Doc/Functions (doc)
Session AFP/GPU_Kernel_PL (AFP)
Session AFP/GenClock (AFP)
Session AFP/General-Triangle (AFP)
Session AFP/Generic_Deriving (AFP)
Session AFP/GewirthPGCProof (AFP)
Session AFP/GoedelGod (AFP)
Session AFP/Goodstein_Lambda (AFP)
Session HOL/HOL-Cardinals (timing)
Session AFP/Binding_Syntax_Theory (AFP)
Session AFP/Ordinals_and_Cardinals (AFP)
Session AFP/Risk_Free_Lending (AFP)
Session HOL/HOL-Hoare
Session HOL/HOL-Hoare_Parallel (timing)
Session HOL/HOL-IMPP
Session HOL/HOL-IOA
Session HOL/HOL-Import
Session HOL/HOL-Lattice
Session HOL/HOL-Library (main timing)
Session AFP/ADS_Functor (AFP)
Session AFP/Approximation_Algorithms (AFP)
Session AFP/ArrowImpossibilityGS (AFP)
Session AFP/Auto2_HOL (AFP)
Session AFP/BNF_CC (AFP)
Session AFP/BNF_Operations (AFP)
Session AFP/Binomial-Heaps (AFP)
Session AFP/Boolean_Expression_Checkers (AFP)
Session AFP/Bounded_Deducibility_Security (AFP)
Session AFP/BD_Security_Compositional (AFP)
Session AFP/CoSMeDis (AFP)
Session AFP/CoCon (AFP)
Session AFP/CoSMed (AFP)
Session AFP/Buildings (AFP)
Session AFP/CRDT (AFP)
Session AFP/IMAP-CRDT (AFP)
Session AFP/Card_Multisets (AFP)
Session AFP/Card_Number_Partitions (AFP)
Session AFP/Category (AFP)
Session Doc/Codegen (doc)
Session AFP/CofGroups (AFP)
Session AFP/Completeness (AFP)
Session AFP/ConcurrentIMP (AFP)
Session AFP/Concurrent_Ref_Alg (AFP)
Session AFP/Conditional_Simplification (AFP)
Session AFP/Conditional_Transfer_Rule (AFP)
Session AFP/CoreC++ (AFP)
Session AFP/Core_DOM (AFP)
Session AFP/Shadow_DOM (AFP)
Session AFP/DOM_Components (AFP)
Session AFP/Core_SC_DOM (AFP)
Session AFP/Shadow_SC_DOM (AFP)
Session AFP/SC_DOM_Components (AFP)
Session Doc/Datatypes (doc)
Session Doc/Corec (doc)
Session AFP/Decl_Sem_Fun_PL (AFP)
Session AFP/Encodability_Process_Calculi (AFP)
Session AFP/Epistemic_Logic (AFP)
Session AFP/Public_Announcement_Logic (AFP)
Session AFP/Stalnaker_Logic (AFP)
Session AFP/Euler_Partition (AFP)
Session AFP/FOL-Fitting (AFP)
Session AFP/FOL_Seq_Calc1 (AFP)
Session AFP/FOL_Axiomatic (AFP)
Session AFP/FOL_Harrison (AFP)
Session AFP/Factored_Transition_System_Bounding (AFP)
Session AFP/FinFun (AFP)
Session AFP/Extended_Finite_State_Machines (AFP)
Session AFP/Extended_Finite_State_Machine_Inference (AFP)
Session AFP/Finger-Trees (AFP)
Session AFP/Finite-Map-Extras (AFP)
Session AFP/Generalized_Counting_Sort (AFP)
Session AFP/Graph_Saturation (AFP)
Session AFP/Group-Ring-Module (AFP)
Session AFP/Valuation (AFP)
Session HOL/HOL-Auth (timing)
Session HOL/HOL-UNITY (timing)
Session HOL/HOL-Bali (timing)
Session HOL/HOL-Combinatorics (main timing)
Session AFP/Blue_Eyes (AFP)
Session AFP/Derangements (AFP)
Session AFP/Discrete_Summation (AFP)
Session AFP/Gauss-Jordan-Elim-Fun (AFP)
Session AFP/Graph_Theory (AFP)
Session AFP/ShortestPath (AFP)
Session HOL/HOL-Computational_Algebra (main timing)
Session AFP/Descartes_Sign_Rule (AFP)
Session HOL/HOL-Algebra (main timing)
Session AFP/Finitely_Generated_Abelian_Groups (AFP)
Session HOL/HOL-Decision_Procs (timing)
Session HOL/HOL-Quotient_Examples (timing)
Session AFP/Interpolation_Polynomials_HOL_Algebra (AFP)
Session AFP/Localization_Ring (AFP)
Session AFP/Orbit_Stabiliser (AFP)
Session AFP/Perfect-Number-Thm (AFP)
Session AFP/Secondary_Sylow (AFP)
Session AFP/Jordan_Hoelder (AFP)
Session AFP/VectorSpace (AFP)
Session HOL/HOL-Analysis (main timing)
Session AFP/Actuarial_Mathematics (AFP)
Session AFP/Cayley_Hamilton (AFP)
Session AFP/Coinductive (AFP)
Session AFP/DynamicArchitectures (AFP)
Session AFP/Architectural_Design_Patterns (AFP)
Session AFP/Lazy-Lists-II (AFP)
Session AFP/Stream_Fusion_Code (AFP)
Session AFP/Topology (AFP)
Session AFP/Complex_Geometry (AFP)
Session AFP/Poincare_Disc (AFP)
Session AFP/Differential_Game_Logic (AFP)
Session AFP/First_Welfare_Theorem (AFP)
Session AFP/Green (AFP)
Session HOL/HOL-Analysis-ex
Session HOL/HOL-Complex_Analysis (main timing)
Session AFP/Cartan_FP (AFP)
Session HOL/HOL-Eisbach
Session AFP/Allen_Calculus (AFP)
Session AFP/Card_Partitions (AFP)
Session AFP/Bell_Numbers_Spivey (AFP)
Session AFP/Card_Equiv_Relations (AFP)
Session AFP/Equivalence_Relation_Enumeration (AFP)
Session AFP/Falling_Factorial_Sum (AFP)
Session AFP/Case_Labeling (AFP)
Session AFP/Clean (AFP)
Session AFP/Combinatorics_Words (AFP)
Session AFP/Combinatorics_Words_Graph_Lemma (AFP)
Session AFP/Dependent_SIFUM_Type_Systems (AFP)
Session AFP/Dependent_SIFUM_Refinement (AFP)
Session Doc/Eisbach (doc)
Session HOL/HOL-Hahn_Banach
Session HOL/HOL-Homology (timing)
Session HOL/HOL-Probability (main timing)
Session AFP/Buffons_Needle (AFP)
Session AFP/Density_Compiler (AFP)
Session AFP/DiscretePricing (AFP)
Session AFP/Ergodic_Theory (AFP)
Session AFP/Gromov_Hyperbolicity (AFP)
Session AFP/Laws_of_Large_Numbers (AFP)
Session AFP/Fisher_Yates (AFP)
Session AFP/Girth_Chromatic (AFP)
Session AFP/Random_Graph_Subgraph_Threshold (AFP)
Session HOL/HOL-Probability-ex (timing)
Session AFP/Hahn_Jordan_Decomposition (AFP)
Session AFP/Lp (AFP)
Session AFP/MDP-Rewards (AFP)
Session AFP/Markov_Models (AFP)
Session AFP/Monad_Normalisation (AFP)
Session AFP/Monomorphic_Monad (AFP)
Session AFP/Neumann_Morgenstern_Utility (AFP)
Session AFP/Probabilistic_Noninterference (AFP)
Session AFP/Probabilistic_System_Zoo (AFP)
Session AFP/Quasi_Borel_Spaces (AFP)
Session AFP/Skip_Lists (AFP)
Session AFP/Source_Coding_Theorem (AFP)
Session AFP/Hyperdual (AFP)
Session AFP/Irrationality_J_Hancl (AFP)
Session AFP/Kuratowski_Closure_Complement (AFP)
Session AFP/Laplace_Transform (AFP)
Session AFP/Lower_Semicontinuous (AFP)
Session AFP/Minkowskis_Theorem (AFP)
Session AFP/Octonions (AFP)
Session AFP/Ptolemys_Theorem (AFP)
Session AFP/Quaternions (AFP)
Session AFP/Rank_Nullity_Theorem (AFP)
Session AFP/Gauss_Jordan (AFP)
Session AFP/Echelon_Form (AFP)
Session AFP/Hermite (AFP)
Session AFP/MDP-Algorithms (AFP)
Session AFP/Tarskis_Geometry (AFP)
Session AFP/Triangle (AFP)
Session AFP/Chord_Segments (AFP)
Session AFP/Stewart_Apollonius (AFP)
Session AFP/Youngs_Inequality (AFP)
Session AFP/pGCL (AFP)
Session HOL/HOL-Examples
Session HOL/HOL-Isar_Examples
Session HOL/HOL-Nonstandard_Analysis (timing)
Session HOL/HOL-Nonstandard_Analysis-Examples (timing)
Session HOL/HOL-Number_Theory (main timing)
Session AFP/Arith_Prog_Rel_Primes (AFP)
Session AFP/Bernoulli (AFP)
Session AFP/E_Transcendental (AFP)
Session AFP/Elliptic_Curves_Group_Law (AFP)
Session AFP/Fermat3_4 (AFP)
Session HOL/HOL-Data_Structures (timing)
Session AFP/Efficient-Mergesort (AFP)
Session HOL/HOL-Codegenerator_Test
Session AFP/Query_Optimization (AFP)
Session HOL/HOL-ex (timing)
Session AFP/Automatic_Refinement (AFP)
Session AFP/Refine_Monadic (AFP)
Session AFP/Lehmer (AFP)
Session AFP/Lifting_the_Exponent (AFP)
Session AFP/Padic_Ints (AFP)
Session AFP/Padic_Field (AFP)
Session AFP/Pratt_Certificate (AFP)
Session AFP/Bertrands_Postulate (AFP)
Session AFP/Prime_Harmonic_Series (AFP)
Session AFP/RSAPSS (AFP)
Session AFP/SumSquares (AFP)
Session AFP/Liouville_Numbers (AFP)
Session AFP/Lucas_Theorem (AFP)
Session AFP/DPRM_Theorem (AFP)
Session AFP/Mason_Stothers (AFP)
Session AFP/Polynomial_Interpolation (AFP)
Session AFP/Formal_Puiseux_Series (AFP)
Session AFP/Probabilistic_Prime_Tests (AFP)
Session AFP/Rep_Fin_Groups (AFP)
Session AFP/Sturm_Sequences (AFP)
Session AFP/Safe_Distance (AFP)
Session AFP/Special_Function_Bounds (AFP)
Session AFP/Sturm_Tarski (AFP)
Session AFP/Budan_Fourier (AFP)
Session AFP/Three_Circles (AFP)
Session AFP/Winding_Number_Eval (AFP)
Session AFP/Count_Complex_Roots (AFP)
Session HOL/HOL-Corec_Examples (timing)
Session HOL/HOL-Datatype_Examples (timing)
Session HOL/HOL-IMP (timing)
Session AFP/Abs_Int_ITP2012 (AFP)
Session AFP/Relational-Incorrectness-Logic (AFP)
Session HOL/HOL-Imperative_HOL (timing)
Session AFP/Auto2_Imperative_HOL (AFP)
Session AFP/Imperative_Insertion_Sort (AFP)
Session HOL/HOL-Induct
Session HOL/HOL-Metis_Examples (timing)
Session HOL/HOL-Proofs (timing)
Session HOL/HOL-Proofs-Extraction (timing)
Session HOL/HOL-Proofs-ex
Session HOL/HOL-Proofs-Lambda (timing)
Session AFP/Applicative_Lifting (AFP)
Session AFP/Free-Groups (AFP)
Session AFP/Stern_Brocot (AFP)
Session AFP/HereditarilyFinite (AFP)
Session AFP/HyperCTL (AFP)
Session AFP/Integration (AFP)
Session AFP/Isabelle_Meta_Model (AFP)
Session AFP/LTL (AFP)
Session AFP/Stuttering_Equivalence (AFP)
Session AFP/Landau_Symbols (AFP)
Session AFP/Akra_Bazzi (AFP)
Session AFP/Catalan_Numbers (AFP)
Session AFP/Error_Function (AFP)
Session AFP/Euler_MacLaurin (AFP)
Session AFP/LightweightJava (AFP)
Session AFP/LinearQuantifierElim (AFP)
Session AFP/List-Infinite (AFP)
Session AFP/Nat-Interval-Logic (AFP)
Session AFP/AutoFocus-Stream (AFP)
Session AFP/Median_Method (AFP)
Session AFP/MuchAdoAboutTwo (AFP)
Session AFP/Optics (AFP)
Session AFP/UTP-Toolkit (AFP)
Session AFP/UTP (AFP)
Session AFP/Order_Lattice_Props (AFP)
Session AFP/POPLmark-deBruijn (AFP)
Session AFP/Pairing_Heap (AFP)
Session AFP/Password_Authentication_Protocol (AFP)
Session AFP/Pell (AFP)
Session AFP/Prefix_Free_Code_Combinators (AFP)
Session AFP/Presburger-Automata (AFP)
Session AFP/Priority_Queue_Braun (AFP)
Session AFP/Program-Conflict-Analysis (AFP)
Session AFP/Regular-Sets (AFP)
Session AFP/Abstract-Rewriting (AFP)
Session AFP/Decreasing-Diagrams (AFP)
Session AFP/First_Order_Terms (AFP)
Session AFP/Stateful_Protocol_Composition_and_Typing (AFP)
Session AFP/Automated_Stateful_Protocol_Verification (AFP)
Session AFP/Matrix (AFP)
Session AFP/Matrix_Tensor (AFP)
Session AFP/Knot_Theory (AFP)
Session AFP/Coinductive_Languages (AFP)
Session AFP/Finite_Automata_HF (AFP)
Session AFP/Functional-Automata (AFP)
Session AFP/Posix-Lexing (AFP)
Session AFP/ResiduatedTransitionSystem (AFP)
Session AFP/Ribbon_Proofs (AFP)
Session AFP/SATSolverVerification (AFP)
Session AFP/Safe_OCL (AFP)
Session AFP/Schutz_Spacetime (AFP)
Session AFP/Selection_Heap_Sort (AFP)
Session AFP/Simplex (AFP)
Session AFP/Skew_Heap (AFP)
Session AFP/Solidity (AFP)
Session AFP/Sort_Encodings (AFP)
Session AFP/Splay_Tree (AFP)
Session AFP/Amortized_Complexity (AFP)
Session AFP/Dynamic_Tables (AFP)
Session AFP/Root_Balanced_Tree (AFP)
Session AFP/Closest_Pair_Points (AFP)
Session AFP/Stable_Matching (AFP)
Session AFP/SuperCalc (AFP)
Session Doc/System (doc)
Session AFP/Szemeredi_Regularity (AFP)
Session AFP/Roth_Arithmetic_Progressions (AFP)
Session AFP/Tail_Recursive_Functions (AFP)
Session AFP/TortoiseHare (AFP)
Session AFP/Trie (AFP)
Session AFP/Flyspeck-Tame (AFP)
Session AFP/Twelvefold_Way (AFP)
Session AFP/Vickrey_Clarke_Groves (AFP)
Session HOL/HOL-Matrix_LP
Session HOL/HOL-MicroJava (timing)
Session HOL/HOL-Mirabelle-ex
Session HOL/HOL-Mutabelle
Session HOL/HOL-NanoJava
Session HOL/HOL-Nitpick_Examples
Session HOL/HOL-Nominal
Session AFP/CCS (AFP)
Session HOL/HOL-Nominal-Examples (timing)
Session AFP/Lam-ml-Normalization (AFP)
Session AFP/Pi_Calculus (AFP)
Session AFP/Psi_Calculi (AFP)
Session AFP/SequentInvertibility (AFP)
Session HOL/HOL-Predicate_Compile_Examples (timing)
Session HOL/HOL-Prolog
Session HOL/HOL-Quickcheck_Examples (timing)
Session HOL/HOL-Real_Asymp
Session AFP/Cotangent_PFD_Formula (AFP)
Session AFP/Fourier (AFP)
Session AFP/Furstenberg_Topology (AFP)
Session HOL/HOL-Real_Asymp-Manual
Session AFP/Sophomores_Dream (AFP)
Session AFP/Stirling_Formula (AFP)
Session AFP/Irrationals_From_THEBOOK (AFP)
Session AFP/Lambert_W (AFP)
Session HOL/HOL-SET_Protocol (timing)
Session HOL/HOL-SMT_Examples (timing)
Session HOL/HOL-SPARK
Session HOL/HOL-SPARK-Examples
Session AFP/RIPEMD-160-SPARK (AFP)
Session HOL/HOL-SPARK-Manual
Session HOL/HOL-Statespace
Session HOL/HOL-TLA
Session HOL/HOL-TLA-Buffer
Session HOL/HOL-TLA-Inc
Session HOL/HOL-TLA-Memory
Session HOL/HOL-TPTP
Session HOL/HOL-Types_To_Sets
Session AFP/Banach_Steinhaus (AFP)
Session AFP/Smooth_Manifolds (AFP)
Session AFP/Types_To_Sets_Extension (AFP)
Session HOL/HOL-Unix
Session HOL/HOL-ZF
Session AFP/Category2 (AFP)
Session HOL/HOLCF (main timing)
Session AFP/Circus (AFP)
Session AFP/HOL-CSP (AFP)
Session HOL/HOLCF-IMP
Session HOL/HOLCF-Library
Session AFP/CSP_RefTK (AFP)
Session HOL/HOLCF-FOCUS
Session HOL/HOLCF-ex
Session AFP/PCF (AFP)
Session AFP/HOLCF-Prelude (AFP)
Session AFP/BirdKMP (AFP)
Session HOL/HOLCF-Tutorial
Session HOL/IOA (timing)
Session HOL/IOA-ABP
Session HOL/IOA-NTP
Session HOL/IOA-Storage
Session HOL/IOA-ex
Session AFP/Shivers-CFA (AFP)
Session AFP/Stream-Fusion (AFP)
Session AFP/Tycon (AFP)
Session AFP/WorkerWrapper (AFP)
Session AFP/Hales_Jewett (AFP)
Session Misc/Haskell
Session AFP/Heard_Of (AFP)
Session AFP/Consensus_Refined (AFP)
Session AFP/Hello_World (AFP)
Session AFP/Hood_Melville_Queue (AFP)
Session AFP/HotelKeyCards (AFP)
Session Doc/How_to_Prove_it (no_doc)
Session AFP/Huffman (AFP)
Session AFP/Hybrid_Logic (AFP)
Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP)
Session AFP/IFC_Tracking (AFP)
Session AFP/IMP2 (AFP)
Session AFP/IMP2_Binary_Heap (AFP)
Session AFP/IMP_Compiler (AFP)
Session AFP/IMP_Compiler_Reuse (AFP)
Session Doc/Implementation (doc)
Session AFP/Implicational_Logic (AFP)
Session AFP/Impossible_Geometry (AFP)
Session AFP/Inductive_Confidentiality (AFP)
Session AFP/Inductive_Inference (AFP)
Session AFP/InfPathElimination (AFP)
Session AFP/Intro_Dest_Elim (AFP)
Session AFP/Involutions2Squares (AFP)
Session AFP/IsaGeoCoq (AFP)
Session AFP/IsaNet (AFP)
Session Doc/Isar_Ref (doc)
Session AFP/Isabelle_C (AFP)
Session Doc/JEdit (doc)
Session AFP/Jacobson_Basic_Algebra (AFP)
Session AFP/Grothendieck_Schemes (AFP)
Session AFP/Pluennecke_Ruzsa_Inequality (AFP)
Session AFP/Khovanskii_Theorem (AFP)
Session AFP/JiveDataStoreModel (AFP)
Session AFP/Key_Agreement_Strong_Adversaries (AFP)
Session AFP/Kleene_Algebra (AFP)
Session AFP/KAD (AFP)
Session AFP/KAT_and_DRA (AFP)
Session AFP/Algebraic_VCs (AFP)
Session AFP/Multirelations (AFP)
Session AFP/Quantales (AFP)
Session AFP/Transformer_Semantics (AFP)
Session AFP/Regular_Algebras (AFP)
Session AFP/Relation_Algebra (AFP)
Session AFP/Relational_Paths (AFP)
Session AFP/Residuated_Lattices (AFP)
Session AFP/Knights_Tour (AFP)
Session AFP/LambdaMu (AFP)
Session AFP/LatticeProperties (AFP)
Session AFP/DataRefinementIBP (AFP)
Session AFP/GraphMarkingIBP (AFP)
Session AFP/Lazy_Case (AFP)
Session AFP/Lifting_Definition_Option (AFP)
Session AFP/List-Index (AFP)
Session AFP/Comparison_Sort_Lower_Bound (AFP)
Session AFP/Jinja (AFP)
Session AFP/Dominance_CHK (AFP)
Session AFP/HRB-Slicing (AFP)
Session AFP/InformationFlowSlicing_Inter (AFP)
Session AFP/Slicing (AFP)
Session AFP/InformationFlowSlicing (AFP)
Session AFP/JinjaDCI (AFP)
Session AFP/Regression_Test_Selection (AFP)
Session AFP/List_Update (AFP)
Session AFP/Quick_Sort_Cost (AFP)
Session AFP/Random_BSTs (AFP)
Session AFP/Randomised_BSTs (AFP)
Session AFP/Treaps (AFP)
Session AFP/Randomised_Social_Choice (AFP)
Session AFP/Fishburn_Impossibility (AFP)
Session AFP/SDS_Impossibility (AFP)
Session AFP/List_Interleaving (AFP)
Session AFP/List_Inversions (AFP)
Session AFP/LocalLexing (AFP)
Session Doc/Locales (doc)
Session AFP/Locally-Nameless-Sigma (AFP)
Session AFP/Logging_Independent_Anonymity (AFP)
Session AFP/Lowe_Ontological_Argument (AFP)
Session Doc/Main (doc)
Session AFP/Marriage (AFP)
Session AFP/Latin_Square (AFP)
Session AFP/Matroids (AFP)
Session AFP/Max-Card-Matching (AFP)
Session AFP/Maximum_Segment_Sum (AFP)
Session AFP/Median_Of_Medians_Selection (AFP)
Session AFP/KD_Tree (AFP)
Session AFP/Menger (AFP)
Session AFP/Mereology (AFP)
Session AFP/Metalogic_ProofChecker (AFP)
Session AFP/MiniML (AFP)
Session AFP/Modular_Assembly_Kit_Security (AFP)
Session AFP/MonoBoolTranAlgebra (AFP)
Session AFP/Name_Carrying_Type_Inference (AFP)
Session AFP/Nano_JSON (AFP)
Session AFP/Nash_Williams (AFP)
Session AFP/No_FTL_observers (AFP)
Session AFP/Nominal2 (AFP)
Session AFP/Incompleteness (AFP)
Session AFP/Surprise_Paradox (AFP)
Session AFP/LambdaAuth (AFP)
Session AFP/Launchbury (AFP)
Session AFP/Call_Arity (AFP)
Session AFP/Modal_Logics_for_NTS (AFP)
Session AFP/Rewriting_Z (AFP)
Session AFP/Noninterference_CSP (AFP)
Session AFP/Noninterference_Ipurge_Unwinding (AFP)
Session AFP/Noninterference_Generic_Unwinding (AFP)
Session AFP/Noninterference_Inductive_Unwinding (AFP)
Session AFP/Noninterference_Sequential_Composition (AFP)
Session AFP/Noninterference_Concurrent_Composition (AFP)
Session AFP/NormByEval (AFP)
Session AFP/OpSets (AFP)
Session AFP/Open_Induction (AFP)
Session AFP/Well_Quasi_Orders (AFP)
Session AFP/Decreasing-Diagrams-II (AFP)
Session AFP/Myhill-Nerode (AFP)
Session AFP/Ordinal (AFP)
Session AFP/Nested_Multisets_Ordinals (AFP)
Session AFP/Design_Theory (AFP)
Session AFP/Undirected_Graph_Theory (AFP)
Session AFP/Lambda_Free_RPOs (AFP)
Session AFP/Lambda_Free_EPO (AFP)
Session AFP/Ordered_Resolution_Prover (AFP)
Session AFP/Chandy_Lamport (AFP)
Session AFP/Saturation_Framework (AFP)
Session AFP/Saturation_Framework_Extensions (AFP)
Session AFP/Progress_Tracking (AFP)
Session AFP/PAL (AFP)
Session AFP/PLM (AFP)
Session AFP/PSemigroupsConvolution (AFP)
Session AFP/Package_logic (AFP)
Session AFP/Combinable_Wands (AFP)
Session AFP/Paraconsistency (AFP)
Session AFP/Parity_Game (AFP)
Session AFP/GaleStewart_Games (AFP)
Session AFP/Partial_Function_MR (AFP)
Session AFP/Physical_Quantities (AFP)
Session AFP/Pop_Refinement (AFP)
Session AFP/Possibilistic_Noninterference (AFP)
Session AFP/Priority_Search_Trees (AFP)
Session AFP/Prim_Dijkstra_Simple (AFP)
Session Doc/Prog_Prove (doc)
Session AFP/Projective_Geometry (AFP)
Session AFP/Proof_Strategy_Language (AFP)
Session AFP/PropResPI (AFP)
Session AFP/Propositional_Proof_Systems (AFP)
Session AFP/PseudoHoops (AFP)
Session AFP/Ramsey-Infinite (AFP)
Session AFP/Real_Power (AFP)
Session AFP/Real_Time_Deque (AFP)
Session AFP/Recursion-Theory-I (AFP)
Session AFP/Minsky_Machines (AFP)
Session AFP/RefinementReactive (AFP)
Session AFP/Regex_Equivalence (AFP)
Session AFP/Relational_Method (AFP)
Session AFP/Resolution_FOL (AFP)
Session AFP/Robbins-Conjecture (AFP)
Session AFP/Roy_Floyd_Warshall (AFP)
Session AFP/SCC_Bloemen_Sequential (AFP)
Session AFP/SIFPL (AFP)
Session AFP/SIFUM_Type_Systems (AFP)
Session AFP/Security_Protocol_Refinement (AFP)
Session AFP/SenSocialChoice (AFP)
Session AFP/Separation_Algebra (AFP)
Session AFP/Hoare_Time (AFP)
Session AFP/Separata (AFP)
Session AFP/Separation_Logic_Unbounded (AFP)
Session AFP/Simpl (AFP)
Session AFP/BDD (AFP)
Session AFP/SimplifiedOntologicalArgument (AFP)
Session AFP/Sliding_Window_Algorithm (AFP)
Session AFP/Statecharts (AFP)
Session AFP/Stellar_Quorums (AFP)
Session AFP/Stone_Algebras (AFP)
Session AFP/Stone_Relation_Algebras (AFP)
Session AFP/Stone_Kleene_Relation_Algebras (AFP)
Session AFP/Aggregation_Algebras (AFP)
Session AFP/Relational_Disjoint_Set_Forests (AFP)
Session AFP/Relational_Minimum_Spanning_Trees (AFP)
Session AFP/Relational_Forests (AFP)
Session AFP/Subset_Boolean_Algebras (AFP)
Session AFP/Correctness_Algebras (AFP)
Session AFP/Store_Buffer_Reduction (AFP)
Session AFP/Strong_Security (AFP)
Session Doc/Sugar (doc)
Session AFP/Sunflowers (AFP)
Session AFP/Clique_and_Monotone_Circuits (AFP)
Session AFP/Syntax_Independent_Logic (AFP)
Session AFP/Goedel_Incompleteness (AFP)
Session AFP/Goedel_HFSet_Semantic (AFP)
Session AFP/Goedel_HFSet_Semanticless (AFP)
Session AFP/Robinson_Arithmetic (AFP)
Session AFP/Szpilrajn (AFP)
Session AFP/Combinatorics_Words_Lyndon (AFP)
Session AFP/TESL_Language (AFP)
Session AFP/TLA (AFP)
Session AFP/Timed_Automata (AFP)
Session AFP/Probabilistic_Timed_Automata (AFP)
Session AFP/Topological_Semantics (AFP)
Session AFP/Transitive-Closure-II (AFP)
Session AFP/Tree_Decomposition (AFP)
Session Doc/Tutorial (doc)
Session Doc/Typeclass_Hierarchy (doc)
Session AFP/Types_Tableaus_and_Goedels_God (AFP)
Session AFP/UPF (AFP)
Session AFP/UPF_Firewall (AFP)
Session AFP/Universal_Turing_Machine (AFP)
Session AFP/Van_der_Waerden (AFP)
Session AFP/VeriComp (AFP)
Session AFP/Interpreter_Optimizations (AFP)
Session AFP/Verified-Prover (AFP)
Session AFP/VolpanoSmith (AFP)
Session AFP/WHATandWHERE_Security (AFP)
Session AFP/Weight_Balanced_Trees (AFP)
Session AFP/Weighted_Arithmetic_Geometric_Mean (AFP)
Session AFP/Word_Lib (AFP)
Session AFP/Complx (AFP)
Session AFP/IEEE_Floating_Point (AFP)
Session AFP/IP_Addresses (AFP)
Session AFP/Simple_Firewall (AFP)
Session AFP/Routing (AFP)
Session AFP/Interval_Arithmetic_Word32 (AFP)
Session AFP/LEM (AFP)
Session AFP/Native_Word (AFP)
Session AFP/Collections (AFP)
Session AFP/Abstract_Completeness (AFP)
Session AFP/Abstract_Soundness (AFP)
Session AFP/FOL_Seq_Calc3 (AFP)
Session AFP/Incredible_Proof_Machine (AFP)
Session AFP/Deriving (AFP)
Session AFP/CAVA_Base (AFP)
Session AFP/CAVA_Automata (AFP)
Session AFP/DFS_Framework (AFP)
Session AFP/Gabow_SCC (AFP)
Session AFP/LTL_to_GBA (AFP)
Session AFP/Promela (AFP)
Session AFP/Containers (AFP)
Session AFP/Collections_Examples (AFP)
Session AFP/Containers-Benchmarks (AFP)
Session AFP/Eval_FO (AFP)
Session AFP/MFOTL_Monitor (AFP)
Session AFP/Generic_Join (AFP)
Session AFP/MFODL_Monitor_Optimized (AFP)
Session AFP/VYDRA_MDL (AFP)
Session AFP/Formula_Derivatives (AFP)
Session AFP/MSO_Regex_Equivalence (AFP)
Session AFP/Show (AFP)
Session AFP/Affine_Arithmetic (AFP)
Session AFP/Ordinary_Differential_Equations (AFP)
Session AFP/Differential_Dynamic_Logic (AFP)
Session AFP/Hybrid_Systems_VCs (AFP)
Session AFP/Matrices_for_ODEs (AFP)
Session AFP/Taylor_Models (AFP)
Session AFP/CakeML (AFP)
Session AFP/Certification_Monads (AFP)
Session AFP/AI_Planning_Languages_Semantics (AFP)
Session AFP/Verified_SAT_Based_AI_Planning (AFP)
Session AFP/Dict_Construction (AFP)
Session AFP/Formula_Derivatives-Examples (AFP)
Session AFP/Monad_Memo_DP (AFP)
Session AFP/Hidden_Markov_Models (AFP)
Session AFP/Optimal_BST (AFP)
Session AFP/Polynomial_Factorization (AFP)
Session AFP/Amicable_Numbers (AFP)
Session AFP/Dirichlet_Series (AFP)
Session AFP/Finite_Fields (AFP)
Session AFP/Universal_Hash_Families (AFP)
Session AFP/Frequency_Moments (AFP)
Session AFP/Zeta_Function (AFP)
Session AFP/Dirichlet_L (AFP)
Session AFP/Gauss_Sums (AFP)
Session AFP/Prime_Number_Theorem (AFP)
Session AFP/Prime_Distribution_Elementary (AFP)
Session AFP/IMO2019 (AFP)
Session AFP/Irrational_Series_Erdos_Straus (AFP)
Session AFP/Transcendence_Series_Hancl_Rucki (AFP)
Session AFP/Zeta_3_Irrational (AFP)
Session AFP/Gaussian_Integers (AFP)
Session AFP/Jordan_Normal_Form (AFP)
Session AFP/Farkas (AFP)
Session AFP/Isabelle_Marries_Dirac (AFP)
Session AFP/Knuth_Bendix_Order (AFP)
Session AFP/Functional_Ordered_Resolution_Prover (AFP)
Session AFP/Regular_Tree_Relations (AFP)
Session AFP/FO_Theory_Rewriting (AFP)
Session AFP/Rewrite_Properties_Reduction (AFP)
Session AFP/Weighted_Path_Order (AFP)
Session AFP/Multiset_Ordering_NPC (AFP)
Session AFP/Linear_Recurrences (AFP)
Session AFP/Perron_Frobenius (AFP)
Session AFP/Stochastic_Matrices (AFP)
Session AFP/Subresultants (AFP)
Session AFP/Berlekamp_Zassenhaus (AFP)
Session AFP/Algebraic_Numbers (AFP)
Session AFP/BenOr_Kozen_Reif (AFP)
Session AFP/LLL_Basis_Reduction (AFP)
Session AFP/LLL_Factorization (AFP)
Session AFP/Linear_Inequalities (AFP)
Session AFP/LP_Duality (AFP)
Session AFP/Linear_Programming (AFP)
Session AFP/Number_Theoretic_Transform (AFP)
Session AFP/CRYSTALS-Kyber (AFP)
Session AFP/Smith_Normal_Form (AFP)
Session AFP/Modular_arithmetic_LLL_and_HNF_algorithms (AFP)
Session AFP/Polynomials (AFP)
Session AFP/Deep_Learning (AFP)
Session AFP/QHLProver (AFP)
Session AFP/Projective_Measurements (AFP)
Session AFP/Commuting_Hermitian (AFP)
Session AFP/Groebner_Bases (AFP)
Session AFP/Fishers_Inequality (AFP)
Session AFP/Groebner_Macaulay (AFP)
Session AFP/Nullstellensatz (AFP)
Session AFP/Signature_Groebner (AFP)
Session AFP/Lambda_Free_KBOs (AFP)
Session AFP/Symmetric_Polynomials (AFP)
Session AFP/Pi_Transcendental (AFP)
Session AFP/Power_Sum_Polynomials (AFP)
Session AFP/Hermite_Lindemann (AFP)
Session AFP/Factor_Algebraic_Polynomial (AFP)
Session AFP/Cubic_Quartic_Equations (AFP)
Session AFP/Linear_Recurrences_Solver (AFP)
Session AFP/Virtual_Substitution (AFP)
Session AFP/Real_Impl (AFP)
Session AFP/Complex_Bounded_Operators (AFP)
Session AFP/Registers (AFP)
Session AFP/QR_Decomposition (AFP)
Session AFP/XML (AFP)
Session AFP/Van_Emde_Boas_Trees (AFP)
Session AFP/Dijkstra_Shortest_Path (AFP)
Session AFP/Koenigsberg_Friendship (AFP)
Session AFP/FOL_Seq_Calc2 (AFP)
Session AFP/Formal_SSA (AFP)
Session AFP/Minimal_SSA (AFP)
Session AFP/Gale_Shapley (AFP)
Session AFP/HOL-ODE-Numerics (AFP)
Session AFP/HOL-ODE-ARCH-COMP (AFP)
Session AFP/HOL-ODE-Examples (AFP large)
Session AFP/Lorenz_Approximation (AFP)
Session AFP/Lorenz_C0 (AFP large)
Session AFP/Lorenz_C1 (AFP large)
Session AFP/Poincare_Bendixson (AFP)
Session AFP/Safe_Range_RC (AFP)
Session AFP/Transition_Systems_and_Automata (AFP)
Session AFP/Adaptive_State_Counting (AFP)
Session AFP/Buchi_Complementation (AFP)
Session AFP/LTL_Master_Theorem (AFP)
Session AFP/LTL_Normal_Form (AFP)
Session AFP/Partial_Order_Reduction (AFP)
Session AFP/SM_Base (AFP)
Session AFP/SM (AFP)
Session AFP/CAVA_Setup (AFP)
Session AFP/CAVA_LTL_Modelchecker (AFP)
Session AFP/Transitive-Closure (AFP)
Session AFP/KBPs (AFP)
Session AFP/LTL_to_DRA (AFP)
Session AFP/Network_Security_Policy_Verification (AFP)
Session AFP/Planarity_Certificates (AFP)
Session AFP/Tree-Automata (AFP)
Session AFP/Datatype_Order_Generator (AFP)
Session AFP/Higher_Order_Terms (AFP)
Session AFP/CakeML_Codegen (AFP)
Session AFP/Old_Datatype_Show (AFP)
Session AFP/WOOT_Strong_Eventual_Consistency (AFP)
Session AFP/FSM_Tests (AFP)
Session AFP/Iptables_Semantics (AFP)
Session AFP/Iptables_Semantics_Examples (AFP)
Session AFP/LOFT (AFP)
Session AFP/Mersenne_Primes (AFP)
Session AFP/MiniSail (AFP)
Session AFP/Separation_Logic_Imperative_HOL (AFP)
Session AFP/Sepref_Prereq (AFP)
Session AFP/ROBDD (AFP)
Session AFP/Refine_Imperative_HOL (AFP)
Session AFP/BTree (AFP)
Session AFP/Floyd_Warshall (AFP)
Session AFP/Sepref_Basic (AFP)
Session AFP/Sepref_IICF (AFP)
Session AFP/Flow_Networks (AFP)
Session AFP/EdmondsKarp_Maxflow (AFP)
Session AFP/MFMC_Countable (AFP)
Session AFP/Probabilistic_While (AFP)
Session AFP/CryptHOL (AFP)
Session AFP/Constructive_Cryptography (AFP)
Session AFP/Game_Based_Crypto (AFP)
Session AFP/Multi_Party_Computation (AFP)
Session AFP/Sigma_Commit_Crypto (AFP)
Session AFP/Constructive_Cryptography_CM (AFP)
Session AFP/Prpu_Maxflow (AFP)
Session AFP/Knuth_Morris_Pratt (AFP)
Session AFP/Kruskal (AFP)
Session AFP/PAC_Checker (AFP)
Session AFP/VerifyThis2018 (AFP)
Session AFP/VerifyThis2019 (AFP)
Session AFP/Simplicial_complexes_and_boolean_functions (AFP)
Session AFP/UpDown_Scheme (AFP)
Session AFP/WebAssembly (AFP)
Session AFP/SPARCv8 (AFP)
Session AFP/X86_Semantics (AFP)
Session AFP/ZFC_in_HOL (AFP)
Session AFP/CZH_Foundations (AFP)
Session AFP/CZH_Elementary_Categories (AFP)
Session AFP/CZH_Universal_Constructions (AFP)
Session AFP/Category3 (AFP)
Session AFP/MonoidalCategory (AFP)
Session AFP/Ordinal_Partitions (AFP)
Session AFP/Wetzels_Problem (AFP)
Session FOL/ZF (main timing)
Session Doc/Logics_ZF (doc)
Session AFP/Recursion-Addition (AFP)
Session FOL/ZF-AC
Session FOL/ZF-Coind
Session FOL/ZF-Constructible
Session AFP/Delta_System_Lemma (AFP)
Session AFP/Transitive_Models (AFP)
Session AFP/Independence_CH (AFP)
Session AFP/Forcing (AFP)
Session FOL/ZF-IMP
Session FOL/ZF-Induct
Session FOL/ZF-UNITY (timing)
Session FOL/ZF-Resid
Session FOL/ZF-ex
Building Groebner_Bases ...
Running Virtual_Substitution ...
Running Functional_Ordered_Resolution_Prover ...
Running Linear_Recurrences_Solver ...
Running PAC_Checker ...
Running Polynomials ...
Building Symmetric_Polynomials ...
Running Fishers_Inequality ...
Symmetric_Polynomials: theory Abstract-Rewriting.Seq
Symmetric_Polynomials: theory Polynomials.MPoly_Type
Symmetric_Polynomials: theory HOL-Combinatorics.Transposition
Symmetric_Polynomials: theory Polynomials.More_Modules
Symmetric_Polynomials: theory Symmetric_Polynomials.Vieta
Symmetric_Polynomials: theory Regular-Sets.Regular_Set
Symmetric_Polynomials: theory Open_Induction.Restricted_Predicates
Symmetric_Polynomials: theory Well_Quasi_Orders.Infinite_Sequences
PAC_Checker: theory Deriving.Derive_Manager
Symmetric_Polynomials: theory Well_Quasi_Orders.Least_Enum
PAC_Checker: theory HOL-Combinatorics.Transposition
PAC_Checker: theory HOL-Library.Conditional_Parametricity
PAC_Checker: theory HOL-Library.Multiset_Order
PAC_Checker: theory Deriving.Generator_Aux
PAC_Checker: theory HOL-Library.FuncSet
PAC_Checker: theory HOL-Library.Fun_Lexorder
PAC_Checker: theory HOL-Library.Function_Algebras
Symmetric_Polynomials: theory HOL-Combinatorics.Permutations
PAC_Checker: theory HOL-Library.Groups_Big_Fun
PAC_Checker: theory Abstract-Rewriting.Seq
Polynomials: theory Deriving.Derive_Manager
Polynomials: theory Deriving.Comparator
Polynomials: theory Deriving.Generator_Aux
Polynomials: theory HOL-Computational_Algebra.Factorial_Ring
Polynomials: theory Polynomials.MPoly_Type
Polynomials: theory Polynomials.More_Modules
Polynomials: theory Matrix.Utility
Polynomials: theory Open_Induction.Restricted_Predicates
PAC_Checker: theory HOL-Library.More_List
Polynomials: theory Well_Quasi_Orders.Infinite_Sequences
PAC_Checker: theory HOL-Library.Sublist
Symmetric_Polynomials: theory Well_Quasi_Orders.Minimal_Elements
Symmetric_Polynomials: theory Polynomials.More_MPoly_Type
Functional_Ordered_Resolution_Prover: theory Deriving.Comparator
Functional_Ordered_Resolution_Prover: theory Deriving.Derive_Manager
Functional_Ordered_Resolution_Prover: theory Deriving.Generator_Aux
Virtual_Substitution: theory Deriving.Generator_Aux
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term
Virtual_Substitution: theory HOL-Library.AList
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Fun_More
Virtual_Substitution: theory Deriving.Derive_Manager
Virtual_Substitution: theory HOL-Library.Code_Abstract_Nat
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Transitive_Closure_More
Virtual_Substitution: theory HOL-Library.Code_Target_Int
Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Order_Union
Virtual_Substitution: theory HOL-Library.Conditional_Parametricity
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Option_Monad
Virtual_Substitution: theory HOL-Library.Fun_Lexorder
Virtual_Substitution: theory HOL-Library.Function_Algebras
Polynomials: theory Well_Quasi_Orders.Least_Enum
Virtual_Substitution: theory HOL-Library.Groups_Big_Fun
Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Seq
PAC_Checker: theory HOL-Library.Countable_Set
Virtual_Substitution: theory Abstract-Rewriting.Seq
Functional_Ordered_Resolution_Prover: theory Word_Lib.Bit_Comprehension
Virtual_Substitution: theory HOL-Library.Code_Target_Nat
Functional_Ordered_Resolution_Prover: theory HOL-Cardinals.Wellorder_Extension
Functional_Ordered_Resolution_Prover: theory Word_Lib.More_Divides
Polynomials: theory Show.Show
Groebner_Bases: theory Containers.Equal
Groebner_Bases: theory Containers.Extend_Partial_Order
Groebner_Bases: theory Containers.List_Fusion
Groebner_Bases: theory Deriving.Comparator
Groebner_Bases: theory Deriving.Generator_Aux
Groebner_Bases: theory Deriving.Derive_Manager
Groebner_Bases: theory Containers.Containers_Auxiliary
Groebner_Bases: theory Jordan_Normal_Form.Missing_Misc
Groebner_Bases: theory Containers.Closure_Set
Fishers_Inequality: theory Card_Partitions.Set_Partition
Fishers_Inequality: theory Polynomials.MPoly_Type
Fishers_Inequality: theory Nested_Multisets_Ordinals.Multiset_More
Fishers_Inequality: theory Polynomials.More_Modules
Fishers_Inequality: theory HOL-Combinatorics.Multiset_Permutations
Fishers_Inequality: theory List-Index.List_Index
Fishers_Inequality: theory Open_Induction.Restricted_Predicates
Fishers_Inequality: theory BenOr_Kozen_Reif.More_Matrix
Linear_Recurrences_Solver: theory Pure-ex.Guess
Linear_Recurrences_Solver: theory HOL-Combinatorics.Stirling
Linear_Recurrences_Solver: theory Polynomials.MPoly_Type
Linear_Recurrences_Solver: theory Deriving.Compare_Rat
Linear_Recurrences_Solver: theory Deriving.Compare_Real
Linear_Recurrences_Solver: theory Polynomials.More_Modules
Linear_Recurrences_Solver: theory Symmetric_Polynomials.Vieta
Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Common
PAC_Checker: theory HOL-Library.FSet
Polynomials: theory Polynomials.Polynomials
Functional_Ordered_Resolution_Prover: theory Word_Lib.Signed_Division_Word
Virtual_Substitution: theory HOL-Library.Ramsey
Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Recurrences_Misc
Groebner_Bases: theory Abstract-Rewriting.Seq
Groebner_Bases: theory Polynomials.MPoly_Type
Linear_Recurrences_Solver: theory Sturm_Sequences.Misc_Polynomial
Polynomials: theory Well_Quasi_Orders.Minimal_Elements
Polynomials: theory Well_Quasi_Orders.Almost_Full
Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Generator
Groebner_Bases: theory Jordan_Normal_Form.Missing_Ring
Symmetric_Polynomials: theory Polynomials.Poly_Mapping_Finite_Map
Linear_Recurrences_Solver: theory Linear_Recurrences.RatFPS
Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
PAC_Checker: theory Polynomials.More_Modules
PAC_Checker: theory Open_Induction.Restricted_Predicates
Linear_Recurrences_Solver: theory Algebraic_Numbers.Compare_Complex
PAC_Checker: theory HOL-Library.Poly_Mapping
Groebner_Bases: theory Polynomials.More_Modules
Fishers_Inequality: theory Well_Quasi_Orders.Infinite_Sequences
Functional_Ordered_Resolution_Prover: theory Deriving.Countable_Generator
Functional_Ordered_Resolution_Prover: theory Lambda_Free_RPOs.Lambda_Free_Util
Linear_Recurrences_Solver: theory Open_Induction.Restricted_Predicates
PAC_Checker: theory PAC_Checker.PAC_Misc
Polynomials: theory Polynomials.More_MPoly_Type
Virtual_Substitution: theory HOL-Library.More_List
Virtual_Substitution: theory HOL-Library.Sublist
Linear_Recurrences_Solver: theory Linear_Recurrences.Eulerian_Polynomials
Virtual_Substitution: theory HOL-Library.While_Combinator
PAC_Checker: theory PAC_Checker.PAC_Version
Linear_Recurrences_Solver: theory Linear_Recurrences.Factorizations
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Seq_More
Functional_Ordered_Resolution_Prover: theory Matrix.Utility
Functional_Ordered_Resolution_Prover: theory Native_Word.Code_Int_Integer_Conversion
Groebner_Bases: theory Deriving.Equality_Generator
PAC_Checker: theory PAC_Checker.More_Loops
Fishers_Inequality: theory Well_Quasi_Orders.Least_Enum
PAC_Checker: theory HOL-Algebra.Congruence
Symmetric_Polynomials: theory Symmetric_Polynomials.Symmetric_Polynomials
Groebner_Bases: theory Containers.Containers_Generator
Virtual_Substitution: theory HOL-Library.FSet
Polynomials: theory Polynomials.OAlist
Groebner_Bases: theory Polynomial_Interpolation.Missing_Unsorted
Polynomials: theory Polynomials.Poly_Mapping_Finite_Map
Functional_Ordered_Resolution_Prover: theory Deriving.Equality_Instances
Functional_Ordered_Resolution_Prover: theory Open_Induction.Restricted_Predicates
Linear_Recurrences_Solver: theory Linear_Recurrences.Pochhammer_Polynomials
PAC_Checker: theory HOL-Library.Disjoint_Sets
Groebner_Bases: theory Groebner_Bases.Code_Target_Rat
Linear_Recurrences_Solver: theory Polynomials.More_MPoly_Type
Virtual_Substitution: theory Polynomials.More_Modules
Virtual_Substitution: theory HOL-Library.Poly_Mapping
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover
Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Elements
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Set
Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full
Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Library
Functional_Ordered_Resolution_Prover: theory Deriving.Compare
Linear_Recurrences_Solver: theory Sturm_Sequences.Sturm_Theorem
Linear_Recurrences_Solver: theory Linear_Recurrences.Partial_Fraction_Decomposition
Virtual_Substitution: theory HOL-Computational_Algebra.Polynomial
Functional_Ordered_Resolution_Prover: theory Deriving.Comparator_Generator
PAC_Checker: theory HOL-Library.Ramsey
Fishers_Inequality: theory Polynomials.More_MPoly_Type
Polynomials: theory Show.Show_Instances
Groebner_Bases: theory Deriving.Equality_Instances
Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Roots_Real_Poly
PAC_Checker: theory Regular-Sets.Regular_Set
Functional_Ordered_Resolution_Prover: theory Polynomial_Factorization.Missing_List
Groebner_Bases: theory Containers.Collection_Enum
Groebner_Bases: theory Polynomials.More_MPoly_Type
PAC_Checker: theory Show.Show
Groebner_Bases: theory Jordan_Normal_Form.Conjugate
Groebner_Bases: theory Containers.Collection_Eq
Virtual_Substitution: theory HOL-Library.Quadratic_Discriminant
Functional_Ordered_Resolution_Prover: theory Show.Show
Linear_Recurrences_Solver: theory Polynomials.Poly_Mapping_Finite_Map
Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Univariate
Linear_Recurrences_Solver: theory Symmetric_Polynomials.Symmetric_Polynomials
PAC_Checker: theory HOL-Combinatorics.Permutations
Fishers_Inequality: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
Virtual_Substitution: theory Matrix.Utility
Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Prelim
Polynomials: theory Well_Quasi_Orders.Minimal_Bad_Sequences
Virtual_Substitution: theory Open_Induction.Restricted_Predicates
Virtual_Substitution: theory Regular-Sets.Regular_Set
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unifiers
Fishers_Inequality: theory Design_Theory.Multisets_Extras
Groebner_Bases: theory Deriving.Compare
Linear_Recurrences_Solver: theory Algebraic_Numbers.Bivariate_Polynomials
Polynomials: theory Well_Quasi_Orders.Almost_Full_Relations
PAC_Checker: theory Well_Quasi_Orders.Infinite_Sequences
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Term_Pair_Multiset
Groebner_Bases: theory Polynomials.OAlist
Linear_Recurrences_Solver: theory Show.Show_Real
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Subsumption
Polynomials: theory Polynomials.Utils
Polynomials: theory Well_Quasi_Orders.Well_Quasi_Orders
PAC_Checker: theory Well_Quasi_Orders.Minimal_Elements
Virtual_Substitution: theory Show.Show
Fishers_Inequality: theory Well_Quasi_Orders.Minimal_Bad_Sequences
Functional_Ordered_Resolution_Prover: theory Word_Lib.More_Arithmetic
Groebner_Bases: theory Deriving.Comparator_Generator
Virtual_Substitution: theory Well_Quasi_Orders.Infinite_Sequences
Groebner_Bases: theory Containers.Lexicographic_Order
Groebner_Bases: theory Containers.DList_Set
Linear_Recurrences_Solver: theory Well_Quasi_Orders.Infinite_Sequences
Fishers_Inequality: theory Design_Theory.Design_Basics
PAC_Checker: theory HOL-Algebra.Order
Fishers_Inequality: theory Fishers_Inequality.Set_Multiset_Extras
Virtual_Substitution: theory Well_Quasi_Orders.Minimal_Elements
Fishers_Inequality: theory Well_Quasi_Orders.Almost_Full_Relations
Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Show_RatFPS
Virtual_Substitution: theory Well_Quasi_Orders.Least_Enum
Linear_Recurrences_Solver: theory Well_Quasi_Orders.Least_Enum
Groebner_Bases: theory Containers.Set_Linorder
Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Elements
Linear_Recurrences_Solver: theory Show.Show_Complex
Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Generator
Polynomials: theory Polynomials.Power_Products
Functional_Ordered_Resolution_Prover: theory Word_Lib.More_Word
Groebner_Bases: theory Containers.RBT_ext
Groebner_Bases: theory Deriving.RBT_Comparator_Impl
Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full
PAC_Checker: theory Well_Quasi_Orders.Least_Enum
Linear_Recurrences_Solver: theory Linear_Recurrences.Rational_FPS_Solver
Fishers_Inequality: theory Polynomials.Utils
Fishers_Inequality: theory Design_Theory.Design_Operations
Fishers_Inequality: theory Well_Quasi_Orders.Well_Quasi_Orders
Groebner_Bases: theory Deriving.Compare_Generator
Fishers_Inequality: theory Groebner_Bases.General
Groebner_Bases: theory Open_Induction.Restricted_Predicates
Functional_Ordered_Resolution_Prover: theory Deriving.Compare_Instances
Fishers_Inequality: theory Polynomials.Power_Products
PAC_Checker: theory Show.Show_Instances
PAC_Checker: theory Native_Word.Uint64
Functional_Ordered_Resolution_Prover: theory Show.Show_Instances
Groebner_Bases: theory Deriving.Compare_Instances
Virtual_Substitution: theory Polynomials.MPoly_Type
Groebner_Bases: theory Polynomial_Interpolation.Ring_Hom
PAC_Checker: theory HOL-Combinatorics.List_Permutation
Fishers_Inequality: theory Design_Theory.Block_Designs
Fishers_Inequality: theory Design_Theory.Sub_Designs
PAC_Checker: theory Nested_Multisets_Ordinals.Multiset_More
Groebner_Bases: theory Regular-Sets.Regular_Set
PAC_Checker: theory Polynomials.MPoly_Type
Symmetric_Polynomials: theory Regular-Sets.Regular_Exp
Virtual_Substitution: theory Show.Show_Instances
Virtual_Substitution: theory Show.Show_Real
Fishers_Inequality: theory Design_Theory.Design_Isomorphisms
Linear_Recurrences_Solver: theory Algebraic_Numbers.Resultant
Symmetric_Polynomials: theory Regular-Sets.NDerivative
Symmetric_Polynomials: theory Regular-Sets.Relation_Interpretation
Groebner_Bases: theory Well_Quasi_Orders.Infinite_Sequences
Groebner_Bases: theory Well_Quasi_Orders.Minimal_Elements
Symmetric_Polynomials: theory Regular-Sets.Equivalence_Checking
PAC_Checker: theory HOL-Algebra.Lattice
Linear_Recurrences_Solver: theory Well_Quasi_Orders.Minimal_Bad_Sequences
Groebner_Bases: theory Well_Quasi_Orders.Least_Enum
Symmetric_Polynomials: theory Regular-Sets.Regexp_Method
Symmetric_Polynomials: theory Well_Quasi_Orders.Almost_Full
Linear_Recurrences_Solver: theory Algebraic_Numbers.Interval_Arithmetic
Virtual_Substitution: theory Polynomials.More_MPoly_Type
Linear_Recurrences_Solver: theory Algebraic_Numbers.Min_Int_Poly
Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Homogenous_Recurrences
Fishers_Inequality: theory Design_Theory.BIBD
Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Pretty
Linear_Recurrences_Solver: theory Algebraic_Numbers.Sturm_Rat
Linear_Recurrences_Solver: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
PAC_Checker: theory Polynomials.More_MPoly_Type
Linear_Recurrences_Solver: theory Algebraic_Numbers.Factors_of_Int_Poly
Linear_Recurrences_Solver: theory Well_Quasi_Orders.Almost_Full_Relations
Polynomials: theory Polynomials.NZM
Polynomials: theory Polynomials.Show_Polynomials
Symmetric_Polynomials: theory Well_Quasi_Orders.Minimal_Bad_Sequences
Symmetric_Polynomials: theory Well_Quasi_Orders.Almost_Full_Relations
Linear_Recurrences_Solver: theory Polynomials.Utils
Functional_Ordered_Resolution_Prover: theory Native_Word.Code_Target_Word_Base
Linear_Recurrences_Solver: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
Symmetric_Polynomials: theory Polynomials.Utils
Symmetric_Polynomials: theory Well_Quasi_Orders.Well_Quasi_Orders
Functional_Ordered_Resolution_Prover: theory Word_Lib.Bit_Shifts_Infix_Syntax
Functional_Ordered_Resolution_Prover: theory Word_Lib.Least_significant_bit
Fishers_Inequality: theory Fishers_Inequality.Design_Extras
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover
PAC_Checker: theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset
Linear_Recurrences_Solver: theory Well_Quasi_Orders.Well_Quasi_Orders
PAC_Checker: theory PAC_Checker.WB_Sort
Functional_Ordered_Resolution_Prover: theory Word_Lib.Most_significant_bit
Functional_Ordered_Resolution_Prover: theory Word_Lib.Generic_set_bit
Linear_Recurrences_Solver: theory Linear_Recurrences.Linear_Inhomogenous_Recurrences
Symmetric_Polynomials: theory Polynomials.Power_Products
Virtual_Substitution: theory HOL-Library.Finite_Map
PAC_Checker: theory HOL-Algebra.Complete_Lattice
Functional_Ordered_Resolution_Prover: theory Native_Word.Code_Target_Integer_Bit
Functional_Ordered_Resolution_Prover: theory Native_Word.Word_Type_Copies
Groebner_Bases: theory Jordan_Normal_Form.Matrix
Linear_Recurrences_Solver: theory Polynomials.Power_Products
Polynomials: theory HOL-Computational_Algebra.Polynomial
PAC_Checker: theory HOL-Library.Finite_Map
Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers
PAC_Checker: theory HOL-Algebra.Group
Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_via_IA
Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class
Fishers_Inequality: theory Polynomials.MPoly_Type_Class
Virtual_Substitution: theory Polynomials.MPoly_Type_Univariate
Linear_Recurrences_Solver: theory Algebraic_Numbers.Algebraic_Numbers_Pre_Impl
PAC_Checker: theory HOL-Algebra.Coset
PAC_Checker: theory HOL-Algebra.FiniteProduct
Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class_Ordered
Fishers_Inequality: theory Polynomials.MPoly_Type_Class_Ordered
Linear_Recurrences_Solver: theory Algebraic_Numbers.Cauchy_Root_Bound
Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Algebraic_Numbers
PAC_Checker: theory HOL-Algebra.Ring
Polynomials: theory Polynomials.MPoly_Type_Class
Polynomials: theory Polynomials.MPoly_Type_Univariate
Groebner_Bases: theory Jordan_Normal_Form.Gauss_Jordan_Elimination
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regular_Exp
Polynomials: theory Polynomials.PP_Type
Groebner_Bases: theory Containers.Collection_Order
Functional_Ordered_Resolution_Prover: theory Regular-Sets.NDerivative
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Relation_Interpretation
PAC_Checker: theory HOL-Algebra.Generated_Groups
PAC_Checker: theory HOL-Algebra.Divisibility
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Equivalence_Checking
Functional_Ordered_Resolution_Prover: theory Regular-Sets.Regexp_Method
Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Abstract_Rewriting
Virtual_Substitution: theory Regular-Sets.Regular_Exp
Polynomials: theory Polynomials.MPoly_Type_Class_Ordered
PAC_Checker: theory HOL-Algebra.Elementary_Groups
Virtual_Substitution: theory Regular-Sets.NDerivative
Virtual_Substitution: theory Regular-Sets.Relation_Interpretation
Virtual_Substitution: theory Regular-Sets.Equivalence_Checking
Virtual_Substitution: theory Regular-Sets.Regexp_Method
Virtual_Substitution: theory Abstract-Rewriting.Abstract_Rewriting
Virtual_Substitution: theory Well_Quasi_Orders.Almost_Full
Groebner_Bases: theory Containers.RBT_Mapping2
Symmetric_Polynomials: theory Polynomials.MPoly_Type_Class_FMap
Functional_Ordered_Resolution_Prover: theory Abstract-Rewriting.Relative_Rewriting
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Matching
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Abstract_Unification
Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.Subterm_and_Context
Symmetric_Polynomials: theory Symmetric_Polynomials.Symmetric_Polynomials_Code
Groebner_Bases: theory Containers.RBT_Set2
Virtual_Substitution: theory Well_Quasi_Orders.Minimal_Bad_Sequences
PAC_Checker: theory HOL-Algebra.AbelCoset
PAC_Checker: theory HOL-Algebra.Module
Polynomials: theory Polynomials.MPoly_Type_Class_FMap
Virtual_Substitution: theory Abstract-Rewriting.SN_Orders
Virtual_Substitution: theory Well_Quasi_Orders.Almost_Full_Relations
Polynomials: theory Polynomials.Quasi_PM_Power_Products
Polynomials: theory Polynomials.MPoly_PM
Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class
Virtual_Substitution: theory Polynomials.Utils
Virtual_Substitution: theory Well_Quasi_Orders.Well_Quasi_Orders
PAC_Checker: theory HOL-Algebra.Ideal
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Unification
Virtual_Substitution: theory Polynomials.Power_Products
Groebner_Bases: theory Containers.Set_Impl
PAC_Checker: theory HOL-Algebra.RingHom
Fishers_Inequality: theory Groebner_Bases.More_MPoly_Type_Class
Virtual_Substitution: theory Polynomials.Polynomials
Fishers_Inequality: theory Groebner_Bases.Macaulay_Matrix
PAC_Checker: theory HOL-Algebra.QuotRing
PAC_Checker: theory HOL-Algebra.UnivPoly
Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.Order_Pair
Polynomials: theory Polynomials.OAlist_Poly_Mapping
Functional_Ordered_Resolution_Prover: theory First_Order_Terms.Matching
Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.Lexicographic_Extension
Fishers_Inequality: theory Fishers_Inequality.Matrix_Vector_Extras
Polynomials: theory Polynomials.Term_Order
Fishers_Inequality: theory Fishers_Inequality.Incidence_Matrices
Fishers_Inequality: theory Fishers_Inequality.Vector_Matrix_Mod
Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.Term_Aux
Preparing Symmetric_Polynomials/document ...
Virtual_Substitution: theory Polynomials.Show_Polynomials
Polynomials: theory Polynomials.MPoly_Type_Class_OAlist
Functional_Ordered_Resolution_Prover: theory Knuth_Bendix_Order.KBO
PAC_Checker: theory HOL-Algebra.Multiplicative_Group
PAC_Checker: theory HOL-Algebra.Ring_Divisibility
PAC_Checker: theory HOL-Algebra.Subrings
Virtual_Substitution: theory Polynomials.MPoly_Type_Class
Finished Symmetric_Polynomials/document (0:00:06 elapsed time)
Preparing Symmetric_Polynomials/outline ...
Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Container
Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Poly_Connection
Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_Ordered
Virtual_Substitution: theory Polynomials.MPoly_Type_Class_Ordered
Finished Symmetric_Polynomials/outline (0:00:03 elapsed time)
PAC_Checker: theory HOL-Algebra.Polynomials
Timing Symmetric_Polynomials (8 threads, 86.476s elapsed time, 197.320s cpu time, 15.708s GC time, factor 2.28)
Finished Symmetric_Polynomials (0:02:37 elapsed time, 0:04:18 cpu time, factor 1.64)
Running Factor_Algebraic_Polynomial ...
Fishers_Inequality: theory Fishers_Inequality.Dual_Systems
Fishers_Inequality: theory Fishers_Inequality.Linear_Bound_Argument
Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide
Fishers_Inequality: theory Fishers_Inequality.Rank_Argument_General
Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality
Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Variations
Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type
Factor_Algebraic_Polynomial: theory Polynomials.More_Modules
Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Vieta
Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Is_Int_To_Int
Factor_Algebraic_Polynomial: theory Open_Induction.Restricted_Predicates
Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_via_IA
Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Infinite_Sequences
Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Least_Enum
Fishers_Inequality: theory Fishers_Inequality.Fishers_Inequality_Root
Groebner_Bases: theory Jordan_Normal_Form.Matrix_IArray_Impl
Virtual_Substitution: theory Polynomials.Poly_Mapping_Finite_Map
Virtual_Substitution: theory Polynomials.MPoly_Type_Class_FMap
Linear_Recurrences_Solver: theory Algebraic_Numbers.Real_Roots
Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Alg
Groebner_Bases: theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl
Preparing Fishers_Inequality/document ...
Virtual_Substitution: theory Virtual_Substitution.MPolyExtension
Virtual_Substitution: theory Virtual_Substitution.ExecutiblePolyProps
Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Elements
Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full
Linear_Recurrences_Solver: theory Algebraic_Numbers.Show_Real_Precise
Factor_Algebraic_Polynomial: theory Polynomials.More_MPoly_Type
Virtual_Substitution: theory Virtual_Substitution.PolyAtoms
Virtual_Substitution: theory Virtual_Substitution.QE
Groebner_Bases: theory Regular-Sets.Regular_Exp
Functional_Ordered_Resolution_Prover: theory Native_Word.Uint32
Linear_Recurrences_Solver: theory Algebraic_Numbers.Complex_Algebraic_Numbers
Functional_Ordered_Resolution_Prover: theory Collections.HashCode
Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Generator
Groebner_Bases: theory Regular-Sets.Relation_Interpretation
Groebner_Bases: theory Regular-Sets.NDerivative
Groebner_Bases: theory Regular-Sets.Equivalence_Checking
Functional_Ordered_Resolution_Prover: theory Deriving.Hash_Instances
Functional_Ordered_Resolution_Prover: theory Deriving.Derive
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.IsaFoR_Term
Virtual_Substitution: theory Virtual_Substitution.Debruijn
Virtual_Substitution: theory Virtual_Substitution.PrettyPrinting
Factor_Algebraic_Polynomial: theory Polynomials.Poly_Mapping_Finite_Map
Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Univariate
Factor_Algebraic_Polynomial: theory Symmetric_Polynomials.Symmetric_Polynomials
Groebner_Bases: theory Regular-Sets.Regexp_Method
Finished Fishers_Inequality/document (0:00:13 elapsed time)
Preparing Fishers_Inequality/outline ...
Groebner_Bases: theory Abstract-Rewriting.Abstract_Rewriting
Groebner_Bases: theory Well_Quasi_Orders.Almost_Full
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Executable_Subsumption
Functional_Ordered_Resolution_Prover: theory Functional_Ordered_Resolution_Prover.Executable_FO_Ordered_Resolution_Prover
Finished Fishers_Inequality/outline (0:00:07 elapsed time)
Timing Fishers_Inequality (8 threads, 61.591s elapsed time, 383.892s cpu time, 26.632s GC time, factor 6.23)
Finished Fishers_Inequality (0:03:02 elapsed time, 0:06:34 cpu time, factor 2.16)
Building Saturation_Framework ...
Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Minimal_Bad_Sequences
Groebner_Bases: theory Well_Quasi_Orders.Minimal_Bad_Sequences
Saturation_Framework: theory Saturation_Framework.Calculus
Saturation_Framework: theory Lambda_Free_RPOs.Lambda_Free_Util
Saturation_Framework: theory Well_Quasi_Orders.Infinite_Sequences
Saturation_Framework: theory Open_Induction.Restricted_Predicates
Groebner_Bases: theory Groebner_Bases.Confluence
Groebner_Bases: theory Well_Quasi_Orders.Almost_Full_Relations
Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Almost_Full_Relations
Saturation_Framework: theory Well_Quasi_Orders.Minimal_Elements
Linear_Recurrences_Solver: theory Polynomials.MPoly_Type_Class_FMap
Factor_Algebraic_Polynomial: theory Polynomials.Utils
Factor_Algebraic_Polynomial: theory Well_Quasi_Orders.Well_Quasi_Orders
Groebner_Bases: theory Polynomials.Utils
Groebner_Bases: theory Well_Quasi_Orders.Well_Quasi_Orders
Virtual_Substitution: theory Virtual_Substitution.Optimizations
Virtual_Substitution: theory Virtual_Substitution.Reindex
Virtual_Substitution: theory Virtual_Substitution.UniAtoms
Saturation_Framework: theory Saturation_Framework.Calculus_Variations
Saturation_Framework: theory Saturation_Framework.Intersection_Calculus
Groebner_Bases: theory Groebner_Bases.General
Factor_Algebraic_Polynomial: theory Polynomials.Power_Products
Groebner_Bases: theory Polynomials.Power_Products
Factor_Algebraic_Polynomial: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
Saturation_Framework: theory Saturation_Framework.Lifting_to_Non_Ground_Calculi
Saturation_Framework: theory Saturation_Framework.Labeled_Lifting_to_Non_Ground_Calculi
Factor_Algebraic_Polynomial: theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW
Saturation_Framework: theory Saturation_Framework.Given_Clause_Architectures
Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
PAC_Checker: theory Regular-Sets.Regular_Exp
PAC_Checker: theory Regular-Sets.NDerivative
PAC_Checker: theory Regular-Sets.Relation_Interpretation
Virtual_Substitution: theory Virtual_Substitution.OptimizationProofs
PAC_Checker: theory Regular-Sets.Equivalence_Checking
Virtual_Substitution: theory Virtual_Substitution.VSAlgos
PAC_Checker: theory Regular-Sets.Regexp_Method
PAC_Checker: theory Well_Quasi_Orders.Almost_Full
Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
PAC_Checker: theory Well_Quasi_Orders.Minimal_Bad_Sequences
PAC_Checker: theory Well_Quasi_Orders.Almost_Full_Relations
PAC_Checker: theory Polynomials.Utils
PAC_Checker: theory Well_Quasi_Orders.Well_Quasi_Orders
Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
PAC_Checker: theory Polynomials.Power_Products
Groebner_Bases: theory Polynomials.MPoly_Type_Class
Groebner_Bases: theory Polynomials.PP_Type
Preparing Polynomials/document ...
PAC_Checker: theory Polynomials.MPoly_Type_Class
Virtual_Substitution: theory Virtual_Substitution.DNF
Virtual_Substitution: theory Virtual_Substitution.LinearCase
Virtual_Substitution: theory Virtual_Substitution.Heuristic
Groebner_Bases: theory Polynomials.MPoly_Type_Class_Ordered
Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
Virtual_Substitution: theory Virtual_Substitution.NegInfinity
Virtual_Substitution: theory Virtual_Substitution.QuadraticCase
PAC_Checker: theory PAC_Checker.PAC_More_Poly
Preparing Saturation_Framework/document ...
PAC_Checker: theory PAC_Checker.PAC_Specification
Linear_Recurrences_Solver: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Solver
Virtual_Substitution: theory Virtual_Substitution.EliminateVariable
Finished Saturation_Framework/document (0:00:04 elapsed time)
Preparing Saturation_Framework/outline ...
Virtual_Substitution: theory Virtual_Substitution.Infinitesimals
Groebner_Bases: theory Groebner_Bases.More_MPoly_Type_Class
Groebner_Bases: theory Polynomials.Quasi_PM_Power_Products
Groebner_Bases: theory Polynomials.OAlist_Poly_Mapping
Groebner_Bases: theory Groebner_Bases.Reduction
Linear_Recurrences_Solver: theory Linear_Recurrences_Solver.Linear_Recurrences_Test
Virtual_Substitution: theory Virtual_Substitution.LuckyFind
Virtual_Substitution: theory Virtual_Substitution.EqualityVS
Finished Saturation_Framework/outline (0:00:03 elapsed time)
Timing Saturation_Framework (8 threads, 10.181s elapsed time, 53.912s cpu time, 1.969s GC time, factor 5.30)
Finished Saturation_Framework (0:00:56 elapsed time, 0:01:33 cpu time, factor 1.67)
Running Power_Sum_Polynomials ...
Virtual_Substitution: theory Virtual_Substitution.NegInfinityUni
Groebner_Bases: theory Groebner_Bases.Macaulay_Matrix
Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class
Virtual_Substitution: theory Virtual_Substitution.InfinitesimalsUni
PAC_Checker: theory PAC_Checker.Finite_Map_Multiset
PAC_Checker: theory PAC_Checker.PAC_Polynomials
PAC_Checker: theory PAC_Checker.PAC_Checker_Specification
PAC_Checker: theory PAC_Checker.PAC_Map_Rel
Virtual_Substitution: theory Virtual_Substitution.DNFUni
Timing Linear_Recurrences_Solver (8 threads, 192.857s elapsed time, 964.420s cpu time, 83.003s GC time, factor 5.00)
Finished Linear_Recurrences_Solver (0:04:30 elapsed time, 0:16:14 cpu time, factor 3.60)
Running Saturation_Framework_Extensions ...
Power_Sum_Polynomials: theory Polynomial_Interpolation.Missing_Unsorted
Power_Sum_Polynomials: theory Matrix.Utility
Power_Sum_Polynomials: theory Polynomial_Interpolation.Ring_Hom
Virtual_Substitution: theory Virtual_Substitution.GeneralVSProofs
Power_Sum_Polynomials: theory Polynomial_Factorization.Missing_List
Groebner_Bases: theory Polynomials.MPoly_PM
PAC_Checker: theory PAC_Checker.PAC_Polynomials_Term
Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.Soundness
Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.Standard_Redundancy_Criterion
Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.Given_Clause_Architectures_Revisited
PAC_Checker: theory PAC_Checker.PAC_Assoc_Map_Rel
Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Container
Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Poly_Connection
Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_Ordered
Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.Clausal_Calculus
Saturation_Framework_Extensions: theory Saturation_Framework_Extensions.FO_Ordered_Resolution_Prover_Revisited
Power_Sum_Polynomials: theory Polynomial_Interpolation.Missing_Polynomial
Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide
Virtual_Substitution: theory Virtual_Substitution.VSQuad
Finished Polynomials/document (0:00:30 elapsed time)
Preparing Polynomials/outline ...
Virtual_Substitution: theory Virtual_Substitution.Exports
PAC_Checker: theory PAC_Checker.PAC_Polynomials_Operations
Virtual_Substitution: theory Virtual_Substitution.HeuristicProofs
Power_Sum_Polynomials: theory Polynomial_Factorization.Missing_Multiset
PAC_Checker: theory PAC_Checker.PAC_Checker
Power_Sum_Polynomials: theory Polynomial_Factorization.Missing_Polynomial_Factorial
Power_Sum_Polynomials: theory Polynomial_Factorization.Order_Polynomial
Power_Sum_Polynomials: theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
Virtual_Substitution: theory Virtual_Substitution.ExportProofs
Power_Sum_Polynomials: theory Polynomial_Factorization.Prime_Factorization
Power_Sum_Polynomials: theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library
Power_Sum_Polynomials: theory Polynomial_Interpolation.Ring_Hom_Poly
Power_Sum_Polynomials: theory Power_Sum_Polynomials.Power_Sum_Polynomials
Finished Polynomials/outline (0:00:14 elapsed time)
Timing Polynomials (8 threads, 96.969s elapsed time, 471.730s cpu time, 44.053s GC time, factor 4.86)
Finished Polynomials (0:04:09 elapsed time, 0:08:08 cpu time, factor 1.96)
Running Myhill-Nerode ...
Power_Sum_Polynomials: theory Polynomial_Factorization.Gauss_Lemma
Preparing Functional_Ordered_Resolution_Prover/document ...
Groebner_Bases: theory Groebner_Bases.Auto_Reduction
Groebner_Bases: theory Groebner_Bases.Groebner_Bases
Power_Sum_Polynomials: theory Polynomial_Factorization.Rational_Root_Test
Factor_Algebraic_Polynomial: theory Polynomials.MPoly_Type_Class_FMap
Myhill-Nerode: theory Abstract-Rewriting.Seq
Myhill-Nerode: theory Open_Induction.Restricted_Predicates
Myhill-Nerode: theory Regular-Sets.Regular_Set
Myhill-Nerode: theory Well_Quasi_Orders.Infinite_Sequences
Myhill-Nerode: theory Well_Quasi_Orders.Least_Enum
Power_Sum_Polynomials: theory Power_Sum_Polynomials.Power_Sum_Puzzle
Finished Functional_Ordered_Resolution_Prover/document (0:00:04 elapsed time)
Preparing Functional_Ordered_Resolution_Prover/outline ...
Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.MPoly_Divide_Code
Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Multivariate_Resultant
Preparing Saturation_Framework_Extensions/document ...
PAC_Checker: theory PAC_Checker.PAC_Checker_Relation
Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly
Myhill-Nerode: theory Well_Quasi_Orders.Minimal_Elements
Finished Functional_Ordered_Resolution_Prover/outline (0:00:02 elapsed time)
Timing Functional_Ordered_Resolution_Prover (8 threads, 292.835s elapsed time, 433.520s cpu time, 25.368s GC time, factor 1.48)
Finished Functional_Ordered_Resolution_Prover (0:04:56 elapsed time, 0:07:16 cpu time, factor 1.47)
Running Well_Quasi_Orders ...
Groebner_Bases: theory Polynomials.Term_Order
PAC_Checker: theory PAC_Checker.PAC_Checker_Init
Preparing Power_Sum_Polynomials/document ...
Finished Saturation_Framework_Extensions/document (0:00:03 elapsed time)
Preparing Saturation_Framework_Extensions/outline ...
Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl
Myhill-Nerode: theory Regular-Sets.Regular_Exp
Well_Quasi_Orders: theory Abstract-Rewriting.Seq
Well_Quasi_Orders: theory Open_Induction.Restricted_Predicates
Well_Quasi_Orders: theory Well_Quasi_Orders.Infinite_Sequences
Well_Quasi_Orders: theory Regular-Sets.Regular_Set
Well_Quasi_Orders: theory Well_Quasi_Orders.Least_Enum
Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly
Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Complex_Poly
Finished Saturation_Framework_Extensions/outline (0:00:02 elapsed time)
Timing Saturation_Framework_Extensions (8 threads, 26.442s elapsed time, 63.200s cpu time, 8.586s GC time, factor 2.39)
Finished Saturation_Framework_Extensions (0:00:30 elapsed time, 0:01:06 cpu time, factor 2.17)
Running Decreasing-Diagrams-II ...
Myhill-Nerode: theory Myhill-Nerode.Folds
Myhill-Nerode: theory Regular-Sets.Derivatives
Myhill-Nerode: theory Regular-Sets.NDerivative
Myhill-Nerode: theory Regular-Sets.Relation_Interpretation
Factor_Algebraic_Polynomial: theory Factor_Algebraic_Polynomial.Factor_Real_Poly
Myhill-Nerode: theory Myhill-Nerode.Myhill_1
Finished Power_Sum_Polynomials/document (0:00:04 elapsed time)
Preparing Power_Sum_Polynomials/outline ...
Decreasing-Diagrams-II: theory Open_Induction.Restricted_Predicates
Decreasing-Diagrams-II: theory HOL-Cardinals.Order_Union
Decreasing-Diagrams-II: theory Well_Quasi_Orders.Least_Enum
Decreasing-Diagrams-II: theory Well_Quasi_Orders.Infinite_Sequences
Finished Power_Sum_Polynomials/outline (0:00:03 elapsed time)
Timing Power_Sum_Polynomials (8 threads, 33.505s elapsed time, 133.241s cpu time, 3.992s GC time, factor 3.98)
Finished Power_Sum_Polynomials (0:00:38 elapsed time, 0:02:17 cpu time, factor 3.61)
Well_Quasi_Orders: theory Open_Induction.Open_Induction
Well_Quasi_Orders: theory Well_Quasi_Orders.Multiset_Extension
Well_Quasi_Orders: theory Well_Quasi_Orders.Minimal_Elements
Decreasing-Diagrams-II: theory HOL-Cardinals.Wellorder_Extension
Running Open_Induction ...
Myhill-Nerode: theory Myhill-Nerode.Myhill_2
Preparing Factor_Algebraic_Polynomial/document ...
Myhill-Nerode: theory Myhill-Nerode.Myhill
Myhill-Nerode: theory Myhill-Nerode.Closures
Myhill-Nerode: theory Myhill-Nerode.Non_Regular_Languages
Open_Induction: theory Open_Induction.Restricted_Predicates
Decreasing-Diagrams-II: theory Well_Quasi_Orders.Multiset_Extension
Decreasing-Diagrams-II: theory Well_Quasi_Orders.Minimal_Elements
Decreasing-Diagrams-II: theory Well_Quasi_Orders.Almost_Full
Open_Induction: theory Open_Induction.Open_Induction
Well_Quasi_Orders: theory Regular-Sets.Regular_Exp
Myhill-Nerode: theory Regular-Sets.Equivalence_Checking
Preparing Open_Induction/document ...
Myhill-Nerode: theory Regular-Sets.Regexp_Method
Myhill-Nerode: theory Well_Quasi_Orders.Almost_Full
Well_Quasi_Orders: theory Regular-Sets.Relation_Interpretation
Well_Quasi_Orders: theory Regular-Sets.NDerivative
Finished Factor_Algebraic_Polynomial/document (0:00:08 elapsed time)
Preparing Factor_Algebraic_Polynomial/outline ...
Myhill-Nerode: theory Well_Quasi_Orders.Minimal_Bad_Sequences
PAC_Checker: theory PAC_Checker.PAC_Checker_Synthesis
Finished Open_Induction/document (0:00:02 elapsed time)
Preparing Open_Induction/outline ...
Myhill-Nerode: theory Well_Quasi_Orders.Almost_Full_Relations
Groebner_Bases: theory Polynomials.MPoly_Type_Class_OAlist
Myhill-Nerode: theory Well_Quasi_Orders.Well_Quasi_Orders
Well_Quasi_Orders: theory Regular-Sets.Equivalence_Checking
Decreasing-Diagrams-II: theory Well_Quasi_Orders.Minimal_Bad_Sequences
Well_Quasi_Orders: theory Regular-Sets.Regexp_Method
Well_Quasi_Orders: theory Well_Quasi_Orders.Almost_Full
Finished Open_Induction/outline (0:00:02 elapsed time)
Timing Open_Induction (8 threads, 1.524s elapsed time, 5.472s cpu time, 0.191s GC time, factor 3.59)
Finished Open_Induction (0:00:07 elapsed time, 0:00:07 cpu time, factor 0.96)
Myhill-Nerode: theory Myhill-Nerode.Closures2
Decreasing-Diagrams-II: theory Well_Quasi_Orders.Almost_Full_Relations
Finished Factor_Algebraic_Polynomial/outline (0:00:05 elapsed time)
Timing Factor_Algebraic_Polynomial (8 threads, 51.135s elapsed time, 211.435s cpu time, 15.487s GC time, factor 4.13)
Finished Factor_Algebraic_Polynomial (0:02:25 elapsed time, 0:03:41 cpu time, factor 1.52)
Preparing Myhill-Nerode/document ...
Well_Quasi_Orders: theory Well_Quasi_Orders.Higman_OI
Well_Quasi_Orders: theory Well_Quasi_Orders.Minimal_Bad_Sequences
Decreasing-Diagrams-II: theory Well_Quasi_Orders.Well_Quasi_Orders
Well_Quasi_Orders: theory Well_Quasi_Orders.Almost_Full_Relations
Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Decreasing_Diagrams_II_Aux
Well_Quasi_Orders: theory Well_Quasi_Orders.Well_Quasi_Orders
Decreasing-Diagrams-II: theory Decreasing-Diagrams-II.Decreasing_Diagrams_II
Well_Quasi_Orders: theory Well_Quasi_Orders.Kruskal
Well_Quasi_Orders: theory Well_Quasi_Orders.Wqo_Multiset
Groebner_Bases: theory Groebner_Bases.Algorithm_Schema
Groebner_Bases: theory Groebner_Bases.Syzygy
Groebner_Bases: theory Groebner_Bases.Reduced_GB
Well_Quasi_Orders: theory Well_Quasi_Orders.Kruskal_Examples
Well_Quasi_Orders: theory Well_Quasi_Orders.Wqo_Instances
Finished Myhill-Nerode/document (0:00:04 elapsed time)
Preparing Myhill-Nerode/outline ...
Preparing Well_Quasi_Orders/document ...
Preparing Decreasing-Diagrams-II/document ...
Finished Myhill-Nerode/outline (0:00:03 elapsed time)
Timing Myhill-Nerode (8 threads, 27.080s elapsed time, 72.742s cpu time, 2.633s GC time, factor 2.69)
Finished Myhill-Nerode (0:00:33 elapsed time, 0:01:16 cpu time, factor 2.25)
Groebner_Bases: theory Groebner_Bases.Groebner_PM
Groebner_Bases: theory Groebner_Bases.Benchmarks
Finished Well_Quasi_Orders/document (0:00:04 elapsed time)
Preparing Well_Quasi_Orders/outline ...
Finished Decreasing-Diagrams-II/document (0:00:03 elapsed time)
Preparing Decreasing-Diagrams-II/outline ...
Finished Decreasing-Diagrams-II/outline (0:00:02 elapsed time)
Timing Decreasing-Diagrams-II (8 threads, 10.595s elapsed time, 52.328s cpu time, 1.682s GC time, factor 4.94)
Finished Decreasing-Diagrams-II (0:00:27 elapsed time, 0:00:55 cpu time, factor 2.01)
Finished Well_Quasi_Orders/outline (0:00:03 elapsed time)
Timing Well_Quasi_Orders (8 threads, 28.300s elapsed time, 65.040s cpu time, 2.596s GC time, factor 2.30)
Finished Well_Quasi_Orders (0:00:31 elapsed time, 0:01:08 cpu time, factor 2.14)
Groebner_Bases: theory Groebner_Bases.Buchberger
Groebner_Bases: theory Groebner_Bases.F4
Groebner_Bases: theory Groebner_Bases.Algorithm_Schema_Impl
Groebner_Bases: theory Groebner_Bases.Buchberger_Examples
Groebner_Bases: theory Groebner_Bases.Reduced_GB_Examples
Groebner_Bases: theory Groebner_Bases.Syzygy_Examples
Groebner_Bases: theory Groebner_Bases.F4_Examples
PAC_Checker: theory PAC_Checker.PAC_Checker_MLton
Preparing PAC_Checker/document ...
Preparing Virtual_Substitution/document ...
Finished PAC_Checker/document (0:00:13 elapsed time)
Preparing PAC_Checker/outline ...
Finished PAC_Checker/outline (0:00:08 elapsed time)
Timing PAC_Checker (8 threads, 372.323s elapsed time, 1076.525s cpu time, 132.198s GC time, factor 2.89)
Finished PAC_Checker (0:06:16 elapsed time, 0:18:00 cpu time, factor 2.87)
Finished Virtual_Substitution/document (0:00:45 elapsed time)
Preparing Virtual_Substitution/outline ...
Finished Virtual_Substitution/outline (0:00:15 elapsed time)
Timing Virtual_Substitution (8 threads, 384.702s elapsed time, 1188.493s cpu time, 94.527s GC time, factor 3.09)
Finished Virtual_Substitution (0:06:28 elapsed time, 0:19:51 cpu time, factor 3.07)
Preparing Groebner_Bases/document ...
Finished Groebner_Bases/document (0:00:23 elapsed time)
Preparing Groebner_Bases/outline ...
Finished Groebner_Bases/outline (0:00:09 elapsed time)
Timing Groebner_Bases (8 threads, 396.400s elapsed time, 1327.811s cpu time, 170.456s GC time, factor 3.35)
Finished Groebner_Bases (0:08:48 elapsed time, 0:27:40 cpu time, factor 3.14)
Running Groebner_Macaulay ...
Running Signature_Groebner ...
Running Nullstellensatz ...
Nullstellensatz: theory HOL-Types_To_Sets.Types_To_Sets
Signature_Groebner: theory Signature_Groebner.Prelims
Nullstellensatz: theory Nullstellensatz.Algebraically_Closed_Fields
Nullstellensatz: theory Nullstellensatz.Lex_Order_PP
Nullstellensatz: theory Nullstellensatz.Univariate_PM
Groebner_Macaulay: theory Groebner_Macaulay.Binomial_Int
Groebner_Macaulay: theory Groebner_Macaulay.Dube_Prelims
Groebner_Macaulay: theory Groebner_Macaulay.Monomial_Module
Groebner_Macaulay: theory Groebner_Macaulay.Degree_Bound_Utils
Groebner_Macaulay: theory Groebner_Macaulay.Degree_Section
Signature_Groebner: theory Signature_Groebner.More_MPoly
Groebner_Macaulay: theory Groebner_Macaulay.Hilbert_Function
Groebner_Macaulay: theory Groebner_Macaulay.Poly_Fun
Nullstellensatz: theory Nullstellensatz.Nullstellensatz
Signature_Groebner: theory Signature_Groebner.Signature_Groebner
Nullstellensatz: theory Nullstellensatz.Nullstellensatz_Field
Groebner_Macaulay: theory Groebner_Macaulay.Groebner_Macaulay
Groebner_Macaulay: theory Groebner_Macaulay.Cone_Decomposition
Preparing Nullstellensatz/document ...
Finished Nullstellensatz/document (0:00:06 elapsed time)
Preparing Nullstellensatz/outline ...
Groebner_Macaulay: theory Groebner_Macaulay.Dube_Bound
Finished Nullstellensatz/outline (0:00:03 elapsed time)
Timing Nullstellensatz (8 threads, 6.404s elapsed time, 22.198s cpu time, 0.851s GC time, factor 3.47)
Finished Nullstellensatz (0:00:16 elapsed time, 0:00:31 cpu time, factor 1.89)
Groebner_Macaulay: theory Groebner_Macaulay.Groebner_Macaulay_Examples
Signature_Groebner: theory Signature_Groebner.Signature_Examples
Preparing Signature_Groebner/document ...
Finished Signature_Groebner/document (0:00:15 elapsed time)
Preparing Signature_Groebner/outline ...
Finished Signature_Groebner/outline (0:00:05 elapsed time)
Timing Signature_Groebner (8 threads, 85.233s elapsed time, 176.374s cpu time, 23.705s GC time, factor 2.07)
Finished Signature_Groebner (0:01:35 elapsed time, 0:03:06 cpu time, factor 1.96)
Preparing Groebner_Macaulay/document ...
Finished Groebner_Macaulay/document (0:00:15 elapsed time)
Preparing Groebner_Macaulay/outline ...
Finished Groebner_Macaulay/outline (0:00:05 elapsed time)
Timing Groebner_Macaulay (8 threads, 177.805s elapsed time, 296.665s cpu time, 55.520s GC time, factor 1.67)
Finished Groebner_Macaulay (0:03:07 elapsed time, 0:05:06 cpu time, factor 1.63)
Presentation in "/media/data/jenkins/workspace/isabelle-all/browser_info"
Presenting Polynomials in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Polynomials" ...
Presenting Groebner_Macaulay in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Groebner_Macaulay" ...
Presenting Virtual_Substitution in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Virtual_Substitution" ...
Presenting Groebner_Bases in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Groebner_Bases" ...
Presenting Nullstellensatz in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Nullstellensatz" ...
Presenting Decreasing-Diagrams-II in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Decreasing-Diagrams-II" ...
Presenting PAC_Checker in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/PAC_Checker" ...
Presenting Signature_Groebner in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Signature_Groebner" ...
Presenting Factor_Algebraic_Polynomial in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Factor_Algebraic_Polynomial" ...
Presenting document Decreasing-Diagrams-II/document
Presenting document Decreasing-Diagrams-II/outline
Presenting document Signature_Groebner/document
Presenting document Nullstellensatz/document
Presenting document Signature_Groebner/outline
Presenting document Nullstellensatz/outline
Presenting document Groebner_Macaulay/document
Presenting document Groebner_Macaulay/outline
Presenting document Polynomials/document
Presenting document Polynomials/outline
Presenting document Factor_Algebraic_Polynomial/document
Presenting document Factor_Algebraic_Polynomial/outline
Presenting document Groebner_Bases/document
Presenting document Virtual_Substitution/document
Presenting document Groebner_Bases/outline
Presenting document Virtual_Substitution/outline
Presenting document PAC_Checker/document
Presenting document PAC_Checker/outline
Presenting theory "Well_Quasi_Orders.Least_Enum"
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "HOL-Library.Groups_Big_Fun"
Presenting theory "HOL-Library.Groups_Big_Fun"
Presenting theory "HOL-Library.Fun_Lexorder"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "HOL-Library.Fun_Lexorder"
Presenting theory "Groebner_Macaulay.Degree_Section"
Presenting theory "Signature_Groebner.Prelims"
Presenting theory "Polynomials.MPoly_Type"
Presenting theory "HOL-Library.More_List"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "HOL-Library.More_List"
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 "Regular-Sets.Equivalence_Checking"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "Signature_Groebner.More_MPoly"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "Nullstellensatz.Algebraically_Closed_Fields"
Presenting theory "Well_Quasi_Orders.Multiset_Extension"
Presenting theory "Well_Quasi_Orders.Least_Enum"
Presenting theory "Well_Quasi_Orders.Least_Enum"
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "Nullstellensatz.Lex_Order_PP"
Presenting theory "Well_Quasi_Orders.Almost_Full"
Presenting theory "Groebner_Macaulay.Degree_Bound_Utils"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
Presenting theory "Well_Quasi_Orders.Almost_Full"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "Groebner_Macaulay.Groebner_Macaulay"
Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
Presenting theory "Polynomials.More_MPoly_Type"
Presenting theory "Polynomials.Utils"
Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
Presenting theory "Polynomials.MPoly_Type"
Presenting theory "Polynomials.MPoly_Type_Univariate"
Presenting theory "Well_Quasi_Orders.Almost_Full"
Presenting theory "HOL-Library.Poly_Mapping"
Presenting theory "HOL-Library.Poly_Mapping"
Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
Presenting theory "Groebner_Macaulay.Binomial_Int"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "Nullstellensatz.Univariate_PM"
Presenting theory "Decreasing-Diagrams-II.Decreasing_Diagrams_II_Aux"
Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
Presenting theory "Symmetric_Polynomials.Vieta"
Presenting theory "Groebner_Macaulay.Poly_Fun"
Presenting theory "Polynomials.MPoly_Type"
Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
Presenting theory "Polynomials.More_MPoly_Type"
Presenting theory "Polynomials.Utils"
Presenting theory "HOL-Cardinals.Order_Union"
Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
Presenting theory "Polynomials.More_MPoly_Type"
Presenting theory "HOL-Cardinals.Wellorder_Extension"
Presenting theory "Groebner_Bases.General"
Presenting theory "Groebner_Macaulay.Monomial_Module"
Presenting theory "HOL-Library.FuncSet"
Presenting theory "Polynomials.MPoly_Type"
Presenting theory "Groebner_Macaulay.Dube_Prelims"
Presenting theory "HOL-Algebra.Congruence"
Presenting theory "Polynomials.More_MPoly_Type"
Presenting theory "Nullstellensatz.Nullstellensatz"
Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
Presenting theory "HOL-Algebra.Order"
Presenting theory "Nullstellensatz.Nullstellensatz_Field"
Presenting theory "Decreasing-Diagrams-II.Decreasing_Diagrams_II"
Presenting Fishers_Inequality in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Fishers_Inequality" ...
Presenting document Fishers_Inequality/document
Presenting document Fishers_Inequality/outline
Presenting Linear_Recurrences_Solver in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Linear_Recurrences_Solver" ...
Presenting theory "Polynomials.Power_Products"
Presenting theory "Card_Partitions.Set_Partition"
Presenting theory "HOL-Algebra.Lattice"
Presenting theory "Groebner_Macaulay.Hilbert_Function"
Presenting theory "Nested_Multisets_Ordinals.Multiset_More"
Presenting theory "Polynomials.Power_Products"
Presenting theory "Nested_Multisets_Ordinals.Duplicate_Free_Multiset"
Presenting theory "Polynomials.More_Modules"
Presenting theory "Linear_Recurrences.RatFPS"
Presenting theory "Polynomials.More_Modules"
Presenting theory "Design_Theory.Multisets_Extras"
Presenting theory "Symmetric_Polynomials.Symmetric_Polynomials"
Presenting theory "HOL-Combinatorics.Stirling"
Presenting theory "Linear_Recurrences.Pochhammer_Polynomials"
Presenting theory "HOL-Computational_Algebra.Polynomial"
Presenting theory "HOL-Combinatorics.Multiset_Permutations"
Presenting theory "Linear_Recurrences.Linear_Recurrences_Misc"
Presenting theory "Fishers_Inequality.Set_Multiset_Extras"
Presenting theory "Well_Quasi_Orders.Least_Enum"
Presenting theory "Power_Sum_Polynomials.Power_Sum_Polynomials_Library"
Presenting theory "Linear_Recurrences.Partial_Fraction_Decomposition"
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "Polynomials.MPoly_Type_Univariate"
Presenting theory "Polynomials.MPoly_Type_Class"
Presenting theory "Linear_Recurrences.Factorizations"
Presenting theory "HOL-Algebra.Complete_Lattice"
Presenting theory "Hermite_Lindemann.More_Multivariate_Polynomial_HLW"
Presenting theory "Well_Quasi_Orders.Least_Enum"
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Linear_Recurrences.Rational_FPS_Solver"
Presenting theory "Linear_Recurrences.Linear_Recurrences_Common"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "Linear_Recurrences.Linear_Homogenous_Recurrences"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Linear_Recurrences.Eulerian_Polynomials"
Presenting theory "Polynomials.MPoly_Type_Class"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Well_Quasi_Orders.Almost_Full"
Presenting theory "Linear_Recurrences.Linear_Inhomogenous_Recurrences"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "Deriving.Compare_Rat"
Presenting theory "Deriving.Compare_Real"
Presenting theory "HOL-Algebra.Group"
Presenting theory "Well_Quasi_Orders.Almost_Full"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
Presenting theory "HOL-Algebra.FiniteProduct"
Presenting theory "HOL-Library.While_Combinator"
Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Polynomials.MPoly_Type_Class_Ordered"
Presenting theory "Algebraic_Numbers.Algebraic_Numbers_Prelim"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "Polynomials.Utils"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
Presenting theory "Polynomials.Utils"
Presenting theory "HOL-Algebra.Ring"
Presenting file "~~/src/HOL/Algebra/ringsimp.ML"
Presenting theory "Algebraic_Numbers.Bivariate_Polynomials"
Presenting theory "Algebraic_Numbers.Resultant"
Presenting theory "Polynomials.MPoly_Type"
Presenting theory "Algebraic_Numbers.Algebraic_Numbers"
Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
Presenting theory "Pure-ex.Guess"
Presenting theory "Polynomials.More_MPoly_Type"
Presenting theory "Groebner_Bases.Confluence"
Presenting theory "Sturm_Sequences.Misc_Polynomial"
Presenting theory "Polynomials.MPoly_Type_Class_Ordered"
Presenting theory "HOL-Algebra.Coset"
Presenting theory "Sturm_Sequences.Sturm_Library"
Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
Presenting theory "Polynomials.Poly_Mapping_Finite_Map"
Presenting theory "HOL-Algebra.AbelCoset"
Presenting theory "Polynomials.Power_Products"
Presenting theory "Sturm_Sequences.Sturm_Theorem"
Presenting theory "Polynomials.More_Modules"
Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
Presenting theory "Polynomials.MPoly_Type_Class_FMap"
Presenting theory "Algebraic_Numbers.Sturm_Rat"
Presenting theory "HOL-Algebra.Ideal"
Presenting theory "Polynomials.PP_Type"
Presenting theory "Deriving.Comparator"
Presenting theory "Abstract-Rewriting.SN_Orders"
Presenting theory "Algebraic_Numbers.Factors_of_Int_Poly"
Presenting theory "Algebraic_Numbers.Min_Int_Poly"
Presenting theory "Polynomials.Power_Products"
Presenting theory "Matrix.Utility"
Presenting theory "Algebraic_Numbers.Algebraic_Numbers_Pre_Impl"
Presenting theory "HOL-Library.Disjoint_Sets"
Presenting theory "Algebraic_Numbers.Cauchy_Root_Bound"
Presenting theory "HOL-Combinatorics.Transposition"
Presenting theory "Polynomials.More_Modules"
Presenting theory "Polynomials.Polynomials"
Presenting theory "Polynomials.MPoly_Type_Class"
Presenting theory "HOL-Library.Sublist"
Presenting theory "Groebner_Bases.Reduction"
Presenting theory "HOL-Library.Ramsey"
Presenting theory "Factor_Algebraic_Polynomial.Poly_Connection"
Presenting theory "Well_Quasi_Orders.Least_Enum"
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "Factor_Algebraic_Polynomial.MPoly_Divide"
Presenting theory "HOL-Combinatorics.Permutations"
Presenting theory "Polynomials.MPoly_Type_Class"
Presenting theory "Polynomials.OAlist"
Presenting theory "HOL-Combinatorics.List_Permutation"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Algebraic_Numbers.Real_Algebraic_Numbers"
Presenting theory "Well_Quasi_Orders.Almost_Full"
Presenting theory "Groebner_Macaulay.Cone_Decomposition"
Presenting theory "Algebraic_Numbers.Real_Roots"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "Polynomials.OAlist_Poly_Mapping"
Presenting theory "Groebner_Bases.Groebner_Bases"
Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
Presenting theory "Algebraic_Numbers.Complex_Roots_Real_Poly"
Presenting theory "Algebraic_Numbers.Compare_Complex"
Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
Presenting theory "Algebraic_Numbers.Interval_Arithmetic"
Presenting theory "Polynomials.Utils"
Presenting theory "Algebraic_Numbers.Complex_Algebraic_Numbers"
Presenting theory "HOL-Library.Function_Algebras"
Presenting theory "Polynomials.MPoly_Type"
Presenting theory "Signature_Groebner.Signature_Groebner"
Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
Presenting theory "Polynomials.Term_Order"
Presenting theory "Polynomials.More_MPoly_Type"
Presenting theory "Polynomials.MPoly_Type_Univariate"
Presenting theory "Symmetric_Polynomials.Vieta"
Presenting theory "HOL-Algebra.Divisibility"
Presenting theory "HOL-Algebra.RingHom"
Presenting theory "Groebner_Macaulay.Dube_Bound"
Presenting theory "Polynomials.MPoly_Type_Class_Ordered"
Presenting theory "Polynomials.MPoly_Type_Class_Ordered"
Presenting theory "Signature_Groebner.Signature_Examples"
Presenting Symmetric_Polynomials in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Symmetric_Polynomials" ...
Presenting document Symmetric_Polynomials/document
Presenting document Symmetric_Polynomials/outline
Presenting theory "Polynomials.MPoly_Type_Class_OAlist"
Presenting theory "Symmetric_Polynomials.Vieta"
Presenting theory "Polynomials.Poly_Mapping_Finite_Map"
Presenting theory "Polynomials.Power_Products"
Presenting theory "Symmetric_Polynomials.Symmetric_Polynomials"
Presenting theory "HOL-Algebra.QuotRing"
Presenting theory "Polynomials.Quasi_PM_Power_Products"
Presenting theory "Polynomials.MPoly_Type"
Presenting theory "Polynomials.More_Modules"
Presenting theory "Power_Sum_Polynomials.Power_Sum_Polynomials_Library"
Presenting theory "Groebner_Macaulay.Groebner_Macaulay_Examples"
Presenting theory "HOL-Algebra.Module"
Presenting Power_Sum_Polynomials in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Power_Sum_Polynomials" ...
Presenting document Power_Sum_Polynomials/document
Presenting document Power_Sum_Polynomials/outline
Presenting theory "Polynomials.MPoly_Type_Class_FMap"
Presenting theory "Groebner_Bases.General"
Presenting theory "Hermite_Lindemann.More_Multivariate_Polynomial_HLW"
Presenting theory "Well_Quasi_Orders.Least_Enum"
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "Factor_Algebraic_Polynomial.MPoly_Divide_Code"
Presenting theory "Factor_Algebraic_Polynomial.MPoly_Container"
Presenting theory "Polynomials.More_MPoly_Type"
Presenting theory "Factor_Algebraic_Polynomial.Multivariate_Resultant"
Presenting theory "HOL-Combinatorics.Transposition"
Presenting theory "Polynomial_Interpolation.Missing_Unsorted"
Presenting theory "Factor_Algebraic_Polynomial.Is_Int_To_Int"
Presenting theory "Groebner_Bases.More_MPoly_Type_Class"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "HOL-Combinatorics.Permutations"
Presenting theory "Polynomials.MPoly_Type_Class"
Presenting theory "Well_Quasi_Orders.Almost_Full"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "Polynomial_Interpolation.Missing_Polynomial"
Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
Presenting theory "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly"
Presenting theory "Polynomial_Factorization.Order_Polynomial"
Presenting theory "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl"
Presenting theory "Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized"
Presenting theory "Symmetric_Polynomials.Symmetric_Polynomials"
Presenting theory "Factor_Algebraic_Polynomial.Roots_via_IA"
Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
Presenting theory "Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "Factor_Algebraic_Polynomial.Factor_Complex_Poly"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Power_Sum_Polynomials.Power_Sum_Polynomials_Library"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "Polynomials.Utils"
Presenting theory "Well_Quasi_Orders.Least_Enum"
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "Factor_Algebraic_Polynomial.Factor_Real_Poly"
Presenting Myhill-Nerode in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Myhill-Nerode" ...
Presenting document Myhill-Nerode/document
Presenting document Myhill-Nerode/outline
Presenting theory "Power_Sum_Polynomials.Power_Sum_Polynomials"
Presenting theory "HOL-Algebra.UnivPoly"
Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Groebner_Bases.Macaulay_Matrix"
Presenting theory "Polynomial_Interpolation.Ring_Hom"
Presenting theory "Well_Quasi_Orders.Almost_Full"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "Polynomial_Interpolation.Ring_Hom_Poly"
Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
Presenting theory "Polynomials.Utils"
Presenting theory "Polynomial_Factorization.Missing_Polynomial_Factorial"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Myhill-Nerode.Folds"
Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
Presenting theory "HOL-Algebra.Generated_Groups"
Presenting theory "Polynomial_Factorization.Gauss_Lemma"
Presenting theory "Matrix.Utility"
Presenting theory "Fishers_Inequality.Matrix_Vector_Extras"
Presenting theory "HOL-Algebra.Elementary_Groups"
Presenting theory "Myhill-Nerode.Myhill_1"
Presenting theory "Polynomials.MPoly_Type_Class_Ordered"
Presenting theory "Myhill-Nerode.Myhill_2"
Presenting theory "Design_Theory.Design_Basics"
Presenting theory "Regular-Sets.Derivatives"
Presenting theory "Polynomial_Factorization.Missing_List"
Presenting theory "Polynomials.Power_Products"
Presenting theory "Myhill-Nerode.Myhill"
Presenting theory "Polynomial_Factorization.Missing_Multiset"
Presenting theory "Myhill-Nerode.Closures"
Presenting theory "Polynomials.Power_Products"
Presenting theory "Polynomials.More_Modules"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Design_Theory.Design_Operations"
Presenting theory "HOL-Algebra.Multiplicative_Group"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "HOL-Library.FSet"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "Polynomials.More_Modules"
Presenting theory "Design_Theory.Block_Designs"
Presenting theory "Polynomials.MPoly_Type_Class"
Presenting theory "Polynomial_Factorization.Prime_Factorization"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "Well_Quasi_Orders.Least_Enum"
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "HOL-Algebra.Ring_Divisibility"
Presenting theory "Polynomial_Factorization.Rational_Root_Test"
Presenting theory "Power_Sum_Polynomials.Power_Sum_Puzzle"
Presenting Functional_Ordered_Resolution_Prover in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Functional_Ordered_Resolution_Prover" ...
Presenting document Functional_Ordered_Resolution_Prover/document
Presenting document Functional_Ordered_Resolution_Prover/outline
Presenting theory "HOL-Algebra.Subrings"
Presenting theory "HOL-Library.AList"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Matrix.Utility"
Presenting theory "Design_Theory.BIBD"
Presenting theory "Polynomials.MPoly_Type_Class_Ordered"
Presenting theory "HOL-Library.Conditional_Parametricity"
Presenting file "~~/src/HOL/Library/conditional_parametricity.ML"
Presenting theory "Polynomials.MPoly_PM"
Presenting theory "Polynomials.Poly_Mapping_Finite_Map"
Presenting theory "Well_Quasi_Orders.Almost_Full"
Presenting theory "Fishers_Inequality.Design_Extras"
Presenting theory "Polynomials.MPoly_Type_Class_FMap"
Presenting theory "Polynomials.MPoly_Type_Class"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "Symmetric_Polynomials.Symmetric_Polynomials_Code"
Presenting Saturation_Framework in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Saturation_Framework" ...
Presenting document Saturation_Framework/document
Presenting document Saturation_Framework/outline
Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
Presenting theory "Lambda_Free_RPOs.Lambda_Free_Util"
Presenting theory "Saturation_Framework.Calculus"
Presenting theory "Saturation_Framework.Intersection_Calculus"
Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
Presenting theory "Saturation_Framework.Calculus_Variations"
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "List-Index.List_Index"
Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Myhill-Nerode.Closures2"
Presenting theory "Design_Theory.Sub_Designs"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "HOL-Library.Finite_Map"
Presenting theory "Factor_Algebraic_Polynomial.Poly_Connection"
Presenting theory "Myhill-Nerode.Non_Regular_Languages"
Presenting Saturation_Framework_Extensions in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Saturation_Framework_Extensions" ...
Presenting document Saturation_Framework_Extensions/document
Presenting document Saturation_Framework_Extensions/outline
Presenting theory "Saturation_Framework_Extensions.Soundness"
Presenting theory "HOL-Computational_Algebra.Factorial_Ring"
Presenting theory "Polynomial_Factorization.Missing_List"
Presenting theory "Saturation_Framework.Lifting_to_Non_Ground_Calculi"
Presenting theory "Polynomials.Poly_Mapping_Finite_Map"
Presenting theory "Factor_Algebraic_Polynomial.MPoly_Divide"
Presenting theory "Design_Theory.Design_Isomorphisms"
Presenting theory "Saturation_Framework.Labeled_Lifting_to_Non_Ground_Calculi"
Presenting theory "HOL-Algebra.Polynomials"
Presenting theory "Saturation_Framework_Extensions.Standard_Redundancy_Criterion"
Presenting theory "Saturation_Framework_Extensions.Clausal_Calculus"
Presenting theory "Saturation_Framework.Given_Clause_Architectures"
Presenting Well_Quasi_Orders in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Well_Quasi_Orders" ...
Presenting theory "Polynomials.MPoly_Type_Class_FMap"
Presenting document Well_Quasi_Orders/document
Presenting document Well_Quasi_Orders/outline
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "HOL-Library.Quadratic_Discriminant"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "HOL-Library.Sublist"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "Well_Quasi_Orders.Least_Enum"
Presenting theory "Lambda_Free_RPOs.Lambda_Free_Util"
Presenting theory "Well_Quasi_Orders.Almost_Full"
Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
Presenting theory "Open_Induction.Open_Induction"
Presenting theory "Saturation_Framework_Extensions.FO_Ordered_Resolution_Prover_Revisited"
Presenting theory "Well_Quasi_Orders.Higman_OI"
Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
Presenting theory "HOL-Library.Ramsey"
Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
Presenting theory "Well_Quasi_Orders.Kruskal"
Presenting theory "Well_Quasi_Orders.Kruskal_Examples"
Presenting theory "Well_Quasi_Orders.Wqo_Instances"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "Fishers_Inequality.Incidence_Matrices"
Presenting theory "Saturation_Framework_Extensions.Given_Clause_Architectures_Revisited"
Presenting Open_Induction in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Open_Induction" ...
Presenting document Open_Induction/document
Presenting document Open_Induction/outline
Presenting theory "Well_Quasi_Orders.Multiset_Extension"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Well_Quasi_Orders.Wqo_Multiset"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Fishers_Inequality.Dual_Systems"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Polynomials.MPoly_Type_Class_Ordered"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Open_Induction.Open_Induction"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "Polynomials.Poly_Mapping_Finite_Map"
Presenting theory "HOL-Computational_Algebra.Polynomial"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "Polynomials.MPoly_Type_Class_FMap"
Presenting theory "Well_Quasi_Orders.Least_Enum"
Presenting theory "Well_Quasi_Orders.Infinite_Sequences"
Presenting theory "Factor_Algebraic_Polynomial.MPoly_Divide_Code"
Presenting theory "Factor_Algebraic_Polynomial.MPoly_Container"
Presenting theory "Factor_Algebraic_Polynomial.Multivariate_Resultant"
Presenting theory "Factor_Algebraic_Polynomial.Is_Int_To_Int"
Presenting theory "Polynomials.MPoly_Type_Univariate"
Presenting theory "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly"
Presenting theory "Matrix.Utility"
Presenting theory "Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover"
Presenting theory "Factor_Algebraic_Polynomial.Roots_of_Algebraic_Poly_Impl"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Factor_Algebraic_Polynomial.Roots_via_IA"
Presenting theory "Factor_Algebraic_Polynomial.Roots_of_Real_Complex_Poly"
Presenting theory "Factor_Algebraic_Polynomial.Factor_Complex_Poly"
Presenting theory "Linear_Recurrences_Solver.Linear_Recurrences_Solver"
Presenting theory "Show.Show_Real"
Presenting theory "Show.Show_Complex"
Presenting theory "Linear_Recurrences_Solver.Linear_Recurrences_Pretty"
Presenting theory "Algebraic_Numbers.Show_Real_Alg"
Presenting theory "Algebraic_Numbers.Show_Real_Precise"
Presenting theory "Linear_Recurrences_Solver.Show_RatFPS"
Presenting theory "Linear_Recurrences_Solver.Linear_Recurrences_Test"
Presenting theory "Well_Quasi_Orders.Almost_Full"
Presenting theory "Deriving.Generator_Aux"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
Presenting theory "Well_Quasi_Orders.Minimal_Elements"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "Well_Quasi_Orders.Minimal_Bad_Sequences"
Presenting theory "Deriving.Comparator"
Presenting theory "Well_Quasi_Orders.Almost_Full_Relations"
Presenting theory "BenOr_Kozen_Reif.More_Matrix"
Presenting theory "Polynomials.Utils"
Presenting theory "HOL-Library.Function_Algebras"
Presenting theory "Polynomials.MPoly_Type"
Presenting theory "Polynomials.More_MPoly_Type"
Presenting theory "Deriving.Comparator_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/comparator_generator.ML"
Presenting theory "Fishers_Inequality.Rank_Argument_General"
Presenting theory "Well_Quasi_Orders.Well_Quasi_Orders"
Presenting theory "Deriving.Compare"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_code.ML"
Presenting theory "Fishers_Inequality.Linear_Bound_Argument"
Presenting theory "Polynomials.Polynomials"
Presenting theory "Deriving.Compare_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_generator.ML"
Presenting theory "Deriving.Compare_Instances"
Presenting theory "Fishers_Inequality.Fishers_Inequality"
Presenting theory "Polynomials.Power_Products"
Presenting theory "Polynomials.More_Modules"
Presenting theory "Deriving.Generator_Aux"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
Presenting theory "Deriving.Equality_Generator"
Presenting file "$AFP/Deriving/Equality_Generator/equality_generator.ML"
Presenting theory "Deriving.Equality_Instances"
Presenting theory "Fishers_Inequality.Vector_Matrix_Mod"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "Word_Lib.More_Arithmetic"
Presenting theory "Word_Lib.More_Divides"
Presenting theory "Fishers_Inequality.Fishers_Inequality_Variations"
Presenting theory "Fishers_Inequality.Fishers_Inequality_Root"
Presenting theory "Polynomials.MPoly_Type_Class"
Presenting theory "Show.Show"
Presenting file "$AFP/Show/show_generator.ML"
Presenting theory "HOL-Library.Countable_Set"
Presenting theory "Show.Show_Instances"
Presenting theory "Polynomials.Show_Polynomials"
Presenting theory "Polynomials.NZM"
Presenting theory "Word_Lib.More_Word"
Presenting theory "PAC_Checker.PAC_More_Poly"
Presenting theory "Word_Lib.Bit_Shifts_Infix_Syntax"
Presenting theory "Word_Lib.Most_significant_bit"
Presenting theory "Word_Lib.Least_significant_bit"
Presenting theory "HOL-Library.FSet"
Presenting theory "Word_Lib.Generic_set_bit"
Presenting theory "Word_Lib.Bit_Comprehension"
Presenting theory "Word_Lib.Signed_Division_Word"
Presenting theory "HOL-Library.Conditional_Parametricity"
Presenting file "~~/src/HOL/Library/conditional_parametricity.ML"
Presenting theory "Native_Word.Code_Target_Word_Base"
Presenting theory "Native_Word.Word_Type_Copies"
Presenting theory "Native_Word.Code_Int_Integer_Conversion"
Presenting theory "Groebner_Bases.Algorithm_Schema"
Presenting theory "Native_Word.Code_Target_Integer_Bit"
Presenting theory "Native_Word.Uint32"
Presenting theory "HOL-Library.Finite_Map"
Presenting theory "Collections.HashCode"
Presenting theory "Deriving.Hash_Generator"
Presenting file "$AFP/Deriving/Hash_Generator/hash_generator.ML"
Presenting theory "Deriving.Hash_Instances"
Presenting theory "HOL-Library.Multiset_Order"
Presenting theory "Deriving.Countable_Generator"
Presenting theory "Deriving.Derive"
Presenting theory "First_Order_Terms.Term"
Presenting theory "Virtual_Substitution.QE"
Presenting theory "Nested_Multisets_Ordinals.Multiset_More"
Presenting theory "First_Order_Terms.Unifiers"
Presenting theory "First_Order_Terms.Term_Pair_Multiset"
Presenting theory "Groebner_Bases.Buchberger"
Presenting theory "Nested_Multisets_Ordinals.Duplicate_Free_Multiset"
Presenting theory "PAC_Checker.Finite_Map_Multiset"
Presenting theory "Regular-Sets.Regular_Set"
Presenting theory "Polynomials.PP_Type"
Presenting theory "Deriving.Comparator"
Presenting theory "Regular-Sets.Regular_Exp"
Presenting theory "Regular-Sets.NDerivative"
Presenting theory "Regular-Sets.Equivalence_Checking"
Presenting theory "Regular-Sets.Relation_Interpretation"
Presenting theory "Regular-Sets.Regexp_Method"
Presenting theory "PAC_Checker.WB_Sort"
Presenting theory "Abstract-Rewriting.Seq"
Presenting theory "PAC_Checker.More_Loops"
Presenting theory "PAC_Checker.PAC_Specification"
Presenting theory "PAC_Checker.PAC_Map_Rel"
Presenting theory "Virtual_Substitution.MPolyExtension"
Presenting theory "PAC_Checker.PAC_Checker_Specification"
Presenting theory "Polynomials.OAlist"
Presenting theory "Virtual_Substitution.ExecutiblePolyProps"
Presenting theory "Abstract-Rewriting.Abstract_Rewriting"
Presenting theory "PAC_Checker.PAC_Polynomials"
Presenting theory "PAC_Checker.PAC_Polynomials_Term"
Presenting theory "Virtual_Substitution.PolyAtoms"
Presenting theory "Polynomials.OAlist_Poly_Mapping"
Presenting theory "First_Order_Terms.Abstract_Unification"
Presenting theory "Virtual_Substitution.Debruijn"
Presenting theory "PAC_Checker.PAC_Polynomials_Operations"
Presenting theory "First_Order_Terms.Option_Monad"
Presenting theory "Virtual_Substitution.Reindex"
Presenting theory "Polynomials.Term_Order"
Presenting theory "Deriving.Generator_Aux"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
Presenting theory "Virtual_Substitution.Optimizations"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "First_Order_Terms.Unification"
Presenting theory "First_Order_Terms.Fun_More"
Presenting theory "First_Order_Terms.Transitive_Closure_More"
Presenting theory "First_Order_Terms.Seq_More"
Presenting theory "Virtual_Substitution.OptimizationProofs"
Presenting theory "Show.Show"
Presenting theory "First_Order_Terms.Subsumption"
Presenting file "$AFP/Show/show_generator.ML"
Presenting theory "Polynomials.MPoly_Type_Class_OAlist"
Presenting theory "Show.Show_Instances"
Presenting theory "PAC_Checker.PAC_Misc"
Presenting theory "HOL-Cardinals.Order_Union"
Presenting theory "Virtual_Substitution.VSAlgos"
Presenting theory "Groebner_Bases.Benchmarks"
Presenting theory "Groebner_Bases.Algorithm_Schema_Impl"
Presenting theory "Groebner_Bases.Code_Target_Rat"
Presenting theory "HOL-Cardinals.Wellorder_Extension"
Presenting theory "Virtual_Substitution.Heuristic"
Presenting theory "HOL-Library.Code_Target_Int"
Presenting theory "HOL-Library.Code_Abstract_Nat"
Presenting theory "Groebner_Bases.Buchberger_Examples"
Presenting theory "HOL-Library.Code_Target_Nat"
Presenting theory "Open_Induction.Restricted_Predicates"
Presenting theory "Groebner_Bases.More_MPoly_Type_Class"
Presenting theory "PAC_Checker.PAC_Checker"
Presenting theory "Deriving.Generator_Aux"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "Native_Word.Uint64"
Presenting theory "PAC_Checker.PAC_Checker_Relation"
Presenting theory "Show.Show"
Presenting file "$AFP/Show/show_generator.ML"
Presenting theory "Groebner_Bases.Auto_Reduction"
Presenting theory "PAC_Checker.PAC_Assoc_Map_Rel"
Presenting theory "Show.Show_Instances"
Presenting theory "Polynomials.Show_Polynomials"
Presenting theory "Virtual_Substitution.PrettyPrinting"
Presenting theory "Abstract-Rewriting.Relative_Rewriting"
Presenting theory "Show.Show_Real"
Presenting theory "Virtual_Substitution.Exports"
Presenting theory "Groebner_Bases.Reduced_GB"
Presenting theory "PAC_Checker.PAC_Checker_Init"
Presenting theory "Knuth_Bendix_Order.Order_Pair"
Presenting theory "PAC_Checker.PAC_Version"
Presenting theory "Virtual_Substitution.LinearCase"
Presenting theory "Groebner_Bases.Reduced_GB_Examples"
Presenting theory "Polynomial_Interpolation.Ring_Hom"
Presenting theory "Jordan_Normal_Form.Missing_Misc"
Presenting theory "Knuth_Bendix_Order.Lexicographic_Extension"
Presenting theory "PAC_Checker.PAC_Checker_Synthesis"
Presenting theory "Jordan_Normal_Form.Missing_Ring"
Presenting theory "PAC_Checker.PAC_Checker_MLton"
Presenting theory "Jordan_Normal_Form.Conjugate"
Presenting theory "Virtual_Substitution.QuadraticCase"
Presenting theory "Knuth_Bendix_Order.Subterm_and_Context"
Presenting theory "Knuth_Bendix_Order.Term_Aux"
Presenting theory "Virtual_Substitution.EliminateVariable"
Presenting theory "Knuth_Bendix_Order.KBO"
Presenting theory "Virtual_Substitution.LuckyFind"
Presenting theory "Jordan_Normal_Form.Matrix"
Presenting theory "Virtual_Substitution.EqualityVS"
Presenting theory "Functional_Ordered_Resolution_Prover.IsaFoR_Term"
Presenting theory "Virtual_Substitution.UniAtoms"
Presenting theory "Virtual_Substitution.NegInfinity"
Presenting theory "First_Order_Terms.Abstract_Matching"
Presenting theory "First_Order_Terms.Matching"
Presenting theory "Virtual_Substitution.NegInfinityUni"
Presenting theory "Virtual_Substitution.Infinitesimals"
Presenting theory "Functional_Ordered_Resolution_Prover.Executable_Subsumption"
Presenting theory "Jordan_Normal_Form.Gauss_Jordan_Elimination"
Presenting theory "Show.Show"
Presenting file "$AFP/Show/show_generator.ML"
Presenting theory "Show.Show_Instances"
Presenting theory "Virtual_Substitution.InfinitesimalsUni"
Presenting theory "Functional_Ordered_Resolution_Prover.Executable_FO_Ordered_Resolution_Prover"
Presenting theory "Groebner_Bases.Macaulay_Matrix"
Presenting theory "Virtual_Substitution.DNFUni"
Presenting theory "Virtual_Substitution.GeneralVSProofs"
Presenting theory "Groebner_Bases.F4"
Presenting theory "Polynomial_Interpolation.Missing_Unsorted"
Presenting theory "Containers.Containers_Auxiliary"
Presenting theory "Virtual_Substitution.DNF"
Presenting theory "Deriving.Generator_Aux"
Presenting file "$AFP/Deriving/bnf_access.ML"
Presenting file "$AFP/Deriving/generator_aux.ML"
Presenting theory "Deriving.Derive_Manager"
Presenting file "$AFP/Deriving/derive_manager.ML"
Presenting theory "Containers.Containers_Generator"
Presenting file "$AFP/Containers/containers_generator.ML"
Presenting theory "Containers.Collection_Enum"
Presenting theory "Virtual_Substitution.VSQuad"
Presenting file "$AFP/Containers/cenum_generator.ML"
Presenting theory "Deriving.Equality_Generator"
Presenting file "$AFP/Deriving/Equality_Generator/equality_generator.ML"
Presenting theory "Deriving.Equality_Instances"
Presenting theory "Containers.Collection_Eq"
Presenting file "$AFP/Containers/ceq_generator.ML"
Presenting theory "Virtual_Substitution.HeuristicProofs"
Presenting theory "Containers.Equal"
Presenting theory "Containers.DList_Set"
Presenting theory "Virtual_Substitution.ExportProofs"
Presenting theory "Containers.List_Fusion"
Presenting theory "Containers.Lexicographic_Order"
Presenting theory "Containers.Extend_Partial_Order"
Presenting theory "Containers.Set_Linorder"
Presenting theory "Deriving.Comparator_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/comparator_generator.ML"
Presenting theory "Deriving.Compare"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_code.ML"
Presenting theory "Deriving.Compare_Generator"
Presenting file "$AFP/Deriving/Comparator_Generator/compare_generator.ML"
Presenting theory "Deriving.Compare_Instances"
Presenting theory "Containers.Collection_Order"
Presenting file "$AFP/Containers/ccompare_generator.ML"
Presenting theory "Containers.RBT_ext"
Presenting theory "Deriving.RBT_Comparator_Impl"
Presenting theory "Containers.RBT_Mapping2"
Presenting theory "Containers.RBT_Set2"
Presenting theory "Containers.Closure_Set"
Presenting theory "Containers.Set_Impl"
Presenting file "$AFP/Containers/set_impl_generator.ML"
Presenting theory "Jordan_Normal_Form.Matrix_IArray_Impl"
Presenting theory "Jordan_Normal_Form.Gauss_Jordan_IArray_Impl"
Presenting theory "Groebner_Bases.F4_Examples"
Presenting theory "Groebner_Bases.Syzygy"
Presenting theory "Groebner_Bases.Syzygy_Examples"
Presenting theory "Polynomials.Quasi_PM_Power_Products"
Presenting theory "Polynomials.MPoly_PM"
Presenting theory "Groebner_Bases.Groebner_PM"

=== TIMING ===

Group AFP: 0:52:01 elapsed time, 2:08:57 cpu time, factor 2.48
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:41 elapsed time, 2:08:57 cpu time, factor 7.73

=== 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