Started by timer
Running in Durability level: MAX_SURVIVABILITY
[Pipeline] Start of Pipeline
[Pipeline] node
Running on workerlrz6 in /media/data/jenkins/workspace/isabelle-dump
[Pipeline] {
[Pipeline] stage
[Pipeline] { (Prepare)
[Pipeline] cleanWs
[WS-CLEANUP] Deleting project workspace...
[WS-CLEANUP] Deferred wipeout is used...
[WS-CLEANUP] done
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Checkout)
[Pipeline] script
[Pipeline] {
[Pipeline] httpRequest
HttpMethod: GET
URL: https://ci.isabelle.systems/jenkins/job/isabelle-all/lastSuccessfulBuild/api/xml?tree=actions[*[_class,mercurialNodeName]]&xpath=freeStyleBuild/action[@_class=%22hudson.plugins.mercurial.MercurialTagAction%22]/mercurialNodeName&wrapper=revs
Sending request to url: https://ci.isabelle.systems/jenkins/job/isabelle-all/lastSuccessfulBuild/api/xml?tree=actions[*[_class,mercurialNodeName]]&xpath=freeStyleBuild/action[@_class=%22hudson.plugins.mercurial.MercurialTagAction%22]/mercurialNodeName&wrapper=revs
Response Code: HTTP/1.1 200 OK
Success code from [100‥399]
[Pipeline] }
[Pipeline] // script
[Pipeline] checkout
$ hg clone --rev 5d750df8e89402c47faa3a268bc7864e990f0446 --noupdate https://isabelle.in.tum.de/repos/isabelle /media/data/jenkins/workspace/isabelle-dump/isabelle
adding changesets
adding manifests
adding file changes
added 73510 changesets with 201008 changes to 11315 files
new changesets a5a9c433f639:5d750df8e894
[isabelle] $ hg update --rev 5d750df8e89402c47faa3a268bc7864e990f0446
3484 files updated, 0 files merged, 0 files removed, 0 files unresolved
[isabelle] $ hg log --rev . --template {node}
[isabelle] $ hg log --rev . --template {rev}
[isabelle] $ hg id --branch
[isabelle] $ hg log --rev 5d750df8e89402c47faa3a268bc7864e990f0446 --template exists\n
exists
[isabelle] $ 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('5d750df8e89402c47faa3a268bc7864e990f0446') and not ancestors(5d750df8e89402c47faa3a268bc7864e990f0446)" --encoding UTF-8 --encodingmode replace
[isabelle] $ hg log --rev . --template {node}
[isabelle] $ hg log --rev . --template {rev}
[isabelle] $ hg id --branch
[Pipeline] checkout
$ hg clone --rev 693ae1ce0d54dd7828051617d4242a9103f1ea7f --noupdate https://foss.heptapod.net/isa-afp/afp-devel /media/data/jenkins/workspace/isabelle-dump/afp
adding changesets
adding manifests
adding file changes
added 11704 changesets with 78892 changes to 12097 files
new changesets 86acbdb19eec:693ae1ce0d54
[afp] $ hg update --rev 693ae1ce0d54dd7828051617d4242a9103f1ea7f
9671 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg id --branch
[afp] $ hg log --rev 693ae1ce0d54dd7828051617d4242a9103f1ea7f --template exists\n
exists
[afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('693ae1ce0d54dd7828051617d4242a9103f1ea7f') and not ancestors(693ae1ce0d54dd7828051617d4242a9103f1ea7f)" --encoding UTF-8 --encodingmode replace
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg id --branch
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Install)
[Pipeline] sh
+ isabelle/bin/isabelle components -a
[Pipeline] sh
+ isabelle/bin/isabelle jedit -bf
### Building graph browser ...
warning: [options] bootstrap class path not set in conjunction with -source 7
warning: [options] source value 7 is obsolete and will be removed in a future release
warning: [options] To suppress warnings about obsolete options, use -Xlint:-options.
Note: Some input files use or override a deprecated API.
Note: Recompile with -Xlint:deprecation for details.
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
3 warnings
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...
[Pipeline] sh
+ isabelle/bin/isabelle ocaml_setup
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
       opam update

[NOTE] Package zarith is already installed (current version is 1.9.1).
[Pipeline] sh
+ isabelle/bin/isabelle ghc_setup
stack will use a sandboxed GHC it installed
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
The Glorious Glasgow Haskell Compilation System, version 8.8.4
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Dump)
[Pipeline] sh
+ isabelle/bin/isabelle dump -o threads=4 -D afp/thys -b Pure -X slow -X large -X very_slow -O dump -a
Loading 735 sessions ...
### Skipping theory HOL-Import.HOL_Light_Import  (undefined HOL_LIGHT_BUNDLE)
### Skipping theory CakeML.Compiler_Test  (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
### Skipping theory CakeML_Codegen.Test_Datatypes  (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
Starting session Pure ...
Loading 130 theories ...
Processing theory Tools.Code_Generator ...
Processing theory HOL.HOL ...
Processing theory HOL.Argo ...
Processing theory HOL.SAT ...
Processing theory HOL.Ctr_Sugar ...
Processing theory HOL.Orderings ...
Processing theory HOL.Groups ...
Processing theory HOL.Lattices ...
Processing theory HOL.Set ...
Processing theory HOL.Fun ...
Processing theory HOL.Complete_Lattices ...
Processing theory HOL.Typedef ...
Processing theory HOL.Inductive ...
Processing theory HOL.Sum_Type ...
Processing theory HOL.Product_Type ...
Processing theory HOL.Complete_Partial_Order ...
Processing theory HOL.Rings ...
Processing theory HOL.Nat ...
Processing theory HOL.Meson ...
Processing theory HOL.ATP ...
Processing theory HOL.Metis ...
Processing theory HOL.Fields ...
Processing theory HOL.Finite_Set ...
Processing theory HOL.Relation ...
Processing theory HOL.Transitive_Closure ...
Processing theory HOL.Wellfounded ...
Processing theory HOL.Fun_Def_Base ...
Processing theory HOL.Hilbert_Choice ...
Processing theory HOL.Wfrec ...
Processing theory HOL.Order_Relation ...
Processing theory HOL.BNF_Wellorder_Relation ...
Processing theory HOL.BNF_Wellorder_Embedding ...
Processing theory HOL.BNF_Wellorder_Constructions ...
Processing theory HOL.Zorn ...
Processing theory HOL.BNF_Cardinal_Order_Relation ...
Processing theory HOL.BNF_Cardinal_Arithmetic ...
Processing theory HOL.BNF_Def ...
Processing theory HOL.BNF_Composition ...
Processing theory HOL.Basic_BNFs ...
Processing theory HOL.BNF_Fixpoint_Base ...
Processing theory HOL.BNF_Least_Fixpoint ...
Processing theory HOL.Basic_BNF_LFPs ...
Processing theory HOL.Transfer ...
Processing theory HOL.Num ...
Processing theory HOL.Power ...
Processing theory HOL.Groups_Big ...
Processing theory HOL.Equiv_Relations ...
Processing theory HOL.Lifting ...
Processing theory HOL.Lifting_Set ...
Processing theory HOL.Quotient ...
Processing theory HOL.Option ...
Processing theory HOL.Extraction ...
Processing theory HOL.Lattices_Big ...
Processing theory HOL.Partial_Function ...
Processing theory HOL.Fun_Def ...
Processing theory HOL.Int ...
Processing theory HOL.Euclidean_Division ...
Processing theory HOL.Parity ...
Processing theory HOL.Divides ...
Processing theory HOL.Code_Numeral ...
Processing theory HOL.Numeral_Simprocs ...
Processing theory HOL.Semiring_Normalization ...
Processing theory HOL.SMT ...
Processing theory HOL.Groebner_Basis ...
Processing theory HOL.Set_Interval ...
Processing theory HOL.Conditionally_Complete_Lattices ...
Processing theory HOL.Filter ...
Processing theory HOL.Presburger ...
Processing theory HOL.Sledgehammer ...
Processing theory HOL.List ...
Processing theory HOL.Groups_List ...
Processing theory HOL.Map ...
Processing theory HOL.Random ...
Processing theory HOL.Factorial ...
Processing theory HOL.Binomial ...
Processing theory HOL.Enum ...
Processing theory HOL.String ...
Processing theory HOL.Predicate ...
Processing theory HOL.Lazy_Sequence ...
Processing theory HOL.Limited_Sequence ...
Processing theory HOL.Typerep ...
Processing theory HOL.Code_Evaluation ...
Processing theory HOL.Quickcheck_Random ...
Processing theory HOL.GCD ...
Processing theory HOL.BNF_Greatest_Fixpoint ...
Processing theory HOL.Random_Pred ...
Processing theory HOL.Random_Sequence ...
Processing theory HOL.Quickcheck_Narrowing ...
Processing theory HOL.Quickcheck_Exhaustive ...
Processing theory HOL.Record ...
Processing theory HOL.Predicate_Compile ...
Processing theory HOL.Nitpick ...
Processing theory HOL.Nunchaku ...
Processing theory Main ...
Processing theory HOL-Examples.Drinker ...
Processing theory HOL-Proofs-ex.XML_Data ...
Processing theory HOL-Library.Cancellation ...
Processing theory HOL-Library.Code_Abstract_Nat ...
Processing theory HOL-Library.Code_Target_Nat ...
Processing theory HOL-Library.Code_Target_Int ...
Processing theory HOL-Library.Code_Target_Numeral ...
Processing theory HOL-Library.Open_State_Syntax ...
Processing theory HOL-Library.Realizers ...
Processing theory HOL-Proofs-Extraction.Warshall ...
Processing theory HOL-Proofs-Extraction.Higman ...
Processing theory HOL-Proofs-Extraction.Util ...
Processing theory HOL-Proofs-Lambda.Commutation ...
Processing theory HOL-Proofs-Extraction.QuotRem ...
Processing theory HOL-Proofs-Extraction.Greatest_Common_Divisor ...
Processing theory HOL-Proofs-Lambda.ListOrder ...
Processing theory HOL-Proofs-ex.Hilbert_Classical ...
Processing theory HOL-Proofs-ex.Proof_Terms ...
Processing theory HOL-Proofs-Lambda.Lambda ...
Processing theory HOL-Proofs-Lambda.ListApplication ...
Processing theory HOL-Proofs-Extraction.Higman_Extraction ...
Processing theory HOL-Proofs-Lambda.ListBeta ...
Processing theory HOL-Proofs-Lambda.InductTermi ...
Processing theory HOL-Proofs-Lambda.NormalForm ...
Processing theory HOL-Proofs-Lambda.Standardization ...
Processing theory HOL-Proofs-Lambda.LambdaType ...
Processing theory HOL-Proofs-Lambda.ParRed ...
Processing theory HOL-Proofs-Lambda.Eta ...
Processing theory HOL-Proofs-Lambda.StrongNorm ...
Processing theory HOL-Library.Multiset ...
Processing theory HOL-Proofs-Extraction.Pigeonhole ...
Removing 17 theories ...
Processing theory HOL-Computational_Algebra.Factorial_Ring ...
Processing theory HOL-Computational_Algebra.Euclidean_Algorithm ...
Processing theory HOL-Computational_Algebra.Primes ...
Processing theory HOL-Proofs-Extraction.Euclid ...
Processing theory HOL-Proofs-Lambda.WeakNorm ...
Starting session Pure ...
Loading 248 theories ...
Processing theory HOL.Hull ...
Processing theory HOL-Library.Disjoint_Sets ...
Processing theory HOL.Modules ...
Processing theory HOL-Library.FuncSet ...
Processing theory HOL-Library.Infinite_Set ...
Processing theory HOL-Library.Nat_Bijection ...
Processing theory HOL.Archimedean_Field ...
Processing theory HOL.Rat ...
Processing theory HOL.Real ...
Processing theory HOL-Library.Old_Datatype ...
Processing theory HOL-Library.Countable ...
Processing theory HOL-Library.Countable_Set ...
Processing theory HOL-Library.Set_Idioms ...
Processing theory HOL-Library.Product_Plus ...
Processing theory HOL-Library.Product_Order ...
Processing theory HOL.Vector_Spaces ...
Processing theory HOL-Library.Countable_Complete_Lattices ...
Processing theory HOL-Library.Phantom_Type ...
Processing theory HOL-Library.Cardinality ...
Processing theory HOL-Combinatorics.Permutations ...
Processing theory HOL-Library.Set_Algebras ...
Processing theory HOL-Library.Numeral_Type ...
Processing theory HOL.Topological_Spaces ...
Processing theory HOL.Real_Vector_Spaces ...
Processing theory HOL.Inequalities ...
Processing theory HOL-Analysis.Metric_Arith ...
Processing theory HOL.Limits ...
Processing theory HOL.Series ...
Processing theory HOL.Deriv ...
Processing theory HOL.NthRoot ...
Processing theory HOL.Transcendental ...
Processing theory HOL.Complex ...
Processing theory HOL.MacLaurin ...
Processing theory Complex_Main ...
Processing theory HOL-Analysis.Continuum_Not_Denumerable ...
Processing theory HOL-Analysis.Inner_Product ...
Processing theory HOL-Analysis.L2_Norm ...
Processing theory HOL-Analysis.Operator_Norm ...
Processing theory HOL-Analysis.Poly_Roots ...
Processing theory HOL-Analysis.Product_Vector ...
Processing theory HOL-Analysis.Euclidean_Space ...
Processing theory HOL-Analysis.Finite_Cartesian_Product ...
Processing theory HOL-Analysis.Linear_Algebra ...
Processing theory HOL-Analysis.Elementary_Topology ...
Processing theory HOL-Library.Discrete ...
Processing theory HOL-Library.Indicator_Function ...
Processing theory HOL-Library.Liminf_Limsup ...
Processing theory HOL-Analysis.Affine ...
Processing theory HOL-Analysis.Cartesian_Space ...
Processing theory HOL-Analysis.Determinants ...
Processing theory HOL-Computational_Algebra.Formal_Power_Series ...
Processing theory HOL-Library.Nonpos_Ints ...
Processing theory HOL-Library.Order_Continuity ...
Processing theory HOL-Library.Sum_of_Squares ...
Processing theory HOL-Library.Extended_Nat ...
Processing theory HOL-Library.Periodic_Fun ...
Processing theory HOL-Analysis.Norm_Arith ...
Processing theory HOL-Analysis.Convex ...
Processing theory HOL-Analysis.Abstract_Topology ...
Processing theory HOL-Analysis.Abstract_Limits ...
Processing theory HOL-Library.Landau_Symbols ...
Processing theory HOL-Analysis.Abstract_Topology_2 ...
Processing theory HOL-Analysis.Connected ...
Processing theory HOL-Analysis.Elementary_Metric_Spaces ...
Processing theory HOL-Library.Extended_Real ...
Processing theory HOL-Analysis.Function_Topology ...
Processing theory HOL-Analysis.Product_Topology ...
Processing theory HOL-Analysis.Function_Metric ...
Processing theory HOL-Analysis.Elementary_Normed_Spaces ...
Processing theory HOL-Library.Extended_Nonnegative_Real ...
Processing theory HOL-Analysis.Sigma_Algebra ...
Processing theory HOL-Analysis.T1_Spaces ...
Processing theory HOL-Analysis.Measurable ...
Processing theory HOL-Analysis.Topology_Euclidean_Space ...
Processing theory HOL-Analysis.Lindelof_Spaces ...
Processing theory HOL-Analysis.Convex_Euclidean_Space ...
Processing theory HOL-Analysis.Extended_Real_Limits ...
Processing theory HOL-Analysis.Summation_Tests ...
Processing theory HOL-Analysis.Uniform_Limit ...
Processing theory HOL-Analysis.Bounded_Continuous_Function ...
Processing theory HOL-Analysis.Measure_Space ...
Processing theory HOL-Analysis.Caratheodory ...
Processing theory HOL-Analysis.Ordered_Euclidean_Space ...
Processing theory HOL-Analysis.Line_Segment ...
Processing theory HOL-Analysis.Bounded_Linear_Function ...
Processing theory HOL-Analysis.Derivative ...
Processing theory HOL-Analysis.Tagged_Division ...
Processing theory HOL-Analysis.Cartesian_Euclidean_Space ...
Processing theory HOL-Analysis.Complex_Analysis_Basics ...
Processing theory HOL-Analysis.Cross3 ...
Processing theory HOL-Analysis.Borel_Space ...
Processing theory HOL-Analysis.Lipschitz ...
Processing theory HOL-Analysis.Regularity ...
Processing theory HOL-Analysis.Starlike ...
Processing theory HOL-Analysis.Continuous_Extension ...
Processing theory HOL-Analysis.Multivariate_Analysis ...
Processing theory HOL-Analysis.Nonnegative_Lebesgue_Integration ...
Processing theory HOL-Analysis.Binary_Product_Measure ...
Processing theory HOL-Analysis.Embed_Measure ...
Processing theory HOL-Analysis.Complex_Transcendental ...
Processing theory HOL-Analysis.Generalised_Binomial_Theorem ...
Processing theory HOL-Analysis.FPS_Convergence ...
Processing theory HOL-Analysis.Harmonic_Numbers ...
Processing theory HOL-Analysis.Infinite_Products ...
Processing theory HOL-Analysis.Finite_Product_Measure ...
Processing theory HOL-Analysis.Path_Connected ...
Processing theory HOL-Analysis.Locally ...
Processing theory HOL-Analysis.Bochner_Integration ...
Processing theory HOL-Analysis.Complete_Measure ...
Processing theory HOL-Analysis.Arcwise_Connected ...
Processing theory HOL-Analysis.Polytope ...
Processing theory HOL-Analysis.Radon_Nikodym ...
Processing theory HOL-Analysis.Weierstrass_Theorems ...
Processing theory HOL-Analysis.Set_Integral ...
Processing theory HOL-Analysis.Infinite_Set_Sum ...
Processing theory HOL-Analysis.Lebesgue_Measure ...
Processing theory HOL-Analysis.Homotopy ...
Processing theory HOL-Analysis.Abstract_Euclidean_Space ...
Processing theory HOL-Analysis.Homeomorphism ...
Processing theory HOL-Analysis.Brouwer_Fixpoint ...
Processing theory HOL-Analysis.Henstock_Kurzweil_Integration ...
Processing theory HOL-Analysis.Integral_Test ...
Processing theory HOL-Analysis.Fashoda_Theorem ...
Processing theory HOL-Analysis.Retracts ...
Processing theory HOL-Analysis.Smooth_Paths ...
Processing theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration ...
Processing theory HOL-Analysis.Interval_Integral ...
Processing theory HOL-Analysis.Lebesgue_Integral_Substitution ...
Processing theory HOL-Analysis.Vitali_Covering_Theorem ...
Processing theory HOL-Analysis.Gamma_Function ...
Processing theory HOL-Analysis.Ball_Volume ...
Processing theory HOL-Analysis.Improper_Integral ...
Processing theory HOL-Analysis.Equivalence_Measurable_On_Borel ...
Processing theory HOL-Analysis.Further_Topology ...
Processing theory HOL-Analysis.Jordan_Curve ...
Processing theory HOL-Analysis.Change_Of_Vars ...
Processing theory HOL-Analysis.Simplex_Content ...
Processing theory HOL-Analysis.Analysis ...
Processing theory HOL-Complex_Analysis.Contour_Integration ...
Processing theory HOL-Complex_Analysis.Cauchy_Integral_Theorem ...
Processing theory HOL-Complex_Analysis.Winding_Numbers ...
Processing theory HOL-Complex_Analysis.Cauchy_Integral_Formula ...
Processing theory HOL-Complex_Analysis.Conformal_Mappings ...
Processing theory HOL-Complex_Analysis.Complex_Singularities ...
Processing theory HOL-Complex_Analysis.Complex_Residues ...
Processing theory HOL-Complex_Analysis.Residue_Theorem ...
Processing theory HOL-Complex_Analysis.Great_Picard ...
Processing theory HOL-Complex_Analysis.Riemann_Mapping ...
Loading 48 theories ...
Processing theory HOL-Complex_Analysis.Complex_Analysis ...
Removing 11 theories ...
Processing theory HOL-Library.Lattice_Syntax ...
Processing theory HOL-Library.Adhoc_Overloading ...
Processing theory HOL-Library.Monad_Syntax ...
Processing theory HOL-Library.Conditional_Parametricity ...
Processing theory HOL-Library.Rewrite ...
Processing theory HOL-Library.Mapping ...
Processing theory HOL-Library.AList ...
Processing theory HOL-Library.AList_Mapping ...
Processing theory HOL-Library.Stream ...
Processing theory HOL-Library.Complete_Partial_Order2 ...
Processing theory HOL-Library.Diagonal_Subsequence ...
Processing theory HOL-Probability.Discrete_Topology ...
Processing theory HOL-Probability.Essential_Supremum ...
Processing theory HOL-Combinatorics.Multiset_Permutations ...
Processing theory HOL-Probability.Stopping_Time ...
Processing theory HOL-Library.FSet ...
Processing theory HOL-Library.Sublist ...
Processing theory HOL-Library.Tree ...
Processing theory HOL-Library.Linear_Temporal_Logic_on_Streams ...
Processing theory HOL-Probability.Tree_Space ...
Processing theory HOL-Probability.Probability_Measure ...
Processing theory HOL-Probability.Distribution_Functions ...
Processing theory HOL-Probability.Weak_Convergence ...
Processing theory HOL-Probability.Helly_Selection ...
Processing theory HOL-Library.Finite_Map ...
Processing theory HOL-Probability.Fin_Map ...
Processing theory HOL-Probability.Conditional_Expectation ...
Processing theory HOL-Probability.Giry_Monad ...
Processing theory HOL-Probability.Projective_Family ...
Processing theory HOL-Probability.Infinite_Product_Measure ...
Processing theory HOL-Probability.Stream_Space ...
Processing theory HOL-Probability.Probability_Mass_Function ...
Processing theory HOL-Probability.PMF_Impl ...
Processing theory HOL-Probability.Random_Permutations ...
Processing theory HOL-Probability.Projective_Limit ...
Processing theory HOL-Probability.Independent_Family ...
Processing theory HOL-Probability.Convolution ...
Processing theory HOL-Probability.Product_PMF ...
Processing theory HOL-Probability.Hoeffding ...
Processing theory HOL-Probability.SPMF ...
Processing theory HOL-Probability.Information ...
Processing theory HOL-Probability.Distributions ...
Processing theory HOL-Probability.Characteristic_Functions ...
Processing theory HOL-Probability.Sinc_Integral ...
Processing theory HOL-Probability.Levy ...
Processing theory HOL-Probability.Central_Limit_Theorem ...
Processing theory HOL-Probability.Probability ...
Processing theory HOL-Probability-ex.Measure_Not_CCC ...
Processing theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure ...
Removing 26 theories ...
Processing theory HOL-Probability-ex.Dining_Cryptographers ...
Loading 39 theories ...
Processing theory HOL-Cardinals.Fun_More ...
Processing theory HOL-Cardinals.Order_Union ...
Processing theory HOL-Library.Fun_Lexorder ...
Processing theory HOL-Algebra.Congruence ...
Processing theory HOL-Library.Groups_Big_Fun ...
Processing theory HOL-Library.More_List ...
Processing theory HOL-Cardinals.Order_Relation_More ...
Processing theory HOL-Cardinals.Wellfounded_More ...
Processing theory HOL-Cardinals.Wellorder_Relation ...
Processing theory HOL-Cardinals.Wellorder_Embedding ...
Processing theory HOL-Cardinals.Wellorder_Constructions ...
Processing theory HOL-Library.Equipollence ...
Processing theory HOL-Cardinals.Cardinal_Order_Relation ...
Processing theory HOL-Cardinals.Cardinal_Arithmetic ...
Processing theory HOL-Algebra.Order ...
Processing theory HOL-Algebra.Lattice ...
Processing theory HOL-Library.Poly_Mapping ...
Processing theory HOL-Algebra.Complete_Lattice ...
Removing 58 theories ...
Processing theory HOL-Algebra.Group ...
Processing theory HOL-Algebra.FiniteProduct ...
Processing theory HOL-Algebra.Coset ...
Processing theory HOL-Algebra.Generated_Groups ...
Processing theory HOL-Algebra.Solvable_Groups ...
Processing theory HOL-Algebra.Ring ...
Processing theory HOL-Algebra.AbelCoset ...
Processing theory HOL-Algebra.Module ...
Processing theory HOL-Algebra.Elementary_Groups ...
Processing theory HOL-Algebra.Product_Groups ...
Processing theory HOL-Algebra.Ideal ...
Processing theory HOL-Algebra.RingHom ...
Processing theory HOL-Algebra.Exact_Sequence ...
Processing theory HOL-Algebra.Free_Abelian_Groups ...
Processing theory HOL-Algebra.UnivPoly ...
Processing theory HOL-Algebra.Multiplicative_Group ...
Processing theory HOL-Homology.Simplices ...
Processing theory HOL-Homology.Homology_Groups ...
Processing theory HOL-Homology.Brouwer_Degree ...
Processing theory HOL-Homology.Invariance_of_Domain ...
Processing theory HOL-Homology.Homology ...
Removing 15 theories ...
Processing theory HOL-Analysis-ex.Approximations ...
Processing theory HOL-Analysis-ex.Metric_Arith_Examples ...
Loading 97 theories ...
Removing 32 theories ...
Processing theory HOL-Data_Structures.Less_False ...
Processing theory HOL-Data_Structures.Sorted_Less ...
Processing theory HOL-Computational_Algebra.Fraction_Field ...
Processing theory HOL-Computational_Algebra.Group_Closure ...
Processing theory HOL-Data_Structures.AList_Upd_Del ...
Processing theory HOL-Data_Structures.Map_Specs ...
Processing theory HOL-Data_Structures.Cmp ...
Processing theory HOL-Data_Structures.List_Ins_Del ...
Processing theory HOL-Data_Structures.Set_Specs ...
Processing theory HOL-Library.BNF_Axiomatization ...
Processing theory HOL-Library.BNF_Corec ...
Processing theory HOL-Library.Boolean_Algebra ...
Processing theory HOL-Computational_Algebra.Normalized_Fraction ...
Processing theory HOL-Computational_Algebra.Nth_Powers ...
Processing theory HOL-Computational_Algebra.Squarefree ...
Processing theory HOL-Library.Multiset_Order ...
Processing theory HOL-Library.Case_Converter ...
Processing theory HOL-Library.Code_Lazy ...
Processing theory HOL-Library.Simps_Case_Conv ...
Processing theory HOL-Library.State_Monad ...
Processing theory HOL-Library.Confluence ...
Processing theory HOL-Examples.Records ...
Processing theory HOL-Library.Code_Test ...
Processing theory HOL-Library.Comparator ...
Processing theory HOL-Library.Confluent_Quotient ...
Processing theory HOL-Library.Dlist ...
Processing theory HOL-Library.Debug ...
Processing theory HOL-Library.Dual_Ordered_Lattice ...
Processing theory HOL-Library.Function_Algebras ...
Processing theory HOL-Library.Function_Division ...
Processing theory HOL-Library.Extended ...
Processing theory HOL-Library.IArray ...
Processing theory HOL-Library.Char_ord ...
Processing theory HOL-Library.Combine_PER ...
Processing theory HOL-Library.Disjoint_FSets ...
Processing theory HOL-Library.ListVector ...
Processing theory HOL-Library.Omega_Words_Fun ...
Processing theory HOL-Library.Option_ord ...
Processing theory HOL-Library.Pattern_Aliases ...
Processing theory HOL-Library.Type_Length ...
Processing theory HOL-Library.Saturated ...
Processing theory HOL-Library.Power_By_Squaring ...
Processing theory HOL-Library.Countable_Set_Type ...
Processing theory HOL-Library.Perm ...
Processing theory HOL-Library.Preorder ...
Processing theory HOL-Library.Quotient_Syntax ...
Processing theory HOL-Library.Quotient_Option ...
Processing theory HOL-Library.Quotient_Product ...
Processing theory HOL-Library.Parallel ...
Processing theory HOL-Library.Bit_Operations ...
Processing theory HOL-Library.Lattice_Constructions ...
Processing theory HOL-Library.Quotient_Set ...
Processing theory HOL-Library.Quotient_List ...
Processing theory HOL-Library.Quotient_Sum ...
Processing theory HOL-Library.Quotient_Type ...
Processing theory HOL-Library.Reflection ...
Processing theory HOL-Library.Subseq_Order ...
Processing theory HOL-Library.Ramsey ...
Processing theory HOL-Library.Signed_Division ...
Processing theory HOL-Library.Transitive_Closure_Table ...
Processing theory HOL-Library.Finite_Lattice ...
Processing theory HOL-Library.Tree_Multiset ...
Processing theory HOL-Library.While_Combinator ...
Processing theory HOL-Library.Sorting_Algorithms ...
Processing theory HOL-Library.Uprod ...
Processing theory HOL-Library.Bourbaki_Witt_Fixpoint ...
Processing theory HOL-Library.Z2 ...
Processing theory HOL-Data_Structures.Tree_Set ...
Processing theory HOL-Data_Structures.Tree_Map ...
Processing theory HOL-Number_Theory.Eratosthenes ...
Processing theory HOL-Library.BigO ...
Processing theory HOL-Library.Going_To_Filter ...
Processing theory HOL-Library.Log_Nat ...
Processing theory HOL-Library.Lub_Glb ...
Processing theory HOL-Library.Quadratic_Discriminant ...
Processing theory HOL-Library.Tree_Real ...
Processing theory HOL-Library.Word ...
Processing theory HOL-Library.Lattice_Algebras ...
Processing theory HOL-Library.Interval ...
Processing theory HOL-Computational_Algebra.Polynomial ...
Processing theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra ...
Processing theory HOL-Computational_Algebra.Polynomial_FPS ...
Processing theory HOL-Computational_Algebra.Formal_Laurent_Series ...
Processing theory HOL-Library.Float ...
Processing theory HOL-Library.Interval_Float ...
Processing theory HOL-Computational_Algebra.Polynomial_Factorial ...
Processing theory HOL-Computational_Algebra.Computational_Algebra ...
Processing theory HOL-Library.Library ...
Processing theory HOL-Library.RBT_Impl ...
Processing theory HOL-Library.RBT ...
Processing theory HOL-Codegenerator_Test.Candidates ...
Processing theory HOL-Codegenerator_Test.Generate_Target_Nat ...
Loading 6 theories ...
Processing theory HOL-Library.Product_Lexorder ...
Processing theory HOL-Library.RBT_Mapping ...
Processing theory HOL-Library.RBT_Set ...
Processing theory HOL-Library.DAList ...
Processing theory HOL-Library.DAList_Multiset ...
Removing 1 theories ...
Processing theory HOL-Codegenerator_Test.Generate_Efficient_Datastructures ...
Loading 2 theories ...
Processing theory HOL-Library.Code_Binary_Nat ...
Removing 4 theories ...
Processing theory HOL-Codegenerator_Test.Generate_Binary_Nat ...
Removing 1 theories ...
Processing theory HOL-Codegenerator_Test.Generate ...
Loading 12 theories ...
Processing theory HOL-Real_Asymp.Inst_Existentials ...
Processing theory HOL-Real_Asymp.Eventuallize ...
Processing theory HOL-Real_Asymp.Lazy_Eval ...
Processing theory HOL-Decision_Procs.Dense_Linear_Order ...
Removing 56 theories ...
Processing theory HOL-Decision_Procs.Approximation_Bounds ...
Processing theory HOL-Real_Asymp.Multiseries_Expansion ...
Processing theory HOL-Real_Asymp.Multiseries_Expansion_Bounds ...
Processing theory HOL-Real_Asymp.Real_Asymp ...
Processing theory HOL-Real_Asymp-Manual.Real_Asymp_Doc ...
Processing theory HOL-Decision_Procs.Approximation ...
Processing theory HOL-Real_Asymp.Real_Asymp_Approx ...
Removing 2 theories ...
Processing theory HOL-Real_Asymp.Real_Asymp_Examples ...
Loading 26 theories ...
Processing theory HOL-Algebra.Exponent ...
Processing theory HOL-Algebra.Bij ...
Processing theory HOL-Combinatorics.List_Permutation ...
Processing theory HOL-Algebra.Sylow ...
Processing theory HOL-Algebra.Galois_Connection ...
Removing 8 theories ...
Processing theory HOL-Algebra.Group_Action ...
Processing theory HOL-Algebra.Zassenhaus ...
Processing theory HOL-Algebra.Ideal_Product ...
Processing theory HOL-Algebra.QuotRing ...
Processing theory HOL-Algebra.Weak_Morphisms ...
Processing theory HOL-Combinatorics.Cycles ...
Processing theory HOL-Algebra.Sym_Groups ...
Processing theory HOL-Algebra.Divisibility ...
Processing theory HOL-Algebra.Subrings ...
Processing theory HOL-Algebra.Generated_Rings ...
Processing theory HOL-Algebra.IntRing ...
Processing theory HOL-Algebra.Chinese_Remainder ...
Processing theory HOL-Algebra.Generated_Fields ...
Processing theory HOL-Algebra.Ring_Divisibility ...
Processing theory HOL-Algebra.Embedded_Algebras ...
Processing theory HOL-Algebra.Polynomials ...
Processing theory HOL-Algebra.Polynomial_Divisibility ...
Processing theory HOL-Algebra.Indexed_Polynomials ...
Processing theory HOL-Algebra.Finite_Extensions ...
Processing theory HOL-Algebra.Algebraic_Closure ...
Loading 19 theories ...
Processing theory HOL-Algebra.Algebra ...
Processing theory HOL-Decision_Procs.DP_Library ...
Processing theory HOL-Library.Old_Recdef ...
Processing theory HOL-Decision_Procs.Conversions ...
Processing theory HOL-Decision_Procs.Algebra_Aux ...
Removing 32 theories ...
Processing theory HOL-Decision_Procs.Commutative_Ring ...
Processing theory HOL-Decision_Procs.Commutative_Ring_Complete ...
Processing theory HOL-Decision_Procs.Reflective_Field ...
Processing theory HOL-Decision_Procs.Commutative_Ring_Ex ...
Processing theory HOL-Decision_Procs.Ferrack ...
Processing theory HOL-Decision_Procs.Dense_Linear_Order_Ex ...
Processing theory HOL-Decision_Procs.Approximation_Ex ...
Processing theory HOL-Decision_Procs.Approximation_Quickcheck_Ex ...
Processing theory HOL-Decision_Procs.Rat_Pair ...
Processing theory HOL-Decision_Procs.Polynomial_List ...
Processing theory HOL-Decision_Procs.Reflected_Multivariate_Polynomial ...
Processing theory HOL-Decision_Procs.Cooper ...
Processing theory HOL-Decision_Procs.Parametric_Ferrante_Rackoff ...
Processing theory HOL-Decision_Procs.MIR ...
Loading 21 theories ...
Processing theory HOL-Decision_Procs.Decision_Procs ...
Processing theory HOL-Nonstandard_Analysis.Free_Ultrafilter ...
Processing theory HOL-Nonstandard_Analysis.StarDef ...
Processing theory HOL-Nonstandard_Analysis.HyperNat ...
Processing theory HOL-Nonstandard_Analysis.HyperDef ...
Processing theory HOL-Nonstandard_Analysis.NSA ...
Processing theory HOL-Nonstandard_Analysis.NSComplex ...
Processing theory HOL-Nonstandard_Analysis.Star ...
Processing theory HOL-Nonstandard_Analysis.HLim ...
Processing theory HOL-Nonstandard_Analysis.HDeriv ...
Processing theory HOL-Nonstandard_Analysis.NatStar ...
Processing theory HOL-Nonstandard_Analysis.HSEQ ...
Processing theory HOL-Nonstandard_Analysis.HSeries ...
Processing theory HOL-Nonstandard_Analysis.HTranscendental ...
Loading 12 theories ...
Processing theory HOL-Nonstandard_Analysis.HLog ...
Processing theory HOL-Nonstandard_Analysis.Hyperreal ...
Processing theory HOL-Nonstandard_Analysis-Examples.NSPrimes ...
Processing theory HOL-Nonstandard_Analysis.NSCA ...
Processing theory HOL-Nonstandard_Analysis.CStar ...
Processing theory HOL-Nonstandard_Analysis.CLim ...
Processing theory HOL-Nonstandard_Analysis.Hypercomplex ...
Processing theory HOL-Nonstandard_Analysis.Nonstandard_Analysis ...
Removing 46 theories ...
Processing theory HOL-Number_Theory.Cong ...
Processing theory HOL-Number_Theory.Mod_Exp ...
Processing theory HOL-Number_Theory.Fib ...
Processing theory HOL-Number_Theory.Prime_Powers ...
Processing theory HOL-Number_Theory.Totient ...
Processing theory HOL-Number_Theory.Residues ...
Processing theory HOL-Number_Theory.Euler_Criterion ...
Processing theory HOL-Number_Theory.Gauss ...
Processing theory HOL-Number_Theory.Pocklington ...
Processing theory HOL-Number_Theory.Residue_Primitive_Roots ...
Processing theory HOL-Number_Theory.Quadratic_Reciprocity ...
Processing theory HOL-Number_Theory.Number_Theory ...
Loading 73 theories ...
Processing theory HOL-Matrix_LP.Compute_Oracle ...
Processing theory HOLCF.Porder ...
Processing theory HOLCF.Pcpo ...
Processing theory HOLCF.Cont ...
Processing theory HOLCF.Adm ...
Processing theory HOLCF.Cpodef ...
Processing theory HOLCF.Fun_Cpo ...
Processing theory HOLCF.Product_Cpo ...
Processing theory HOLCF.Cfun ...
Processing theory HOLCF.Completion ...
Processing theory HOLCF.Cprod ...
Processing theory HOLCF.Deflation ...
Processing theory HOLCF.Fix ...
Processing theory HOLCF.Sfun ...
Processing theory HOLCF.Sprod ...
Processing theory HOL-Hahn_Banach.Zorn_Lemma ...
Processing theory HOLCF.Discrete ...
Processing theory HOL-Hahn_Banach.Bounds ...
Processing theory HOL-Hahn_Banach.Vector_Space ...
Processing theory HOL-Hahn_Banach.Linearform ...
Processing theory HOL-Hahn_Banach.Subspace ...
Processing theory HOL-Hahn_Banach.Function_Order ...
Processing theory HOL-Hahn_Banach.Normed_Space ...
Processing theory HOL-Hahn_Banach.Function_Norm ...
Processing theory HOL-Hahn_Banach.Hahn_Banach_Ext_Lemmas ...
Processing theory HOL-Hahn_Banach.Hahn_Banach_Sup_Lemmas ...
Processing theory HOL-Hahn_Banach.Hahn_Banach_Lemmas ...
Processing theory HOL-Hahn_Banach.Hahn_Banach ...
Processing theory HOL-Matrix_LP.LP ...
Processing theory HOL-Matrix_LP.ComputeHOL ...
Processing theory HOLCF.Up ...
Processing theory HOLCF.Lift ...
Processing theory HOLCF.One ...
Processing theory HOLCF.Tr ...
Processing theory HOLCF.Ssum ...
Processing theory HOLCF.Fixrec ...
Processing theory HOL-Matrix_LP.ComputeFloat ...
Processing theory HOL-Matrix_LP.ComputeNumeral ...
Processing theory HOLCF.Map_Functions ...
Processing theory HOLCF.Domain_Aux ...
Processing theory HOLCF.Bifinite ...
Processing theory HOLCF.Universal ...
Processing theory HOLCF.Algebraic ...
Processing theory HOLCF.Compact_Basis ...
Processing theory HOLCF.LowerPD ...
Processing theory HOLCF.UpperPD ...
Processing theory HOLCF.ConvexPD ...
Processing theory HOLCF.Representable ...
Processing theory HOLCF.Domain ...
Processing theory HOLCF.Powerdomains ...
Processing theory HOLCF ...
Processing theory HOLCF-Library.Bool_Discrete ...
Processing theory HOLCF-Library.Char_Discrete ...
Processing theory HOLCF-Library.Defl_Bifinite ...
Processing theory HOLCF-Library.Int_Discrete ...
Processing theory HOLCF-Library.List_Cpo ...
Processing theory HOLCF-Library.Nat_Discrete ...
Processing theory HOLCF-Library.Sum_Cpo ...
Processing theory HOL-Matrix_LP.Matrix ...
Processing theory HOL-Matrix_LP.SparseMatrix ...
Removing 36 theories ...
Processing theory HOLCF-Library.List_Predomain ...
Processing theory HOLCF-Library.Option_Cpo ...
Processing theory HOLCF-Library.Stream ...
Loading 37 theories ...
Processing theory HOLCF-FOCUS.Fstream ...
Processing theory HOLCF-FOCUS.FOCUS ...
Processing theory HOLCF-FOCUS.Fstreams ...
Processing theory HOLCF-FOCUS.Stream_adm ...
Processing theory HOLCF-Library.HOLCF_Library ...
Processing theory HOLCF-ex.Dagstuhl ...
Processing theory HOLCF-ex.Focus_ex ...
Processing theory HOL-Matrix_LP.Cplex ...
Processing theory HOLCF-FOCUS.Buffer ...
Processing theory HOLCF-FOCUS.Buffer_adm ...
Processing theory HOL-Data_Structures.Array_Specs ...
Processing theory HOL-IMP.Star ...
Processing theory HOL-Combinatorics.Stirling ...
Processing theory HOL-Data_Structures.Time_Funs ...
Processing theory HOL-Data_Structures.Tree2 ...
Processing theory HOL-Data_Structures.Isin2 ...
Processing theory HOL-Data_Structures.Lookup2 ...
Processing theory Codegen.Setup ...
Processing theory HOL-Data_Structures.Trie_Fun ...
Processing theory HOL-Data_Structures.AVL_Set_Code ...
Processing theory HOL-Combinatorics.Combinatorics ...
Processing theory HOL-Combinatorics.Guide ...
Processing theory HOL-Data_Structures.Sorting ...
Processing theory HOL-Data_Structures.RBT ...
Processing theory Codegen.Introduction ...
Processing theory Codegen.Foundations ...
Processing theory HOL-IMP.Types ...
Processing theory HOL-Data_Structures.Braun_Tree ...
Processing theory HOL-Types_To_Sets.Prerequisites ...
Processing theory HOL-IMP.Poly_Types ...
Processing theory HOL-Data_Structures.RBT_Set ...
Processing theory HOL-Data_Structures.RBT_Map ...
Processing theory HOL-Data_Structures.Selection ...
Processing theory HOL-Data_Structures.Trie_Map ...
Processing theory HOL-Data_Structures.Set2_Join ...
Removing 42 theories ...
Processing theory HOL-Types_To_Sets.Types_To_Sets ...
Processing theory HOL-Data_Structures.Array_Braun ...
Processing theory HOL-Data_Structures.RBT_Set2 ...
Processing theory HOL-Types_To_Sets.Group_On_With ...
Processing theory HOL-Types_To_Sets.Linear_Algebra_On_With ...
Processing theory HOL-Data_Structures.Set2_Join_RBT ...
Processing theory HOL-ex.Function_Growth ...
Processing theory HOL-Types_To_Sets.Linear_Algebra_On ...
Removing 14 theories ...
Processing theory HOL-Data_Structures.AVL_Set ...
Processing theory HOL-Data_Structures.AVL_Map ...
Removing 3 theories ...
Processing theory HOL-Data_Structures.Brother12_Set ...
Processing theory HOL-Data_Structures.Brother12_Map ...
Loading 43 theories ...
Processing theory HOL-TPTP.TPTP_Parser ...
Processing theory HOL-Library.LaTeXsugar ...
Processing theory HOL-Library.Refute ...
Processing theory HOL-Nitpick_Examples.Hotel_Nits ...
Removing 3 theories ...
Processing theory HOL-Nitpick_Examples.Induct_Nits ...
Processing theory HOL-Nitpick_Examples.Mini_Nits ...
Processing theory HOL-Nitpick_Examples.Mono_Nits ...
Processing theory HOL-Nitpick_Examples.Tests_Nits ...
Processing theory HOL-Nitpick_Examples.Integer_Nits ...
Processing theory HOL-Nitpick_Examples.Pattern_Nits ...
Processing theory HOL-Nitpick_Examples.Record_Nits ...
Processing theory Codegen.Adaptation ...
Processing theory HOL-Nitpick_Examples.Manual_Nits ...
Processing theory HOL-Nitpick_Examples.Datatype_Nits ...
Processing theory HOL-Nitpick_Examples.Core_Nits ...
Processing theory Codegen.Evaluation ...
Processing theory Typeclass_Hierarchy.Setup ...
Processing theory HOL-Library.OptionalSugar ...
Processing theory Codegen.Further ...
Processing theory HOL-Nitpick_Examples.Special_Nits ...
Processing theory Codegen.Inductive_Predicate ...
Processing theory Typeclass_Hierarchy.Typeclass_Hierarchy ...
Processing theory HOL-ex.SOS_Cert ...
Processing theory HOL-Data_Structures.Balance ...
Processing theory HOL-TPTP.TPTP_Interpret ...
Processing theory HOL-TPTP.ATP_Problem_Import ...
Processing theory HOL-TPTP.TPTP_Proof_Reconstruction ...
Processing theory Sugar.Sugar ...
Processing theory Codegen.Refinement ...
Processing theory Codegen.Computations ...
Processing theory HOL-ex.SOS ...
Processing theory HOL-Nitpick_Examples.Typedef_Nits ...
Processing theory HOL-ex.HarmonicSeries ...
Processing theory HOL-ex.Pythagoras ...
Processing theory HOL-ex.Sqrt ...
Processing theory HOL-ex.Sqrt_Script ...
Processing theory HOL-ex.Normalization_by_Evaluation ...
Removing 26 theories ...
Processing theory HOL-ex.Triangular_Numbers ...
Processing theory HOL-ex.Sum_of_Powers ...
Processing theory HOL-ex.Reflection_Examples ...
Processing theory HOL-Nitpick_Examples.Refute_Nits ...
Processing theory HOL-Nitpick_Examples.Nitpick_Examples ...
Removing 19 theories ...
Processing theory HOL-ex.Parallel_Example ...
Loading 29 theories ...
Processing theory HOL-Data_Structures.Priority_Queue_Specs ...
Processing theory Tutorial.Examples ...
Processing theory HOL-Computational_Algebra.Field_as_Ring ...
Processing theory Tutorial.Numbers ...
Processing theory HOL-Library.Code_Real_Approx_By_Float ...
Processing theory HOL-Metis_Examples.Clausification ...
Processing theory HOL-Mutabelle.MutabelleExtra ...
Processing theory How_to_Prove_it.How_to_Prove_it ...
Processing theory HOL-Data_Structures.Leftist_Heap ...
Processing theory Prog_Prove.Bool_nat_list ...
Processing theory HOL-Data_Structures.Binomial_Heap ...
Removing 13 theories ...
Processing theory HOL-SMT_Examples.SMT_Examples ...
Processing theory HOL-SMT_Examples.SMT_Examples_Verit ...
Removing 2 theories ...
Processing theory HOL-TPTP.ATP_Theory_Export ...
Processing theory HOL-TPTP.THF_Arith ...
Processing theory HOL-ex.BinEx ...
Processing theory HOL-SMT_Examples.SMT_Tests ...
Processing theory HOL-SMT_Examples.SMT_Tests_Verit ...
Processing theory HOL-Corec_Examples.Paper_Examples ...
Processing theory HOL-ex.Argo_Examples ...
Processing theory HOL-ex.Ballot ...
Processing theory HOL-ex.Code_Binary_Nat_examples ...
Processing theory HOL-Types_To_Sets.T2_Spaces ...
Processing theory HOL-Types_To_Sets.Unoverload_Def ...
Processing theory HOL-ex.Gauge_Integration ...
Processing theory HOL-ex.Eval_Examples ...
Removing 14 theories ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Examples ...
Removing 3 theories ...
Processing theory HOL-ex.Cubic_Quartic ...
Removing 1 theories ...
Processing theory HOL-ex.Dedekind_Real ...
Loading 24 theories ...
Processing theory HOL-Bali.Basis ...
Processing theory HOL-Bali.Table ...
Processing theory HOL-Bali.Name ...
Processing theory HOL-Bali.Type ...
Processing theory HOL-Bali.Value ...
Removing 10 theories ...
Processing theory HOL-Bali.Term ...
Processing theory HOL-Bali.Decl ...
Processing theory HOL-Bali.TypeRel ...
Processing theory HOL-Bali.DeclConcepts ...
Processing theory HOL-Bali.State ...
Processing theory HOL-Bali.Conform ...
Processing theory HOL-Bali.WellType ...
Processing theory HOL-Bali.Eval ...
Processing theory HOL-Bali.DefiniteAssignment ...
Processing theory HOL-Bali.WellForm ...
Processing theory HOL-Bali.Example ...
Processing theory HOL-Bali.DefiniteAssignmentCorrect ...
Processing theory HOL-Bali.TypeSafe ...
Processing theory HOL-Bali.Evaln ...
Processing theory HOL-Bali.Trans ...
Processing theory HOL-Bali.AxSem ...
Processing theory HOL-Bali.AxCompl ...
Processing theory HOL-Bali.AxExample ...
Processing theory HOL-Bali.AxSound ...
Loading 56 theories ...
Removing 24 theories ...
Processing theory IOA-ABP.Lemmas ...
Processing theory IOA-ABP.Packet ...
Processing theory IOA-NTP.Lemmas ...
Processing theory IOA-NTP.Multiset ...
Processing theory IOA.Asig ...
Processing theory IOA-NTP.Packet ...
Processing theory IOA.Pred ...
Processing theory HOL-Isar_Examples.Fibonacci ...
Processing theory IOA-Storage.Action ...
Processing theory IOA.Automata ...
Processing theory IOA.Seq ...
Processing theory IOA.Sequence ...
Processing theory IOA.TL ...
Processing theory IOA.Traces ...
Processing theory IOA.CompoExecs ...
Processing theory IOA.RefMappings ...
Processing theory IOA.RefCorrectness ...
Processing theory IOA.Simulations ...
Processing theory IOA.CompoScheds ...
Processing theory IOA.Deadlock ...
Processing theory IOA.SimCorrectness ...
Processing theory IOA.ShortExecutions ...
Processing theory HOL-ex.Code_Timing ...
Processing theory IOA-ABP.Action ...
Processing theory HOL-Nominal.Nominal ...
Processing theory IOA-NTP.Action ...
Processing theory IOA.CompoTraces ...
Processing theory IOA.Compositionality ...
Processing theory IOA.IOA ...
Processing theory IOA-ABP.Env ...
Processing theory IOA-ABP.Receiver ...
Processing theory IOA-ABP.Sender ...
Processing theory IOA-ABP.Spec ...
Processing theory IOA-NTP.Overview ...
Processing theory IOA-NTP.Receiver ...
Processing theory IOA-NTP.Sender ...
Processing theory IOA-NTP.Spec ...
Processing theory IOA-Storage.Impl ...
Processing theory IOA-Storage.Spec ...
Processing theory IOA-Storage.Correctness ...
Processing theory IOA.TLS ...
Processing theory IOA.LiveIOA ...
Processing theory IOA-ABP.Abschannel ...
Processing theory IOA-ABP.Abschannel_finite ...
Processing theory IOA-ABP.Impl ...
Processing theory IOA-ABP.Impl_finite ...
Processing theory IOA-ABP.Correctness ...
Processing theory IOA-NTP.Abschannel ...
Processing theory IOA-NTP.Impl ...
Processing theory IOA-NTP.Correctness ...
Processing theory IOA.Abstraction ...
Processing theory IOA-ex.TrivEx ...
Processing theory IOA-ex.TrivEx2 ...
Removing 56 theories ...
Processing theory HOL-Nominal-Examples.Class1 ...
Processing theory HOL-Nominal-Examples.Class2 ...
Processing theory HOL-Nominal-Examples.Class3 ...
Loading 90 theories ...
Processing theory HOL-Eisbach.Eisbach ...
Processing theory HOL-Eisbach.Eisbach_Tools ...
Processing theory HOLCF-Library.HOL_Cpo ...
Processing theory HOL-SMT_Examples.SMT_Word_Examples ...
Processing theory HOL-SPARK-Examples.RMD ...
Processing theory HOL-MicroJava.Semilat ...
Processing theory HOL-MicroJava.JBasis ...
Processing theory HOL-MicroJava.AuxLemmas ...
Processing theory HOL-SPARK.SPARK_Setup ...
Processing theory HOL-SPARK.SPARK ...
Processing theory HOL-SPARK-Examples.Greatest_Common_Divisor ...
Processing theory HOL-SPARK-Examples.RMD_Specification ...
Processing theory HOL-SPARK-Examples.Hash ...
Processing theory HOL-SPARK-Examples.Sqrt ...
Processing theory HOL-MicroJava.Type ...
Processing theory HOL-SPARK-Examples.K_L ...
Processing theory HOL-SPARK-Examples.K_R ...
Processing theory HOL-SPARK-Examples.F ...
Processing theory HOL-SPARK-Manual.Proc1 ...
Processing theory HOL-SPARK-Manual.Proc2 ...
Processing theory HOL-SPARK-Manual.VC_Principles ...
Processing theory HOL-SPARK-Manual.Simple_Greatest_Common_Divisor ...
Processing theory HOL-SPARK-Examples.Longest_Increasing_Subsequence ...
Processing theory HOL-SPARK-Manual.Reference ...
Processing theory HOL-SPARK-Manual.Example_Verification ...
Processing theory HOL-MicroJava.Decl ...
Processing theory HOL-MicroJava.SystemClasses ...
Processing theory HOL-MicroJava.TypeRel ...
Processing theory HOL-MicroJava.WellForm ...
Processing theory HOL-MicroJava.Err ...
Processing theory HOL-MicroJava.Opt ...
Processing theory HOL-MicroJava.Value ...
Processing theory HOL-MicroJava.State ...
Processing theory HOL-MicroJava.Exceptions ...
Processing theory HOL-SPARK-Manual.Complex_Types ...
Processing theory HOL-ex.Bit_Lists ...
Removing 29 theories ...
Processing theory HOL-MicroJava.Product ...
Processing theory HOL-MicroJava.Listn ...
Processing theory HOL-MicroJava.Typing_Framework ...
Processing theory HOL-MicroJava.SemilatAlg ...
Processing theory HOL-MicroJava.Kildall ...
Processing theory HOL-MicroJava.Typing_Framework_err ...
Processing theory HOL-MicroJava.Semilattices ...
Processing theory HOL-MicroJava.LBVSpec ...
Processing theory HOL-MicroJava.LBVCorrect ...
Processing theory HOL-MicroJava.JType ...
Processing theory HOL-SPARK-Examples.RMD_Lemmas ...
Processing theory HOL-MicroJava.JVMType ...
Processing theory HOL-SPARK-Examples.R_L ...
Processing theory HOL-SPARK-Examples.R_R ...
Processing theory HOL-SPARK-Examples.Round ...
Processing theory HOL-MicroJava.Term ...
Processing theory HOL-MicroJava.WellType ...
Processing theory HOL-MicroJava.TypeInf ...
Processing theory HOL-MicroJava.Conform ...
Processing theory HOL-MicroJava.JVMState ...
Processing theory HOL-MicroJava.LBVComplete ...
Processing theory HOL-MicroJava.Abstract_BV ...
Processing theory HOL-SPARK-Examples.S_L ...
Processing theory HOL-Eisbach.Example_Metric ...
Processing theory HOL-SPARK-Examples.S_R ...
Processing theory HOL-MicroJava.Eval ...
Processing theory HOL-MicroJava.Example ...
Processing theory HOL-MicroJava.JVMInstructions ...
Processing theory HOL-MicroJava.JVMExceptions ...
Processing theory HOL-MicroJava.JVMExecInstr ...
Processing theory HOL-MicroJava.JVMExec ...
Processing theory HOL-MicroJava.DefsComp ...
Processing theory HOL-MicroJava.Index ...
Processing theory HOL-MicroJava.TranslCompTp ...
Processing theory HOL-MicroJava.TranslComp ...
Processing theory HOL-MicroJava.JVMDefensive ...
Processing theory HOL-MicroJava.LemmasComp ...
Processing theory HOL-MicroJava.JVMListExample ...
Processing theory HOL-MicroJava.JListExample ...
Processing theory HOL-MicroJava.JTypeSafe ...
Removing 21 theories ...
Processing theory HOL-MicroJava.Effect ...
Processing theory HOL-MicroJava.BVSpec ...
Processing theory HOL-MicroJava.Altern ...
Processing theory HOL-MicroJava.EffectMono ...
Processing theory HOL-MicroJava.Correct ...
Processing theory HOL-MicroJava.Typing_Framework_JVM ...
Processing theory HOL-MicroJava.JVM ...
Processing theory HOL-MicroJava.LBVJVM ...
Processing theory HOL-MicroJava.CorrComp ...
Processing theory HOL-MicroJava.BVSpecTypeSafe ...
Processing theory HOL-MicroJava.BVNoTypeError ...
Processing theory HOL-MicroJava.BVExample ...
Processing theory HOL-MicroJava.CorrCompTp ...
Loading 77 theories ...
Processing theory HOL-MicroJava.MicroJava ...
Processing theory HOL-Cardinals.Wellorder_Extension ...
Processing theory HOL-Imperative_HOL.Sorted_List ...
Processing theory HOL-IMP.AExp ...
Processing theory HOL-IMP.BExp ...
Processing theory HOL-IMP.Com ...
Processing theory HOL-Auth.Message ...
Processing theory HOL-Auth.Event ...
Processing theory HOL-Auth.Public ...
Processing theory HOL-IMP.Big_Step ...
Processing theory HOL-Imperative_HOL.List_Sublist ...
Processing theory HOLCF-IMP.Denotational ...
Processing theory HOLCF-IMP.HoareEx ...
Processing theory HOLCF-ex.Dnat ...
Processing theory HOLCF-Tutorial.Fixrec_ex ...
Processing theory HOLCF-Tutorial.New_Domain ...
Removing 65 theories ...
Processing theory HOLCF-ex.Fix2 ...
Processing theory HOL-Cardinals.Ordinal_Arithmetic ...
Processing theory HOL-Cardinals.Cardinals ...
Processing theory HOL-Cardinals.Bounded_Set ...
Processing theory HOLCF-ex.Concurrency_Monad ...
Processing theory HOLCF-ex.Domain_Proofs ...
Processing theory HOLCF-ex.Hoare ...
Processing theory HOLCF-ex.Letrec ...
Processing theory HOLCF-ex.Loop ...
Processing theory HOLCF-ex.Pattern_Match ...
Processing theory HOLCF-ex.Powerdomain_ex ...
Processing theory HOL-Quotient_Examples.Int_Pow ...
Processing theory HOL-UNITY.ListOrder ...
Processing theory HOL-UNITY.UNITY ...
Processing theory HOL-UNITY.Constrains ...
Processing theory HOL-UNITY.FP ...
Processing theory HOL-Imperative_HOL.Heap ...
Processing theory HOL-Imperative_HOL.Heap_Monad ...
Processing theory HOL-Imperative_HOL.Array ...
Processing theory HOL-Imperative_HOL.Ref ...
Processing theory HOL-Imperative_HOL.Imperative_HOL ...
Processing theory HOL-Imperative_HOL.Overview ...
Processing theory HOL-Imperative_HOL.Subarray ...
Processing theory HOL-UNITY.WFair ...
Processing theory HOLCF-Tutorial.Domain_ex ...
Processing theory HOL-Imperative_HOL.Imperative_Reverse ...
Processing theory HOL-UNITY.SubstAx ...
Processing theory HOL-UNITY.Detects ...
Processing theory HOL-UNITY.Follows ...
Processing theory HOL-UNITY.Union ...
Processing theory HOL-UNITY.Comp ...
Processing theory HOL-UNITY.Guar ...
Processing theory HOL-Imperative_HOL.Imperative_Quicksort ...
Processing theory HOL-Imperative_HOL.Linked_Lists ...
Removing 62 theories ...
Processing theory HOL-UNITY.Transformers ...
Processing theory HOL-UNITY.ProgressSets ...
Processing theory HOL-ex.Sorting_Algorithms_Examples ...
Processing theory HOL-UNITY.Extend ...
Processing theory HOL-UNITY.Rename ...
Processing theory HOL-UNITY.Lift_prog ...
Processing theory HOL-UNITY.PPROD ...
Processing theory HOL-UNITY.UNITY_Main ...
Processing theory HOL-UNITY.AllocBase ...
Processing theory HOL-UNITY.Counterc ...
Processing theory HOL-UNITY.Counter ...
Processing theory HOL-Imperative_HOL.SatChecker ...
Processing theory HOL-UNITY.PriorityAux ...
Processing theory HOL-Imperative_HOL.Imperative_HOL_ex ...
Processing theory HOL-UNITY.Handshake ...
Processing theory HOL-UNITY.Priority ...
Processing theory HOL-UNITY.Progress ...
Processing theory HOL-UNITY.TimerArray ...
Processing theory HOL-UNITY.Channel ...
Processing theory HOL-UNITY.Common ...
Processing theory HOL-UNITY.Reach ...
Processing theory HOL-UNITY.Client ...
Processing theory HOL-UNITY.Mutex ...
Processing theory HOL-UNITY.NSP_Bad ...
Processing theory HOL-UNITY.Alloc ...
Processing theory HOL-UNITY.AllocImpl ...
Processing theory HOL-UNITY.Lift ...
Loading 52 theories ...
Processing theory HOL-UNITY.Reachability ...
Removing 45 theories ...
Processing theory Isar_Ref.Base ...
Processing theory Datatypes.Setup ...
Processing theory HOL-ZF.LProd ...
Processing theory HOL-ex.Quicksort ...
Processing theory HOL-Library.List_Lexorder ...
Processing theory HOL-Datatype_Examples.Prelim ...
Processing theory HOL-ex.Bubblesort ...
Processing theory HOL-ex.MergeSort ...
Processing theory HOL-Datatype_Examples.DTree ...
Processing theory HOL-Datatype_Examples.Gram_Lang ...
Processing theory HOL-Datatype_Examples.Parallel_Composition ...
Processing theory HOL-Datatype_Examples.Lambda_Term ...
Removing 8 theories ...
Processing theory HOL-Datatype_Examples.TreeFsetI ...
Processing theory Datatypes.Datatypes ...
Removing 2 theories ...
Processing theory Corec.Corec ...
Processing theory HOL-Nominal-Examples.CK_Machine ...
Processing theory HOL-Nominal-Examples.CR_Takahashi ...
Processing theory HOL-Nominal-Examples.Contexts ...
Processing theory HOL-Nominal-Examples.Crary ...
Removing 6 theories ...
Processing theory HOL-Nominal-Examples.Height ...
Processing theory HOL-Nominal-Examples.Lam_Funs ...
Processing theory HOL-Nominal-Examples.Compile ...
Processing theory HOL-Datatype_Examples.Misc_Datatype ...
Processing theory HOL-Nominal-Examples.CR ...
Processing theory HOL-Datatype_Examples.Misc_Primrec ...
Processing theory HOL-Nominal-Examples.SN ...
Processing theory HOL-Nominal-Examples.LocalWeakening ...
Processing theory HOL-Nominal-Examples.Fsub ...
Processing theory HOL-Datatype_Examples.Misc_Codatatype ...
Processing theory HOL-Datatype_Examples.Misc_Primcorec ...
Processing theory HOL-Nominal-Examples.Support ...
Processing theory HOL-Nominal-Examples.VC_Condition ...
Processing theory HOL-Nominal-Examples.Standardization ...
Processing theory HOL-Nominal-Examples.SOS ...
Processing theory HOL-Nominal-Examples.Type_Preservation ...
Processing theory HOL-Nominal-Examples.Lambda_mu ...
Processing theory HOL-ex.Radix_Sort ...
Processing theory HOL-Quotient_Examples.Quotient_FSet ...
Processing theory HOL-Data_Structures.Heaps ...
Processing theory HOL-UNITY.Project ...
Processing theory HOL-UNITY.ELT ...
Processing theory HOL-ZF.HOLZF ...
Processing theory HOL-ZF.Zet ...
Processing theory HOL-ZF.MainZF ...
Processing theory HOL-ZF.Games ...
Processing theory HOL-ex.Transfer_Debug ...
Processing theory HOL-Nominal-Examples.Weakening ...
Processing theory HOL-ex.Code_Lazy_Demo ...
Processing theory HOL-Nominal-Examples.W ...
Processing theory HOL-Nominal-Examples.Pattern ...
Processing theory Isar_Ref.HOL_Specific ...
Processing theory HOL-ex.Termination ...
Loading 112 theories ...
Removing 53 theories ...
Processing theory Tutorial.Setup ...
Processing theory HOL-Auth.All_Symmetric ...
Processing theory HOL-Auth.Extensions ...
Processing theory Tutorial.Message ...
Processing theory Tutorial.Event ...
Processing theory Tutorial.Public ...
Processing theory Tutorial.NS_Public ...
Processing theory HOL-Auth.Analz ...
Processing theory HOL-Auth.Guard ...
Processing theory HOL-Auth.List_Msg ...
Processing theory HOL-Auth.CertifiedEmail ...
Processing theory HOL-Auth.GuardK ...
Processing theory HOL-Auth.Guard_Public ...
Processing theory HOL-Auth.Shared ...
Processing theory HOL-Auth.KerberosIV ...
Processing theory HOL-Auth.Guard_NS_Public ...
Processing theory HOL-Auth.KerberosIV_Gets ...
Processing theory HOL-Auth.P2 ...
Removing 4 theories ...
Processing theory HOL-Auth.NS_Public ...
Processing theory HOL-Auth.NS_Public_Bad ...
Processing theory HOL-Auth.Kerberos_BAN ...
Processing theory HOL-Auth.Kerberos_BAN_Gets ...
Processing theory HOL-Auth.Proto ...
Processing theory HOL-Auth.KerberosV ...
Processing theory HOL-Auth.P1 ...
Processing theory HOL-Auth.Auth_Guard_Public ...
Processing theory HOL-Auth.NS_Shared ...
Processing theory HOL-Auth.OtwayRees ...
Processing theory HOL-Auth.OtwayReesBella ...
Processing theory HOL-Auth.OtwayRees_AN ...
Processing theory HOL-Auth.OtwayRees_Bad ...
Processing theory HOL-Auth.WooLam ...
Processing theory HOL-Auth.Recur ...
Processing theory HOL-Auth.Yahalom2 ...
Processing theory HOL-Auth.Yahalom_Bad ...
Processing theory HOL-Hoare_Parallel.Graph ...
Processing theory HOL-Auth.Guard_Shared ...
Processing theory HOL-Auth.Guard_OtwayRees ...
Processing theory HOL-Auth.Guard_Yahalom ...
Processing theory HOL-Auth.Auth_Guard_Shared ...
Processing theory HOL-Hoare_Parallel.Quote_Antiquote ...
Processing theory HOL-Auth.Yahalom ...
Processing theory HOL-Auth.ZhouGollmann ...
Processing theory HOL-Auth.Auth_Shared ...
Processing theory HOL-IMP.Abs_Int_Tests ...
Processing theory HOL-IMP.Vars ...
Processing theory HOL-IMP.Complete_Lattice ...
Processing theory HOL-Hoare_Parallel.RG_Com ...
Processing theory HOL-IMP.ACom ...
Processing theory HOL-Hoare_Parallel.OG_Com ...
Processing theory HOL-Hoare_Parallel.OG_Tran ...
Processing theory HOL-Hoare_Parallel.OG_Hoare ...
Processing theory HOL-Hoare_Parallel.OG_Tactics ...
Processing theory HOL-Hoare_Parallel.OG_Syntax ...
Processing theory HOL-IMP.Collecting ...
Processing theory HOL-Lattice.Orders ...
Processing theory HOL-Lattice.Bounds ...
Processing theory HOL-Lattice.Lattice ...
Processing theory HOL-Lattice.CompleteLattice ...
Processing theory HOL-Auth.EventSC ...
Processing theory HOL-Auth.Smartcard ...
Removing 37 theories ...
Processing theory HOL-Hoare_Parallel.Gar_Coll ...
Processing theory HOL-Auth.ShoupRubin ...
Processing theory HOL-Auth.ShoupRubinBella ...
Processing theory HOL-Auth.Auth_Smartcard ...
Removing 6 theories ...
Processing theory HOL-Hoare_Parallel.RG_Tran ...
Processing theory HOL-Auth.TLS ...
Processing theory HOL-Auth.Auth_Public ...
Processing theory HOL-IMP.Abs_Int_init ...
Processing theory HOL-Library.Prefix_Order ...
Processing theory HOL-Metis_Examples.Big_O ...
Processing theory HOL-TLA.Intensional ...
Processing theory HOL-TLA.Stfun ...
Processing theory HOL-TLA.Action ...
Processing theory HOL-TLA.Init ...
Processing theory HOL-IMP.Abs_Int0 ...
Processing theory HOL-IMP.Abs_State ...
Processing theory HOL-IMP.Abs_Int1 ...
Processing theory HOL-Hoare_Parallel.Mul_Gar_Coll ...
Processing theory HOL-TLA.TLA ...
Processing theory HOL-TLA-Buffer.Buffer ...
Processing theory HOL-TLA-Buffer.DBuffer ...
Processing theory HOL-Hoare_Parallel.OG_Examples ...
Processing theory HOL-SET_Protocol.Message_SET ...
Processing theory HOL-SET_Protocol.Event_SET ...
Processing theory HOL-SET_Protocol.Public_SET ...
Processing theory HOL-IMP.Abs_Int1_parity ...
Processing theory HOL-IMP.Abs_Int2 ...
Processing theory HOL-SET_Protocol.Merchant_Registration ...
Processing theory HOL-Hoare_Parallel.RG_Hoare ...
Processing theory HOL-Hoare_Parallel.RG_Syntax ...
Processing theory HOL-IMP.Abs_Int1_const ...
Removing 17 theories ...
Processing theory HOL-TLA-Memory.RPCMemoryParams ...
Processing theory HOL-TLA-Memory.MemoryParameters ...
Processing theory HOL-TLA-Memory.ProcedureInterface ...
Processing theory HOL-TLA-Inc.Inc ...
Processing theory HOL-TLA-Memory.RPCParameters ...
Processing theory HOL-TLA-Memory.MemClerkParameters ...
Processing theory HOL-SET_Protocol.Cardholder_Registration ...
Processing theory HOL-TLA-Memory.Memory ...
Processing theory HOL-TLA-Memory.RPC ...
Processing theory HOL-TLA-Memory.MemClerk ...
Processing theory HOL-IMP.Abs_Int2_ivl ...
Processing theory HOL-Unix.Nested_Environment ...
Processing theory HOL-Hoare_Parallel.RG_Examples ...
Processing theory HOL-Hoare_Parallel.Hoare_Parallel ...
Removing 17 theories ...
Processing theory HOL-Unix.Unix ...
Processing theory HOL-ex.Residue_Ring ...
Processing theory HOL-SET_Protocol.Purchase ...
Processing theory HOL-SET_Protocol.SET_Protocol ...
Processing theory HOL-TLA-Memory.MemoryImplementation ...
Processing theory HOL-IMP.Abs_Int3 ...
Loading 213 theories ...
Processing theory Classes.Setup ...
Processing theory Eisbach.Base ...
Processing theory Eisbach.Manual ...
Processing theory Eisbach.Preface ...
Processing theory Implementation.Base ...
Processing theory JEdit.Base ...
Processing theory Implementation.Proof ...
Processing theory Implementation.Syntax ...
Processing theory JEdit.JEdit ...
Processing theory Locales.Examples ...
Processing theory Locales.Examples1 ...
Processing theory Locales.Examples2 ...
Processing theory Prog_Prove.LaTeXsugar ...
Processing theory Tutorial.Base ...
Processing theory Prog_Prove.Isar ...
Processing theory Classes.Classes ...
Processing theory Implementation.Tactic ...
Processing theory Locales.Examples3 ...
Processing theory Tutorial.PDL ...
Processing theory Tutorial.TPrimes ...
Processing theory Tutorial.Forward ...
Processing theory Tutorial.Even ...
Processing theory Tutorial.Overloading ...
Processing theory Prog_Prove.Logic ...
Processing theory Tutorial.CTL ...
Processing theory Tutorial.CTLind ...
Processing theory Tutorial.Tree ...
Processing theory Tutorial.Tree2 ...
Processing theory Tutorial.Axioms ...
Processing theory HOL-Data_Structures.Queue_Spec ...
Processing theory HOL-Data_Structures.Reverse ...
Processing theory HOL-Data_Structures.Queue_2Lists ...
Processing theory Tutorial.Advanced ...
Removing 71 theories ...
Processing theory Tutorial.ABexpr ...
Processing theory Tutorial.Nested ...
Processing theory HOL-Data_Structures.Tries_Binary ...
Processing theory HOL-Data_Structures.Tree23 ...
Processing theory HOL-Data_Structures.Tree23_of_List ...
Processing theory HOL-Data_Structures.Tree234 ...
Processing theory HOL-Datatype_Examples.TreeFI ...
Processing theory HOL-Hoare.Arith2 ...
Processing theory HOL-Hoare.Heap ...
Processing theory HOL-Hoare.Hoare_Syntax ...
Processing theory HOL-Hoare.Hoare_Tac ...
Processing theory HOL-Hoare.SepLogHeap ...
Processing theory HOL-IMP.ASM ...
Processing theory HOL-Hoare.Hoare_Logic ...
Processing theory HOL-Hoare.Examples ...
Processing theory HOL-Hoare.ExamplesTC ...
Processing theory HOL-Hoare.HeapSyntax ...
Processing theory HOL-Hoare.Hoare_Logic_Abort ...
Processing theory HOL-Hoare.ExamplesAbort ...
Processing theory HOL-Hoare.HeapSyntaxAbort ...
Processing theory HOL-Hoare.Pointer_ExamplesAbort ...
Processing theory HOL-Hoare.SchorrWaite ...
Processing theory HOL-Hoare.Pointers0 ...
Processing theory HOL-Hoare.Separation ...
Processing theory HOL-IMP.Denotational ...
Processing theory HOL-IMP.Hoare ...
Processing theory HOL-Hoare.Pointer_Examples ...
Processing theory HOL-IMP.Hoare_Examples ...
Processing theory HOL-IMP.Hoare_Sound_Complete ...
Processing theory HOL-Isar_Examples.Hoare ...
Processing theory HOL-Isar_Examples.Hoare_Ex ...
Processing theory HOL-Data_Structures.Tree23_Set ...
Processing theory HOL-IMP.Hoare_Total ...
Processing theory HOL-IMP.Hoare_Total_EX ...
Processing theory HOL-IMP.Hoare_Total_EX2 ...
Processing theory HOL-IMP.VCG_Total_EX ...
Removing 30 theories ...
Processing theory HOL-IMP.Sec_Type_Expr ...
Processing theory HOL-IMP.Sec_Typing ...
Processing theory HOL-IMP.Sec_TypingT ...
Processing theory HOL-IMP.VCG ...
Processing theory HOL-IMP.Def_Init ...
Processing theory HOL-IMP.Def_Init_Exp ...
Processing theory HOL-IMP.Def_Init_Big ...
Processing theory HOL-IMP.Sem_Equiv ...
Processing theory HOL-IMP.Fold ...
Processing theory HOL-IMP.Live ...
Processing theory HOL-IMP.VCG_Total_EX2 ...
Processing theory HOL-IMP.Procs ...
Processing theory HOL-IMP.Procs_Dyn_Vars_Dyn ...
Removing 12 theories ...
Processing theory HOL-IMP.Collecting1 ...
Processing theory HOL-IMP.Procs_Stat_Vars_Dyn ...
Processing theory HOL-IMP.Collecting_Examples ...
Processing theory HOL-IMP.Def_Init_Small ...
Processing theory HOL-IMP.Small_Step ...
Processing theory HOL-IMP.Procs_Stat_Vars_Stat ...
Processing theory HOL-IMP.Finite_Reachable ...
Processing theory HOL-IOA.Asig ...
Processing theory HOL-Data_Structures.Tree23_Map ...
Processing theory HOL-IMPP.Com ...
Processing theory HOL-IMPP.Natural ...
Processing theory HOL-IMPP.Hoare ...
Processing theory HOL-IMPP.Misc ...
Processing theory HOL-IMPP.EvenOdd ...
Processing theory HOL-Import.Import_Setup ...
Processing theory HOL-Import.HOL_Light_Maps ...
Processing theory HOL-IOA.IOA ...
Processing theory HOL-IOA.Solve ...
Processing theory HOL-IMP.Compiler ...
Processing theory HOL-Corec_Examples.LFilter ...
Processing theory HOL-IMP.Compiler2 ...
Processing theory HOL-Corec_Examples.Iterate_GPV ...
Processing theory HOL-Corec_Examples.GPV_Bare_Bones ...
Processing theory HOL-Corec_Examples.Merge_A ...
Processing theory HOL-Corec_Examples.Merge_B ...
Processing theory HOL-Corec_Examples.Merge_C ...
Removing 32 theories ...
Processing theory HOL-Corec_Examples.Merge_D ...
Removing 4 theories ...
Processing theory HOL-Corec_Examples.Merge_Poly ...
Processing theory HOL-Data_Structures.Tree234_Set ...
Removing 1 theories ...
Processing theory HOL-Corec_Examples.Simple_Nesting ...
Removing 1 theories ...
Processing theory HOL-Corec_Examples.Misc_Mono ...
Removing 1 theories ...
Processing theory HOL-Corec_Examples.Stream_Friends ...
Processing theory HOL-Library.Code_Prolog ...
Processing theory HOL-ex.Simps_Case_Conv_Examples ...
Processing theory HOL-Corec_Examples.Small_Concrete ...
Removing 4 theories ...
Processing theory HOL-Predicate_Compile_Examples.Context_Free_Grammar_Example ...
Processing theory HOL-Predicate_Compile_Examples.Lambda_Example ...
Processing theory HOL-Predicate_Compile_Examples.Code_Prolog_Examples ...
Processing theory HOL-Data_Structures.Tree234_Map ...
Processing theory HOL-ex.Conditional_Parametricity_Examples ...
Processing theory HOL-Datatype_Examples.Cyclic_List ...
Processing theory HOL-Library.Datatype_Records ...
Processing theory HOL-Metis_Examples.Abstraction ...
Processing theory HOL-Datatype_Examples.FAE_Sequence ...
Processing theory HOL-Datatype_Examples.Free_Idempotent_Monoid ...
Processing theory HOL-Datatype_Examples.Regex_ACI ...
Processing theory HOL-Corec_Examples.TLList_Friends ...
Processing theory HOL-ex.Datatype_Record_Examples ...
Processing theory HOL-Examples.Knaster_Tarski ...
Processing theory HOL-ex.IArray_Examples ...
Processing theory HOL-Examples.Adhoc_Overloading_Examples ...
Processing theory HOL-Datatype_Examples.Regex_ACIDZ ...
Removing 27 theories ...
Processing theory HOL-Datatype_Examples.Koenig ...
Processing theory HOL-Corec_Examples.Type_Class ...
Processing theory HOL-Induct.Sexp ...
Processing theory HOL-Induct.SList ...
Processing theory HOL-ex.Perm_Fragments ...
Processing theory HOL-ex.Specifications_with_bundle_mixins ...
Processing theory HOL-Library.Predicate_Compile_Alternative_Defs ...
Processing theory HOL-Library.Predicate_Compile_Quickcheck ...
Processing theory HOL-Quotient_Examples.Quotient_Int ...
Processing theory HOL-Datatype_Examples.Process ...
Processing theory HOL-Datatype_Examples.Stream_Processor ...
Processing theory HOL-Corec_Examples.Stream_Processor ...
Processing theory HOL-Codegenerator_Test.Code_Lazy_Test ...
Processing theory HOL-Codegenerator_Test.Code_Test_GHC ...
Processing theory HOL-Codegenerator_Test.Code_Test_OCaml ...
Processing theory HOL-Codegenerator_Test.Code_Test_PolyML ...
Removing 20 theories ...
Processing theory HOL-Codegenerator_Test.Code_Test_MLton ...
Processing theory HOL-Codegenerator_Test.Code_Test_SMLNJ ...
Processing theory HOL-Codegenerator_Test.Code_Test_Scala ...
Processing theory HOL-Predicate_Compile_Examples.IMP_1 ...
Processing theory HOL-Predicate_Compile_Examples.IMP_2 ...
Processing theory HOL-Predicate_Compile_Examples.IMP_3 ...
Processing theory HOL-Corec_Examples.Misc_Poly ...
Processing theory HOL-Predicate_Compile_Examples.Reg_Exp_Example ...
Processing theory HOL-Quotient_Examples.Quotient_Rat ...
Processing theory HOL-Quotient_Examples.DList ...
Processing theory HOL-ex.Transitive_Closure_Table_Ex ...
Processing theory HOL-Predicate_Compile_Examples.IMP_4 ...
Removing 25 theories ...
Processing theory HOL-Predicate_Compile_Examples.Predicate_Compile_Tests ...
Processing theory HOL-Predicate_Compile_Examples.Predicate_Compile_Quickcheck_Examples ...
Processing theory HOL-Data_Structures.Interval_Tree ...
Processing theory HOL-Data_Structures.AA_Set ...
Processing theory HOL-Data_Structures.AVL_Bal2_Set ...
Processing theory HOL-ex.While_Combinator_Example ...
Processing theory HOL-IMP.Live_True ...
Processing theory HOL-ex.Refute_Examples ...
Removing 14 theories ...
Processing theory HOL-Metis_Examples.Type_Encodings ...
Processing theory HOL-Mirabelle.Mirabelle ...
Processing theory HOL-Mirabelle.Mirabelle_Test ...
Processing theory HOL-Data_Structures.AA_Map ...
Processing theory HOL-Metis_Examples.Tarski ...
Processing theory HOL-Data_Structures.AVL_Bal_Set ...
Processing theory HOL-NanoJava.Term ...
Processing theory HOL-NanoJava.Decl ...
Processing theory HOL-NanoJava.TypeRel ...
Processing theory HOL-NanoJava.State ...
Processing theory HOL-NanoJava.AxSem ...
Processing theory HOL-NanoJava.OpSem ...
Processing theory HOL-NanoJava.Equivalence ...
Processing theory HOL-NanoJava.Example ...
Processing theory HOL-Predicate_Compile_Examples.List_Examples ...
Processing theory HOL-Predicate_Compile_Examples.Hotel_Example ...
Processing theory HOL-Predicate_Compile_Examples.Hotel_Example_Prolog ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Nesting ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Nesting_Example ...
Processing theory HOL-Quotient_Examples.Lift_Fun ...
Processing theory HOL-Quotient_Examples.Quotient_Message ...
Processing theory HOL-Predicate_Compile_Examples.Specialisation_Examples ...
Processing theory HOL-Predicate_Compile_Examples.Examples ...
Processing theory HOL-TPTP.MaSh_Export_Base ...
Processing theory HOL-TPTP.MaSh_Eval ...
Processing theory HOL-Types_To_Sets.Finite ...
Processing theory HOL-UNITY.Deadlock ...
Processing theory HOL-ex.Birthday_Paradox ...
Processing theory HOL-UNITY.Network ...
Processing theory HOL-UNITY.Token ...
Processing theory HOL-ex.Execute_Choice ...
Processing theory HOL-ex.Rewrite_Examples ...
Processing theory HOL-Statespace.DistinctTreeProver ...
Processing theory HOL-Statespace.StateFun ...
Processing theory HOL-Statespace.StateSpaceLocale ...
Processing theory HOL-Statespace.StateSpaceSyntax ...
Processing theory HOL-ex.Tarski ...
Processing theory HOL-ex.ThreeDivides ...
Processing theory HOL-Quickcheck_Examples.Hotel_Example ...
Processing theory HOL-Data_Structures.Height_Balanced_Tree ...
Removing 61 theories ...
Processing theory HOL-Metis_Examples.Proxies ...
Processing theory HOL-Statespace.StateSpaceEx ...
Processing theory HOL-ex.Functions ...
Loading 154 theories ...
Processing theory Implementation.Eq ...
Processing theory Implementation.Integration ...
Processing theory Implementation.Local_Theory ...
Processing theory Isar_Ref.Document_Preparation ...
Processing theory Implementation.Isar ...
Processing theory Isar_Ref.Framework ...
Processing theory Implementation.Prelim ...
Processing theory Isar_Ref.Outer_Syntax ...
Processing theory Isar_Ref.Preface ...
Processing theory Isar_Ref.Generic ...
Processing theory Isar_Ref.Inner_Syntax ...
Processing theory Isar_Ref.Proof ...
Processing theory Isar_Ref.Proof_Script ...
Processing theory Isar_Ref.Quick_Reference ...
Processing theory Isar_Ref.Symbols ...
Processing theory Prog_Prove.Basics ...
Processing theory Implementation.Logic ...
Processing theory Isar_Ref.Synopsis ...
Processing theory Implementation.ML ...
Processing theory Isar_Ref.Spec ...
Processing theory Prog_Prove.MyList ...
Processing theory Tutorial.simp2 ...
Processing theory Functions.Functions ...
Processing theory Tutorial.Fundata ...
Processing theory Tutorial.Mutual ...
Processing theory Tutorial.Star ...
Processing theory Main.Main_Doc ...
Processing theory Tutorial.CodeGen ...
Processing theory Tutorial.fun0 ...
Processing theory Tutorial.Itrev ...
Processing theory Tutorial.Plus ...
Processing theory Tutorial.Documents ...
Processing theory Tutorial.AdvancedInd ...
Processing theory Tutorial.appendix ...
Processing theory Tutorial.case_exprs ...
Processing theory Prog_Prove.Types_and_funs ...
Processing theory Tutorial.unfoldnested ...
Processing theory Tutorial.natsum ...
Processing theory Tutorial.pairs2 ...
Processing theory Tutorial.prime_def ...
Removing 51 theories ...
Processing theory Tutorial.AB ...
Processing theory Tutorial.Option2 ...
Processing theory Tutorial.fakenat ...
Processing theory Tutorial.simp ...
Processing theory Tutorial.types ...
Processing theory Tutorial.Ifexpr ...
Processing theory Tutorial.Basic ...
Processing theory Tutorial.Blast ...
Processing theory Tutorial.Force ...
Processing theory Tutorial.Tacticals ...
Processing theory Tutorial.find2 ...
Processing theory Tutorial.Functions ...
Processing theory Tutorial.Recur ...
Processing theory Tutorial.Relations ...
Processing theory Tutorial.ToyList_Test ...
Processing theory Tutorial.Pairs ...
Processing theory Tutorial.ToyList ...
Processing theory Tutorial.Records ...
Processing theory Tutorial.Trie ...
Processing theory Tutorial.Typedefs ...
Processing theory HOL-Datatype_Examples.Datatype_Simproc_Tests ...
Processing theory HOL-Datatype_Examples.Milner_Tofte ...
Processing theory HOL-Datatype_Examples.TLList ...
Processing theory HOL-Eisbach.Examples ...
Processing theory HOL-Eisbach.Tests ...
Processing theory HOL-Examples.Ackermann ...
Processing theory HOL-Examples.Cantor ...
Processing theory HOL-Examples.Commands ...
Processing theory HOL-Examples.Groebner_Examples ...
Processing theory HOL-Examples.Iff_Oracle ...
Processing theory HOL-Examples.Induction_Schema ...
Processing theory HOL-Examples.Peirce ...
Processing theory HOL-Examples.ML ...
Processing theory HOL-Examples.Seq ...
Processing theory HOL-Examples.Coherent ...
Processing theory HOL-IMP.C_like ...
Processing theory HOL-Datatype_Examples.Lift_BNF ...
Processing theory HOL-Datatype_Examples.Compat ...
Processing theory HOL-Induct.Comb ...
Processing theory HOL-Induct.Common_Patterns ...
Processing theory HOL-Induct.Com ...
Processing theory HOL-Induct.Infinitely_Branching_Tree ...
Processing theory HOL-Induct.Nested_Datatype ...
Processing theory HOL-Induct.Ordinals ...
Processing theory HOL-Induct.Sigma_Algebra ...
Processing theory HOL-Induct.PropLog ...
Processing theory HOL-Induct.QuoDataType ...
Processing theory HOL-Isar_Examples.Basic_Logic ...
Processing theory HOL-Isar_Examples.Group ...
Processing theory HOL-Isar_Examples.Group_Context ...
Processing theory HOL-Induct.QuoNestedDataType ...
Processing theory HOL-Induct.Term ...
Processing theory HOL-Isar_Examples.Group_Notepad ...
Processing theory HOL-Induct.ABexp ...
Processing theory HOL-Isar_Examples.Expr_Compiler ...
Processing theory HOL-Isar_Examples.Mutilated_Checkerboard ...
Processing theory HOL-Isar_Examples.Puzzle ...
Processing theory HOL-Isar_Examples.Structured_Statements ...
Processing theory HOL-Isar_Examples.Summation ...
Processing theory HOL-Library.List_Lenlexorder ...
Processing theory HOL-Metis_Examples.Sets ...
Processing theory HOL-Quickcheck_Examples.Completeness ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Interfaces ...
Processing theory HOL-Metis_Examples.Binary_Tree ...
Processing theory HOL-Metis_Examples.Trans_Closure ...
Processing theory HOL-Quotient_Examples.Lift_DList ...
Processing theory HOL-Quotient_Examples.Lift_FSet ...
Processing theory HOL-Quotient_Examples.Lift_Set ...
Processing theory HOL-IMP.OO ...
Processing theory HOL-Metis_Examples.Message ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples ...
Processing theory HOL-ex.Antiquote ...
Processing theory HOL-ex.Arith_Examples ...
Processing theory HOL-ex.CTL ...
Removing 77 theories ...
Processing theory HOL-ex.Case_Product ...
Processing theory HOL-ex.Classical ...
Processing theory HOL-ex.Coercion_Examples ...
Processing theory HOL-ex.Computations ...
Processing theory HOL-ex.Erdoes_Szekeres ...
Processing theory HOL-ex.Executable_Relation ...
Processing theory HOL-ex.Guess ...
Processing theory HOL-ex.Cartouche_Examples ...
Processing theory HOL-ex.Chinese ...
Processing theory HOL-ex.Hex_Bin_Examples ...
Processing theory HOL-ex.Intuitionistic ...
Processing theory HOL-ex.Join_Theory ...
Processing theory HOL-ex.Lagrange ...
Processing theory HOL-ex.List_to_Set_Comprehension_Examples ...
Processing theory HOL-ex.Multiquote ...
Processing theory HOL-ex.NatSum ...
Processing theory HOL-ex.MonoidGroup ...
Processing theory HOL-ex.PER ...
Processing theory HOL-ex.Peano_Axioms ...
Processing theory HOL-ex.LocaleTest2 ...
Processing theory HOL-ex.Hebrew ...
Processing theory HOL-Quotient_Examples.Lifting_Code_Dt_Test ...
Processing theory HOL-SMT_Examples.Boogie ...
Processing theory HOL-ex.SAT_Examples ...
Processing theory HOL-ex.Primrec ...
Removing 25 theories ...
Processing theory HOL-ex.Set_Comprehension_Pointfree_Examples ...
Processing theory HOL-ex.Serbian ...
Processing theory HOL-ex.Set_Theory ...
Processing theory HOL-ex.Sketch_and_Explore ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Narrowing_Examples ...
Removing 5 theories ...
Processing theory HOL-ex.Simproc_Tests ...
Processing theory HOL-ex.Transfer_Int_Nat ...
Processing theory HOL-ex.veriT_Preprocessing ...
Processing theory HOL-ex.Sudoku ...
Processing theory HOL-ex.Unification ...
Removing 5 theories ...
Processing theory HOL-ex.Tree23 ...
Processing theory HOL-ex.PresburgerEx ...
Removing 2 theories ...
Processing theory HOL-ex.Meson_Test ...
Loading 233 theories ...
Processing theory CTT.CTT ...
Processing theory CTT.Elimination ...
Processing theory CTT.Equality ...
Processing theory CTT.Synthesis ...
Processing theory CTT.Typechecking ...
Processing theory Cube.Cube ...
Processing theory Cube.Example ...
Processing theory Isar_Ref.First_Order_Logic ...
Processing theory System.Base ...
Processing theory System.Misc ...
Processing theory System.Phabricator ...
Processing theory System.Presentation ...
Processing theory System.Server ...
Processing theory IFOL ...
Processing theory Logics_ZF.IFOL_examples ...
Processing theory FOL ...
Processing theory CCL.Set ...
Processing theory CCL.Lfp ...
Processing theory CCL.Gfp ...
Processing theory CCL.CCL ...
Processing theory Logics_ZF.FOL_examples ...
Processing theory Logics_ZF.If ...
Processing theory FOL-ex.Foundation ...
Processing theory FOL-ex.Intuitionistic ...
Processing theory FOL-ex.Propositional_Int ...
Processing theory FOL-ex.Quantifiers_Int ...
Processing theory IFOLP ...
Processing theory FOLP ...
Processing theory System.Environment ...
Processing theory System.Sessions ...
Processing theory CCL.Term ...
Processing theory CCL.Trancl ...
Processing theory FOL-ex.If ...
Processing theory FOL-ex.Intro ...
Processing theory FOL-ex.Miniscope ...
Processing theory FOL-ex.Nat ...
Processing theory CCL.Type ...
Processing theory CCL.Fix ...
Processing theory CCL.Hered ...
Processing theory CCL.Wfd ...
Processing theory CCL.Nat ...
Processing theory CCL.List ...
Processing theory CCL.Flag ...
Processing theory CCL.Stream ...
Processing theory FOL-ex.Classical ...
Processing theory FOL-ex.Nat_Class ...
Processing theory FOL-ex.Natural_Numbers ...
Processing theory FOL-ex.Prolog ...
Processing theory FOL-ex.Propositional_Cla ...
Processing theory FOL-ex.Quantifiers_Cla ...
Processing theory LCF.LCF ...
Processing theory LCF.Ex1 ...
Processing theory LCF.Ex2 ...
Processing theory LCF.Ex3 ...
Processing theory LCF.Ex4 ...
Processing theory ZF.ZF_Base ...
Processing theory ZF.upair ...
Processing theory ZF.pair ...
Processing theory ZF.Bool ...
Processing theory ZF.equalities ...
Processing theory ZF.Fixedpt ...
Processing theory ZF.Sum ...
Processing theory ZF.func ...
Processing theory ZF.Perm ...
Processing theory ZF.Trancl ...
Processing theory ZF.EquivClass ...
Processing theory FOL-ex.Locale_Test1 ...
Processing theory FOL-ex.Locale_Test2 ...
Processing theory FOL-ex.Locale_Test3 ...
Processing theory FOL-ex.Locale_Test ...
Processing theory ZF.WF ...
Processing theory ZF.Order ...
Removing 189 theories ...
Processing theory ZF.Ordinal ...
Processing theory ZF.OrdQuant ...
Processing theory ZF.Nat ...
Processing theory ZF.Epsilon ...
Processing theory ZF.QPair ...
Processing theory ZF.Inductive ...
Processing theory ZF.Finite ...
Processing theory FOLP-ex.Classical ...
Processing theory FOLP-ex.If ...
Processing theory FOLP-ex.Intro ...
Processing theory FOLP-ex.Nat ...
Processing theory FOLP-ex.Propositional_Cla ...
Processing theory FOLP-ex.Quantifiers_Cla ...
Processing theory FOLP-ex.Foundation ...
Processing theory FOLP-ex.Intuitionistic ...
Processing theory FOLP-ex.Propositional_Int ...
Processing theory FOLP-ex.Quantifiers_Int ...
Processing theory HOL-Eisbach.Eisbach_Old_Appl_Syntax ...
Processing theory HOL-Eisbach.Examples_FOL ...
Processing theory HOL-Mirabelle-ex.Ex ...
Processing theory Pure-Examples.First_Order_Logic ...
Processing theory Pure-Examples.Higher_Order_Logic ...
Processing theory Sequents.Sequents ...
Processing theory Sequents.ILL ...
Processing theory Sequents.ILL_predlog ...
Processing theory Sequents.Washing ...
Processing theory Sequents.LK0 ...
Processing theory Sequents.LK ...
Processing theory Sequents.Hard_Quantifiers ...
Processing theory Sequents.Nat ...
Processing theory Sequents.Propositional ...
Processing theory Sequents.Quantifiers ...
Processing theory Sequents.Modal0 ...
Processing theory Sequents.S4 ...
Processing theory Sequents.S43 ...
Processing theory Sequents.T ...
Processing theory HOL-Prolog.HOHH ...
Processing theory HOL-Prolog.Func ...
Processing theory HOL-Prolog.Type ...
Processing theory HOL-Prolog.Test ...
Processing theory Haskell.Haskell ...
Processing theory SML.Examples ...
Processing theory Spec_Check.Spec_Check ...
Processing theory Spec_Check.Examples ...
Processing theory System.Scala ...
Processing theory ZF.OrderArith ...
Processing theory ZF.OrderType ...
Processing theory ZF.Cardinal ...
Processing theory ZF.Univ ...
Processing theory ZF.Arith ...
Processing theory ZF.ArithSimp ...
Processing theory ZF.Int ...
Processing theory ZF.CardinalArith ...
Processing theory ZF.QUniv ...
Processing theory ZF.Datatype ...
Processing theory Haskell.Test ...
Processing theory ZF.Bin ...
Processing theory ZF.List ...
Processing theory ZF.IntDiv ...
Processing theory ZF ...
Processing theory Logics_ZF.ZF_Isar ...
Processing theory ZF.AC ...
Processing theory ZF.Zorn ...
Processing theory ZF.Cardinal_AC ...
Processing theory ZF.InfDatatype ...
Processing theory ZF-AC.AC_Equiv ...
Processing theory ZF-AC.AC18_AC19 ...
Processing theory ZF-AC.AC7_AC9 ...
Processing theory ZF-AC.Cardinal_aux ...
Processing theory ZF-AC.WO6_WO1 ...
Processing theory ZF-AC.Hartog ...
Processing theory ZF-AC.AC16_lemmas ...
Processing theory ZF-AC.AC16_WO4 ...
Processing theory ZF-AC.DC ...
Processing theory ZF-AC.HH ...
Processing theory ZF-AC.AC15_WO6 ...
Processing theory ZF-AC.AC17_AC1 ...
Processing theory ZF-AC.WO1_AC ...
Processing theory ZF-AC.WO1_WO7 ...
Processing theory ZF-AC.WO2_AC16 ...
Processing theory ZF-Coind.Language ...
Processing theory ZF-Coind.Types ...
Processing theory ZF-Coind.Map ...
Processing theory ZF-Coind.Values ...
Processing theory ZF-Coind.Dynamic ...
Processing theory ZF-Coind.Static ...
Processing theory ZF-Constructible.MetaExists ...
Processing theory ZF-Coind.ECR ...
Processing theory ZF-Constructible.Normal ...
Processing theory ZF-Induct.Acc ...
Processing theory ZF-Constructible.Formula ...
Processing theory ZF-Constructible.Reflection ...
Processing theory ZF-Induct.Binary_Trees ...
Processing theory ZF-Induct.Comb ...
Processing theory ZF-Induct.FoldSet ...
Processing theory ZF-Induct.ListN ...
Processing theory ZF-Induct.Mutil ...
Processing theory ZF-Induct.Ntree ...
Processing theory ZF-Constructible.Relative ...
Processing theory ZF-Constructible.L_axioms ...
Processing theory ZF-Constructible.Wellorderings ...
Processing theory ZF-Constructible.WFrec ...
Processing theory ZF-Constructible.WF_absolute ...
Processing theory ZF-IMP.Com ...
Processing theory ZF-IMP.Denotation ...
Processing theory ZF-IMP.Equiv ...
Processing theory ZF-Induct.Primrec ...
Processing theory ZF-Induct.Rmap ...
Processing theory ZF-Induct.Term ...
Processing theory ZF-Induct.Tree_Forest ...
Processing theory ZF-Resid.Redex ...
Processing theory ZF-Resid.Substitution ...
Processing theory ZF-Resid.Residuals ...
Processing theory ZF-UNITY.State ...
Processing theory ZF-Induct.PropLog ...
Processing theory ZF-Resid.Reduction ...
Processing theory ZF-Resid.Confluence ...
Processing theory ZFC ...
Processing theory ZF-Induct.Brouwer ...
Processing theory ZF-ex.BinEx ...
Processing theory ZF-UNITY.GenPrefix ...
Processing theory ZF-UNITY.UNITY ...
Processing theory ZF-UNITY.Constrains ...
Processing theory ZF-UNITY.FP ...
Processing theory ZF-ex.CoUnit ...
Processing theory ZF-Induct.Datatypes ...
Processing theory Logics_ZF.ZF_examples ...
Processing theory ZF-Constructible.Separation ...
Processing theory ZF-Constructible.AC_in_L ...
Processing theory ZF-Constructible.Rank ...
Processing theory ZF-Induct.Multiset ...
Processing theory ZF-UNITY.MultisetSum ...
Processing theory ZF-UNITY.Monotonicity ...
Processing theory ZF-UNITY.Increasing ...
Processing theory ZF-UNITY.WFair ...
Processing theory ZF-UNITY.SubstAx ...
Processing theory ZF-UNITY.Follows ...
Processing theory ZF-UNITY.Mutex ...
Processing theory ZF-UNITY.Union ...
Processing theory ZF-UNITY.Comp ...
Processing theory ZF-ex.Commutation ...
Processing theory ZF-ex.LList ...
Processing theory ZF-ex.NatSum ...
Processing theory ZF-ex.Ramsey ...
Processing theory ZF-ex.misc ...
Processing theory ZF-Constructible.Datatype_absolute ...
Processing theory ZF-Constructible.Internalize ...
Processing theory ZF-Constructible.Rec_Separation ...
Processing theory ZF-Constructible.Rank_Separation ...
Processing theory ZF-Constructible.Satisfies_absolute ...
Processing theory ZF-Constructible.DPow_absolute ...
Processing theory ZF-ex.Group ...
Processing theory ZF-ex.Ring ...
Processing theory ZF-ex.Limit ...
Processing theory ZF-ex.Primes ...
Processing theory ZF-UNITY.Guar ...
Processing theory ZF-UNITY.AllocBase ...
Processing theory ZF-UNITY.ClientImpl ...
Processing theory ZF-UNITY.AllocImpl ...
Processing theory ZF-UNITY.Distributor ...
Processing theory ZF-UNITY.Merge ...
Exception in thread "Isabelle.process_manager" java.nio.file.NoSuchFileException: /tmp/isabelle-jenkins/process9587427150158769418/poly-stats-29958
	at java.base/sun.nio.fs.UnixException.translateToIOException(UnixException.java:92)
	at java.base/sun.nio.fs.UnixException.rethrowAsIOException(UnixException.java:106)
	at java.base/sun.nio.fs.UnixException.rethrowAsIOException(UnixException.java:111)
	at java.base/sun.nio.fs.UnixFileAttributeViews$Basic.readAttributes(UnixFileAttributeViews.java:55)
	at java.base/sun.nio.fs.UnixFileSystemProvider.readAttributes(UnixFileSystemProvider.java:148)
	at java.base/sun.nio.fs.LinuxFileSystemProvider.readAttributes(LinuxFileSystemProvider.java:99)
	at java.base/java.nio.file.Files.readAttributes(Files.java:1843)
	at java.base/java.nio.file.FileTreeWalker.getAttributes(FileTreeWalker.java:219)
	at java.base/java.nio.file.FileTreeWalker.visit(FileTreeWalker.java:276)
	at java.base/java.nio.file.FileTreeWalker.next(FileTreeWalker.java:373)
	at java.base/java.nio.file.Files.walkFileTree(Files.java:2840)
	at java.base/java.nio.file.Files.walkFileTree(Files.java:2876)
	at isabelle.Isabelle_System$.rm_tree(isabelle_system.scala:348)
	at isabelle.ML_Process$.$anonfun$apply$9(ml_process.scala:136)
	at isabelle.Bash$Process.do_cleanup(bash.scala:154)
	at isabelle.Bash$Process.join(bash.scala:163)
	at isabelle.Prover.$anonfun$process_result$1(prover.scala:102)
	at isabelle.Exn$.capture(exn.scala:61)
	at isabelle.Thread_Future.$anonfun$thread$1(future.scala:156)
	at isabelle.Isabelle_Thread$.$anonfun$fork$2(isabelle_thread.scala:65)
	at isabelle.Isabelle_Thread.run(isabelle_thread.scala:141)
