Console Output

+ bin/isabelle dump -o threads=8 -D afp/thys -X slow -X large -X very_slow -a
Loading 735 sessions ...
Build started for Isabelle/Pure ...
Building Pure ...
Finished Pure (0:00:27 elapsed time, 0:00:27 cpu time, factor 0.98)
### Skipping theory HOL-Import.HOL_Light_Import  (undefined HOL_LIGHT_BUNDLE)
### Skipping theory HOL-Codegenerator_Test.Code_Test_MLton  (undefined ISABELLE_MLTON)
### Skipping theory HOL-Codegenerator_Test.Code_Test_SMLNJ  (undefined ISABELLE_SMLNJ)
### Skipping theory HOL-Library.Code_Prolog  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.Code_Prolog_Examples  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.Context_Free_Grammar_Example  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.Hotel_Example  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.Hotel_Example_Prolog  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.Lambda_Example  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.List_Examples  (undefined ISABELLE_SWIPL)
### Skipping theory HOL-Predicate_Compile_Examples.Reg_Exp_Example  (undefined ISABELLE_SWIPL)
### Skipping theory PAC_Checker.PAC_Checker_MLton  (undefined ISABELLE_MLTON)
### Skipping theory Buchi_Complementation.Complementation_Build  (undefined ISABELLE_MLTON)
### Skipping theory CakeML.Compiler_Test  (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
### Skipping theory CakeML_Codegen.Test_Datatypes  (undefined ISABELLE_CAKEML_HOME, ISABELLE_CC)
### Skipping theory Native_Word.Native_Word_Test_MLton  (undefined ISABELLE_MLTON)
### Skipping theory Native_Word.Native_Word_Test_MLton2  (undefined ISABELLE_MLTON)
### Skipping theory Native_Word.Native_Word_Test_SMLNJ  (undefined ISABELLE_SMLNJ)
### Skipping theory Native_Word.Native_Word_Test_SMLNJ2  (undefined ISABELLE_SMLNJ)
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.Product_Type ...
Processing theory HOL.Complete_Partial_Order ...
Processing theory HOL.Sum_Type ...
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.Wfrec ...
Processing theory HOL.Order_Relation ...
Processing theory HOL.Hilbert_Choice ...
Processing theory HOL.BNF_Wellorder_Relation ...
Processing theory HOL.BNF_Wellorder_Embedding ...
Processing theory HOL.Zorn ...
Processing theory HOL.BNF_Wellorder_Constructions ...
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.Option ...
Processing theory HOL.Extraction ...
Processing theory HOL.Lattices_Big ...
Processing theory HOL.Partial_Function ...
Processing theory HOL.Fun_Def ...
Processing theory HOL.Quotient ...
Processing theory HOL.Int ...
Processing theory HOL.Euclidean_Division ...
Processing theory HOL.Parity ...
Processing theory HOL.Divides ...
Processing theory HOL.Numeral_Simprocs ...
Processing theory HOL.Semiring_Normalization ...
Processing theory HOL.Groebner_Basis ...
Processing theory HOL.SMT ...
Processing theory HOL.Code_Numeral ...
Processing theory HOL.Set_Interval ...
Processing theory HOL.Presburger ...
Processing theory HOL.Conditionally_Complete_Lattices ...
Processing theory HOL.Sledgehammer ...
Processing theory HOL.Filter ...
Processing theory HOL.List ...
Processing theory HOL.Map ...
Processing theory HOL.Groups_List ...
Processing theory HOL.Factorial ...
Processing theory HOL.Random ...
Processing theory HOL.Binomial ...
Processing theory HOL.Enum ...
Processing theory HOL.String ...
Processing theory HOL.Typerep ...
Processing theory HOL.Predicate ...
Processing theory HOL.Lazy_Sequence ...
Processing theory HOL.Limited_Sequence ...
Processing theory HOL.GCD ...
Processing theory HOL.BNF_Greatest_Fixpoint ...
Processing theory HOL.Code_Evaluation ...
Processing theory HOL.Quickcheck_Random ...
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.Nitpick ...
Processing theory HOL.Nunchaku ...
Processing theory HOL.Predicate_Compile ...
Processing theory Main ...
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-Proofs-Extraction.Util ...
Processing theory HOL-Examples.Drinker ...
Processing theory HOL-Proofs-ex.XML_Data ...
Processing theory HOL-Library.Open_State_Syntax ...
Processing theory HOL-Library.Realizers ...
Processing theory HOL-Proofs-Extraction.QuotRem ...
Processing theory HOL-Proofs-Lambda.ListOrder ...
Processing theory HOL-Proofs-Lambda.Commutation ...
Processing theory HOL-Proofs-ex.Hilbert_Classical ...
Processing theory HOL-Proofs-ex.Proof_Terms ...
Processing theory HOL-Proofs-Extraction.Warshall ...
Processing theory HOL-Proofs-Extraction.Higman ...
Processing theory HOL-Proofs-Lambda.Lambda ...
Processing theory HOL-Proofs-Lambda.ListApplication ...
Processing theory HOL-Proofs-Lambda.LambdaType ...
Processing theory HOL-Proofs-Lambda.ParRed ...
Processing theory HOL-Proofs-Lambda.ListBeta ...
Processing theory HOL-Proofs-Lambda.InductTermi ...
Processing theory HOL-Proofs-Lambda.StrongNorm ...
Processing theory HOL-Proofs-Lambda.NormalForm ...
Processing theory HOL-Proofs-Lambda.Standardization ...
Removing 8 theories ...
Processing theory HOL-Proofs-Extraction.Greatest_Common_Divisor ...
Processing theory HOL-Proofs-Lambda.Eta ...
Processing theory HOL-Proofs-Extraction.Higman_Extraction ...
Processing theory HOL-Library.Multiset ...
Processing theory HOL-Proofs-Extraction.Pigeonhole ...
Processing theory HOL-Computational_Algebra.Factorial_Ring ...
Removing 9 theories ...
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-Library.FuncSet ...
Processing theory HOL-Library.Infinite_Set ...
Processing theory HOL-Library.Nat_Bijection ...
Processing theory HOL-Library.Old_Datatype ...
Processing theory HOL-Library.Phantom_Type ...
Processing theory HOL-Library.Cardinality ...
Processing theory HOL-Library.Numeral_Type ...
Processing theory HOL-Library.Product_Plus ...
Processing theory HOL-Library.Product_Order ...
Processing theory HOL-Library.Set_Algebras ...
Processing theory HOL.Modules ...
Processing theory HOL.Vector_Spaces ...
Processing theory HOL.Archimedean_Field ...
Processing theory HOL.Rat ...
Processing theory HOL.Real ...
Processing theory HOL-Library.Countable ...
Processing theory HOL-Library.Countable_Set ...
Processing theory HOL-Library.Set_Idioms ...
Processing theory HOL-Combinatorics.Permutations ...
Processing theory HOL-Library.Countable_Complete_Lattices ...
Processing theory HOL.Topological_Spaces ...
Processing theory HOL.Real_Vector_Spaces ...
Processing theory HOL-Analysis.Metric_Arith ...
Processing theory HOL.Inequalities ...
Processing theory HOL.Limits ...
Processing theory HOL.Deriv ...
Processing theory HOL.NthRoot ...
Processing theory HOL.Series ...
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.L2_Norm ...
Processing theory HOL-Analysis.Operator_Norm ...
Processing theory HOL-Analysis.Poly_Roots ...
Processing theory HOL-Library.Indicator_Function ...
Processing theory HOL-Library.Order_Continuity ...
Processing theory HOL-Library.Sum_of_Squares ...
Processing theory HOL-Analysis.Norm_Arith ...
Processing theory HOL-Library.Liminf_Limsup ...
Processing theory HOL-Library.Nonpos_Ints ...
Processing theory HOL-Analysis.Inner_Product ...
Processing theory HOL-Analysis.Product_Vector ...
Processing theory HOL-Analysis.Euclidean_Space ...
Processing theory HOL-Library.Discrete ...
Processing theory HOL-Library.Extended_Nat ...
Processing theory HOL-Library.Periodic_Fun ...
Processing theory HOL-Analysis.Finite_Cartesian_Product ...
Processing theory HOL-Analysis.Linear_Algebra ...
Processing theory HOL-Library.Landau_Symbols ...
Processing theory HOL-Analysis.Elementary_Topology ...
Processing theory HOL-Analysis.Affine ...
Processing theory HOL-Analysis.Cartesian_Space ...
Processing theory HOL-Analysis.Determinants ...
Processing theory HOL-Library.Extended_Real ...
Processing theory HOL-Analysis.Convex ...
Processing theory HOL-Library.Extended_Nonnegative_Real ...
Processing theory HOL-Computational_Algebra.Formal_Power_Series ...
Processing theory HOL-Analysis.Abstract_Topology ...
Processing theory HOL-Analysis.Abstract_Limits ...
Processing theory HOL-Analysis.Sigma_Algebra ...
Processing theory HOL-Analysis.Measurable ...
Processing theory HOL-Analysis.Abstract_Topology_2 ...
Processing theory HOL-Analysis.Connected ...
Processing theory HOL-Analysis.Elementary_Metric_Spaces ...
Processing theory HOL-Analysis.Measure_Space ...
Processing theory HOL-Analysis.Caratheodory ...
Processing theory HOL-Analysis.Function_Topology ...
Processing theory HOL-Analysis.Product_Topology ...
Processing theory HOL-Analysis.Elementary_Normed_Spaces ...
Processing theory HOL-Analysis.Function_Metric ...
Processing theory HOL-Analysis.T1_Spaces ...
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.Line_Segment ...
Processing theory HOL-Analysis.Summation_Tests ...
Processing theory HOL-Analysis.Uniform_Limit ...
Processing theory HOL-Analysis.Bounded_Continuous_Function ...
Processing theory HOL-Analysis.Bounded_Linear_Function ...
Processing theory HOL-Analysis.Tagged_Division ...
Processing theory HOL-Analysis.Ordered_Euclidean_Space ...
Processing theory HOL-Analysis.Derivative ...
Processing theory HOL-Analysis.Cartesian_Euclidean_Space ...
Processing theory HOL-Analysis.Complex_Analysis_Basics ...
Processing theory HOL-Analysis.Borel_Space ...
Processing theory HOL-Analysis.Cross3 ...
Processing theory HOL-Analysis.Lipschitz ...
Processing theory HOL-Analysis.Starlike ...
Processing theory HOL-Analysis.Multivariate_Analysis ...
Processing theory HOL-Analysis.Regularity ...
Processing theory HOL-Analysis.Continuous_Extension ...
Processing theory HOL-Analysis.Nonnegative_Lebesgue_Integration ...
Processing theory HOL-Analysis.Complex_Transcendental ...
Processing theory HOL-Analysis.Generalised_Binomial_Theorem ...
Processing theory HOL-Analysis.Binary_Product_Measure ...
Processing theory HOL-Analysis.Embed_Measure ...
Processing theory HOL-Analysis.FPS_Convergence ...
Processing theory HOL-Analysis.Harmonic_Numbers ...
Processing theory HOL-Analysis.Finite_Product_Measure ...
Processing theory HOL-Analysis.Infinite_Products ...
Processing theory HOL-Analysis.Path_Connected ...
Processing theory HOL-Analysis.Locally ...
Processing theory HOL-Analysis.Weierstrass_Theorems ...
Processing theory HOL-Analysis.Bochner_Integration ...
Processing theory HOL-Analysis.Arcwise_Connected ...
Processing theory HOL-Analysis.Polytope ...
Processing theory HOL-Analysis.Radon_Nikodym ...
Processing theory HOL-Analysis.Complete_Measure ...
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.Fashoda_Theorem ...
Processing theory HOL-Analysis.Henstock_Kurzweil_Integration ...
Processing theory HOL-Analysis.Integral_Test ...
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.Vitali_Covering_Theorem ...
Processing theory HOL-Analysis.Lebesgue_Integral_Substitution ...
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 ...
Processing theory HOL-Library.Adhoc_Overloading ...
Processing theory HOL-Library.Monad_Syntax ...
Processing theory HOL-Library.Lattice_Syntax ...
Processing theory HOL-Library.Rewrite ...
Processing theory HOL-Library.Conditional_Parametricity ...
Processing theory HOL-Library.Diagonal_Subsequence ...
Processing theory HOL-Probability.Discrete_Topology ...
Processing theory HOL-Combinatorics.Multiset_Permutations ...
Processing theory HOL-Library.Mapping ...
Processing theory HOL-Library.Stream ...
Processing theory HOL-Probability.Essential_Supremum ...
Processing theory HOL-Probability.Stopping_Time ...
Processing theory HOL-Library.AList ...
Processing theory HOL-Library.AList_Mapping ...
Processing theory HOL-Library.Complete_Partial_Order2 ...
Processing theory HOL-Library.FSet ...
Processing theory HOL-Library.Tree ...
Processing theory HOL-Probability.Tree_Space ...
Processing theory HOL-Library.Sublist ...
Removing 11 theories ...
Processing theory HOL-Library.Linear_Temporal_Logic_on_Streams ...
Processing theory HOL-Probability.Probability_Measure ...
Processing theory HOL-Probability.Distribution_Functions ...
Processing theory HOL-Probability.Weak_Convergence ...
Processing theory HOL-Library.Finite_Map ...
Processing theory HOL-Probability.Helly_Selection ...
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.Projective_Limit ...
Processing theory HOL-Probability.Probability_Mass_Function ...
Processing theory HOL-Probability.PMF_Impl ...
Processing theory HOL-Probability.Random_Permutations ...
Processing theory HOL-Probability.Independent_Family ...
Processing theory HOL-Probability.Convolution ...
Processing theory HOL-Probability.Product_PMF ...
Processing theory HOL-Probability.SPMF ...
Sending interrupt signal to process
+ true