+ 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)
Sending interrupt signal to process
Sending interrupt signal to process
+ true
![[Jenkins]](/jenkins/static/77e8e0f1/images/svgs/logo.svg){kind=logo}
