Console Output

Started by timer
Running in Durability level: MAX_SURVIVABILITY
[Pipeline] Start of Pipeline
[Pipeline] node
Running on workerlrz6 in /media/data/jenkins/workspace/isabelle-dump
[Pipeline] {
[Pipeline] timeout
Timeout set to expire in 1 day 6 hr
[Pipeline] {
[Pipeline] stage
[Pipeline] { (Prepare)
[Pipeline] cleanWs
[WS-CLEANUP] Deleting project workspace...
[WS-CLEANUP] Deferred wipeout is used...
[WS-CLEANUP] done
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Checkout)
[Pipeline] script
[Pipeline] {
[Pipeline] httpRequest
HttpMethod: GET
URL: https://ci.isabelle.systems/jenkins/job/isabelle-all/lastSuccessfulBuild/api/xml?tree=actions[*[_class,mercurialNodeName]]&xpath=freeStyleBuild/action[@_class=%22hudson.plugins.mercurial.MercurialTagAction%22]/mercurialNodeName&wrapper=revs
Sending request to url: https://ci.isabelle.systems/jenkins/job/isabelle-all/lastSuccessfulBuild/api/xml?tree=actions[*[_class,mercurialNodeName]]&xpath=freeStyleBuild/action[@_class=%22hudson.plugins.mercurial.MercurialTagAction%22]/mercurialNodeName&wrapper=revs
Response Code: HTTP/1.1 200 OK
Success code from java.util.stream.IntPipeline$Head@4e9dcb28
[Pipeline] }
[Pipeline] // script
[Pipeline] checkout
$ hg clone --rev d030b988d470061e400b8e4ed78ea337281e7001 --noupdate https://isabelle.in.tum.de/repos/isabelle /media/data/jenkins/workspace/isabelle-dump
adding changesets
adding manifests
adding file changes
added 74148 changesets with 202867 changes to 11442 files
new changesets a5a9c433f639:d030b988d470
[isabelle-dump] $ hg update --rev d030b988d470061e400b8e4ed78ea337281e7001
3457 files updated, 0 files merged, 0 files removed, 0 files unresolved
[isabelle-dump] $ hg log --rev . --template {node}
[isabelle-dump] $ hg log --rev . --template {rev}
[isabelle-dump] $ hg id --branch
[isabelle-dump] $ hg log --rev 6d8674ffb962256e2760e34e66fcc8eb0aa67fd0 --template exists\n
exists
[isabelle-dump] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('d030b988d470061e400b8e4ed78ea337281e7001') and not ancestors(6d8674ffb962256e2760e34e66fcc8eb0aa67fd0)" --encoding UTF-8 --encodingmode replace
[isabelle-dump] $ hg log --rev . --template {node}
[isabelle-dump] $ hg log --rev . --template {rev}
[isabelle-dump] $ hg id --branch
[Pipeline] checkout
$ hg clone --rev 34754976c5bf15e62139cb21ec528a78a0ca0119 --noupdate https://foss.heptapod.net/isa-afp/afp-devel /media/data/jenkins/workspace/isabelle-dump/afp
adding changesets
adding manifests
adding file changes
added 11963 changesets with 80630 changes to 12351 files
new changesets 86acbdb19eec:34754976c5bf
[afp] $ hg update --rev 34754976c5bf15e62139cb21ec528a78a0ca0119
9899 files updated, 0 files merged, 0 files removed, 0 files unresolved
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg id --branch
[afp] $ hg log --rev 6beec57f7d3f73746ac97ee20cda20cd251756a3 --template exists\n
exists
[afp] $ hg log --template "<changeset node='{node}' author='{author|xmlescape}' rev='{rev}' date='{date}'><msg>{desc|xmlescape}</msg>{file_adds % '<addedFile>{file|xmlescape}</addedFile>'}{file_dels % '<deletedFile>{file|xmlescape}</deletedFile>'}{files % '<file>{file|xmlescape}</file>'}<parents>{parents}</parents></changeset>\n" --rev "ancestors('34754976c5bf15e62139cb21ec528a78a0ca0119') and not ancestors(6beec57f7d3f73746ac97ee20cda20cd251756a3)" --encoding UTF-8 --encodingmode replace
[afp] $ hg log --rev . --template {node}
[afp] $ hg log --rev . --template {rev}
[afp] $ hg id --branch
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Install)
[Pipeline] sh
+ bin/isabelle components -a
### Missing Isabelle component: "/media/data/jenkins/.isabelle/contrib/jedit-20210802"
Getting "https://isabelle.sketis.net/components/jedit-20210802.tar.gz"
Unpacking "/media/data/jenkins/.isabelle/contrib/jedit-20210802.tar.gz"
[Pipeline] sh
+ bin/isabelle jedit -bf
### Building Isabelle/Scala (/media/data/jenkins/workspace/isabelle-dump/lib/classes/isabelle.jar) ...
### Building graph browser (/media/data/jenkins/workspace/isabelle-dump/lib/classes/isabelle_graphbrowser.jar) ...
Note: Some input files use unchecked or unsafe operations.
Note: Recompile with -Xlint:unchecked for details.
### Building Isabelle/Scala/Admin (/media/data/jenkins/workspace/isabelle-dump/lib/classes/isabelle_admin.jar) ...
[Pipeline] sh
+ bin/isabelle ocaml_setup
# Run eval $(opam env) to update the current shell environment
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
       opam update

[NOTE] Package zarith is already installed (current version is 1.12).
[Pipeline] sh
+ bin/isabelle ghc_setup
stack will use a sandboxed GHC it installed
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
The Glorious Glasgow Haskell Compilation System, version 8.10.4
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Dump)
[Pipeline] sh
+ bin/isabelle dump -o threads=4 -D afp/thys -b Pure -X slow -X large -X very_slow -O dump -a
Loading 751 sessions ...
Build started for Isabelle/Pure ...
Building Pure ...
Finished Pure (0:00:28 elapsed time, 0:00:27 cpu time, factor 0.96)
### 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 133 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.Boolean_Algebras ...
Processing theory HOL.Set ...
Processing theory HOL.Fun ...
Processing theory HOL.Typedef ...
Processing theory HOL.Complete_Lattices ...
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.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.Numeral_Simprocs ...
Processing theory HOL.SMT ...
Processing theory HOL.Semiring_Normalization ...
Processing theory HOL.Groebner_Basis ...
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.Binomial ...
Processing theory HOL.Enum ...
Processing theory HOL.Bit_Operations ...
Processing theory HOL.Code_Numeral ...
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.Random ...
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.Predicate_Compile ...
Processing theory HOL.Mirabelle ...
Processing theory HOL.GCD ...
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.Higman ...
Processing theory HOL-Proofs-Extraction.Util ...
Processing theory HOL-Proofs-Extraction.QuotRem ...
Processing theory HOL-Proofs-Lambda.Commutation ...
Processing theory HOL-Proofs-Extraction.Warshall ...
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-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-Extraction.Higman_Extraction ...
Processing theory HOL-Proofs-Lambda.Eta ...
Processing theory HOL-Proofs-Lambda.NormalForm ...
Processing theory HOL-Proofs-Lambda.Standardization ...
Processing theory HOL-Proofs-Extraction.Pigeonhole ...
Processing theory HOL-Library.Multiset ...
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 252 theories ...
Processing theory HOL-Combinatorics.Transposition ...
Processing theory HOL.Hull ...
Processing theory HOL-Library.Disjoint_Sets ...
Processing theory HOL-Library.FuncSet ...
Processing theory HOL.Modules ...
Processing theory HOL.Archimedean_Field ...
Processing theory HOL-Library.Infinite_Set ...
Processing theory HOL-Library.Nat_Bijection ...
Processing theory HOL-Library.Old_Datatype ...
Processing theory HOL.Rat ...
Processing theory HOL-Library.Countable ...
Processing theory HOL-Library.Countable_Set ...
Processing theory HOL.Real ...
Processing theory HOL.Vector_Spaces ...
Processing theory HOL-Library.Phantom_Type ...
Processing theory HOL-Library.Cardinality ...
Processing theory HOL-Library.Set_Idioms ...
Processing theory HOL-Library.Product_Plus ...
Processing theory HOL-Library.Product_Order ...
Processing theory HOL-Library.Set_Algebras ...
Processing theory HOL-Library.Numeral_Type ...
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.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.Elementary_Topology ...
Processing theory HOL-Analysis.Linear_Algebra ...
Processing theory HOL-Library.Discrete ...
Processing theory HOL-Analysis.Affine ...
Processing theory HOL-Analysis.Cartesian_Space ...
Processing theory HOL-Library.Indicator_Function ...
Processing theory HOL-Library.Liminf_Limsup ...
Processing theory HOL-Library.Nonpos_Ints ...
Processing theory HOL-Analysis.Determinants ...
Processing theory HOL-Library.Order_Continuity ...
Processing theory HOL-Library.Extended_Nat ...
Processing theory HOL-Library.Periodic_Fun ...
Processing theory HOL-Analysis.Convex ...
Processing theory HOL-Analysis.Abstract_Topology ...
Processing theory HOL-Analysis.Abstract_Limits ...
Processing theory HOL-Computational_Algebra.Formal_Power_Series ...
Processing theory HOL-Library.Landau_Symbols ...
Processing theory HOL-Library.Sum_of_Squares ...
Processing theory HOL-Analysis.Norm_Arith ...
Processing theory HOL-Analysis.Abstract_Topology_2 ...
Processing theory HOL-Analysis.Connected ...
Processing theory HOL-Library.Extended_Real ...
Processing theory HOL-Analysis.Function_Topology ...
Processing theory HOL-Analysis.Elementary_Metric_Spaces ...
Processing theory HOL-Library.Extended_Nonnegative_Real ...
Processing theory HOL-Analysis.Product_Topology ...
Processing theory HOL-Analysis.Elementary_Normed_Spaces ...
Processing theory HOL-Analysis.Function_Metric ...
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.Line_Segment ...
Processing theory HOL-Analysis.Lindelof_Spaces ...
Processing theory HOL-Analysis.Convex_Euclidean_Space ...
Processing theory HOL-Analysis.Measure_Space ...
Processing theory HOL-Analysis.Caratheodory ...
Processing theory HOL-Analysis.Ordered_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.Tagged_Division ...
Processing theory HOL-Analysis.Bounded_Linear_Function ...
Processing theory HOL-Analysis.Derivative ...
Processing theory HOL-Analysis.Cartesian_Euclidean_Space ...
Processing theory HOL-Analysis.Cross3 ...
Processing theory HOL-Analysis.Complex_Analysis_Basics ...
Processing theory HOL-Analysis.Starlike ...
Processing theory HOL-Analysis.Lipschitz ...
Processing theory HOL-Analysis.Continuous_Extension ...
Processing theory HOL-Analysis.Borel_Space ...
Processing theory HOL-Analysis.Regularity ...
Processing theory HOL-Analysis.Multivariate_Analysis ...
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.Harmonic_Numbers ...
Processing theory HOL-Analysis.FPS_Convergence ...
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.Bochner_Integration ...
Processing theory HOL-Analysis.Arcwise_Connected ...
Processing theory HOL-Analysis.Complete_Measure ...
Processing theory HOL-Analysis.Polytope ...
Processing theory HOL-Analysis.Radon_Nikodym ...
Processing theory HOL-Analysis.Set_Integral ...
Processing theory HOL-Analysis.Weierstrass_Theorems ...
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.Lebesgue_Integral_Substitution ...
Processing theory HOL-Analysis.Gamma_Function ...
Processing theory HOL-Analysis.Ball_Volume ...
Processing theory HOL-Analysis.Vitali_Covering_Theorem ...
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.Adhoc_Overloading ...
Processing theory HOL-Library.Monad_Syntax ...
Processing theory HOL-Library.Conditional_Parametricity ...
Processing theory HOL-Library.Lattice_Syntax ...
Processing theory HOL-Library.Rewrite ...
Processing theory HOL-Library.AList ...
Processing theory HOL-Library.Stream ...
Processing theory HOL-Library.Complete_Partial_Order2 ...
Processing theory HOL-Library.FSet ...
Processing theory HOL-Library.Sublist ...
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-Library.Linear_Temporal_Logic_on_Streams ...
Processing theory HOL-Probability.Stopping_Time ...
Processing theory HOL-Library.Mapping ...
Processing theory HOL-Library.AList_Mapping ...
Processing theory HOL-Library.Tree ...
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-Library.Finite_Map ...
Processing theory HOL-Probability.Helly_Selection ...
Processing theory HOL-Probability.Conditional_Expectation ...
Processing theory HOL-Probability.Fin_Map ...
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 ...
Removing 25 theories ...
Processing theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure ...
Processing theory HOL-Probability-ex.Dining_Cryptographers ...
Loading 39 theories ...
Processing theory HOL-Library.Fun_Lexorder ...
Processing theory HOL-Cardinals.Fun_More ...
Processing theory HOL-Cardinals.Order_Union ...
Processing theory HOL-Cardinals.Order_Relation_More ...
Processing theory HOL-Cardinals.Wellfounded_More ...
Processing theory HOL-Cardinals.Wellorder_Relation ...
Processing theory HOL-Library.Groups_Big_Fun ...
Processing theory HOL-Library.More_List ...
Removing 59 theories ...
Processing theory HOL-Cardinals.Wellorder_Embedding ...
Processing theory HOL-Library.Equipollence ...
Processing theory HOL-Cardinals.Wellorder_Constructions ...
Processing theory HOL-Cardinals.Cardinal_Order_Relation ...
Processing theory HOL-Cardinals.Cardinal_Arithmetic ...
Processing theory HOL-Algebra.Congruence ...
Processing theory HOL-Algebra.Order ...
Processing theory HOL-Algebra.Lattice ...
Processing theory HOL-Library.Poly_Mapping ...
Processing theory HOL-Algebra.Complete_Lattice ...
Processing theory HOL-Algebra.Group ...
Processing theory HOL-Algebra.FiniteProduct ...
Processing theory HOL-Algebra.Coset ...
Processing theory HOL-Algebra.Ring ...
Processing theory HOL-Algebra.Module ...
Processing theory HOL-Algebra.Generated_Groups ...
Processing theory HOL-Algebra.Solvable_Groups ...
Processing theory HOL-Algebra.Elementary_Groups ...
Processing theory HOL-Algebra.AbelCoset ...
Processing theory HOL-Algebra.Ideal ...
Processing theory HOL-Algebra.RingHom ...
Processing theory HOL-Algebra.Product_Groups ...
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 95 theories ...
Removing 32 theories ...
Processing theory HOL-Data_Structures.Less_False ...
Processing theory HOL-Data_Structures.Sorted_Less ...
Processing theory HOL-Computational_Algebra.Group_Closure ...
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-Computational_Algebra.Fraction_Field ...
Processing theory HOL-Data_Structures.AList_Upd_Del ...
Processing theory HOL-Data_Structures.Map_Specs ...
Processing theory HOL-Computational_Algebra.Nth_Powers ...
Processing theory HOL-Library.State_Monad ...
Processing theory HOL-Library.Case_Converter ...
Processing theory HOL-Library.BNF_Corec ...
Processing theory HOL-Computational_Algebra.Squarefree ...
Processing theory HOL-Library.Code_Lazy ...
Processing theory HOL-Library.Simps_Case_Conv ...
Processing theory HOL-Computational_Algebra.Normalized_Fraction ...
Processing theory HOL-Library.Multiset_Order ...
Processing theory HOL-Library.Confluence ...
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.IArray ...
Processing theory HOL-Library.Omega_Words_Fun ...
Processing theory HOL-Library.Combine_PER ...
Processing theory HOL-Library.ListVector ...
Processing theory HOL-Examples.Records ...
Processing theory HOL-Library.Extended ...
Processing theory HOL-Library.Char_ord ...
Processing theory HOL-Library.Disjoint_FSets ...
Processing theory HOL-Library.Option_ord ...
Processing theory HOL-Library.Pattern_Aliases ...
Processing theory HOL-Library.Code_Cardinality ...
Processing theory HOL-Library.Type_Length ...
Processing theory HOL-Library.Parallel ...
Processing theory HOL-Library.Saturated ...
Processing theory HOL-Library.Power_By_Squaring ...
Processing theory HOL-Library.Quotient_Syntax ...
Processing theory HOL-Library.Countable_Set_Type ...
Processing theory HOL-Library.Preorder ...
Processing theory HOL-Library.Quotient_Option ...
Processing theory HOL-Library.Quotient_Product ...
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.Lattice_Constructions ...
Processing theory HOL-Library.Finite_Lattice ...
Processing theory HOL-Library.Subseq_Order ...
Processing theory HOL-Library.Signed_Division ...
Processing theory HOL-Library.Transitive_Closure_Table ...
Processing theory HOL-Library.Ramsey ...
Processing theory HOL-Library.Tree_Multiset ...
Processing theory HOL-Data_Structures.Tree_Set ...
Processing theory HOL-Data_Structures.Tree_Map ...
Processing theory HOL-Library.Uprod ...
Processing theory HOL-Library.While_Combinator ...
Processing theory HOL-Library.Bourbaki_Witt_Fixpoint ...
Processing theory HOL-Library.Z2 ...
Processing theory HOL-Library.Sorting_Algorithms ...
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.Word ...
Processing theory HOL-Library.Lub_Glb ...
Processing theory HOL-Library.Quadratic_Discriminant ...
Processing theory HOL-Library.Tree_Real ...
Processing theory HOL-Library.Lattice_Algebras ...
Processing theory HOL-Computational_Algebra.Polynomial ...
Processing theory HOL-Computational_Algebra.Polynomial_FPS ...
Processing theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra ...
Processing theory HOL-Computational_Algebra.Formal_Laurent_Series ...
Processing theory HOL-Library.Float ...
Processing theory HOL-Computational_Algebra.Polynomial_Factorial ...
Processing theory HOL-Computational_Algebra.Computational_Algebra ...
Processing theory HOL-Library.Interval ...
Processing theory HOL-Library.Interval_Float ...
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 7 theories ...
Processing theory HOL-Real_Asymp.Inst_Existentials ...
Processing theory HOL-Real_Asymp.Eventuallize ...
Processing theory HOL-Real_Asymp.Lazy_Eval ...
Removing 57 theories ...
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.Real_Asymp_Examples ...
Loading 5 theories ...
Processing theory HOL-Library.Code_Target_Numeral_Float ...
Processing theory HOL-Decision_Procs.Dense_Linear_Order ...
Removing 1 theories ...
Processing theory HOL-Decision_Procs.Approximation_Bounds ...
Processing theory HOL-Decision_Procs.Approximation ...
Processing theory HOL-Real_Asymp.Real_Asymp_Approx ...
Processing theory HOL-Real_Asymp-Manual.Real_Asymp_Doc ...
Loading 26 theories ...
Processing theory HOL-Algebra.Exponent ...
Processing theory HOL-Combinatorics.List_Permutation ...
Processing theory HOL-Algebra.Bij ...
Processing theory HOL-Algebra.Sylow ...
Processing theory HOL-Combinatorics.Cycles ...
Processing theory HOL-Algebra.Group_Action ...
Processing theory HOL-Algebra.Galois_Connection ...
Processing theory HOL-Algebra.Zassenhaus ...
Processing theory HOL-Algebra.Ideal_Product ...
Processing theory HOL-Algebra.Sym_Groups ...
Processing theory HOL-Algebra.QuotRing ...
Processing theory HOL-Algebra.Divisibility ...
Removing 9 theories ...
Processing theory HOL-Algebra.Weak_Morphisms ...
Processing theory HOL-Algebra.Chinese_Remainder ...
Processing theory HOL-Algebra.Subrings ...
Processing theory HOL-Algebra.Generated_Rings ...
Processing theory HOL-Algebra.Generated_Fields ...
Processing theory HOL-Algebra.IntRing ...
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.Finite_Extensions ...
Processing theory HOL-Algebra.Indexed_Polynomials ...
Processing theory HOL-Algebra.Algebraic_Closure ...
Loading 19 theories ...
Processing theory HOL-Algebra.Algebra ...
Processing theory HOL-Decision_Procs.Conversions ...
Processing theory HOL-Decision_Procs.DP_Library ...
Processing theory HOL-Library.Old_Recdef ...
Processing theory HOL-Decision_Procs.Algebra_Aux ...
Removing 33 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 ...
Processing theory HOL-Decision_Procs.Decision_Procs ...
Loading 21 theories ...
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 ...
Loading 12 theories ...
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 ...
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 47 theories ...
Processing theory HOL-Number_Theory.Fib ...
Processing theory HOL-Number_Theory.Prime_Powers ...
Processing theory HOL-Number_Theory.Cong ...
Processing theory HOL-Number_Theory.Mod_Exp ...
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 ...
Loading 61 theories ...
Processing theory HOL-Number_Theory.Number_Theory ...
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-Matrix_LP.LP ...
Processing theory HOL-Matrix_LP.ComputeHOL ...
Processing theory HOLCF.Discrete ...
Processing theory HOL-Matrix_LP.ComputeFloat ...
Processing theory HOLCF.Up ...
Processing theory HOLCF.Lift ...
Processing theory HOLCF.One ...
Processing theory HOLCF.Tr ...
Processing theory HOLCF.Ssum ...
Processing theory HOL-Matrix_LP.ComputeNumeral ...
Processing theory HOLCF.Fixrec ...
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 HOL-Matrix_LP.Matrix ...
Removing 23 theories ...
Processing theory HOLCF.Powerdomains ...
Processing theory HOLCF ...
Processing theory HOLCF-Library.Bool_Discrete ...
Processing theory HOLCF-Library.Char_Discrete ...
Processing theory HOLCF-Library.Int_Discrete ...
Processing theory HOLCF-Library.Nat_Discrete ...
Processing theory HOLCF-Library.Sum_Cpo ...
Processing theory HOLCF-Library.Option_Cpo ...
Processing theory HOLCF-Library.Defl_Bifinite ...
Processing theory HOLCF-Library.List_Cpo ...
Processing theory HOLCF-Library.List_Predomain ...
Processing theory HOLCF-Library.Stream ...
Processing theory HOLCF-FOCUS.Fstream ...
Loading 32 theories ...
Processing theory HOLCF-FOCUS.FOCUS ...
Processing theory HOLCF-FOCUS.Buffer ...
Processing theory HOLCF-FOCUS.Fstreams ...
Processing theory HOLCF-FOCUS.Stream_adm ...
Processing theory HOLCF-FOCUS.Buffer_adm ...
Processing theory HOLCF-Library.HOLCF_Library ...
Processing theory HOLCF-ex.Dagstuhl ...
Processing theory HOLCF-ex.Focus_ex ...
Processing theory HOL-Matrix_LP.SparseMatrix ...
Processing theory HOL-Matrix_LP.Cplex ...
Processing theory HOL-Data_Structures.Array_Specs ...
Processing theory HOL-Hahn_Banach.Zorn_Lemma ...
Processing theory HOL-Combinatorics.Stirling ...
Processing theory HOL-Combinatorics.Orbits ...
Processing theory HOL-Data_Structures.Tree2 ...
Processing theory HOL-Data_Structures.Isin2 ...
Processing theory HOL-Combinatorics.Perm ...
Processing theory HOL-Data_Structures.Lookup2 ...
Processing theory HOL-Hahn_Banach.Bounds ...
Processing theory HOL-Data_Structures.Trie_Fun ...
Processing theory HOL-Combinatorics.Combinatorics ...
Processing theory HOL-Data_Structures.AVL_Set_Code ...
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-Data_Structures.Braun_Tree ...
Processing theory HOL-Data_Structures.RBT ...
Processing theory HOL-Hahn_Banach.Hahn_Banach ...
Processing theory HOL-Data_Structures.RBT_Set ...
Processing theory HOL-Data_Structures.Array_Braun ...
Removing 48 theories ...
Processing theory HOL-Data_Structures.RBT_Map ...
Processing theory HOL-Data_Structures.Trie_Map ...
Removing 3 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 33 theories ...
Processing theory HOL-IMP.Star ...
Processing theory HOL-Data_Structures.Time_Funs ...
Processing theory HOL-Nitpick_Examples.Datatype_Nits ...
Removing 3 theories ...
Processing theory HOL-Nitpick_Examples.Hotel_Nits ...
Processing theory HOL-Data_Structures.Set2_Join ...
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.Pattern_Nits ...
Processing theory HOL-Nitpick_Examples.Record_Nits ...
Processing theory HOL-Nitpick_Examples.Manual_Nits ...
Processing theory HOL-Nitpick_Examples.Tests_Nits ...
Processing theory Codegen.Setup ...
Processing theory HOL-Nitpick_Examples.Core_Nits ...
Processing theory HOL-Nitpick_Examples.Special_Nits ...
Processing theory HOL-Nitpick_Examples.Integer_Nits ...
Processing theory Codegen.Introduction ...
Processing theory Codegen.Foundations ...
Processing theory HOL-Data_Structures.Sorting ...
Removing 2 theories ...
Processing theory HOL-Types_To_Sets.Prerequisites ...
Processing theory HOL-Types_To_Sets.Types_To_Sets ...
Processing theory HOL-Data_Structures.RBT_Set2 ...
Processing theory HOL-Data_Structures.Selection ...
Processing theory HOL-Data_Structures.Set2_Join_RBT ...
Processing theory HOL-IMP.Types ...
Processing theory HOL-IMP.Poly_Types ...
Processing theory HOL-Nitpick_Examples.Typedef_Nits ...
Processing theory HOL-Types_To_Sets.Group_On_With ...
Processing theory HOL-Types_To_Sets.Linear_Algebra_On_With ...
Processing theory HOL-ex.Function_Growth ...
Processing theory HOL-Types_To_Sets.Linear_Algebra_On ...
Processing theory HOL-Nitpick_Examples.Refute_Nits ...
Loading 21 theories ...
Processing theory HOL-Nitpick_Examples.Nitpick_Examples ...
Removing 31 theories ...
Processing theory HOL-TPTP.TPTP_Parser ...
Processing theory HOL-Library.LaTeXsugar ...
Processing theory HOL-Library.Refute ...
Processing theory Typeclass_Hierarchy.Setup ...
Processing theory Codegen.Evaluation ...
Processing theory Codegen.Further ...
Processing theory HOL-Library.OptionalSugar ...
Processing theory Codegen.Adaptation ...
Processing theory Codegen.Inductive_Predicate ...
Processing theory Typeclass_Hierarchy.Typeclass_Hierarchy ...
Processing theory HOL-ex.SOS_Cert ...
Processing theory HOL-TPTP.TPTP_Interpret ...
Processing theory HOL-TPTP.ATP_Problem_Import ...
Processing theory Codegen.Refinement ...
Processing theory Sugar.Sugar ...
Processing theory Codegen.Computations ...
Processing theory HOL-ex.SOS ...
Processing theory HOL-ex.Sum_of_Powers ...
Processing theory HOL-ex.Triangular_Numbers ...
Processing theory HOL-Data_Structures.Balance ...
Loading 29 theories ...
Processing theory HOL-TPTP.TPTP_Proof_Reconstruction ...
Processing theory HOL-Examples.Sqrt ...
Processing theory HOL-Library.Code_Real_Approx_By_Float ...
Processing theory HOL-Data_Structures.Priority_Queue_Specs ...
Processing theory HOL-Mutabelle.MutabelleExtra ...
Processing theory HOL-Data_Structures.Leftist_Heap ...
Processing theory HOL-Metis_Examples.Clausification ...
Processing theory HOL-SMT_Examples.SMT_Examples ...
Removing 29 theories ...
Processing theory HOL-TPTP.ATP_Theory_Export ...
Processing theory HOL-TPTP.THF_Arith ...
Processing theory HOL-SMT_Examples.SMT_Examples_Verit ...
Processing theory HOL-SMT_Examples.SMT_Tests_Verit ...
Processing theory HOL-ex.BinEx ...
Processing theory HOL-ex.Argo_Examples ...
Processing theory HOL-ex.Ballot ...
Processing theory HOL-SMT_Examples.SMT_Tests ...
Processing theory HOL-ex.Code_Binary_Nat_examples ...
Processing theory HOL-ex.Gauge_Integration ...
Processing theory HOL-ex.Eval_Examples ...
Removing 12 theories ...
Processing theory HOL-ex.HarmonicSeries ...
Processing theory HOL-ex.Dedekind_Real ...
Processing theory HOL-ex.Pythagoras ...
Processing theory HOL-ex.Normalization_by_Evaluation ...
Removing 4 theories ...
Processing theory HOL-ex.Sqrt_Script ...
Processing theory HOL-Types_To_Sets.T2_Spaces ...
Processing theory HOL-Types_To_Sets.Unoverload_Def ...
Processing theory HOL-ex.Reflection_Examples ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Examples ...
Removing 8 theories ...
Processing theory HOL-ex.Parallel_Example ...
Removing 2 theories ...
Processing theory HOL-ex.Cubic_Quartic ...
Loading 7 theories ...
Processing theory Tutorial.Examples ...
Processing theory Tutorial.Numbers ...
Processing theory HOL-Computational_Algebra.Field_as_Ring ...
Processing theory How_to_Prove_it.How_to_Prove_it ...
Processing theory Prog_Prove.Bool_nat_list ...
Processing theory HOL-Data_Structures.Binomial_Heap ...
Removing 8 theories ...
Processing theory HOL-Corec_Examples.Paper_Examples ...
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.AxExample ...
Processing theory HOL-Bali.AxCompl ...
Processing theory HOL-Bali.AxSound ...
Loading 56 theories ...
Processing theory IOA-ABP.Lemmas ...
Processing theory IOA-ABP.Packet ...
Processing theory IOA-NTP.Lemmas ...
Processing theory IOA-NTP.Multiset ...
Processing theory IOA-NTP.Packet ...
Processing theory IOA.Asig ...
Processing theory IOA.Pred ...
Processing theory HOL-Isar_Examples.Fibonacci ...
Processing theory IOA.Automata ...
Processing theory IOA-Storage.Action ...
Processing theory IOA.Seq ...
Processing theory IOA.Sequence ...
Processing theory IOA.TL ...
Processing theory IOA.Traces ...
Processing theory IOA-ABP.Action ...
Processing theory IOA-NTP.Action ...
Removing 25 theories ...
Processing theory IOA.RefMappings ...
Processing theory HOL-ex.Code_Timing ...
Processing theory IOA.CompoExecs ...
Processing theory IOA.CompoScheds ...
Processing theory IOA.RefCorrectness ...
Processing theory IOA.Deadlock ...
Processing theory IOA.Simulations ...
Processing theory IOA.SimCorrectness ...
Processing theory IOA.ShortExecutions ...
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-ABP.Abschannel ...
Processing theory IOA-ABP.Abschannel_finite ...
Processing theory IOA-ABP.Impl ...
Processing theory IOA-ABP.Impl_finite ...
Processing theory HOL-Nominal.Nominal ...
Processing theory IOA-Storage.Impl ...
Processing theory IOA-NTP.Spec ...
Processing theory IOA-Storage.Spec ...
Processing theory IOA-NTP.Sender ...
Processing theory IOA-Storage.Correctness ...
Processing theory IOA-ABP.Correctness ...
Processing theory IOA.TLS ...
Processing theory IOA.LiveIOA ...
Processing theory IOA.Abstraction ...
Processing theory IOA-ex.TrivEx ...
Processing theory IOA-ex.TrivEx2 ...
Processing theory IOA-NTP.Abschannel ...
Processing theory IOA-NTP.Impl ...
Processing theory IOA-NTP.Correctness ...
Removing 55 theories ...
Processing theory HOL-Nominal-Examples.Class1 ...
Processing theory HOL-Nominal-Examples.Class2 ...
Processing theory HOL-Nominal-Examples.Class3 ...
Loading 83 theories ...
Processing theory HOL-Eisbach.Eisbach ...
Processing theory HOL-Eisbach.Eisbach_Tools ...
Processing theory HOLCF-Library.HOL_Cpo ...
Processing theory HOLCF-Tutorial.New_Domain ...
Processing theory HOLCF-ex.Dnat ...
Processing theory HOLCF-ex.Fix2 ...
Processing theory HOLCF-ex.Concurrency_Monad ...
Processing theory HOLCF-ex.Hoare ...
Processing theory HOLCF-ex.Letrec ...
Processing theory HOL-IMP.AExp ...
Processing theory HOLCF-ex.Loop ...
Processing theory HOLCF-Tutorial.Fixrec_ex ...
Processing theory HOLCF-ex.Domain_Proofs ...
Processing theory HOLCF-ex.Pattern_Match ...
Processing theory HOL-MicroJava.Semilat ...
Processing theory HOL-MicroJava.JBasis ...
Processing theory HOL-MicroJava.AuxLemmas ...
Processing theory HOL-IMP.BExp ...
Processing theory HOL-IMP.Com ...
Processing theory HOL-IMP.Big_Step ...
Processing theory HOLCF-IMP.Denotational ...
Processing theory HOLCF-IMP.HoareEx ...
Processing theory HOLCF-ex.Powerdomain_ex ...
Processing theory HOL-Quotient_Examples.Int_Pow ...
Processing theory HOL-Eisbach.Example_Metric ...
Processing theory HOL-MicroJava.Err ...
Processing theory HOL-MicroJava.Listn ...
Processing theory HOL-MicroJava.Typing_Framework ...
Processing theory HOL-MicroJava.Opt ...
Processing theory HOL-MicroJava.Product ...
Processing theory HOL-MicroJava.SemilatAlg ...
Processing theory HOL-MicroJava.Typing_Framework_err ...
Processing theory HOL-MicroJava.Semilattices ...
Processing theory HOL-MicroJava.Type ...
Processing theory HOL-MicroJava.Decl ...
Processing theory HOL-MicroJava.SystemClasses ...
Processing theory HOL-MicroJava.TypeRel ...
Processing theory HOL-MicroJava.WellForm ...
Processing theory HOL-MicroJava.JType ...
Processing theory HOL-MicroJava.Value ...
Processing theory HOL-MicroJava.State ...
Processing theory HOL-MicroJava.Exceptions ...
Processing theory HOLCF-Tutorial.Domain_ex ...
Processing theory HOL-MicroJava.Term ...
Processing theory HOL-MicroJava.WellType ...
Removing 74 theories ...
Processing theory HOL-MicroJava.TypeInf ...
Processing theory HOL-MicroJava.Kildall ...
Processing theory HOL-MicroJava.LBVSpec ...
Processing theory HOL-MicroJava.LBVComplete ...
Processing theory HOL-MicroJava.LBVCorrect ...
Processing theory HOL-MicroJava.Abstract_BV ...
Processing theory HOL-MicroJava.JVMType ...
Processing theory HOL-MicroJava.Conform ...
Processing theory HOL-MicroJava.JVMState ...
Processing theory HOL-MicroJava.Eval ...
Processing theory HOL-MicroJava.JListExample ...
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.LemmasComp ...
Processing theory HOL-MicroJava.JVMListExample ...
Processing theory HOL-MicroJava.JTypeSafe ...
Processing theory HOL-MicroJava.JVMDefensive ...
Processing theory HOL-MicroJava.Effect ...
Processing theory HOL-MicroJava.BVSpec ...
Processing theory HOL-MicroJava.Altern ...
Processing theory HOL-MicroJava.EffectMono ...
Processing theory HOL-MicroJava.Typing_Framework_JVM ...
Processing theory HOL-MicroJava.JVM ...
Processing theory HOL-MicroJava.Correct ...
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 93 theories ...
Processing theory HOL-MicroJava.MicroJava ...
Processing theory HOL-Cardinals.Wellorder_Extension ...
Processing theory HOL-Imperative_HOL.Sorted_List ...
Processing theory HOL-ZF.LProd ...
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-Auth.Message ...
Processing theory HOL-Auth.Event ...
Processing theory HOL-Auth.Public ...
Removing 60 theories ...
Processing theory HOL-Imperative_HOL.List_Sublist ...
Processing theory HOL-Imperative_HOL.Subarray ...
Processing theory HOL-Cardinals.Ordinal_Arithmetic ...
Processing theory HOL-Cardinals.Cardinals ...
Processing theory HOL-Nominal-Examples.Lam_Funs ...
Processing theory HOL-Nominal-Examples.CR ...
Processing theory HOL-Nominal-Examples.SN ...
Processing theory HOL-SMT_Examples.SMT_Word_Examples ...
Processing theory HOL-Cardinals.Bounded_Set ...
Processing theory HOL-SPARK-Examples.RMD ...
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-Imperative_HOL.Imperative_Quicksort ...
Processing theory HOL-Imperative_HOL.Imperative_Reverse ...
Processing theory HOL-SPARK-Examples.F ...
Processing theory HOL-SPARK-Examples.Longest_Increasing_Subsequence ...
Processing theory HOL-SPARK-Examples.K_L ...
Processing theory HOL-SPARK-Examples.K_R ...
Processing theory HOL-SPARK-Examples.Sqrt ...
Processing theory HOL-SPARK-Manual.Proc1 ...
Processing theory HOL-SPARK-Manual.Proc2 ...
Processing theory HOL-SPARK-Manual.VC_Principles ...
Processing theory HOL-SPARK-Manual.Reference ...
Processing theory HOL-SPARK-Manual.Simple_Greatest_Common_Divisor ...
Processing theory HOL-SPARK-Manual.Example_Verification ...
Processing theory HOL-SPARK-Examples.RMD_Lemmas ...
Processing theory HOL-SPARK-Examples.Hash ...
Processing theory HOL-Data_Structures.Heaps ...
Processing theory HOL-SPARK-Examples.R_L ...
Processing theory HOL-Imperative_HOL.Linked_Lists ...
Processing theory HOL-SPARK-Examples.R_R ...
Processing theory HOL-SPARK-Examples.S_L ...
Processing theory HOL-SPARK-Examples.S_R ...
Processing theory HOL-UNITY.ListOrder ...
Processing theory HOL-UNITY.UNITY ...
Processing theory HOL-UNITY.FP ...
Processing theory HOL-UNITY.Constrains ...
Processing theory HOL-UNITY.WFair ...
Processing theory HOL-UNITY.SubstAx ...
Processing theory HOL-UNITY.Detects ...
Processing theory HOL-ZF.HOLZF ...
Processing theory HOL-ZF.Zet ...
Processing theory HOL-ZF.MainZF ...
Processing theory HOL-ZF.Games ...
Processing theory HOL-SPARK-Examples.Round ...
Processing theory HOL-SPARK-Manual.Complex_Types ...
Removing 50 theories ...
Processing theory HOL-UNITY.Follows ...
Processing theory HOL-UNITY.Union ...
Processing theory HOL-UNITY.Comp ...
Processing theory HOL-UNITY.Guar ...
Processing theory HOL-UNITY.Extend ...
Processing theory HOL-UNITY.Rename ...
Processing theory HOL-Imperative_HOL.SatChecker ...
Processing theory HOL-Imperative_HOL.Imperative_HOL_ex ...
Processing theory HOL-UNITY.Lift_prog ...
Processing theory HOL-UNITY.PPROD ...
Processing theory HOL-UNITY.Transformers ...
Processing theory HOL-UNITY.ProgressSets ...
Processing theory HOL-UNITY.UNITY_Main ...
Processing theory HOL-UNITY.AllocBase ...
Processing theory HOL-UNITY.Counterc ...
Processing theory HOL-UNITY.PriorityAux ...
Processing theory HOL-UNITY.Counter ...
Processing theory HOL-UNITY.Handshake ...
Processing theory HOL-UNITY.Alloc ...
Processing theory HOL-UNITY.AllocImpl ...
Processing theory HOL-ex.Termination ...
Processing theory HOL-UNITY.TimerArray ...
Processing theory HOL-UNITY.Channel ...
Processing theory HOL-UNITY.Common ...
Processing theory HOL-UNITY.Priority ...
Processing theory HOL-UNITY.Progress ...
Processing theory HOL-UNITY.NSP_Bad ...
Processing theory HOL-UNITY.Reach ...
Processing theory HOL-ex.Sorting_Algorithms_Examples ...
Processing theory HOL-UNITY.Client ...
Processing theory HOL-UNITY.Mutex ...
Processing theory HOL-UNITY.Lift ...
Processing theory HOL-UNITY.Reachability ...
Loading 42 theories ...
Removing 46 theories ...
Processing theory Isar_Ref.Base ...
Processing theory Datatypes.Setup ...
Processing theory HOL-Library.List_Lexorder ...
Processing theory HOL-Datatype_Examples.Prelim ...
Processing theory HOL-ex.Bubblesort ...
Processing theory HOL-ex.Quicksort ...
Processing theory HOL-Datatype_Examples.DTree ...
Processing theory HOL-Datatype_Examples.Parallel_Composition ...
Processing theory HOL-ex.MergeSort ...
Processing theory HOL-Datatype_Examples.Lambda_Term ...
Processing theory HOL-Datatype_Examples.Gram_Lang ...
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.CR_Takahashi ...
Processing theory HOL-Nominal-Examples.CK_Machine ...
Processing theory HOL-Nominal-Examples.Contexts ...
Processing theory HOL-Nominal-Examples.Height ...
Processing theory HOL-Nominal-Examples.Crary ...
Processing theory HOL-Nominal-Examples.Lambda_mu ...
Processing theory HOL-Nominal-Examples.Compile ...
Removing 9 theories ...
Processing theory HOL-Datatype_Examples.Misc_Datatype ...
Processing theory HOL-Datatype_Examples.Misc_Primrec ...
Processing theory HOL-Datatype_Examples.Misc_Codatatype ...
Processing theory HOL-Datatype_Examples.Misc_Primcorec ...
Processing theory HOL-Nominal-Examples.LocalWeakening ...
Processing theory HOL-Nominal-Examples.Fsub ...
Processing theory HOL-Nominal-Examples.Support ...
Processing theory HOL-Nominal-Examples.Standardization ...
Processing theory HOL-Nominal-Examples.VC_Condition ...
Processing theory HOL-Nominal-Examples.SOS ...
Processing theory HOL-Nominal-Examples.Weakening ...
Processing theory HOL-Nominal-Examples.Type_Preservation ...
Processing theory HOL-Quotient_Examples.Quotient_FSet ...
Processing theory HOL-ex.Radix_Sort ...
Processing theory HOL-ex.Transfer_Debug ...
Processing theory HOL-UNITY.Project ...
Processing theory HOL-UNITY.ELT ...
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 ...
Loading 104 theories ...
Removing 38 theories ...
Processing theory HOL-Auth.All_Symmetric ...
Processing theory HOL-Auth.Extensions ...
Processing theory HOL-Auth.Analz ...
Processing theory HOL-Auth.CertifiedEmail ...
Processing theory HOL-Auth.List_Msg ...
Processing theory HOL-Auth.Guard ...
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.NS_Public ...
Processing theory HOL-Auth.Guard_Shared ...
Processing theory HOL-Auth.Kerberos_BAN ...
Processing theory HOL-Auth.Proto ...
Processing theory HOL-Auth.KerberosV ...
Processing theory HOL-Auth.P2 ...
Processing theory HOL-Auth.P1 ...
Processing theory HOL-Auth.Auth_Guard_Public ...
Processing theory HOL-Auth.NS_Public_Bad ...
Processing theory HOL-Auth.Kerberos_BAN_Gets ...
Processing theory HOL-Auth.NS_Shared ...
Processing theory HOL-Auth.OtwayRees ...
Processing theory HOL-Auth.OtwayRees_AN ...
Processing theory HOL-Auth.OtwayRees_Bad ...
Processing theory HOL-Auth.Recur ...
Processing theory HOL-Auth.WooLam ...
Processing theory HOL-Auth.OtwayReesBella ...
Processing theory HOL-Auth.Yahalom2 ...
Processing theory HOL-Auth.Yahalom_Bad ...
Processing theory HOL-Auth.Guard_OtwayRees ...
Processing theory HOL-Auth.Yahalom ...
Processing theory HOL-Auth.ZhouGollmann ...
Processing theory HOL-Auth.Auth_Shared ...
Processing theory HOL-Auth.Guard_Yahalom ...
Processing theory HOL-Auth.Auth_Guard_Shared ...
Processing theory HOL-Hoare_Parallel.Quote_Antiquote ...
Processing theory HOL-IMP.Abs_Int_Tests ...
Processing theory HOL-IMP.Complete_Lattice ...
Processing theory HOL-Hoare_Parallel.Graph ...
Processing theory HOL-IMP.Vars ...
Processing theory HOL-Hoare_Parallel.RG_Com ...
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-Auth.EventSC ...
Processing theory HOL-Auth.Smartcard ...
Processing theory HOL-IMP.ACom ...
Processing theory HOL-IMP.Collecting ...
Removing 33 theories ...
Processing theory HOL-Hoare_Parallel.Gar_Coll ...
Processing theory HOL-Auth.ShoupRubin ...
Processing theory HOL-Auth.ShoupRubinBella ...
Processing theory HOL-Auth.Auth_Smartcard ...
Processing theory HOL-Library.Prefix_Order ...
Processing theory HOL-IMP.Abs_Int_init ...
Processing theory HOL-Auth.TLS ...
Processing theory HOL-Auth.Auth_Public ...
Removing 15 theories ...
Processing theory HOL-Hoare_Parallel.RG_Tran ...
Processing theory HOL-IMP.Abs_Int0 ...
Processing theory HOL-IMP.Abs_State ...
Processing theory HOL-SET_Protocol.Message_SET ...
Processing theory HOL-IMP.Abs_Int1 ...
Processing theory HOL-IMP.Abs_Int1_parity ...
Processing theory HOL-Hoare_Parallel.Mul_Gar_Coll ...
Processing theory HOL-IMP.Abs_Int2 ...
Processing theory HOL-Hoare_Parallel.OG_Examples ...
Processing theory HOL-SET_Protocol.Event_SET ...
Processing theory HOL-SET_Protocol.Public_SET ...
Processing theory HOL-SET_Protocol.Merchant_Registration ...
Processing theory HOL-IMP.Abs_Int1_const ...
Processing theory HOL-TLA.Intensional ...
Processing theory HOL-Hoare_Parallel.RG_Hoare ...
Processing theory HOL-Hoare_Parallel.RG_Syntax ...
Removing 2 theories ...
Processing theory HOL-TLA.Stfun ...
Processing theory HOL-TLA.Action ...
Processing theory HOL-TLA.Init ...
Processing theory HOL-SET_Protocol.Cardholder_Registration ...
Processing theory HOL-TLA.TLA ...
Processing theory HOL-TLA-Buffer.Buffer ...
Processing theory HOL-TLA-Buffer.DBuffer ...
Processing theory HOL-TLA-Memory.RPCMemoryParams ...
Processing theory HOL-TLA-Inc.Inc ...
Processing theory HOL-TLA-Memory.MemoryParameters ...
Processing theory HOL-TLA-Memory.ProcedureInterface ...
Processing theory HOL-Hoare_Parallel.RG_Examples ...
Processing theory HOL-Hoare_Parallel.Hoare_Parallel ...
Processing theory HOL-TLA-Memory.RPCParameters ...
Processing theory HOL-TLA-Memory.Memory ...
Processing theory HOL-TLA-Memory.RPC ...
Processing theory HOL-IMP.Abs_Int2_ivl ...
Processing theory HOL-TLA-Memory.MemClerkParameters ...
Processing theory HOL-TLA-Memory.MemClerk ...
Processing theory HOL-Unix.Nested_Environment ...
Processing theory HOL-ex.Execute_Choice ...
Processing theory Haskell.Haskell ...
Processing theory HOL-SET_Protocol.Purchase ...
Processing theory HOL-SET_Protocol.SET_Protocol ...
Processing theory HOL-Unix.Unix ...
Removing 33 theories ...
Processing theory Haskell.Test ...
Processing theory HOL-TLA-Memory.MemoryImplementation ...
Processing theory HOL-IMP.Abs_Int3 ...
Loading 188 theories ...
Processing theory Classes.Setup ...
Processing theory Eisbach.Base ...
Processing theory Eisbach.Preface ...
Processing theory Prog_Prove.LaTeXsugar ...
Processing theory Tutorial.Base ...
Processing theory Locales.Examples ...
Processing theory Locales.Examples1 ...
Processing theory Locales.Examples2 ...
Processing theory Prog_Prove.Isar ...
Processing theory Locales.Examples3 ...
Processing theory Prog_Prove.Logic ...
Processing theory Tutorial.CTL ...
Processing theory Tutorial.CTLind ...
Processing theory Tutorial.PDL ...
Processing theory Tutorial.TPrimes ...
Processing theory Tutorial.Forward ...
Processing theory Tutorial.Setup ...
Processing theory Tutorial.Even ...
Processing theory Tutorial.Overloading ...
Processing theory Tutorial.Axioms ...
Processing theory HOL-ex.Specifications_with_bundle_mixins ...
Processing theory Classes.Classes ...
Processing theory Tutorial.Advanced ...
Processing theory Tutorial.Message ...
Processing theory Tutorial.Event ...
Processing theory Tutorial.Public ...
Processing theory HOL-Data_Structures.Tree23 ...
Processing theory Tutorial.ABexpr ...
Processing theory Tutorial.Nested ...
Processing theory Tutorial.NS_Public ...
Processing theory HOL-Hoare.Arith2 ...
Processing theory HOL-Datatype_Examples.TreeFI ...
Processing theory HOL-Hoare.Heap ...
Processing theory HOL-Hoare.Hoare_Syntax ...
Processing theory HOL-Hoare.Hoare_Tac ...
Processing theory HOL-Data_Structures.Tries_Binary ...
Processing theory HOL-Data_Structures.Tree23_of_List ...
Processing theory HOL-Hoare.SepLogHeap ...
Processing theory HOL-Hoare.Hoare_Logic ...
Processing theory HOL-Data_Structures.Tree234 ...
Processing theory HOL-IMP.ASM ...
Processing theory HOL-Hoare.Hoare_Logic_Abort ...
Removing 56 theories ...
Processing theory HOL-Hoare.ExamplesTC ...
Processing theory HOL-Hoare.HeapSyntax ...
Processing theory HOL-Hoare.Examples ...
Processing theory HOL-Hoare.Pointers0 ...
Processing theory HOL-Hoare.ExamplesAbort ...
Processing theory HOL-Hoare.HeapSyntaxAbort ...
Processing theory HOL-Hoare.Pointer_ExamplesAbort ...
Processing theory HOL-Hoare.SchorrWaite ...
Processing theory HOL-Isar_Examples.Hoare ...
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-Isar_Examples.Hoare_Ex ...
Processing theory HOL-IMP.Hoare_Sound_Complete ...
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.Sec_Type_Expr ...
Processing theory HOL-IMP.VCG_Total_EX ...
Processing theory HOL-IMP.VCG ...
Removing 26 theories ...
Processing theory HOL-IMP.Def_Init ...
Processing theory HOL-IMP.Sem_Equiv ...
Processing theory HOL-IMP.Sec_Typing ...
Processing theory HOL-IMP.Sec_TypingT ...
Processing theory HOL-IMP.Def_Init_Exp ...
Processing theory HOL-IMP.Def_Init_Big ...
Processing theory HOL-IMP.Fold ...
Processing theory HOL-IMP.VCG_Total_EX2 ...
Processing theory HOL-IMP.Collecting1 ...
Processing theory HOL-IMP.Collecting_Examples ...
Processing theory HOL-IMP.Live ...
Processing theory HOL-Data_Structures.Tree23_Map ...
Processing theory HOL-IMP.Procs ...
Processing theory HOL-IMP.Procs_Dyn_Vars_Dyn ...
Processing theory HOL-IMP.Procs_Stat_Vars_Dyn ...
Processing theory HOL-IMP.Procs_Stat_Vars_Stat ...
Removing 22 theories ...
Processing theory HOL-IMP.Def_Init_Small ...
Processing theory HOL-IMP.Small_Step ...
Processing theory HOL-IMP.Finite_Reachable ...
Processing theory HOL-IOA.Asig ...
Processing theory HOL-IOA.IOA ...
Processing theory HOL-IOA.Solve ...
Processing theory HOL-Lattice.Orders ...
Processing theory HOL-Lattice.Bounds ...
Processing theory HOL-Lattice.Lattice ...
Processing theory HOL-Lattice.CompleteLattice ...
Processing theory HOL-IMP.Compiler ...
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-IMP.Compiler2 ...
Processing theory HOL-Corec_Examples.LFilter ...
Processing theory HOL-Corec_Examples.Merge_A ...
Processing theory HOL-Corec_Examples.Merge_B ...
Processing theory HOL-Corec_Examples.Merge_C ...
Processing theory HOL-Corec_Examples.Iterate_GPV ...
Processing theory HOL-Corec_Examples.GPV_Bare_Bones ...
Removing 23 theories ...
Processing theory HOL-Corec_Examples.Merge_D ...
Removing 4 theories ...
Processing theory HOL-Corec_Examples.Merge_Poly ...
Removing 1 theories ...
Processing theory HOL-Corec_Examples.Simple_Nesting ...
Processing theory HOL-Data_Structures.Tree234_Set ...
Removing 1 theories ...
Processing theory HOL-ex.Conditional_Parametricity_Examples ...
Processing theory HOL-Corec_Examples.Stream_Friends ...
Processing theory HOL-Corec_Examples.Misc_Mono ...
Processing theory HOL-Corec_Examples.Small_Concrete ...
Processing theory HOL-Datatype_Examples.Cyclic_List ...
Processing theory HOL-Datatype_Examples.FAE_Sequence ...
Removing 7 theories ...
Processing theory HOL-ex.Perm_Fragments ...
Processing theory HOL-Library.Datatype_Records ...
Processing theory HOL-Metis_Examples.Abstraction ...
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.IArray_Examples ...
Processing theory HOL-Examples.Adhoc_Overloading_Examples ...
Processing theory HOL-ex.Datatype_Record_Examples ...
Processing theory HOL-Datatype_Examples.Regex_ACIDZ ...
Removing 21 theories ...
Processing theory HOL-Induct.Sexp ...
Processing theory HOL-Corec_Examples.Stream_Processor ...
Processing theory HOL-Datatype_Examples.Koenig ...
Processing theory HOL-Corec_Examples.Type_Class ...
Processing theory HOL-Data_Structures.Tree234_Map ...
Processing theory HOL-Codegenerator_Test.Code_Lazy_Test ...
Processing theory HOL-Corec_Examples.Misc_Poly ...
Removing 9 theories ...
Processing theory HOL-Codegenerator_Test.Code_Test_PolyML ...
Processing theory HOL-Codegenerator_Test.Code_Test_GHC ...
Processing theory HOL-Codegenerator_Test.Code_Test_OCaml ...
Processing theory HOL-Codegenerator_Test.Code_Test_Scala ...
Processing theory HOL-Induct.SList ...
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-Predicate_Compile_Examples.IMP_1 ...
Processing theory HOL-Quotient_Examples.Quotient_Rat ...
Processing theory HOL-Predicate_Compile_Examples.IMP_2 ...
Processing theory HOL-Quotient_Examples.DList ...
Processing theory HOL-Predicate_Compile_Examples.IMP_3 ...
Processing theory HOL-Datatype_Examples.Process ...
Processing theory HOL-Datatype_Examples.Stream_Processor ...
Processing theory HOL-Predicate_Compile_Examples.IMP_4 ...
Processing theory HOL-ex.Transitive_Closure_Table_Ex ...
Processing theory HOL-Metis_Examples.Big_O ...
Removing 33 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.AVL_Bal2_Set ...
Processing theory HOL-ex.Refute_Examples ...
Processing theory HOL-ex.While_Combinator_Example ...
Processing theory HOL-Metis_Examples.Type_Encodings ...
Processing theory HOL-IMP.Live_True ...
Processing theory HOL-Metis_Examples.Tarski ...
Processing theory HOL-Data_Structures.AA_Set ...
Removing 15 theories ...
Processing theory HOL-Data_Structures.AA_Map ...
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.Specialisation_Examples ...
Processing theory HOL-Metis_Examples.Proxies ...
Processing theory HOL-Types_To_Sets.Finite ...
Processing theory HOL-Statespace.DistinctTreeProver ...
Processing theory HOL-Statespace.StateFun ...
Processing theory HOL-Statespace.StateSpaceLocale ...
Processing theory HOL-Statespace.StateSpaceSyntax ...
Processing theory HOL-UNITY.Deadlock ...
Processing theory HOL-Quickcheck_Examples.Hotel_Example ...
Processing theory HOL-UNITY.Network ...
Processing theory HOL-UNITY.Token ...
Processing theory HOL-ex.Birthday_Paradox ...
Processing theory HOL-ex.Residue_Ring ...
Processing theory HOL-Predicate_Compile_Examples.Examples ...
Removing 35 theories ...
Processing theory HOL-ex.ThreeDivides ...
Processing theory HOL-ex.Tarski ...
Processing theory HOL-Statespace.StateSpaceEx ...
Processing theory HOL-Data_Structures.Height_Balanced_Tree ...
Processing theory HOL-ex.Functions ...
Loading 174 theories ...
Processing theory Eisbach.Manual ...
Processing theory Implementation.Base ...
Processing theory Implementation.Eq ...
Processing theory Implementation.Integration ...
Processing theory Implementation.Local_Theory ...
Processing theory Implementation.Isar ...
Processing theory Implementation.Proof ...
Processing theory Implementation.Syntax ...
Processing theory Isar_Ref.Inner_Syntax ...
Processing theory Isar_Ref.Outer_Syntax ...
Processing theory Isar_Ref.Preface ...
Processing theory Isar_Ref.Proof ...
Processing theory Isar_Ref.Proof_Script ...
Processing theory Isar_Ref.Quick_Reference ...
Processing theory Isar_Ref.Symbols ...
Processing theory Implementation.Prelim ...
Processing theory JEdit.Base ...
Processing theory Isar_Ref.Spec ...
Processing theory Isar_Ref.Synopsis ...
Processing theory Prog_Prove.Basics ...
Processing theory Implementation.Logic ...
Processing theory Implementation.Tactic ...
Processing theory JEdit.JEdit ...
Processing theory Prog_Prove.MyList ...
Processing theory Tutorial.simp2 ...
Processing theory Tutorial.Fundata ...
Processing theory Tutorial.CodeGen ...
Processing theory Implementation.ML ...
Processing theory Tutorial.fun0 ...
Processing theory Main.Main_Doc ...
Processing theory Tutorial.Documents ...
Processing theory Tutorial.Mutual ...
Processing theory Tutorial.Star ...
Processing theory Tutorial.AdvancedInd ...
Processing theory Tutorial.Itrev ...
Processing theory Tutorial.Plus ...
Processing theory Prog_Prove.Types_and_funs ...
Processing theory Tutorial.appendix ...
Processing theory Tutorial.case_exprs ...
Processing theory Tutorial.Ifexpr ...
Processing theory Tutorial.unfoldnested ...
Processing theory Tutorial.Option2 ...
Processing theory Tutorial.Tree ...
Processing theory Tutorial.Tree2 ...
Processing theory Tutorial.natsum ...
Processing theory Tutorial.pairs2 ...
Processing theory Tutorial.prime_def ...
Processing theory Tutorial.types ...
Processing theory Tutorial.Blast ...
Processing theory Tutorial.Force ...
Processing theory Tutorial.simp ...
Processing theory Tutorial.Tacticals ...
Processing theory Tutorial.find2 ...
Processing theory Tutorial.Functions ...
Processing theory Tutorial.Recur ...
Processing theory Tutorial.fakenat ...
Processing theory Tutorial.Basic ...
Processing theory Tutorial.Relations ...
Processing theory Tutorial.ToyList_Test ...
Processing theory Tutorial.Pairs ...
Processing theory HOL-Data_Structures.Queue_Spec ...
Processing theory HOL-Data_Structures.Reverse ...
Processing theory Tutorial.AB ...
Processing theory Tutorial.ToyList ...
Processing theory Tutorial.Records ...
Processing theory Tutorial.Typedefs ...
Processing theory Tutorial.Trie ...
Removing 87 theories ...
Processing theory HOL-Eisbach.Examples ...
Processing theory HOL-Data_Structures.Queue_2Lists ...
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-Datatype_Examples.TLList ...
Processing theory HOL-Datatype_Examples.Datatype_Simproc_Tests ...
Processing theory HOL-Datatype_Examples.Milner_Tofte ...
Processing theory HOL-Examples.Coherent ...
Processing theory HOL-Examples.Iff_Oracle ...
Processing theory HOL-Examples.Induction_Schema ...
Processing theory HOL-Examples.Peirce ...
Processing theory HOL-Import.Import_Setup ...
Processing theory HOL-Import.HOL_Light_Maps ...
Processing theory HOL-Examples.ML ...
Processing theory HOL-Examples.Seq ...
Processing theory HOL-IMP.C_like ...
Processing theory HOL-Induct.Com ...
Processing theory HOL-Induct.Comb ...
Processing theory HOL-Induct.Common_Patterns ...
Processing theory HOL-Induct.Infinitely_Branching_Tree ...
Processing theory HOL-Induct.Ordinals ...
Processing theory HOL-Induct.ABexp ...
Processing theory HOL-Induct.Nested_Datatype ...
Processing theory HOL-Induct.Sigma_Algebra ...
Processing theory HOL-Induct.QuoDataType ...
Processing theory HOL-IMP.OO ...
Processing theory HOL-Induct.PropLog ...
Processing theory HOL-Isar_Examples.Basic_Logic ...
Processing theory HOL-Isar_Examples.Group ...
Processing theory HOL-Isar_Examples.Group_Context ...
Processing theory HOL-Isar_Examples.Group_Notepad ...
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.Code_Prolog ...
Processing theory HOL-Examples.Knaster_Tarski ...
Processing theory HOL-ex.Simps_Case_Conv_Examples ...
Processing theory HOL-Library.List_Lenlexorder ...
Processing theory HOL-Metis_Examples.Sets ...
Processing theory HOL-Induct.QuoNestedDataType ...
Processing theory HOL-Induct.Term ...
Processing theory HOL-Quickcheck_Examples.Completeness ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Interfaces ...
Processing theory HOL-Isar_Examples.Expr_Compiler ...
Processing theory HOL-Metis_Examples.Trans_Closure ...
Processing theory HOL-Metis_Examples.Binary_Tree ...
Processing theory HOL-Datatype_Examples.Lift_BNF ...
Processing theory HOL-Datatype_Examples.Compat ...
Removing 60 theories ...
Processing theory HOL-Quotient_Examples.Lift_DList ...
Processing theory HOL-Quotient_Examples.Lift_FSet ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Nesting ...
Processing theory HOL-Quotient_Examples.Lift_Set ...
Processing theory HOL-Quotient_Examples.Lift_Fun ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Nesting_Example ...
Processing theory HOL-Quotient_Examples.Quotient_Message ...
Processing theory HOL-Metis_Examples.Message ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples ...
Processing theory HOL-TPTP.MaSh_Export_Base ...
Processing theory HOL-TPTP.MaSh_Eval ...
Processing theory HOL-ex.Antiquote ...
Processing theory HOL-ex.Arith_Examples ...
Processing theory HOL-ex.Case_Product ...
Processing theory HOL-ex.CTL ...
Processing theory HOL-ex.Cartouche_Examples ...
Processing theory HOL-ex.Chinese ...
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.Guess ...
Processing theory HOL-ex.Executable_Relation ...
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.MonoidGroup ...
Processing theory HOL-ex.Multiquote ...
Processing theory HOL-ex.NatSum ...
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 ...
Removing 37 theories ...
Processing theory HOL-SMT_Examples.Boogie ...
Processing theory HOL-ex.Rewrite_Examples ...
Processing theory HOL-ex.Primrec ...
Processing theory HOL-ex.SAT_Examples ...
Removing 5 theories ...
Processing theory HOL-ex.Serbian ...
Processing theory HOL-ex.Set_Comprehension_Pointfree_Examples ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Narrowing_Examples ...
Processing theory HOL-ex.Simproc_Tests ...
Processing theory HOL-ex.Sketch_and_Explore ...
Processing theory HOL-ex.Transfer_Int_Nat ...
Processing theory HOL-ex.Set_Theory ...
Processing theory HOL-ex.veriT_Preprocessing ...
Processing theory HOL-ex.Sudoku ...
Processing theory HOL-ex.Unification ...
Removing 10 theories ...
Processing theory HOL-ex.Tree23 ...
Processing theory HOL-ex.PresburgerEx ...
Processing theory HOL-ex.Meson_Test ...
Loading 122 theories ...
Removing 3 theories ...
Processing theory IFOL ...
Processing theory FOL ...
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.QPair ...
Processing theory Isar_Ref.Document_Preparation ...
Processing theory Isar_Ref.Framework ...
Processing theory Isar_Ref.Generic ...
Processing theory Functions.Functions ...
Processing theory ZF.Trancl ...
Processing theory ZF.EquivClass ...
Processing theory ZF.WF ...
Processing theory ZF.Order ...
Processing theory ZF.Ordinal ...
Processing theory ZF.OrdQuant ...
Processing theory ZF.Nat ...
Processing theory ZF.Epsilon ...
Processing theory ZF.Inductive ...
Processing theory ZF.Finite ...
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.QUniv ...
Processing theory ZF.Datatype ...
Processing theory ZF.Int ...
Processing theory ZF.CardinalArith ...
Processing theory ZF.Bin ...
Processing theory ZF.List ...
Processing theory ZF.IntDiv ...
Processing theory ZF ...
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-Coind.ECR ...
Processing theory ZF-Constructible.MetaExists ...
Processing theory ZF-Constructible.Normal ...
Processing theory ZF-Induct.Acc ...
Processing theory ZF-Constructible.Formula ...
Processing theory ZF-Constructible.Reflection ...
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.FoldSet ...
Processing theory ZF-Induct.Multiset ...
Processing theory ZF-Resid.Redex ...
Processing theory ZF-Resid.Substitution ...
Processing theory ZF-Resid.Residuals ...
Processing theory ZF-Resid.Reduction ...
Processing theory ZF-Resid.Confluence ...
Processing theory ZF-UNITY.GenPrefix ...
Processing theory ZF-UNITY.State ...
Processing theory ZF-UNITY.UNITY ...
Processing theory ZF-UNITY.Constrains ...
Processing theory ZF-UNITY.FP ...
Processing theory ZFC ...
Processing theory Logics_ZF.ZF_examples ...
Processing theory ZF-Induct.Brouwer ...
Processing theory ZF-Constructible.Separation ...
Processing theory ZF-Constructible.AC_in_L ...
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-Constructible.Rank ...
Processing theory ZF-UNITY.Union ...
Processing theory ZF-UNITY.Comp ...
Processing theory ZF-UNITY.Guar ...
Processing theory ZF-UNITY.AllocBase ...
Processing theory ZF-UNITY.Distributor ...
Processing theory ZF-UNITY.Merge ...
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 ...
Removing 156 theories ...
Processing theory ZF-UNITY.ClientImpl ...
Processing theory ZF-UNITY.AllocImpl ...
Loading 110 theories ...
Processing theory System.Base ...
Processing theory Cube.Cube ...
Processing theory Cube.Example ...
Processing theory System.Presentation ...
Processing theory Isar_Ref.First_Order_Logic ...
Processing theory System.Phabricator ...
Processing theory Logics_ZF.IFOL_examples ...
Processing theory CTT.CTT ...
Processing theory CTT.Elimination ...
Processing theory CTT.Equality ...
Processing theory CTT.Synthesis ...
Processing theory CTT.Typechecking ...
Processing theory System.Server ...
Processing theory CCL.Set ...
Processing theory CCL.Lfp ...
Processing theory CCL.Gfp ...
Processing theory CCL.CCL ...
Processing theory CCL.Term ...
Processing theory CCL.Type ...
Processing theory CCL.Fix ...
Processing theory CCL.Hered ...
Processing theory CCL.Trancl ...
Processing theory System.Environment ...
Processing theory CCL.Wfd ...
Processing theory CCL.Nat ...
Processing theory CCL.List ...
Processing theory CCL.Flag ...
Processing theory CCL.Stream ...
Processing theory Logics_ZF.FOL_examples ...
Processing theory FOL-ex.Classical ...
Processing theory FOL-ex.If ...
Processing theory Logics_ZF.If ...
Processing theory FOL-ex.Intro ...
Processing theory FOL-ex.Miniscope ...
Processing theory FOL-ex.Nat ...
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 Logics_ZF.ZF_Isar ...
Processing theory LCF.LCF ...
Processing theory LCF.Ex1 ...
Processing theory LCF.Ex2 ...
Processing theory LCF.Ex3 ...
Processing theory LCF.Ex4 ...
Processing theory ZF-Induct.Binary_Trees ...
Processing theory ZF-Induct.ListN ...
Processing theory ZF-Induct.Comb ...
Processing theory ZF-Induct.Mutil ...
Processing theory ZF-Induct.Ntree ...
Processing theory ZF-Induct.Primrec ...
Processing theory ZF-Induct.Rmap ...
Processing theory ZF-Induct.Term ...
Processing theory ZF-Induct.Tree_Forest ...
Processing theory ZF-ex.BinEx ...
Processing theory ZF-ex.CoUnit ...
Processing theory ZF-ex.Commutation ...
Processing theory ZF-ex.LList ...
Processing theory ZF-ex.NatSum ...
Processing theory ZF-Induct.PropLog ...
Processing theory FOL-ex.Foundation ...
Processing theory ZF-Induct.Datatypes ...
Processing theory System.Misc ...
Processing theory System.Sessions ...
Processing theory System.Scala ...
Processing theory ZF-ex.Primes ...
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 FOLP-ex.If ...
Processing theory FOLP-ex.Intro ...
Processing theory FOLP-ex.Propositional_Cla ...
Processing theory FOLP-ex.Quantifiers_Cla ...
Processing theory FOLP-ex.Foundation ...
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 Pure-Examples.First_Order_Logic ...
Processing theory Pure-Examples.Higher_Order_Logic ...
Processing theory Sequents.Sequents ...
Processing theory Sequents.ILL ...
Processing theory Sequents.LK0 ...
Processing theory Sequents.LK ...
Processing theory ZF-ex.Limit ...
Processing theory FOLP-ex.Nat ...
Processing theory FOL-ex.Locale_Test1 ...
Processing theory FOL-ex.Locale_Test2 ...
Processing theory FOL-ex.Locale_Test3 ...
Processing theory FOL-ex.Locale_Test ...
Removing 150 theories ...
Processing theory FOLP-ex.Classical ...
Processing theory FOLP-ex.Intuitionistic ...
Processing theory Sequents.ILL_predlog ...
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.T ...
Processing theory HOL-Prolog.HOHH ...
Processing theory SML.Examples ...
Processing theory Sequents.Washing ...
Processing theory Sequents.S43 ...
Processing theory HOL-Prolog.Func ...
Processing theory HOL-Prolog.Type ...
Processing theory HOL-Prolog.Test ...
Starting session Pure ...
Loading 358 theories ...
Processing theory Landau_Symbols.Group_Sort ...
Processing theory Bernoulli.Bernoulli ...
Processing theory Landau_Symbols.Landau_Real_Products ...
Processing theory Sturm_Tarski.PolyMisc ...
Processing theory Landau_Symbols.Landau_Simprocs ...
Processing theory Landau_Symbols.Landau_More ...
Processing theory Bernoulli.Periodic_Bernpoly ...
Processing theory Sturm_Tarski.Sturm_Tarski ...
Processing theory Budan_Fourier.BF_Misc ...
Processing theory Winding_Number_Eval.Missing_Topology ...
Processing theory Dirichlet_Series.Dirichlet_Misc ...
Processing theory Dirichlet_Series.Multiplicative_Function ...
Processing theory Bernoulli.Bernoulli_FPS ...
Processing theory Dirichlet_Series.Dirichlet_Product ...
Processing theory Dirichlet_Series.Dirichlet_Series ...
Processing theory Dirichlet_Series.Moebius_Mu ...
Processing theory Dirichlet_Series.More_Totient ...
Processing theory Dirichlet_Series.Divisor_Count ...
Processing theory Prime_Distribution_Elementary.Primes_Omega ...
Processing theory Dirichlet_Series.Liouville_Lambda ...
Processing theory Dirichlet_Series.Arithmetic_Summatory ...
Processing theory Dirichlet_Series.Euler_Products ...
Processing theory Dirichlet_Series.Partial_Summation ...
Processing theory Stirling_Formula.Stirling_Formula ...
Processing theory Winding_Number_Eval.Missing_Algebraic ...
Processing theory Winding_Number_Eval.Missing_Analysis ...
Processing theory Winding_Number_Eval.Missing_Transcendental ...
Processing theory Bernoulli.Bernoulli_Zeta ...
Processing theory Euler_MacLaurin.Euler_MacLaurin ...
Processing theory Euler_MacLaurin.Euler_MacLaurin_Landau ...
Processing theory Dirichlet_Series.Dirichlet_Series_Analysis ...
Processing theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics ...
Processing theory Zeta_Function.Zeta_Library ...
Processing theory Winding_Number_Eval.Cauchy_Index_Theorem ...
Processing theory Winding_Number_Eval.Winding_Number_Eval ...
Processing theory Zeta_Function.Zeta_Function ...
Processing theory Prime_Number_Theorem.Prime_Number_Theorem_Library ...
Processing theory Prime_Number_Theorem.Newman_Ingham_Tauberian ...
Processing theory Prime_Number_Theorem.Prime_Counting_Functions ...
Processing theory Prime_Distribution_Elementary.Lcm_Nat_Upto ...
Processing theory Prime_Distribution_Elementary.Prime_Distribution_Elementary_Library ...
Processing theory Prime_Distribution_Elementary.More_Dirichlet_Misc ...
Processing theory Prime_Distribution_Elementary.Primorial ...
Processing theory Prime_Distribution_Elementary.Elementary_Prime_Bounds ...
Processing theory Prime_Distribution_Elementary.Partial_Zeta_Bounds ...
Processing theory Prime_Number_Theorem.Mertens_Theorems ...
Processing theory Prime_Number_Theorem.Prime_Number_Theorem ...
Processing theory Prime_Distribution_Elementary.Shapiro_Tauberian ...
Processing theory Prime_Distribution_Elementary.Moebius_Mu_Sum ...
Processing theory Prime_Distribution_Elementary.PNT_Consequences ...
Processing theory Irrational_Series_Erdos_Straus.Irrational_Series_Erdos_Straus ...
Processing theory Transcendence_Series_Hancl_Rucki.Transcendence_Series ...
Loading 56 theories ...
Removing 39 theories ...
Processing theory DiscretePricing.Generated_Subalgebra ...
Processing theory DiscretePricing.Filtration ...
Processing theory DiscretePricing.Martingale ...
Processing theory DiscretePricing.Disc_Cond_Expect ...
Processing theory DiscretePricing.Infinite_Coin_Toss_Space ...
Processing theory DiscretePricing.Geometric_Random_Walk ...
Processing theory DiscretePricing.Fair_Price ...
Processing theory DiscretePricing.CRR_Model ...
Processing theory DiscretePricing.Option_Price_Examples ...
Processing theory Winding_Number_Eval.Winding_Number_Eval_Examples ...
Loading 22 theories ...
Removing 16 theories ...
Processing theory MFMC_Countable.MFMC_Misc ...
Processing theory Flow_Networks.Graph ...
Processing theory Flow_Networks.Network ...
Processing theory Flow_Networks.Residual_Graph ...
Processing theory Flow_Networks.Augmenting_Flow ...
Processing theory Flow_Networks.Augmenting_Path ...
Processing theory Flow_Networks.Ford_Fulkerson ...
Processing theory MFMC_Countable.MFMC_Network ...
Processing theory EdmondsKarp_Maxflow.EdmondsKarp_Termination_Abstract ...
Processing theory MFMC_Countable.MFMC_Finite ...
Processing theory MFMC_Countable.MFMC_Web ...
Processing theory MFMC_Countable.MFMC_Flow_Attainability ...
Processing theory MFMC_Countable.MFMC_Reduction ...
Processing theory MFMC_Countable.Matrix_For_Marginals ...
Processing theory MFMC_Countable.MFMC_Bounded ...
Processing theory MFMC_Countable.MFMC_Unbounded ...
Processing theory MFMC_Countable.Rel_PMF_Characterisation_MFMC ...
Processing theory MFMC_Countable.Max_Flow_Min_Cut_Countable ...
Loading 12 theories ...
Processing theory Coinductive.Coinductive_Nat ...
Removing 8 theories ...
Processing theory Coinductive.Coinductive_List ...
Processing theory Coinductive.Coinductive_Stream ...
Processing theory Markov_Models.Markov_Models_Auxiliary ...
Processing theory Markov_Models.Discrete_Time_Markov_Chain ...
Processing theory Probabilistic_Noninterference.Interface ...
Processing theory Probabilistic_Noninterference.Language_Semantics ...
Processing theory Probabilistic_Noninterference.Resumption_Based ...
Processing theory Probabilistic_Noninterference.Compositionality ...
Processing theory Probabilistic_Noninterference.Syntactic_Criteria ...
Processing theory Probabilistic_Noninterference.Concrete ...
Loading 23 theories ...
Processing theory Regular-Sets.Regular_Set ...
Processing theory List-Index.List_Index ...
Processing theory List_Update.Inversion ...
Processing theory List_Update.On_Off ...
Processing theory List_Update.Prob_Theory ...
Processing theory List_Update.Swaps ...
Processing theory List_Update.Bit_Strings ...
Processing theory List_Update.Competitive_Analysis ...
Processing theory Regular-Sets.Regular_Exp ...
Processing theory Regular-Sets.NDerivative ...
Processing theory Regular-Sets.Equivalence_Checking ...
Removing 3 theories ...
Processing theory List_Update.RExp_Var ...
Processing theory List_Update.Move_to_Front ...
Processing theory List_Update.Partial_Cost_Model ...
Processing theory List_Update.OPT2 ...
Processing theory List_Update.Phase_Partitioning ...
Processing theory List_Update.MTF2_Effects ...
Processing theory List_Update.List_Factoring ...
Processing theory List_Update.BIT ...
Processing theory List_Update.BIT_pairwise ...
Processing theory List_Update.BIT_2comp_on2 ...
Processing theory List_Update.TS ...
Processing theory List_Update.Comb ...
Loading 9 theories ...
Processing theory Fourier.Confine ...
Processing theory Fourier.Fourier_Aux2 ...
Processing theory Fourier.Periodic ...
Processing theory Ergodic_Theory.SG_Library_Complement ...
Processing theory Lp.Functional_Spaces ...
Removing 18 theories ...
Processing theory Lp.Lp ...
Processing theory Fourier.Lspace ...
Processing theory Fourier.Square_Integrable ...
Processing theory Fourier.Fourier ...
Loading 9 theories ...
Removing 9 theories ...
Processing theory Density_Compiler.Density_Predicates ...
Processing theory Density_Compiler.PDF_Transformations ...
Processing theory Density_Compiler.PDF_Values ...
Processing theory Density_Compiler.PDF_Semantics ...
Processing theory Density_Compiler.PDF_Density_Contexts ...
Processing theory Density_Compiler.PDF_Target_Semantics ...
Processing theory Density_Compiler.PDF_Target_Density_Contexts ...
Processing theory Density_Compiler.PDF_Compiler_Pred ...
Processing theory Density_Compiler.PDF_Compiler ...
Loading 2 theories ...
Removing 9 theories ...
Processing theory Error_Function.Error_Function ...
Processing theory Error_Function.Error_Function_Asymptotics ...
Processing theory Probabilistic_Noninterference.Trace_Based ...
Processing theory Cartan_FP.Cartan ...
Loading 49 theories ...
Removing 23 theories ...
Processing theory VectorSpace.FunctionLemmas ...
Processing theory Regular-Sets.Relation_Interpretation ...
Processing theory VectorSpace.RingModuleFacts ...
Processing theory VectorSpace.MonoidSums ...
Processing theory Regular-Sets.Regexp_Method ...
Processing theory Jordan_Normal_Form.Missing_Misc ...
Processing theory Matrix.Utility ...
Processing theory Abstract-Rewriting.Seq ...
Processing theory Jordan_Normal_Form.Missing_Ring ...
Processing theory Jordan_Normal_Form.Conjugate ...
Processing theory Polynomial_Interpolation.Ring_Hom ...
Processing theory Polynomial_Interpolation.Missing_Unsorted ...
Processing theory Abstract-Rewriting.Abstract_Rewriting ...
Processing theory Abstract-Rewriting.SN_Orders ...
Processing theory Polynomial_Interpolation.Missing_Polynomial ...
Processing theory Polynomial_Factorization.Order_Polynomial ...
Processing theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized ...
Processing theory VectorSpace.LinearCombinations ...
Processing theory Matrix.Ordered_Semiring ...
Processing theory Polynomial_Interpolation.Ring_Hom_Poly ...
Processing theory VectorSpace.SumSpaces ...
Processing theory Matrix.Matrix_Legacy ...
Processing theory Jordan_Normal_Form.Matrix ...
Processing theory Jordan_Normal_Form.Gauss_Jordan_Elimination ...
Processing theory Jordan_Normal_Form.Column_Operations ...
Processing theory VectorSpace.VectorSpace ...
Processing theory Jordan_Normal_Form.Missing_VectorSpace ...
Processing theory Matrix_Tensor.Matrix_Tensor ...
Processing theory Jordan_Normal_Form.Determinant ...
Processing theory Jordan_Normal_Form.Char_Poly ...
Processing theory Jordan_Normal_Form.Jordan_Normal_Form ...
Processing theory Isabelle_Marries_Dirac.Basics ...
Processing theory Isabelle_Marries_Dirac.Binary_Nat ...
Processing theory Jordan_Normal_Form.VS_Connect ...
Processing theory Jordan_Normal_Form.Gram_Schmidt ...
Processing theory Jordan_Normal_Form.Schur_Decomposition ...
Processing theory Isabelle_Marries_Dirac.Quantum ...
Processing theory Isabelle_Marries_Dirac.Complex_Vectors ...
Processing theory Isabelle_Marries_Dirac.Tensor ...
Processing theory Isabelle_Marries_Dirac.More_Tensor ...
Processing theory Jordan_Normal_Form.Jordan_Normal_Form_Existence ...
Processing theory QHLProver.Complex_Matrix ...
Processing theory QHLProver.Gates ...
Processing theory Projective_Measurements.Linear_Algebra_Complements ...
Processing theory Projective_Measurements.Projective_Measurements ...
Processing theory Projective_Measurements.CHSH_Inequality ...
Loading 3 theories ...
Removing 22 theories ...
Processing theory Monomorphic_Monad.Monomorphic_Monad ...
Processing theory Monomorphic_Monad.Monad_Overloading ...
Processing theory Monomorphic_Monad.Just_Do_It_Examples ...
Processing theory Monomorphic_Monad.Interpreter ...
Loading 33 theories ...
Removing 4 theories ...
Processing theory Ergodic_Theory.Fekete ...
Processing theory Gromov_Hyperbolicity.Library_Complements ...
Processing theory Gromov_Hyperbolicity.Eexp_Eln ...
Processing theory Gromov_Hyperbolicity.Hausdorff_Distance ...
Processing theory Gromov_Hyperbolicity.Isometries ...
Processing theory Gromov_Hyperbolicity.Metric_Completion ...
Processing theory Gromov_Hyperbolicity.Gromov_Hyperbolicity ...
Processing theory Gromov_Hyperbolicity.Gromov_Boundary ...
Processing theory Gromov_Hyperbolicity.Morse_Gromov_Theorem ...
Processing theory Gromov_Hyperbolicity.Boundary_Extension ...
Processing theory Gromov_Hyperbolicity.Busemann_Function ...
Processing theory Gromov_Hyperbolicity.Isometries_Classification ...
Loading 15 theories ...
Processing theory Treaps.Probability_Misc ...
Processing theory Comparison_Sort_Lower_Bound.Linorder_Relations ...
Removing 6 theories ...
Processing theory Treaps.Random_List_Permutation ...
Processing theory Quick_Sort_Cost.Randomised_Quick_Sort ...
Processing theory Quick_Sort_Cost.Quick_Sort_Average_Case ...
Processing theory Random_BSTs.Random_BSTs ...
Processing theory Treaps.Treap ...
Processing theory Treaps.Treap_Sort_and_BSTs ...
Processing theory Treaps.Random_Treap ...
Loading 7 theories ...
Removing 9 theories ...
Processing theory First_Welfare_Theorem.Syntax ...
Processing theory Neumann_Morgenstern_Utility.PMF_Composition ...
Processing theory Neumann_Morgenstern_Utility.Lotteries ...
Processing theory First_Welfare_Theorem.Preferences ...
Processing theory First_Welfare_Theorem.Utility_Functions ...
Processing theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem ...
Processing theory Neumann_Morgenstern_Utility.Expected_Utility ...
Processing theory MFMC_Countable.Rel_PMF_Characterisation ...
Removing 15 theories ...
Processing theory Gromov_Hyperbolicity.Bonk_Schramm_Extension ...
Loading 5 theories ...
Removing 7 theories ...
Processing theory Skip_Lists.Misc ...
Processing theory Monad_Normalisation.Monad_Normalisation ...
Processing theory Skip_Lists.Pi_pmf ...
Processing theory Skip_Lists.Geometric_PMF ...
Processing theory Skip_Lists.Skip_List ...
Loading 9 theories ...
Removing 4 theories ...
Processing theory Probabilistic_System_Zoo.Nonempty_Bounded_Set ...
Processing theory Probabilistic_System_Zoo.Probabilistic_Hierarchy ...
Processing theory Probabilistic_System_Zoo.Vardi ...
Processing theory Probabilistic_System_Zoo.Vardi_Counterexample ...
Processing theory Monad_Normalisation.Monad_Normalisation_Test ...
Loading 42 theories ...
Removing 7 theories ...
Processing theory Probabilistic_Prime_Tests.Legendre_Symbol ...
Processing theory Probabilistic_Prime_Tests.Algebraic_Auxiliaries ...
Processing theory Probabilistic_Prime_Tests.Generalized_Primality_Test ...
Processing theory Probabilistic_Prime_Tests.Residues_Nat ...
Processing theory Probabilistic_Prime_Tests.Jacobi_Symbol ...
Processing theory Probabilistic_Prime_Tests.QuadRes ...
Processing theory Probabilistic_Prime_Tests.Euler_Witness ...
Loading 3 theories ...
Processing theory Probabilistic_Prime_Tests.Solovay_Strassen_Test ...
Processing theory Probabilistic_Prime_Tests.Carmichael_Numbers ...
Processing theory Probabilistic_Prime_Tests.Fermat_Witness ...
Processing theory Probabilistic_Prime_Tests.Miller_Rabin_Test ...
Processing theory Probabilistic_Prime_Tests.Fermat_Test ...
Removing 9 theories ...
Processing theory Fisher_Yates.Fisher_Yates ...
Processing theory Buffons_Needle.Buffons_Needle ...
Loading 7 theories ...
Removing 27 theories ...
Processing theory Green.General_Utils ...
Processing theory Green.Derivs ...
Processing theory Green.Integrals ...
Processing theory Green.Paths ...
Processing theory Green.Green ...
Processing theory Green.SymmetricR2Shapes ...
Processing theory Green.DiamExample ...
Removing 1 theories ...
Processing theory Green.CircExample ...
Processing theory Source_Coding_Theorem.Source_Coding_Theorem ...
Loading 17 theories ...
Processing theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities ...
Processing theory Ordinary_Differential_Equations.Vector_Derivative_On ...
Processing theory Ordinary_Differential_Equations.Gronwall ...
Processing theory Ordinary_Differential_Equations.Interval_Integral_HK ...
Processing theory Affine_Arithmetic.Executable_Euclidean_Space ...
Removing 14 theories ...
Processing theory Ordinary_Differential_Equations.ODE_Auxiliarities ...
Processing theory Ordinary_Differential_Equations.Initial_Value_Problem ...
Processing theory Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative ...
Processing theory Hybrid_Systems_VCs.HS_Preliminaries ...
Processing theory Matrices_for_ODEs.MTX_Preliminaries ...
Processing theory Matrices_for_ODEs.MTX_Norms ...
Processing theory Hybrid_Systems_VCs.HS_ODEs ...
Processing theory Matrices_for_ODEs.SQ_MTX ...
Processing theory Matrices_for_ODEs.MTX_Flows ...
Processing theory Hybrid_Systems_VCs.HS_VC_Spartan ...
Processing theory Matrices_for_ODEs.MTX_Examples ...
Loading 27 theories ...
Removing 5 theories ...
Processing theory Kleene_Algebra.Signatures ...
Processing theory Order_Lattice_Props.Sup_Lattice ...
Processing theory Kleene_Algebra.Dioid ...
Processing theory Order_Lattice_Props.Order_Duality ...
Processing theory Kleene_Algebra.Conway ...
Processing theory Kleene_Algebra.Kleene_Algebra ...
Processing theory Kleene_Algebra.PHL_KA ...
Processing theory KAT_and_DRA.Test_Dioid ...
Processing theory KAT_and_DRA.Conway_Tests ...
Processing theory KAT_and_DRA.KAT ...
Processing theory KAT_and_DRA.PHL_KAT ...
Processing theory Hybrid_Systems_VCs.HS_VC_KAT ...
Processing theory Order_Lattice_Props.Order_Lattice_Props ...
Processing theory Order_Lattice_Props.Galois_Connections ...
Processing theory Order_Lattice_Props.Fixpoint_Fusion ...
Processing theory Transformer_Semantics.Powerset_Monad ...
Processing theory Order_Lattice_Props.Closure_Operators ...
Processing theory Quantales.Quantales ...
Processing theory Quantales.Quantale_Star ...
Processing theory Transformer_Semantics.Isotone_Transformers ...
Processing theory Transformer_Semantics.Sup_Inf_Preserving_Transformers ...
Processing theory Transformer_Semantics.Kleisli_Transformers ...
Processing theory Transformer_Semantics.Kleisli_Quantaloid ...
Processing theory Transformer_Semantics.Kleisli_Quantale ...
Processing theory Hybrid_Systems_VCs.HS_VC_KA_ndfun ...
Processing theory Hybrid_Systems_VCs.HS_VC_KAT_ndfun ...
Processing theory Hybrid_Systems_VCs.HS_VC_KAT_Examples_ndfun ...
Loading 3 theories ...
Processing theory Hybrid_Systems_VCs.HS_VC_KA_rel ...
Processing theory Hybrid_Systems_VCs.HS_VC_KAT_rel ...
Processing theory Hybrid_Systems_VCs.HS_VC_KAT_Examples_rel ...
Loading 2 theories ...
Removing 10 theories ...
Processing theory Hybrid_Systems_VCs.HS_VC_PT ...
Loading 7 theories ...
Processing theory Hybrid_Systems_VCs.HS_VC_PT_Examples ...
Processing theory KAD.Domain_Semiring ...
Removing 2 theories ...
Processing theory KAD.Antidomain_Semiring ...
Processing theory KAD.Range_Semiring ...
Processing theory KAD.Modal_Kleene_Algebra ...
Processing theory Hybrid_Systems_VCs.HS_VC_MKA ...
Processing theory Hybrid_Systems_VCs.HS_VC_MKA_ndfun ...
Processing theory Hybrid_Systems_VCs.HS_VC_MKA_Examples_ndfun ...
Processing theory Hybrid_Systems_VCs.HS_VC_Examples ...
Loading 2 theories ...
Removing 19 theories ...
Processing theory Hybrid_Systems_VCs.HS_VC_MKA_rel ...
Loading 6 theories ...
Processing theory Hybrid_Systems_VCs.HS_VC_MKA_Examples_rel ...
Processing theory Laplace_Transform.Lerch_Lemma ...
Processing theory Laplace_Transform.Laplace_Transform_Library ...
Processing theory Laplace_Transform.Piecewise_Continuous ...
Processing theory Laplace_Transform.Existence ...
Loading 3 theories ...
Processing theory Laplace_Transform.Uniqueness ...
Processing theory Laplace_Transform.Laplace_Transform ...
Processing theory Prime_Harmonic_Series.Prime_Harmonic_Misc ...
Processing theory Prime_Harmonic_Series.Squarefree_Nat ...
Processing theory Prime_Harmonic_Series.Prime_Harmonic ...
Removing 23 theories ...
Processing theory Irrationality_J_Hancl.Irrationality_J_Hancl ...
Processing theory Furstenberg_Topology.Furstenberg_Topology ...
Loading 2 theories ...
Processing theory Catalan_Numbers.Catalan_Auxiliary_Integral ...
Processing theory Catalan_Numbers.Catalan_Numbers ...
Loading 11 theories ...
Removing 47 theories ...
Processing theory Smooth_Manifolds.Analysis_More ...
Processing theory Smooth_Manifolds.Chart ...
Processing theory Smooth_Manifolds.Topological_Manifold ...
Processing theory Smooth_Manifolds.Smooth ...
Processing theory Smooth_Manifolds.Bump_Function ...
Processing theory Smooth_Manifolds.Differentiable_Manifold ...
Processing theory Smooth_Manifolds.Partition_Of_Unity ...
Processing theory Smooth_Manifolds.Tangent_Space ...
Processing theory Smooth_Manifolds.Cotangent_Space ...
Processing theory Smooth_Manifolds.Sphere ...
Loading 3 theories ...
Removing 6 theories ...
Processing theory Smooth_Manifolds.Projective_Space ...
Processing theory Smooth_Manifolds.Product_Manifold ...
Loading 7 theories ...
Processing theory UpDown_Scheme.Grid_Point ...
Removing 12 theories ...
Processing theory UpDown_Scheme.Grid ...
Processing theory UpDown_Scheme.UpDown_Scheme ...
Processing theory UpDown_Scheme.Triangular_Function ...
Processing theory UpDown_Scheme.Down ...
Processing theory UpDown_Scheme.Up ...
Processing theory UpDown_Scheme.Up_Down ...
Removing 4 theories ...
Processing theory Minkowskis_Theorem.Minkowskis_Theorem ...
Loading 2 theories ...
Processing theory Banach_Steinhaus.Banach_Steinhaus_Missing ...
Processing theory Banach_Steinhaus.Banach_Steinhaus ...
Loading 27 theories ...
Processing theory Deep_Learning.DL_Missing_Finite_Set ...
Processing theory Jordan_Normal_Form.DL_Missing_List ...
Processing theory Deep_Learning.DL_Concrete_Matrices ...
Processing theory Deep_Learning.DL_Flatten_Matrix ...
Processing theory Deep_Learning.Tensor ...
Processing theory Polynomials.MPoly_Type ...
Removing 14 theories ...
Processing theory Deep_Learning.Tensor_Subtensor ...
Processing theory Deep_Learning.Lebesgue_Functional ...
Processing theory Deep_Learning.Tensor_Plus ...
Processing theory Deep_Learning.Tensor_Scalar_Mult ...
Processing theory Jordan_Normal_Form.DL_Missing_Sublist ...
Processing theory Polynomials.More_MPoly_Type ...
Processing theory Deep_Learning.Tensor_Matricization ...
Processing theory Jordan_Normal_Form.DL_Submatrix ...
Processing theory Polynomials.MPoly_Type_Univariate ...
Processing theory Deep_Learning.Tensor_Product ...
Processing theory Deep_Learning.Tensor_Unit_Vec ...
Processing theory Deep_Learning.Tensor_Rank ...
Processing theory Deep_Learning.Lebesgue_Zero_Set ...
Processing theory Jordan_Normal_Form.DL_Rank ...
Processing theory Deep_Learning.DL_Rank_CP_Rank ...
Processing theory Jordan_Normal_Form.DL_Rank_Submatrix ...
Processing theory Deep_Learning.DL_Network ...
Processing theory Deep_Learning.DL_Shallow_Model ...
Processing theory Deep_Learning.DL_Deep_Model ...
Processing theory Deep_Learning.DL_Deep_Model_Poly ...
Loading 30 theories ...
Processing theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity ...
Removing 54 theories ...
Processing theory Gauss_Jordan.Code_Set ...
Processing theory Gauss_Jordan.Code_Z2 ...
Processing theory QR_Decomposition.IArray_Addenda_QR ...
Processing theory Rank_Nullity_Theorem.Dual_Order ...
Processing theory Rank_Nullity_Theorem.Mod_Type ...
Processing theory Rank_Nullity_Theorem.Miscellaneous ...
Processing theory Gauss_Jordan.Code_Matrix ...
Processing theory Gauss_Jordan.Rref ...
Processing theory Rank_Nullity_Theorem.Fundamental_Subspaces ...
Processing theory Rank_Nullity_Theorem.Dim_Formula ...
Processing theory Gauss_Jordan.Rank ...
Processing theory Gauss_Jordan.Elementary_Operations ...
Processing theory QR_Decomposition.Matrix_To_IArray_QR ...
Processing theory Gauss_Jordan.Gauss_Jordan ...
Processing theory Gauss_Jordan.Linear_Maps ...
Processing theory Gauss_Jordan.Gauss_Jordan_PA ...
Processing theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces ...
Processing theory Gauss_Jordan.Determinants2 ...
Processing theory Gauss_Jordan.Inverse ...
Processing theory Gauss_Jordan.System_Of_Equations ...
Processing theory Gauss_Jordan.Examples_Gauss_Jordan_Abstract ...
Processing theory QR_Decomposition.Miscellaneous_QR ...
Processing theory QR_Decomposition.Projections ...
Processing theory QR_Decomposition.Gram_Schmidt ...
Processing theory QR_Decomposition.QR_Decomposition ...
Processing theory QR_Decomposition.Gram_Schmidt_IArrays ...
Loading 16 theories ...
Processing theory QR_Decomposition.QR_Decomposition_IArrays ...
Processing theory QR_Decomposition.QR_Efficient ...
Processing theory Deriving.Derive_Manager ...
Processing theory Deriving.Generator_Aux ...
Processing theory Real_Impl.Real_Impl_Auxiliary ...
Processing theory Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary ...
Processing theory Show.Show ...
Processing theory Show.Show_Real ...
Processing theory Show.Show_Instances ...
Processing theory Cauchy.CauchysMeanTheorem ...
Processing theory Sqrt_Babylonian.Log_Impl ...
Processing theory Sqrt_Babylonian.NthRoot_Impl ...
Removing 1 theories ...
Processing theory Sqrt_Babylonian.Sqrt_Babylonian ...
Processing theory Real_Impl.Prime_Product ...
Processing theory Real_Impl.Real_Impl ...
Processing theory Real_Impl.Real_Unique_Impl ...
Processing theory QR_Decomposition.Examples_QR_Abstract_Symbolic ...
Processing theory QR_Decomposition.Examples_QR_IArrays_Symbolic ...
Loading 3 theories ...
Processing theory Gauss_Jordan.Code_Real_Approx_By_Float_Haskell ...
Processing theory QR_Decomposition.Examples_QR_IArrays_Float ...
Processing theory QR_Decomposition.Least_Squares_Approximation ...
Removing 17 theories ...
Processing theory QR_Decomposition.Examples_QR_Abstract_Float ...
Loading 18 theories ...
Processing theory pGCL.Misc ...
Processing theory pGCL.Expectations ...
Processing theory pGCL.Transformers ...
Processing theory pGCL.Induction ...
Processing theory pGCL.Embedding ...
Processing theory pGCL.Healthiness ...
Processing theory pGCL.Continuity ...
Removing 6 theories ...
Processing theory pGCL.LoopInduction ...
Processing theory pGCL.Sublinearity ...
Processing theory pGCL.WellDefined ...
Processing theory pGCL.Determinism ...
Processing theory pGCL.Loops ...
Processing theory pGCL.Algebra ...
Processing theory pGCL.StructuredReasoning ...
Processing theory pGCL.Automation ...
Processing theory pGCL.Termination ...
Processing theory pGCL.pGCL ...
Processing theory pGCL.Primitives ...
Processing theory pGCL.Monty ...
Removing 2 theories ...
Processing theory pGCL.LoopExamples ...
Loading 12 theories ...
Processing theory Gauss_Jordan.IArray_Addenda ...
Processing theory Gauss_Jordan.Matrix_To_IArray ...
Processing theory Gauss_Jordan.Gauss_Jordan_IArrays ...
Processing theory Gauss_Jordan.Determinants_IArrays ...
Processing theory Gauss_Jordan.Gauss_Jordan_PA_IArrays ...
Processing theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces_IArrays ...
Processing theory Gauss_Jordan.Inverse_IArrays ...
Processing theory Gauss_Jordan.System_Of_Equations_IArrays ...
Removing 18 theories ...
Processing theory Gauss_Jordan.Examples_Gauss_Jordan_IArrays ...
Processing theory Gauss_Jordan.Code_Generation_IArrays ...
Processing theory Gauss_Jordan.Code_Rational ...
Processing theory Gauss_Jordan.Code_Generation_IArrays_Haskell ...
Processing theory Gauss_Jordan.Code_Generation_IArrays_SML ...
Loading 9 theories ...
Processing theory Tarskis_Geometry.Action ...
Processing theory Tarskis_Geometry.Metric ...
Processing theory Tarskis_Geometry.Miscellany ...
Processing theory Tarskis_Geometry.Linear_Algebra2 ...
Processing theory Tarskis_Geometry.Tarski ...
Processing theory Tarskis_Geometry.Euclid_Tarski ...
Removing 29 theories ...
Processing theory Tarskis_Geometry.Projective ...
Processing theory Tarskis_Geometry.Hyperbolic_Tarski ...
Loading 10 theories ...
Processing theory Differential_Game_Logic.Identifiers ...
Processing theory Differential_Game_Logic.Lib ...
Processing theory Differential_Game_Logic.Syntax ...
Processing theory Differential_Game_Logic.Ids ...
Removing 8 theories ...
Processing theory Differential_Game_Logic.Denotational_Semantics ...
Processing theory Differential_Game_Logic.Axioms ...
Processing theory Differential_Game_Logic.Static_Semantics ...
Processing theory Differential_Game_Logic.Coincidence ...
Processing theory Differential_Game_Logic.USubst ...
Loading 16 theories ...
Processing theory Differential_Game_Logic.Differential_Game_Logic ...
Processing theory Separation_Logic_Imperative_HOL.Syntax_Match ...
Processing theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add ...
Processing theory Separation_Logic_Imperative_HOL.Run ...
Removing 10 theories ...
Processing theory Automatic_Refinement.Misc ...
Processing theory Separation_Logic_Imperative_HOL.Assertions ...
Processing theory Separation_Logic_Imperative_HOL.Hoare_Triple ...
Processing theory Separation_Logic_Imperative_HOL.Automation ...
Loading 7 theories ...
Processing theory Separation_Logic_Imperative_HOL.Sep_Main ...
Processing theory UpDown_Scheme.Imperative ...
Processing theory Sturm_Sequences.Misc_Polynomial ...
Processing theory Sturm_Sequences.Sturm_Library ...
Removing 4 theories ...
Processing theory Sturm_Sequences.Sturm_Theorem ...
Processing theory Sturm_Sequences.Sturm_Method ...
Processing theory Sturm_Sequences.Sturm ...
Processing theory Safe_Distance.Safe_Distance ...
Processing theory Safe_Distance.Safe_Distance_Reaction ...
Removing 1 theories ...
Processing theory Safe_Distance.Evaluation ...
Loading 4 theories ...
Processing theory First_Welfare_Theorem.Argmax ...
Processing theory First_Welfare_Theorem.Consumers ...
Processing theory First_Welfare_Theorem.Common ...
Processing theory First_Welfare_Theorem.Private_Ownership_Economy ...
Processing theory First_Welfare_Theorem.Exchange_Economy ...
Processing theory First_Welfare_Theorem.Arrow_Debreu_Model ...
Removing 16 theories ...
Processing theory QR_Decomposition.Generalizations2 ...
Loading 3 theories ...
Processing theory Triangle.Angles ...
Processing theory Triangle.Triangle ...
Processing theory Stewart_Apollonius.Stewart_Apollonius ...
Processing theory Chord_Segments.Chord_Segments ...
Loading 2 theories ...
Removing 9 theories ...
Processing theory Octonions.Cross_Product_7 ...
Processing theory Octonions.Octonions ...
Loading 2 theories ...
Processing theory Cayley_Hamilton.Square_Matrix ...
Processing theory Cayley_Hamilton.Cayley_Hamilton ...
Removing 4 theories ...
Processing theory Quaternions.Quaternions ...
Processing theory Ptolemys_Theorem.Ptolemys_Theorem ...
Removing 2 theories ...
Processing theory Lower_Semicontinuous.Lower_Semicontinuous ...
Removing 1 theories ...
Processing theory Kuratowski_Closure_Complement.KuratowskiClosureComplementTheorem ...
Loading 8 theories ...
Processing theory Store_Buffer_Reduction.SyntaxTweaks ...
Removing 21 theories ...
Processing theory Store_Buffer_Reduction.ReduceStoreBuffer ...
Processing theory Store_Buffer_Reduction.ReduceStoreBufferSimulation ...
Processing theory Store_Buffer_Reduction.PIMP ...
Loading 39 theories ...
Processing theory Store_Buffer_Reduction.Abbrevs ...
Processing theory Store_Buffer_Reduction.Preliminaries ...
Processing theory Store_Buffer_Reduction.Variants ...
Processing theory Store_Buffer_Reduction.Text ...
Processing theory Psi_Calculi.Chain ...
Removing 8 theories ...
Processing theory Psi_Calculi.Subst_Term ...
Processing theory Psi_Calculi.Agent ...
Processing theory Psi_Calculi.Close_Subst ...
Processing theory Psi_Calculi.Structural_Congruence ...
Processing theory Psi_Calculi.Frame ...
Processing theory Psi_Calculi.Semantics ...
Processing theory Psi_Calculi.Simulation ...
Processing theory Psi_Calculi.Sum ...
Processing theory Psi_Calculi.Tau_Chain ...
Processing theory Psi_Calculi.Weak_Stat_Imp ...
Processing theory Psi_Calculi.Weak_Stat_Imp_Pres ...
Processing theory Psi_Calculi.Bisimulation ...
Processing theory Psi_Calculi.Weak_Simulation ...
Processing theory Psi_Calculi.Weak_Cong_Simulation ...
Processing theory Psi_Calculi.Sim_Pres ...
Processing theory Psi_Calculi.Bisim_Pres ...
Processing theory Psi_Calculi.Sim_Struct_Cong ...
Processing theory Psi_Calculi.Bisim_Struct_Cong ...
Processing theory Psi_Calculi.Bisim_Subst ...
Processing theory Psi_Calculi.Weak_Bisimulation ...
Processing theory Psi_Calculi.Weak_Psi_Congruence ...
Processing theory Psi_Calculi.Weak_Sim_Pres ...
Processing theory Psi_Calculi.Weak_Bisim_Pres ...
Processing theory Psi_Calculi.Weakening ...
Processing theory Psi_Calculi.Weaken_Transition ...
Processing theory Psi_Calculi.Weaken_Stat_Imp ...
Processing theory Psi_Calculi.Weaken_Simulation ...
Processing theory Psi_Calculi.Weaken_Bisimulation ...
Processing theory Psi_Calculi.Weak_Bisim_Struct_Cong ...
Processing theory Psi_Calculi.Weak_Cong_Sim_Pres ...
Processing theory Psi_Calculi.Weak_Cong_Pres ...
Processing theory Psi_Calculi.Weak_Cong_Struct_Cong ...
Processing theory Psi_Calculi.Weak_Congruence ...
Processing theory Psi_Calculi.Tau ...
Processing theory Psi_Calculi.Tau_Sim ...
Processing theory Psi_Calculi.Tau_Stat_Imp ...
Processing theory Psi_Calculi.Tau_Laws_Weak ...
Processing theory Psi_Calculi.Tau_Laws_No_Weak ...
Loading 26 theories ...
Removing 17 theories ...
Processing theory FinFun.FinFun ...
Processing theory Nominal2.Nominal2_Base ...
Processing theory Nominal2.Nominal2_Abs ...
Processing theory Nominal2.Nominal2_FCB ...
Processing theory Nominal2.Nominal2 ...
Processing theory MiniSail.Nominal-Utils ...
Processing theory MiniSail.Syntax ...
Processing theory MiniSail.IVSubst ...
Processing theory MiniSail.SyntaxL ...
Processing theory MiniSail.BTVSubst ...
Processing theory MiniSail.Wellformed ...
Processing theory MiniSail.RCLogic ...
Processing theory MiniSail.WellformedL ...
Processing theory MiniSail.SubstMethods ...
Processing theory MiniSail.Typing ...
Processing theory MiniSail.Operational ...
Processing theory MiniSail.RCLogicL ...
Processing theory MiniSail.TypingL ...
Processing theory MiniSail.ContextSubtypingL ...
Processing theory MiniSail.BTVSubstTypingL ...
Processing theory MiniSail.IVSubstTypingL ...
Processing theory MiniSail.Safety ...
Processing theory MiniSail.MiniSail ...
Processing theory Psi_Calculi.Weak_Bisim_Subst ...
Loading 2 theories ...
Removing 45 theories ...
Processing theory KD_Tree.KD_Tree ...
Processing theory KD_Tree.Range_Search ...
Processing theory KD_Tree.Nearest_Neighbors ...
Loading 2 theories ...
Processing theory Median_Of_Medians_Selection.Median_Of_Medians_Selection ...
Processing theory KD_Tree.Build ...
Loading 30 theories ...
Removing 21 theories ...
Processing theory CoreC++.Auxiliary ...
Processing theory CoreC++.Type ...
Processing theory CoreC++.Value ...
Processing theory CoreC++.Expr ...
Processing theory CoreC++.Decl ...
Processing theory CoreC++.ClassRel ...
Processing theory CoreC++.SubObj ...
Processing theory CoreC++.Objects ...
Processing theory CoreC++.Exceptions ...
Processing theory CoreC++.State ...
Processing theory CoreC++.Syntax ...
Processing theory CoreC++.SystemClasses ...
Processing theory CoreC++.TypeRel ...
Processing theory CoreC++.WellType ...
Processing theory CoreC++.Annotate ...
Processing theory CoreC++.WellTypeRT ...
Processing theory CoreC++.Conform ...
Processing theory CoreC++.WellForm ...
Processing theory CoreC++.WWellForm ...
Processing theory CoreC++.BigStep ...
Processing theory CoreC++.DefAss ...
Processing theory CoreC++.CWellForm ...
Processing theory CoreC++.SmallStep ...
Processing theory CoreC++.Equivalence ...
Processing theory CoreC++.Progress ...
Processing theory CoreC++.HeapExtension ...
Processing theory CoreC++.TypeSafe ...
Processing theory CoreC++.Determinism ...
Processing theory CoreC++.Execute ...
Loading 12 theories ...
Processing theory CoreC++.CoreC++ ...
Processing theory Encodability_Process_Calculi.Relations ...
Processing theory Encodability_Process_Calculi.ProcessCalculi ...
Processing theory Encodability_Process_Calculi.SimulationRelations ...
Processing theory Encodability_Process_Calculi.Encodings ...
Removing 30 theories ...
Processing theory Encodability_Process_Calculi.SourceTargetRelation ...
Processing theory Encodability_Process_Calculi.DivergenceReflection ...
Processing theory Encodability_Process_Calculi.SuccessSensitiveness ...
Processing theory Encodability_Process_Calculi.FullAbstraction ...
Processing theory Encodability_Process_Calculi.OperationalCorrespondence ...
Processing theory Encodability_Process_Calculi.CombinedCriteria ...
Loading 21 theories ...
Processing theory Featherweight_OCL.UML_Types ...
Removing 10 theories ...
Processing theory Featherweight_OCL.UML_Logic ...
Processing theory Featherweight_OCL.UML_Tools ...
Processing theory Featherweight_OCL.UML_PropertyProfiles ...
Processing theory Featherweight_OCL.UML_Boolean ...
Processing theory Featherweight_OCL.UML_String ...
Processing theory Featherweight_OCL.UML_Void ...
Processing theory Featherweight_OCL.UML_Pair ...
Processing theory Featherweight_OCL.UML_Integer ...
Processing theory Featherweight_OCL.UML_Real ...
Processing theory Featherweight_OCL.UML_Sequence ...
Processing theory Featherweight_OCL.UML_Bag ...
Processing theory Featherweight_OCL.UML_Set ...
Processing theory Featherweight_OCL.UML_Library ...
Processing theory Featherweight_OCL.UML_State ...
Processing theory Featherweight_OCL.UML_Contracts ...
Processing theory Featherweight_OCL.UML_Main ...
Processing theory Featherweight_OCL.Analysis_UML ...
Processing theory Featherweight_OCL.Analysis_OCL ...
Processing theory Featherweight_OCL.Design_UML ...
Loading 17 theories ...
Processing theory Featherweight_OCL.Design_OCL ...
Processing theory Native_Word.Code_Int_Integer_Conversion ...
Processing theory Word_Lib.More_Arithmetic ...
Processing theory Pell.Pell ...
Removing 21 theories ...
Processing theory Mersenne_Primes.Lucas_Lehmer_Auxiliary ...
Processing theory Mersenne_Primes.Lucas_Lehmer ...
Processing theory Word_Lib.More_Divides ...
Processing theory Word_Lib.Bit_Comprehension ...
Processing theory Word_Lib.More_Word ...
Processing theory Word_Lib.Least_significant_bit ...
Processing theory Word_Lib.Most_significant_bit ...
Processing theory Word_Lib.Generic_set_bit ...
Processing theory Native_Word.Code_Symbolic_Bits_Int ...
Processing theory Native_Word.Bits_Integer ...
Processing theory Native_Word.Code_Target_Bits_Int ...
Processing theory Mersenne_Primes.Lucas_Lehmer_Code ...
Loading 8 theories ...
Removing 30 theories ...
Processing theory Gaussian_Integers.Gaussian_Integers ...
Processing theory Polynomial_Factorization.Missing_List ...
Processing theory Polynomial_Factorization.Missing_Multiset ...
Processing theory Gaussian_Integers.Gaussian_Integers_Pythagorean_Triples ...
Processing theory Gaussian_Integers.Gaussian_Integers_Sums_Of_Two_Squares ...
Processing theory Polynomial_Factorization.Prime_Factorization ...
Processing theory Gaussian_Integers.Gaussian_Integers_Test ...
Processing theory Gaussian_Integers.Gaussian_Integers_Everything ...
Loading 4 theories ...
Removing 5 theories ...
Processing theory Pell.Efficient_Discrete_Sqrt ...
Processing theory Pell.Pell_Algorithm ...
Processing theory Pell.Pell_Algorithm_Test ...
Loading 62 theories ...
Processing theory Interpreter_Optimizations.Dynamic ...
Processing theory Interpreter_Optimizations.Op ...
Processing theory Interpreter_Optimizations.OpInl ...
Processing theory VeriComp.Transfer_Extras ...
Processing theory VeriComp.Well_founded ...
Processing theory VeriComp.Inf ...
Processing theory Interpreter_Optimizations.List_util ...
Processing theory Interpreter_Optimizations.Option_Extra ...
Processing theory Interpreter_Optimizations.AList_Extra ...
Processing theory VeriComp.Behaviour ...
Processing theory VeriComp.Semantics ...
Processing theory VeriComp.Language ...
Processing theory VeriComp.Simulation ...
Processing theory VeriComp.Compiler ...
Processing theory Interpreter_Optimizations.Result ...
Removing 4 theories ...
Processing theory Interpreter_Optimizations.Env ...
Processing theory Interpreter_Optimizations.Map_Extra ...
Processing theory Interpreter_Optimizations.Global ...
Processing theory Interpreter_Optimizations.Unboxed ...
Processing theory Interpreter_Optimizations.OpUbx ...
Processing theory Interpreter_Optimizations.Unboxed_lemmas ...
Processing theory Interpreter_Optimizations.Inca ...
Processing theory Interpreter_Optimizations.Inca_Verification ...
Processing theory Interpreter_Optimizations.Ubx ...
Processing theory Interpreter_Optimizations.Ubx_Verification ...
Processing theory Interpreter_Optimizations.Inca_to_Ubx_simulation ...
Processing theory Interpreter_Optimizations.Inca_to_Ubx_compiler ...
Loading 4 theories ...
Removing 5 theories ...
Processing theory Formal_Puiseux_Series.Puiseux_Laurent_Library ...
Processing theory Formal_Puiseux_Series.Puiseux_Polynomial_Library ...
Processing theory Formal_Puiseux_Series.FPS_Hensel ...
Processing theory Formal_Puiseux_Series.Formal_Puiseux_Series ...
Loading 9 theories ...
Processing theory Padic_Ints.Supplementary_Ring_Facts ...
Removing 4 theories ...
Processing theory Padic_Ints.Extended_Int ...
Processing theory Padic_Ints.Function_Ring ...
Processing theory Padic_Ints.Padic_Construction ...
Processing theory Padic_Ints.Padic_Integers ...
Processing theory Padic_Ints.Padic_Int_Topology ...
Processing theory Padic_Ints.Cring_Poly ...
Processing theory Padic_Ints.Padic_Int_Polynomials ...
wrapper script does not seem to be touching the log file in /media/data/jenkins/workspace/isabelle-dump@tmp/durable-f447c949
(JENKINS-48300: if on an extremely laggy filesystem, consider -Dorg.jenkinsci.plugins.durabletask.BourneShellScript.HEARTBEAT_CHECK_INTERVAL=86400)
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Store)
Stage "Store" skipped due to earlier failure(s)
[Pipeline] }
[Pipeline] // stage
[Pipeline] }
[Pipeline] // timeout
[Pipeline] }
[Pipeline] // node
[Pipeline] End of Pipeline
ERROR: script returned exit code -1
Finished: FAILURE