[EnvInject] - Loading node environment variables.
workermtahpc (mta_hpc) in workspace /media/data/jenkins/workspace/isabelle-all Building remotely on
[isabelle-all] $ hg showconfig paths.default
[isabelle-all] $ hg pull --rev default
http://isabelle.in.tum.de/repos/isabelle/ pulling from
https://isabelle.in.tum.de/repos/isabelle/ real URL is
[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
[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
https://foss.heptapod.net/isa-afp/afp-devel/ pulling from
[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
[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
[isabelle-all] $ /bin/sh -xe /tmp/jenkins379689937063665897.sh
### 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) ...
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
[NOTE] Package zarith is already installed (current version is 1.12). 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
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m -Xmx8g"
ML_HOME="/media/data/jenkins/.isabelle/contrib/polyml-test-bafe319bc3a6-1/x86_64_32-linux"
Session Doc/Sledgehammer (doc) Session AFP/Abortable_Linearizable_Modules (AFP) Session AFP/Abstract-Hoare-Logics (AFP) Session AFP/Ackermanns_not_PR (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/Boolos_Curious_Inference (AFP) Session AFP/BytecodeLogicJmlTypes (AFP) Session AFP/C2KA_DistributedSystems (AFP) Session AFP/Sqrt_Babylonian (AFP) Session AFP/ClockSynchInst (AFP) Session AFP/Compiling-Exceptions-Correctly (AFP) Session AFP/Complete_Non_Orders (AFP) Session AFP/ComponentDependencies (AFP) Session AFP/Concurrent_Revisions (AFP) Session AFP/Constructor_Funs (AFP) Session AFP/CryptoBasedCompositionalProperties (AFP) Session AFP/DPT-SAT-Solver (AFP) Session AFP/Dedekind_Real (AFP) Session Doc/Demo_Easychair (doc) Session Doc/Demo_FoilTeX (doc) Session AFP/Depth-First-Search (AFP) Session AFP/Digit_Expansions (AFP) Session AFP/Diophantine_Eqns_Lin_Hom (AFP) Session AFP/Example-Submission (AFP) Session AFP/FeatherweightJava (AFP) Session AFP/Featherweight_OCL (AFP) Session AFP/FileRefinement (AFP) Session AFP/FocusStreamsCaseStudies (AFP) Session AFP/Foundation_of_geometry (AFP) Session AFP/Free-Boolean-Algebra (AFP) Session AFP/Fresh_Identifiers (AFP) Session AFP/FunWithFunctions (AFP) Session AFP/FunWithTilings (AFP) Session AFP/GPU_Kernel_PL (AFP) Session AFP/General-Triangle (AFP) Session AFP/Generic_Deriving (AFP) Session AFP/GewirthPGCProof (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_Parallel (timing) Session HOL/HOL-Library (main timing) Session AFP/Approximation_Algorithms (AFP) Session AFP/ArrowImpossibilityGS (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/Card_Multisets (AFP) Session AFP/Card_Number_Partitions (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/DOM_Components (AFP) Session AFP/Shadow_SC_DOM (AFP) Session AFP/SC_DOM_Components (AFP) 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_Seq_Calc1 (AFP) Session AFP/FOL_Axiomatic (AFP) Session AFP/FOL_Harrison (AFP) Session AFP/Factored_Transition_System_Bounding (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 HOL/HOL-UNITY (timing) Session HOL/HOL-Combinatorics (main timing) 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 HOL/HOL-Analysis (main timing) Session AFP/Actuarial_Mathematics (AFP) Session AFP/Cayley_Hamilton (AFP) Session AFP/DynamicArchitectures (AFP) Session AFP/Architectural_Design_Patterns (AFP) Session AFP/Lazy-Lists-II (AFP) Session AFP/Stream_Fusion_Code (AFP) Session AFP/Complex_Geometry (AFP) Session AFP/Poincare_Disc (AFP) Session AFP/Differential_Game_Logic (AFP) Session AFP/First_Welfare_Theorem (AFP) Session HOL/HOL-Complex_Analysis (main timing) 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/Combinatorics_Words (AFP) Session AFP/Combinatorics_Words_Graph_Lemma (AFP) Session AFP/Dependent_SIFUM_Type_Systems (AFP) Session AFP/Dependent_SIFUM_Refinement (AFP) Session HOL/HOL-Homology (timing) Session HOL/HOL-Probability (main timing) Session AFP/Buffons_Needle (AFP) Session AFP/Density_Compiler (AFP) Session AFP/DiscretePricing (AFP) Session AFP/Ergodic_Theory (AFP) Session AFP/Gromov_Hyperbolicity (AFP) Session AFP/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/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/Source_Coding_Theorem (AFP) Session AFP/Irrationality_J_Hancl (AFP) Session AFP/Kuratowski_Closure_Complement (AFP) Session AFP/Laplace_Transform (AFP) Session AFP/Lower_Semicontinuous (AFP) Session AFP/Minkowskis_Theorem (AFP) Session AFP/Ptolemys_Theorem (AFP) Session AFP/Rank_Nullity_Theorem (AFP) Session AFP/Gauss_Jordan (AFP) Session AFP/Echelon_Form (AFP) Session AFP/MDP-Algorithms (AFP) Session AFP/Tarskis_Geometry (AFP) Session AFP/Chord_Segments (AFP) Session AFP/Stewart_Apollonius (AFP) Session AFP/Youngs_Inequality (AFP) 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/E_Transcendental (AFP) Session AFP/Elliptic_Curves_Group_Law (AFP) Session HOL/HOL-Data_Structures (timing) Session AFP/Efficient-Mergesort (AFP) Session HOL/HOL-Codegenerator_Test Session AFP/Query_Optimization (AFP) Session AFP/Automatic_Refinement (AFP) Session AFP/Refine_Monadic (AFP) Session AFP/Lifting_the_Exponent (AFP) Session AFP/Pratt_Certificate (AFP) Session AFP/Bertrands_Postulate (AFP) Session AFP/Prime_Harmonic_Series (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 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-Metis_Examples (timing) Session HOL/HOL-Proofs (timing) Session HOL/HOL-Proofs-Extraction (timing) Session HOL/HOL-Proofs-Lambda (timing) Session AFP/Applicative_Lifting (AFP) Session AFP/Stern_Brocot (AFP) Session AFP/HereditarilyFinite (AFP) Session AFP/Isabelle_Meta_Model (AFP) Session AFP/Stuttering_Equivalence (AFP) Session AFP/Landau_Symbols (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/Order_Lattice_Props (AFP) Session AFP/POPLmark-deBruijn (AFP) Session AFP/Pairing_Heap (AFP) Session AFP/Password_Authentication_Protocol (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_Tensor (AFP) Session AFP/Coinductive_Languages (AFP) Session AFP/Finite_Automata_HF (AFP) Session AFP/Functional-Automata (AFP) Session AFP/Posix-Lexing (AFP) Session AFP/ResiduatedTransitionSystem (AFP) Session AFP/Ribbon_Proofs (AFP) Session AFP/SATSolverVerification (AFP) Session AFP/Schutz_Spacetime (AFP) Session AFP/Selection_Heap_Sort (AFP) Session AFP/Sort_Encodings (AFP) Session AFP/Amortized_Complexity (AFP) Session AFP/Dynamic_Tables (AFP) Session AFP/Root_Balanced_Tree (AFP) Session AFP/Closest_Pair_Points (AFP) Session AFP/Stable_Matching (AFP) Session AFP/Szemeredi_Regularity (AFP) Session AFP/Roth_Arithmetic_Progressions (AFP) Session AFP/Tail_Recursive_Functions (AFP) Session AFP/TortoiseHare (AFP) Session AFP/Flyspeck-Tame (AFP) Session AFP/Twelvefold_Way (AFP) Session AFP/Vickrey_Clarke_Groves (AFP) Session HOL/HOL-MicroJava (timing) Session HOL/HOL-Nitpick_Examples Session HOL/HOL-Nominal-Examples (timing) Session AFP/Lam-ml-Normalization (AFP) Session AFP/SequentInvertibility (AFP) Session HOL/HOL-Predicate_Compile_Examples (timing) Session HOL/HOL-Quickcheck_Examples (timing) Session AFP/Cotangent_PFD_Formula (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 HOL/HOL-SET_Protocol (timing) Session HOL/HOL-SMT_Examples (timing) Session HOL/HOL-SPARK-Examples Session AFP/RIPEMD-160-SPARK (AFP) Session AFP/Banach_Steinhaus (AFP) Session AFP/Smooth_Manifolds (AFP) Session AFP/Types_To_Sets_Extension (AFP) Session HOL/HOLCF (main timing) Session AFP/HOLCF-Prelude (AFP) Session AFP/Stream-Fusion (AFP) Session AFP/WorkerWrapper (AFP) Session AFP/Hales_Jewett (AFP) Session AFP/Consensus_Refined (AFP) Session AFP/Hood_Melville_Queue (AFP) Session AFP/HotelKeyCards (AFP) Session Doc/How_to_Prove_it (no_doc) Session AFP/Hybrid_Logic (AFP) Session AFP/Hybrid_Multi_Lane_Spatial_Logic (AFP) Session AFP/IFC_Tracking (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/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/Algebraic_VCs (AFP) Session AFP/Multirelations (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/LatticeProperties (AFP) Session AFP/DataRefinementIBP (AFP) Session AFP/GraphMarkingIBP (AFP) Session AFP/Lifting_Definition_Option (AFP) Session AFP/Comparison_Sort_Lower_Bound (AFP) Session AFP/Dominance_CHK (AFP) Session AFP/InformationFlowSlicing_Inter (AFP) Session AFP/InformationFlowSlicing (AFP) Session AFP/Regression_Test_Selection (AFP) Session AFP/Quick_Sort_Cost (AFP) Session AFP/Randomised_BSTs (AFP) Session AFP/Randomised_Social_Choice (AFP) Session AFP/Fishburn_Impossibility (AFP) Session AFP/SDS_Impossibility (AFP) Session AFP/List_Interleaving (AFP) Session AFP/List_Inversions (AFP) Session AFP/Locally-Nameless-Sigma (AFP) Session AFP/Logging_Independent_Anonymity (AFP) Session AFP/Lowe_Ontological_Argument (AFP) Session AFP/Latin_Square (AFP) Session AFP/Max-Card-Matching (AFP) Session AFP/Maximum_Segment_Sum (AFP) Session AFP/Median_Of_Medians_Selection (AFP) Session AFP/Metalogic_ProofChecker (AFP) Session AFP/Modular_Assembly_Kit_Security (AFP) Session AFP/MonoBoolTranAlgebra (AFP) Session AFP/Name_Carrying_Type_Inference (AFP) Session AFP/Nash_Williams (AFP) Session AFP/No_FTL_observers (AFP) Session AFP/Incompleteness (AFP) Session AFP/Surprise_Paradox (AFP) Session AFP/Modal_Logics_for_NTS (AFP) Session AFP/Noninterference_CSP (AFP) Session AFP/Noninterference_Ipurge_Unwinding (AFP) Session AFP/Noninterference_Generic_Unwinding (AFP) Session AFP/Noninterference_Inductive_Unwinding (AFP) Session AFP/Noninterference_Sequential_Composition (AFP) Session AFP/Noninterference_Concurrent_Composition (AFP) Session AFP/Open_Induction (AFP) Session AFP/Well_Quasi_Orders (AFP) Session AFP/Decreasing-Diagrams-II (AFP) Session AFP/Myhill-Nerode (AFP) Session AFP/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/PSemigroupsConvolution (AFP) Session AFP/Package_logic (AFP) Session AFP/Combinable_Wands (AFP) Session AFP/Paraconsistency (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 AFP/Projective_Geometry (AFP) Session AFP/Proof_Strategy_Language (AFP) Session AFP/Propositional_Proof_Systems (AFP) Session AFP/Ramsey-Infinite (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/SIFUM_Type_Systems (AFP) Session AFP/Security_Protocol_Refinement (AFP) Session AFP/SenSocialChoice (AFP) Session AFP/Separation_Algebra (AFP) Session AFP/Separation_Logic_Unbounded (AFP) Session AFP/SimplifiedOntologicalArgument (AFP) Session AFP/Sliding_Window_Algorithm (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 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/Combinatorics_Words_Lyndon (AFP) Session AFP/TESL_Language (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/Typeclass_Hierarchy (doc) Session AFP/Types_Tableaus_and_Goedels_God (AFP) Session AFP/UPF_Firewall (AFP) Session AFP/Universal_Turing_Machine (AFP) Session AFP/Van_der_Waerden (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/IEEE_Floating_Point (AFP) Session AFP/IP_Addresses (AFP) Session AFP/Simple_Firewall (AFP) Session AFP/Interval_Arithmetic_Word32 (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/CAVA_Automata (AFP) Session AFP/DFS_Framework (AFP) Session AFP/Collections_Examples (AFP) Session AFP/Containers-Benchmarks (AFP) Session AFP/MFOTL_Monitor (AFP) Session AFP/Generic_Join (AFP) Session AFP/MFODL_Monitor_Optimized (AFP) Session AFP/Formula_Derivatives (AFP) Session AFP/MSO_Regex_Equivalence (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/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/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/Prime_Number_Theorem (AFP) Session AFP/Prime_Distribution_Elementary (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/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/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/Deep_Learning (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/Complex_Bounded_Operators (AFP) Session AFP/QR_Decomposition (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/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/CAVA_LTL_Modelchecker (AFP) Session AFP/Transitive-Closure (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/Iptables_Semantics (AFP) Session AFP/Iptables_Semantics_Examples (AFP) Session AFP/Mersenne_Primes (AFP) Session AFP/Separation_Logic_Imperative_HOL (AFP) Session AFP/Sepref_Prereq (AFP) Session AFP/Refine_Imperative_HOL (AFP) Session AFP/Floyd_Warshall (AFP) Session AFP/Sepref_Basic (AFP) Session AFP/Flow_Networks (AFP) Session AFP/EdmondsKarp_Maxflow (AFP) Session AFP/MFMC_Countable (AFP) Session AFP/Probabilistic_While (AFP) Session AFP/Constructive_Cryptography (AFP) Session AFP/Game_Based_Crypto (AFP) Session AFP/Multi_Party_Computation (AFP) Session AFP/Sigma_Commit_Crypto (AFP) Session AFP/Constructive_Cryptography_CM (AFP) Session AFP/Prpu_Maxflow (AFP) Session AFP/Knuth_Morris_Pratt (AFP) Session AFP/VerifyThis2018 (AFP) Session AFP/VerifyThis2019 (AFP) Session AFP/Simplicial_complexes_and_boolean_functions (AFP) Session AFP/UpDown_Scheme (AFP) Session AFP/X86_Semantics (AFP) Session AFP/CZH_Foundations (AFP) Session AFP/CZH_Elementary_Categories (AFP) Session AFP/CZH_Universal_Constructions (AFP) Session AFP/MonoidalCategory (AFP) Session AFP/Ordinal_Partitions (AFP) Session AFP/Wetzels_Problem (AFP) Session AFP/Recursion-Addition (AFP) Session AFP/Delta_System_Lemma (AFP) Session AFP/Transitive_Models (AFP) Session AFP/Independence_CH (AFP) Running Virtual_Substitution ... Running Functional_Ordered_Resolution_Prover ... Running Linear_Recurrences_Solver ... 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 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 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) 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) 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 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 Signature_Groebner ... 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 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 "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 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 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"
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
using [/media/data/jenkins/workspace/isabelle-all/bin/isabelle] Preparing site generation in out/hugo Cleaning up generated files... Build in /media/data/jenkins/workspace/isabelle-all/afp/web/index.html
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