Aborted by Administrative User
Sending interrupt signal to process
Aborted by Administrative User
Sending interrupt signal to process
Click here to forcibly terminate running steps
+ true
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Store)
[Pipeline] zip
Writing zip file of /media/data/jenkins/workspace/isabelle-dump/dump to /media/data/jenkins/workspace/isabelle-dump/dump.zip
Click here to forcibly terminate running steps
Aborted by Administrative User
[Pipeline] }
[Pipeline] // stage
[Pipeline] }
[Pipeline] // node
[Pipeline] End of Pipeline
java.lang.InterruptedException
	at java.lang.Object.wait(Native Method)
	at hudson.remoting.Request.call(Request.java:177)
	at hudson.remoting.Channel.call(Channel.java:1000)
	at hudson.FilePath.act(FilePath.java:1158)
	at hudson.FilePath.act(FilePath.java:1147)
	at org.jenkinsci.plugins.pipeline.utility.steps.zip.ZipStepExecution.run(ZipStepExecution.java:93)
	at org.jenkinsci.plugins.pipeline.utility.steps.zip.ZipStepExecution.run(ZipStepExecution.java:58)
	at org.jenkinsci.plugins.workflow.steps.SynchronousNonBlockingStepExecution.lambda$start$0(SynchronousNonBlockingStepExecution.java:47)
	at java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:511)
	at java.util.concurrent.FutureTask.run(FutureTask.java:266)
	at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
	at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
	at java.lang.Thread.run(Thread.java:748)
Finished: ABORTED