Console Output

Started by timer
[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: Status code 200 is in the accepted range: 100:399
[Pipeline] }
[Pipeline] // script
[Pipeline] checkout
$ hg clone --rev 8a48a9be91ce3157569020717f3ab62ae99de456 --noupdate https://isabelle.in.tum.de/repos/isabelle /media/data/jenkins/workspace/isabelle-dump
adding changesets
adding manifests
adding file changes
added 75080 changesets with 205333 changes to 11462 files
new changesets a5a9c433f639:8a48a9be91ce
[isabelle-dump] $ hg update --rev 8a48a9be91ce3157569020717f3ab62ae99de456
3473 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 78c2a92a8be405385c6a419c5a2bb6579cef286c --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('8a48a9be91ce3157569020717f3ab62ae99de456') and not ancestors(78c2a92a8be405385c6a419c5a2bb6579cef286c)" --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 390f230578c5cb582865d36f647b60cb526bac17 --noupdate https://foss.heptapod.net/isa-afp/afp-devel /media/data/jenkins/workspace/isabelle-dump/afp
adding changesets
adding manifests
adding file changes
added 12423 changesets with 84924 changes to 13435 files
new changesets 86acbdb19eec:390f230578c5
[afp] $ hg update --rev 390f230578c5cb582865d36f647b60cb526bac17
10888 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 3e0d4252153bd5bb9431dbe3ffbe88e33a5eb47c --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('390f230578c5cb582865d36f647b60cb526bac17') and not ancestors(3e0d4252153bd5bb9431dbe3ffbe88e33a5eb47c)" --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
[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) ...
### Building Findfacts Importer (/media/data/jenkins/workspace/findfacts-importer-0.4.4/importer-isabelle/isa-lib/findfacts-importer.jar) ...
### Building Findfacts Build Importer (/media/data/jenkins/workspace/findfacts-importer-0.4.4/importer-isabelle-build/isa-lib/findfacts-build-importer.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.7
[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 803 sessions ...
WARNING: sun.reflect.Reflection.getCallerClass is not supported. This will impact performance.
Build started for Isabelle/Pure ...
Building Pure ...
Finished Pure (0:00:26 elapsed time, 0:00:25 cpu time, factor 0.97)
### 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.Fields ...
Processing theory HOL.Meson ...
Processing theory HOL.Finite_Set ...
Processing theory HOL.Relation ...
Processing theory HOL.Transitive_Closure ...
Processing theory HOL.Wellfounded ...
Processing theory HOL.Fun_Def_Base ...
Processing theory HOL.Wfrec ...
Processing theory HOL.Order_Relation ...
Processing theory HOL.BNF_Wellorder_Relation ...
Processing theory HOL.Hilbert_Choice ...
Processing theory HOL.BNF_Wellorder_Embedding ...
Processing theory HOL.BNF_Wellorder_Constructions ...
Processing theory HOL.Zorn ...
Processing theory HOL.ATP ...
Processing theory HOL.BNF_Cardinal_Order_Relation ...
Processing theory HOL.BNF_Cardinal_Arithmetic ...
Processing theory HOL.Metis ...
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.Equiv_Relations ...
Processing theory HOL.Transfer ...
Processing theory HOL.Lifting ...
Processing theory HOL.Option ...
Processing theory HOL.Extraction ...
Processing theory HOL.Partial_Function ...
Processing theory HOL.Fun_Def ...
Processing theory HOL.Num ...
Processing theory HOL.Power ...
Processing theory HOL.Quotient ...
Processing theory HOL.Groups_Big ...
Processing theory HOL.Lattices_Big ...
Processing theory HOL.Lifting_Set ...
Processing theory HOL.Int ...
Processing theory HOL.Euclidean_Division ...
Processing theory HOL.Parity ...
Processing theory HOL.Divides ...
Processing theory HOL.Numeral_Simprocs ...
Processing theory HOL.Semiring_Normalization ...
Processing theory HOL.SMT ...
Processing theory HOL.Groebner_Basis ...
Processing theory HOL.Set_Interval ...
Processing theory HOL.Conditionally_Complete_Lattices ...
Processing theory HOL.Presburger ...
Processing theory HOL.Sledgehammer ...
Processing theory HOL.Filter ...
Processing theory HOL.List ...
Processing theory HOL.Groups_List ...
Processing theory HOL.Map ...
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.Typerep ...
Processing theory HOL.Random ...
Processing theory HOL.BNF_Greatest_Fixpoint ...
Processing theory HOL.Limited_Sequence ...
Processing theory HOL.Code_Evaluation ...
Processing theory HOL.Quickcheck_Random ...
Processing theory HOL.Random_Pred ...
Processing theory HOL.Random_Sequence ...
Processing theory HOL.Quickcheck_Exhaustive ...
Processing theory HOL.Record ...
Processing theory HOL.Quickcheck_Narrowing ...
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.Util ...
Processing theory HOL-Proofs-Extraction.QuotRem ...
Processing theory HOL-Proofs-Lambda.Commutation ...
Processing theory HOL-Proofs-Extraction.Warshall ...
Processing theory HOL-Proofs-Extraction.Higman ...
Processing theory HOL-Proofs-Extraction.Greatest_Common_Divisor ...
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.ListOrder ...
Processing theory HOL-Proofs-Lambda.ListBeta ...
Processing theory HOL-Proofs-Lambda.InductTermi ...
Processing theory HOL-Proofs-Lambda.StrongNorm ...
Processing theory HOL-Proofs-Lambda.NormalForm ...
Processing theory HOL-Proofs-ex.Hilbert_Classical ...
Processing theory HOL-Proofs-ex.Proof_Terms ...
Processing theory HOL-Library.Multiset ...
Processing theory HOL-Proofs-Extraction.Higman_Extraction ...
Removing 12 theories ...
Processing theory HOL-Proofs-Lambda.Eta ...
Processing theory HOL-Proofs-Lambda.Standardization ...
Processing theory HOL-Proofs-Extraction.Pigeonhole ...
Processing theory HOL-Computational_Algebra.Factorial_Ring ...
Processing theory HOL-Computational_Algebra.Euclidean_Algorithm ...
Removing 5 theories ...
Processing theory HOL-Computational_Algebra.Primes ...
Processing theory HOL-Proofs-Extraction.Euclid ...
Removing 10 theories ...
Processing theory HOL-Proofs-Lambda.WeakNorm ...
Starting session Pure ...
Loading 254 theories ...
Processing theory HOL-Combinatorics.Transposition ...
Processing theory HOL.Hull ...
Processing theory HOL-Library.FuncSet ...
Processing theory HOL-Library.Disjoint_Sets ...
Processing theory HOL-Library.Infinite_Set ...
Processing theory HOL.Modules ...
Processing theory HOL-Library.Nat_Bijection ...
Processing theory HOL.Archimedean_Field ...
Processing theory HOL.Rat ...
Processing theory HOL-Library.Old_Datatype ...
Processing theory HOL-Library.Countable ...
Processing theory HOL-Library.Phantom_Type ...
Processing theory HOL-Library.Cardinality ...
Processing theory HOL.Real ...
Processing theory HOL.Vector_Spaces ...
Processing theory HOL-Library.Product_Plus ...
Processing theory HOL-Library.Product_Order ...
Processing theory HOL-Library.Set_Algebras ...
Processing theory HOL-Library.Countable_Set ...
Processing theory HOL-Library.Set_Idioms ...
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-Library.Complex_Order ...
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-Library.Indicator_Function ...
Processing theory HOL-Library.Liminf_Limsup ...
Processing theory HOL-Library.Nonpos_Ints ...
Processing theory HOL-Analysis.Affine ...
Processing theory HOL-Analysis.Cartesian_Space ...
Processing theory HOL-Analysis.Determinants ...
Processing theory HOL-Computational_Algebra.Formal_Power_Series ...
Processing theory HOL-Library.Order_Continuity ...
Processing theory HOL-Library.Extended_Nat ...
Processing theory HOL-Library.Periodic_Fun ...
Processing theory HOL-Library.Sum_of_Squares ...
Processing theory HOL-Analysis.Norm_Arith ...
Processing theory HOL-Analysis.Convex ...
Processing theory HOL-Analysis.Abstract_Topology ...
Processing theory HOL-Analysis.Abstract_Limits ...
Processing theory HOL-Library.Landau_Symbols ...
Processing theory HOL-Analysis.Abstract_Topology_2 ...
Processing theory HOL-Analysis.Connected ...
Processing theory HOL-Analysis.Elementary_Metric_Spaces ...
Processing theory HOL-Library.Extended_Real ...
Processing theory HOL-Library.Extended_Nonnegative_Real ...
Processing theory HOL-Analysis.Function_Topology ...
Processing theory HOL-Analysis.Product_Topology ...
Processing theory HOL-Analysis.Function_Metric ...
Processing theory HOL-Analysis.Elementary_Normed_Spaces ...
Processing theory HOL-Analysis.Sigma_Algebra ...
Processing theory HOL-Analysis.Measurable ...
Processing theory HOL-Analysis.T1_Spaces ...
Processing theory HOL-Analysis.Infinite_Sum ...
Processing theory HOL-Analysis.Measure_Space ...
Processing theory HOL-Analysis.Topology_Euclidean_Space ...
Processing theory HOL-Analysis.Lindelof_Spaces ...
Processing theory HOL-Analysis.Caratheodory ...
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.Line_Segment ...
Processing theory HOL-Analysis.Convex_Euclidean_Space ...
Processing theory HOL-Analysis.Ordered_Euclidean_Space ...
Processing theory HOL-Analysis.Bounded_Linear_Function ...
Processing theory HOL-Analysis.Tagged_Division ...
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.Lipschitz ...
Processing theory HOL-Analysis.Borel_Space ...
Processing theory HOL-Analysis.Regularity ...
Processing theory HOL-Analysis.Starlike ...
Processing theory HOL-Analysis.Continuous_Extension ...
Processing theory HOL-Analysis.Multivariate_Analysis ...
Processing theory HOL-Analysis.Nonnegative_Lebesgue_Integration ...
Processing theory HOL-Analysis.Binary_Product_Measure ...
Processing theory HOL-Analysis.Embed_Measure ...
Processing theory HOL-Analysis.Complex_Transcendental ...
Processing theory HOL-Analysis.Generalised_Binomial_Theorem ...
Processing theory HOL-Analysis.FPS_Convergence ...
Processing theory HOL-Analysis.Harmonic_Numbers ...
Processing theory HOL-Analysis.Infinite_Products ...
Processing theory HOL-Analysis.Finite_Product_Measure ...
Processing theory HOL-Analysis.Path_Connected ...
Processing theory HOL-Analysis.Locally ...
Processing theory HOL-Analysis.Bochner_Integration ...
Processing theory HOL-Analysis.Complete_Measure ...
Processing theory HOL-Analysis.Arcwise_Connected ...
Processing theory HOL-Analysis.Polytope ...
Processing theory HOL-Analysis.Radon_Nikodym ...
Processing theory HOL-Analysis.Lebesgue_Measure ...
Processing theory HOL-Analysis.Weierstrass_Theorems ...
Processing theory HOL-Analysis.Set_Integral ...
Processing theory HOL-Analysis.Infinite_Set_Sum ...
Processing theory HOL-Analysis.Homotopy ...
Processing theory HOL-Analysis.Abstract_Euclidean_Space ...
Processing theory HOL-Analysis.Homeomorphism ...
Processing theory HOL-Analysis.Brouwer_Fixpoint ...
Processing theory HOL-Analysis.Henstock_Kurzweil_Integration ...
Processing theory HOL-Analysis.Integral_Test ...
Processing theory HOL-Analysis.Fashoda_Theorem ...
Processing theory HOL-Analysis.Retracts ...
Processing theory HOL-Analysis.Smooth_Paths ...
Processing theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration ...
Processing theory HOL-Analysis.Interval_Integral ...
Processing theory HOL-Analysis.Lebesgue_Integral_Substitution ...
Processing theory HOL-Analysis.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.Great_Picard ...
Processing theory HOL-Complex_Analysis.Residue_Theorem ...
Processing theory HOL-Complex_Analysis.Riemann_Mapping ...
Loading 47 theories ...
Processing theory HOL-Complex_Analysis.Complex_Analysis ...
Processing theory HOL-Library.Adhoc_Overloading ...
Processing theory HOL-Library.Monad_Syntax ...
Processing theory HOL-Library.Conditional_Parametricity ...
Processing theory HOL-Library.Rewrite ...
Processing theory HOL-Library.AList ...
Processing theory HOL-Library.Stream ...
Processing theory HOL-Combinatorics.Multiset_Permutations ...
Processing theory HOL-Library.Diagonal_Subsequence ...
Processing theory HOL-Library.Mapping ...
Processing theory HOL-Library.AList_Mapping ...
Processing theory HOL-Probability.Discrete_Topology ...
Processing theory HOL-Library.Complete_Partial_Order2 ...
Processing theory HOL-Library.FSet ...
Processing theory HOL-Probability.Essential_Supremum ...
Processing theory HOL-Library.Sublist ...
Processing theory HOL-Library.Tree ...
Processing theory HOL-Library.Linear_Temporal_Logic_on_Streams ...
Processing theory HOL-Probability.Stopping_Time ...
Processing theory HOL-Probability.Tree_Space ...
Processing theory HOL-Library.Finite_Map ...
Processing theory HOL-Probability.Probability_Measure ...
Processing theory HOL-Probability.Distribution_Functions ...
Removing 11 theories ...
Processing theory HOL-Probability.Weak_Convergence ...
Processing theory HOL-Probability.Helly_Selection ...
Processing theory HOL-Probability.Fin_Map ...
Processing theory HOL-Probability.Conditional_Expectation ...
Processing theory HOL-Probability.Giry_Monad ...
Processing theory HOL-Probability.Projective_Family ...
Processing theory HOL-Probability.Infinite_Product_Measure ...
Processing theory HOL-Probability.Stream_Space ...
Processing theory HOL-Probability.Probability_Mass_Function ...
Processing theory HOL-Probability.PMF_Impl ...
Processing theory HOL-Probability.Random_Permutations ...
Processing theory HOL-Probability.Projective_Limit ...
Processing theory HOL-Probability.Independent_Family ...
Processing theory HOL-Probability.Convolution ...
Processing theory HOL-Probability.Product_PMF ...
Processing theory HOL-Probability.Hoeffding ...
Processing theory HOL-Probability.SPMF ...
Processing theory HOL-Probability.Information ...
Processing theory HOL-Probability.Distributions ...
Processing theory HOL-Probability.Characteristic_Functions ...
Processing theory HOL-Probability.Sinc_Integral ...
Processing theory HOL-Probability.Levy ...
Processing theory HOL-Probability.Central_Limit_Theorem ...
Processing theory HOL-Probability.Probability ...
Processing theory HOL-Probability-ex.Measure_Not_CCC ...
Processing theory HOL-Probability-ex.Koepf_Duermuth_Countermeasure ...
Processing theory HOL-Probability-ex.Dining_Cryptographers ...
Loading 39 theories ...
Removing 86 theories ...
Processing theory HOL-Library.Fun_Lexorder ...
Processing theory HOL-Cardinals.Fun_More ...
Processing theory HOL-Cardinals.Order_Relation_More ...
Processing theory HOL-Cardinals.Order_Union ...
Processing theory HOL-Cardinals.Wellfounded_More ...
Processing theory HOL-Cardinals.Wellorder_Relation ...
Processing theory HOL-Cardinals.Wellorder_Embedding ...
Processing theory HOL-Library.Groups_Big_Fun ...
Processing theory HOL-Library.More_List ...
Processing theory HOL-Algebra.Congruence ...
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.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.Generated_Groups ...
Processing theory HOL-Algebra.Solvable_Groups ...
Processing theory HOL-Algebra.Ring ...
Processing theory HOL-Algebra.AbelCoset ...
Processing theory HOL-Algebra.Module ...
Processing theory HOL-Algebra.Elementary_Groups ...
Processing theory HOL-Algebra.Ideal ...
Processing theory HOL-Algebra.RingHom ...
Processing theory HOL-Algebra.Exact_Sequence ...
Processing theory HOL-Algebra.Product_Groups ...
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 ...
Processing theory HOL-Computational_Algebra.Fraction_Field ...
Processing theory HOL-Computational_Algebra.Group_Closure ...
Processing theory HOL-Data_Structures.Cmp ...
Processing theory HOL-Data_Structures.Less_False ...
Processing theory HOL-Data_Structures.Sorted_Less ...
Processing theory HOL-Data_Structures.AList_Upd_Del ...
Processing theory HOL-Data_Structures.Map_Specs ...
Processing theory HOL-Data_Structures.List_Ins_Del ...
Processing theory HOL-Data_Structures.Set_Specs ...
Processing theory HOL-Library.State_Monad ...
Processing theory HOL-Library.BNF_Axiomatization ...
Processing theory HOL-Computational_Algebra.Normalized_Fraction ...
Processing theory HOL-Computational_Algebra.Nth_Powers ...
Processing theory HOL-Computational_Algebra.Squarefree ...
Processing theory HOL-Library.Case_Converter ...
Processing theory HOL-Library.Code_Lazy ...
Processing theory HOL-Library.Simps_Case_Conv ...
Processing theory HOL-Examples.Records ...
Removing 32 theories ...
Processing theory HOL-Library.BNF_Corec ...
Processing theory HOL-Library.Multiset_Order ...
Processing theory HOL-Library.Combine_PER ...
Processing theory HOL-Library.Confluence ...
Processing theory HOL-Library.Debug ...
Processing theory HOL-Library.Code_Test ...
Processing theory HOL-Library.Confluent_Quotient ...
Processing theory HOL-Library.Dual_Ordered_Lattice ...
Processing theory HOL-Library.Function_Algebras ...
Processing theory HOL-Library.Function_Division ...
Processing theory HOL-Library.Comparator ...
Processing theory HOL-Library.ListVector ...
Processing theory HOL-Library.Dlist ...
Processing theory HOL-Library.IArray ...
Processing theory HOL-Library.Omega_Words_Fun ...
Processing theory HOL-Library.Extended ...
Processing theory HOL-Library.Disjoint_FSets ...
Processing theory HOL-Library.Char_ord ...
Processing theory HOL-Library.Option_ord ...
Processing theory HOL-Library.Ramsey ...
Processing theory HOL-Library.Pattern_Aliases ...
Processing theory HOL-Library.Code_Cardinality ...
Processing theory HOL-Library.Type_Length ...
Processing theory HOL-Library.Saturated ...
Processing theory HOL-Library.Power_By_Squaring ...
Processing theory HOL-Library.Preorder ...
Processing theory HOL-Library.Quotient_Syntax ...
Processing theory HOL-Library.Countable_Set_Type ...
Processing theory HOL-Library.Parallel ...
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.Signed_Division ...
Processing theory HOL-Library.Subseq_Order ...
Processing theory HOL-Library.Transitive_Closure_Table ...
Processing theory HOL-Library.Tree_Multiset ...
Processing theory HOL-Data_Structures.Tree_Set ...
Processing theory HOL-Data_Structures.Tree_Map ...
Processing theory HOL-Library.Z2 ...
Processing theory HOL-Number_Theory.Eratosthenes ...
Processing theory HOL-Library.Sorting_Algorithms ...
Processing theory HOL-Library.Uprod ...
Processing theory HOL-Library.While_Combinator ...
Processing theory HOL-Library.Bourbaki_Witt_Fixpoint ...
Processing theory HOL-Library.BigO ...
Processing theory HOL-Library.Going_To_Filter ...
Processing theory HOL-Library.Log_Nat ...
Processing theory HOL-Library.Lub_Glb ...
Processing theory HOL-Library.Quadratic_Discriminant ...
Processing theory HOL-Library.Tree_Real ...
Processing theory HOL-Library.Word ...
Processing theory HOL-Library.Lattice_Algebras ...
Processing theory HOL-Computational_Algebra.Polynomial ...
Processing theory HOL-Computational_Algebra.Fundamental_Theorem_Algebra ...
Processing theory HOL-Computational_Algebra.Polynomial_FPS ...
Processing theory HOL-Computational_Algebra.Polynomial_Factorial ...
Processing theory HOL-Computational_Algebra.Formal_Laurent_Series ...
Processing theory HOL-Computational_Algebra.Computational_Algebra ...
Processing theory HOL-Library.Float ...
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 ...
Processing theory HOL-Decision_Procs.Approximation_Bounds ...
Removing 1 theories ...
Processing theory HOL-Decision_Procs.Approximation ...
Processing theory HOL-Real_Asymp.Real_Asymp_Approx ...
Removing 1 theories ...
Processing theory HOL-Real_Asymp-Manual.Real_Asymp_Doc ...
Loading 26 theories ...
Processing theory HOL-Algebra.Exponent ...
Processing theory HOL-Algebra.Bij ...
Processing theory HOL-Algebra.Sylow ...
Processing theory HOL-Combinatorics.List_Permutation ...
Processing theory HOL-Algebra.Galois_Connection ...
Processing theory HOL-Algebra.Group_Action ...
Processing theory HOL-Algebra.Ideal_Product ...
Processing theory HOL-Algebra.Zassenhaus ...
Processing theory HOL-Algebra.QuotRing ...
Processing theory HOL-Algebra.Weak_Morphisms ...
Processing theory HOL-Combinatorics.Cycles ...
Processing theory HOL-Algebra.Sym_Groups ...
Processing theory HOL-Algebra.IntRing ...
Removing 8 theories ...
Processing theory HOL-Algebra.Chinese_Remainder ...
Processing theory HOL-Algebra.Divisibility ...
Processing theory HOL-Algebra.Subrings ...
Processing theory HOL-Algebra.Generated_Rings ...
Processing theory HOL-Algebra.Generated_Fields ...
Processing theory HOL-Algebra.Ring_Divisibility ...
Processing theory HOL-Algebra.Embedded_Algebras ...
Processing theory HOL-Algebra.Polynomials ...
Processing theory HOL-Algebra.Polynomial_Divisibility ...
Processing theory HOL-Algebra.Finite_Extensions ...
Processing theory HOL-Algebra.Indexed_Polynomials ...
Processing theory HOL-Algebra.Algebraic_Closure ...
Loading 19 theories ...
Processing theory HOL-Algebra.Algebra ...
Removing 33 theories ...
Processing theory HOL-Decision_Procs.DP_Library ...
Processing theory HOL-Library.Old_Recdef ...
Processing theory HOL-Decision_Procs.Conversions ...
Processing theory HOL-Decision_Procs.Algebra_Aux ...
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.Rat_Pair ...
Processing theory HOL-Decision_Procs.Approximation_Ex ...
Processing theory HOL-Decision_Procs.Approximation_Quickcheck_Ex ...
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 50 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.Up ...
Processing theory HOLCF.Discrete ...
Processing theory HOLCF.Lift ...
Processing theory HOLCF.One ...
Processing theory HOLCF.Tr ...
Processing theory HOLCF.Ssum ...
Processing theory HOL-Matrix_LP.ComputeFloat ...
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 HOLCF.Powerdomains ...
Processing theory HOLCF ...
Processing theory HOL-Matrix_LP.Matrix ...
Removing 23 theories ...
Processing theory HOLCF-Library.Stream ...
Processing theory HOLCF-FOCUS.Fstream ...
Processing theory HOLCF-FOCUS.FOCUS ...
Processing theory HOLCF-FOCUS.Stream_adm ...
Processing theory HOLCF-ex.Dagstuhl ...
Processing theory HOLCF-ex.Focus_ex ...
Processing theory HOLCF-FOCUS.Buffer ...
Processing theory HOLCF-FOCUS.Buffer_adm ...
Processing theory HOL-Matrix_LP.SparseMatrix ...
Loading 25 theories ...
Processing theory HOL-Matrix_LP.Cplex ...
Processing theory HOL-Hahn_Banach.Zorn_Lemma ...
Processing theory HOLCF-Library.Int_Discrete ...
Processing theory HOLCF-Library.Nat_Discrete ...
Processing theory HOLCF-Library.Bool_Discrete ...
Processing theory HOLCF-Library.Char_Discrete ...
Processing theory HOLCF-Library.List_Cpo ...
Processing theory HOL-Hahn_Banach.Bounds ...
Processing theory HOLCF-Library.Defl_Bifinite ...
Processing theory HOLCF-Library.Sum_Cpo ...
Processing theory HOLCF-Library.Option_Cpo ...
Processing theory HOL-Hahn_Banach.Vector_Space ...
Processing theory HOL-Hahn_Banach.Linearform ...
Processing theory HOLCF-Library.List_Predomain ...
Processing theory HOL-Hahn_Banach.Subspace ...
Processing theory HOL-Hahn_Banach.Function_Order ...
Processing theory HOL-Hahn_Banach.Normed_Space ...
Processing theory HOL-Hahn_Banach.Function_Norm ...
Processing theory HOL-Hahn_Banach.Hahn_Banach_Ext_Lemmas ...
Processing theory HOL-Hahn_Banach.Hahn_Banach_Sup_Lemmas ...
Processing theory HOL-Hahn_Banach.Hahn_Banach_Lemmas ...
Processing theory HOL-Hahn_Banach.Hahn_Banach ...
Processing theory HOLCF-FOCUS.Fstreams ...
Processing theory HOLCF-Library.HOLCF_Library ...
Removing 37 theories ...
Processing theory HOL-Data_Structures.Brother12_Set ...
Processing theory HOL-Data_Structures.Brother12_Map ...
Loading 30 theories ...
Processing theory HOL-Data_Structures.Array_Specs ...
Processing theory HOL-Data_Structures.Time_Funs ...
Processing theory HOL-Combinatorics.Stirling ...
Processing theory HOL-Combinatorics.Perm ...
Processing theory HOL-Data_Structures.Trie_Fun ...
Processing theory HOL-Combinatorics.Orbits ...
Processing theory HOL-Data_Structures.Tree2 ...
Processing theory HOL-Data_Structures.Isin2 ...
Processing theory HOL-Data_Structures.AVL_Set_Code ...
Processing theory HOL-Data_Structures.Lookup2 ...
Processing theory HOL-Combinatorics.Combinatorics ...
Processing theory HOL-Data_Structures.Braun_Tree ...
Processing theory HOL-Data_Structures.Sorting ...
Processing theory HOL-Data_Structures.RBT ...
Processing theory HOL-Types_To_Sets.Prerequisites ...
Processing theory HOL-Types_To_Sets.Types_To_Sets ...
Processing theory HOL-Data_Structures.Selection ...
Processing theory HOL-Data_Structures.Set2_Join ...
Removing 13 theories ...
Processing theory HOL-Data_Structures.RBT_Set ...
Processing theory HOL-Data_Structures.RBT_Map ...
Processing theory HOL-Data_Structures.Trie_Map ...
Processing theory HOL-Types_To_Sets.Group_On_With ...
Processing theory HOL-Types_To_Sets.Linear_Algebra_On_With ...
Processing theory HOL-Data_Structures.Array_Braun ...
Processing theory HOL-Data_Structures.RBT_Set2 ...
Processing theory HOL-ex.Function_Growth ...
Processing theory HOL-Types_To_Sets.Linear_Algebra_On ...
Processing theory HOL-Data_Structures.Set2_Join_RBT ...
Removing 17 theories ...
Processing theory HOL-Data_Structures.AVL_Set ...
Processing theory HOL-Data_Structures.AVL_Map ...
Loading 35 theories ...
Processing theory HOL-IMP.Star ...
Processing theory HOL-Library.LaTeXsugar ...
Processing theory HOL-Nitpick_Examples.Hotel_Nits ...
Removing 4 theories ...
Processing theory HOL-Nitpick_Examples.Datatype_Nits ...
Processing theory HOL-Nitpick_Examples.Induct_Nits ...
Processing theory HOL-Nitpick_Examples.Mono_Nits ...
Processing theory HOL-Nitpick_Examples.Manual_Nits ...
Processing theory HOL-Nitpick_Examples.Mini_Nits ...
Processing theory HOL-Nitpick_Examples.Pattern_Nits ...
Processing theory HOL-Nitpick_Examples.Integer_Nits ...
Processing theory HOL-Nitpick_Examples.Tests_Nits ...
Processing theory Codegen.Setup ...
Processing theory Codegen.Adaptation ...
Processing theory Codegen.Evaluation ...
Processing theory Codegen.Further ...
Processing theory HOL-Nitpick_Examples.Record_Nits ...
Processing theory Codegen.Computations ...
Processing theory Codegen.Inductive_Predicate ...
Processing theory Typeclass_Hierarchy.Setup ...
Processing theory Typeclass_Hierarchy.Typeclass_Hierarchy ...
Processing theory HOL-Nitpick_Examples.Special_Nits ...
Processing theory HOL-Library.OptionalSugar ...
Processing theory Sugar.Sugar ...
Processing theory Codegen.Introduction ...
Processing theory Codegen.Foundations ...
Processing theory Codegen.Refinement ...
Processing theory HOL-IMP.Types ...
Processing theory HOL-IMP.Poly_Types ...
Processing theory HOL-Nitpick_Examples.Core_Nits ...
Processing theory HOL-ex.SOS ...
Processing theory HOL-ex.SOS_Cert ...
Processing theory HOL-Data_Structures.Balance ...
Removing 21 theories ...
Processing theory HOL-Nitpick_Examples.Typedef_Nits ...
Processing theory HOL-Nitpick_Examples.Refute_Nits ...
Loading 29 theories ...
Processing theory HOL-Nitpick_Examples.Nitpick_Examples ...
Processing theory HOL-TPTP.TPTP_Parser ...
Processing theory HOL-Library.Refute ...
Processing theory HOL-TPTP.ATP_Theory_Export ...
Processing theory HOL-TPTP.THF_Arith ...
Processing theory HOL-SMT_Examples.SMT_Examples ...
Removing 18 theories ...
Processing theory HOL-TPTP.TPTP_Interpret ...
Processing theory HOL-TPTP.ATP_Problem_Import ...
Processing theory HOL-TPTP.TPTP_Proof_Reconstruction ...
Processing theory HOL-SMT_Examples.SMT_Examples_Verit ...
Processing theory HOL-ex.Code_Binary_Nat_examples ...
Processing theory HOL-ex.Argo_Examples ...
Processing theory HOL-ex.Ballot ...
Processing theory HOL-ex.BinEx ...
Processing theory HOL-SMT_Examples.SMT_Tests_Verit ...
Processing theory HOL-ex.Gauge_Integration ...
Processing theory HOL-SMT_Examples.SMT_Tests ...
Processing theory HOL-ex.HarmonicSeries ...
Processing theory HOL-ex.Dedekind_Real ...
Processing theory HOL-ex.Normalization_by_Evaluation ...
Processing theory HOL-ex.Pythagoras ...
Processing theory HOL-ex.Sqrt_Script ...
Processing theory HOL-ex.Eval_Examples ...
Processing theory HOL-ex.Triangular_Numbers ...
Processing theory HOL-Types_To_Sets.T2_Spaces ...
Processing theory HOL-Types_To_Sets.Unoverload_Def ...
Processing theory HOL-ex.Sum_of_Powers ...
Removing 23 theories ...
Processing theory HOL-ex.Reflection_Examples ...
Removing 2 theories ...
Processing theory HOL-ex.Parallel_Example ...
Processing theory HOL-ex.Cubic_Quartic ...
Loading 14 theories ...
Removing 3 theories ...
Processing theory HOL-Data_Structures.Priority_Queue_Specs ...
Processing theory Tutorial.Examples ...
Processing theory How_to_Prove_it.How_to_Prove_it ...
Processing theory Tutorial.Numbers ...
Processing theory HOL-Computational_Algebra.Field_as_Ring ...
Processing theory HOL-Examples.Sqrt ...
Processing theory HOL-Library.Code_Real_Approx_By_Float ...
Processing theory HOL-Metis_Examples.Clausification ...
Processing theory HOL-Mutabelle.MutabelleExtra ...
Processing theory Prog_Prove.Bool_nat_list ...
Processing theory HOL-Data_Structures.Leftist_Heap ...
Processing theory HOL-Data_Structures.Binomial_Heap ...
Removing 12 theories ...
Processing theory HOL-Corec_Examples.Paper_Examples ...
Removing 1 theories ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_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 12 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 ...
Loading 54 theories ...
Processing theory HOL-Bali.AxSound ...
Processing theory IOA-ABP.Packet ...
Processing theory IOA-NTP.Lemmas ...
Processing theory IOA-ABP.Lemmas ...
Processing theory IOA.Asig ...
Processing theory IOA-NTP.Multiset ...
Processing theory IOA-NTP.Packet ...
Processing theory IOA.Pred ...
Processing theory IOA-Storage.Action ...
Processing theory IOA.Automata ...
Processing theory IOA.Seq ...
Processing theory IOA-ABP.Action ...
Processing theory IOA-NTP.Action ...
Removing 24 theories ...
Processing theory IOA.Sequence ...
Processing theory IOA.TL ...
Processing theory IOA.Traces ...
Processing theory IOA.CompoExecs ...
Processing theory IOA.CompoScheds ...
Processing theory IOA.RefMappings ...
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-ABP.Abschannel ...
Processing theory IOA-ABP.Abschannel_finite ...
Processing theory IOA-ABP.Impl ...
Processing theory IOA-ABP.Impl_finite ...
Processing theory IOA-NTP.Abschannel ...
Processing theory IOA-NTP.Receiver ...
Processing theory IOA-NTP.Sender ...
Processing theory HOL-Nominal.Nominal ...
Processing theory IOA-NTP.Impl ...
Processing theory IOA-NTP.Spec ...
Processing theory IOA-NTP.Correctness ...
Processing theory IOA-Storage.Impl ...
Processing theory IOA-ABP.Correctness ...
Processing theory IOA-Storage.Spec ...
Processing theory IOA-Storage.Correctness ...
Processing theory IOA.TLS ...
Processing theory IOA.LiveIOA ...
Processing theory IOA.Abstraction ...
Processing theory IOA-ex.TrivEx ...
Processing theory IOA-ex.TrivEx2 ...
Removing 50 theories ...
Processing theory HOL-Nominal-Examples.Class1 ...
Processing theory HOL-Nominal-Examples.Class2 ...
Processing theory HOL-Nominal-Examples.Class3 ...
Loading 66 theories ...
Processing theory HOL-Eisbach.Eisbach ...
Processing theory HOL-Eisbach.Eisbach_Tools ...
Processing theory HOL-Isar_Examples.Fibonacci ...
Processing theory HOLCF-Library.HOL_Cpo ...
Processing theory HOL-MicroJava.JBasis ...
Processing theory HOL-MicroJava.Semilat ...
Processing theory HOL-MicroJava.AuxLemmas ...
Processing theory HOL-MicroJava.Err ...
Processing theory HOL-MicroJava.Opt ...
Processing theory HOL-MicroJava.Product ...
Processing theory HOL-ex.Code_Timing ...
Processing theory HOL-Eisbach.Example_Metric ...
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.Value ...
Processing theory HOL-MicroJava.State ...
Processing theory HOL-MicroJava.Exceptions ...
Removing 26 theories ...
Processing theory HOL-MicroJava.Listn ...
Processing theory HOL-MicroJava.Typing_Framework ...
Processing theory HOL-MicroJava.SemilatAlg ...
Processing theory HOL-MicroJava.Kildall ...
Processing theory HOL-MicroJava.LBVSpec ...
Processing theory HOL-MicroJava.LBVComplete ...
Processing theory HOL-MicroJava.LBVCorrect ...
Processing theory HOL-MicroJava.Typing_Framework_err ...
Processing theory HOL-MicroJava.Abstract_BV ...
Processing theory HOL-MicroJava.Semilattices ...
Processing theory HOL-MicroJava.JType ...
Processing theory HOL-MicroJava.JVMType ...
Processing theory HOL-MicroJava.Term ...
Processing theory HOL-MicroJava.WellType ...
Processing theory HOL-MicroJava.TypeInf ...
Processing theory HOL-MicroJava.Conform ...
Processing theory HOL-MicroJava.JVMState ...
Processing theory HOL-MicroJava.Eval ...
Processing theory HOL-MicroJava.Example ...
Processing theory HOL-MicroJava.JListExample ...
Processing theory HOL-MicroJava.JTypeSafe ...
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.JVMDefensive ...
Processing theory HOL-MicroJava.JVMListExample ...
Processing theory HOL-MicroJava.CorrComp ...
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.Correct ...
Processing theory HOL-MicroJava.JVM ...
Processing theory HOL-MicroJava.LBVJVM ...
Processing theory HOL-MicroJava.BVSpecTypeSafe ...
Processing theory HOL-MicroJava.BVNoTypeError ...
Processing theory HOL-MicroJava.BVExample ...
Processing theory HOL-MicroJava.CorrCompTp ...
Loading 81 theories ...
Processing theory HOL-MicroJava.MicroJava ...
Processing theory HOL-Imperative_HOL.Sorted_List ...
Processing theory HOL-IMP.AExp ...
Processing theory HOL-IMP.BExp ...
Processing theory HOLCF-Tutorial.New_Domain ...
Processing theory HOLCF-ex.Dnat ...
Processing theory HOL-IMP.Com ...
Processing theory HOL-IMP.Big_Step ...
Processing theory HOLCF-IMP.Denotational ...
Processing theory HOLCF-IMP.HoareEx ...
Processing theory HOLCF-Tutorial.Fixrec_ex ...
Processing theory HOLCF-ex.Concurrency_Monad ...
Processing theory HOLCF-ex.Domain_Proofs ...
Processing theory HOLCF-ex.Fix2 ...
Processing theory HOLCF-ex.Hoare ...
Processing theory HOLCF-ex.Letrec ...
Processing theory HOLCF-ex.Loop ...
Processing theory HOLCF-ex.Pattern_Match ...
Removing 72 theories ...
Processing theory HOL-Imperative_HOL.List_Sublist ...
Processing theory HOLCF-ex.Powerdomain_ex ...
Processing theory HOL-Imperative_HOL.Heap ...
Processing theory HOL-SMT_Examples.SMT_Word_Examples ...
Processing theory HOL-Imperative_HOL.Heap_Monad ...
Processing theory HOL-Imperative_HOL.Array ...
Processing theory HOL-Imperative_HOL.Ref ...
Processing theory HOL-Imperative_HOL.Imperative_HOL ...
Processing theory HOL-Imperative_HOL.Overview ...
Processing theory HOL-Imperative_HOL.Subarray ...
Processing theory HOL-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-Quotient_Examples.Int_Pow ...
Processing theory HOL-SPARK-Examples.RMD_Lemmas ...
Processing theory HOL-UNITY.ListOrder ...
Processing theory HOL-UNITY.UNITY ...
Processing theory HOL-UNITY.Constrains ...
Processing theory HOLCF-Tutorial.Domain_ex ...
Processing theory HOL-SPARK-Examples.F ...
Processing theory HOL-SPARK-Examples.Longest_Increasing_Subsequence ...
Processing theory HOL-SPARK-Examples.K_R ...
Processing theory HOL-SPARK-Examples.Sqrt ...
Processing theory HOL-Imperative_HOL.Imperative_Reverse ...
Processing theory HOL-SPARK-Examples.Hash ...
Processing theory HOL-SPARK-Examples.K_L ...
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-Imperative_HOL.Imperative_Quicksort ...
Processing theory HOL-SPARK-Examples.R_L ...
Processing theory HOL-SPARK-Examples.R_R ...
Processing theory HOL-UNITY.FP ...
Processing theory HOL-SPARK-Examples.S_L ...
Processing theory HOL-SPARK-Examples.S_R ...
Processing theory HOL-UNITY.WFair ...
Processing theory HOL-UNITY.SubstAx ...
Processing theory HOL-UNITY.Detects ...
Processing theory HOL-UNITY.Follows ...
Processing theory HOL-SPARK-Examples.Round ...
Processing theory HOL-UNITY.Union ...
Processing theory HOL-UNITY.Comp ...
Processing theory HOL-ex.Sorting_Algorithms_Examples ...
Removing 71 theories ...
Processing theory HOL-Imperative_HOL.Linked_Lists ...
Processing theory HOL-SPARK-Manual.Complex_Types ...
Processing theory HOL-UNITY.Guar ...
Processing theory HOL-UNITY.Extend ...
Processing theory HOL-UNITY.Rename ...
Processing theory HOL-UNITY.Lift_prog ...
Processing theory HOL-UNITY.PPROD ...
Processing theory HOL-UNITY.Transformers ...
Processing theory HOL-UNITY.ProgressSets ...
Processing theory HOL-UNITY.UNITY_Main ...
Processing theory HOL-UNITY.AllocBase ...
Processing theory HOL-Imperative_HOL.SatChecker ...
Processing theory HOL-UNITY.Client ...
Processing theory HOL-UNITY.Alloc ...
Processing theory HOL-UNITY.AllocImpl ...
Processing theory HOL-Imperative_HOL.Imperative_HOL_ex ...
Loading 63 theories ...
Removing 19 theories ...
Processing theory HOL-Cardinals.Wellorder_Extension ...
Processing theory HOL-ZF.LProd ...
Processing theory HOL-ex.Bubblesort ...
Processing theory HOL-ex.MergeSort ...
Processing theory HOL-ex.Quicksort ...
Processing theory HOL-Auth.Message ...
Processing theory HOL-Library.List_Lexorder ...
Processing theory HOL-Datatype_Examples.Prelim ...
Processing theory HOL-Datatype_Examples.DTree ...
Processing theory HOL-Datatype_Examples.Parallel_Composition ...
Processing theory HOL-Auth.Event ...
Processing theory HOL-Auth.Public ...
Processing theory HOL-Datatype_Examples.Gram_Lang ...
Processing theory HOL-Cardinals.Ordinal_Arithmetic ...
Processing theory HOL-Cardinals.Cardinals ...
Processing theory HOL-Cardinals.Bounded_Set ...
Processing theory HOL-Nominal-Examples.CR_Takahashi ...
Removing 21 theories ...
Processing theory HOL-Nominal-Examples.Contexts ...
Processing theory HOL-Nominal-Examples.Crary ...
Processing theory HOL-Nominal-Examples.Height ...
Processing theory HOL-Nominal-Examples.CK_Machine ...
Processing theory HOL-Nominal-Examples.Compile ...
Processing theory HOL-Nominal-Examples.Lam_Funs ...
Processing theory HOL-Nominal-Examples.CR ...
Processing theory HOL-Nominal-Examples.SN ...
Processing theory HOL-Nominal-Examples.LocalWeakening ...
Processing theory HOL-Nominal-Examples.SOS ...
Processing theory HOL-Nominal-Examples.Lambda_mu ...
Processing theory HOL-Nominal-Examples.Fsub ...
Removing 12 theories ...
Processing theory HOL-Nominal-Examples.Support ...
Processing theory HOL-Nominal-Examples.VC_Condition ...
Processing theory HOL-Nominal-Examples.Standardization ...
Processing theory HOL-Nominal-Examples.Type_Preservation ...
Processing theory HOL-Nominal-Examples.Weakening ...
Processing theory HOL-Nominal-Examples.W ...
Processing theory HOL-Nominal-Examples.Pattern ...
Processing theory HOL-ex.Radix_Sort ...
Processing theory HOL-Data_Structures.Heaps ...
Processing theory HOL-Quotient_Examples.Quotient_FSet ...
Processing theory HOL-UNITY.Counter ...
Processing theory HOL-UNITY.Counterc ...
Processing theory HOL-UNITY.Handshake ...
Processing theory HOL-UNITY.PriorityAux ...
Processing theory HOL-UNITY.Progress ...
Removing 18 theories ...
Processing theory HOL-Datatype_Examples.Misc_Datatype ...
Processing theory HOL-Datatype_Examples.Misc_Primrec ...
Processing theory HOL-ex.Code_Lazy_Demo ...
Processing theory HOL-UNITY.Priority ...
Processing theory HOL-UNITY.TimerArray ...
Processing theory HOL-UNITY.Channel ...
Processing theory HOL-Datatype_Examples.Misc_Codatatype ...
Processing theory HOL-Datatype_Examples.Misc_Primcorec ...
Processing theory HOL-UNITY.Common ...
Processing theory HOL-UNITY.NSP_Bad ...
Processing theory HOL-UNITY.Reach ...
Processing theory HOL-ZF.HOLZF ...
Processing theory HOL-ZF.Zet ...
Processing theory HOL-ZF.MainZF ...
Processing theory HOL-UNITY.Lift ...
Processing theory HOL-UNITY.Mutex ...
Processing theory HOL-ZF.Games ...
Processing theory HOL-UNITY.Reachability ...
Processing theory HOL-ex.Termination ...
Loading 72 theories ...
Processing theory Isar_Ref.Base ...
Processing theory Datatypes.Setup ...
Processing theory HOL-Auth.All_Symmetric ...
Processing theory HOL-Auth.Extensions ...
Removing 34 theories ...
Processing theory HOL-Auth.Analz ...
Processing theory HOL-Auth.Guard ...
Processing theory HOL-Auth.GuardK ...
Processing theory HOL-Auth.Guard_Public ...
Processing theory HOL-Auth.Guard_NS_Public ...
Processing theory HOL-Auth.KerberosIV_Gets ...
Processing theory HOL-Auth.List_Msg ...
Processing theory HOL-Auth.KerberosIV ...
Processing theory HOL-Auth.KerberosV ...
Processing theory HOL-Auth.Shared ...
Processing theory HOL-Auth.Kerberos_BAN ...
Processing theory HOL-Auth.Proto ...
Processing theory HOL-Auth.P2 ...
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.P1 ...
Processing theory HOL-Auth.Auth_Guard_Public ...
Removing 7 theories ...
Processing theory HOL-Auth.Yahalom_Bad ...
Processing theory HOL-Auth.OtwayReesBella ...
Processing theory HOL-Auth.Yahalom2 ...
Processing theory HOL-Auth.Guard_Shared ...
Processing theory HOL-Auth.Yahalom ...
Processing theory HOL-Auth.ZhouGollmann ...
Processing theory HOL-Auth.Auth_Shared ...
Processing theory HOL-Auth.Guard_OtwayRees ...
Processing theory HOL-Auth.Guard_Yahalom ...
Processing theory HOL-Auth.Auth_Guard_Shared ...
Processing theory HOL-Hoare_Parallel.Quote_Antiquote ...
Processing theory HOL-Hoare_Parallel.Graph ...
Processing theory HOL-Hoare_Parallel.RG_Com ...
Processing theory HOL-Hoare_Parallel.OG_Com ...
Processing theory HOL-Hoare_Parallel.OG_Tran ...
Processing theory HOL-Auth.EventSC ...
Processing theory HOL-Auth.Smartcard ...
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.ShoupRubin ...
Processing theory HOL-Hoare_Parallel.Gar_Coll ...
Removing 26 theories ...
Processing theory HOL-Auth.ShoupRubinBella ...
Processing theory HOL-Auth.Auth_Smartcard ...
Processing theory HOL-Hoare_Parallel.RG_Tran ...
Processing theory HOL-Hoare_Parallel.Mul_Gar_Coll ...
Removing 6 theories ...
Processing theory HOL-Datatype_Examples.TreeFsetI ...
Processing theory HOL-Datatype_Examples.Lambda_Term ...
Processing theory HOL-Hoare_Parallel.OG_Examples ...
Processing theory HOL-Hoare_Parallel.RG_Hoare ...
Processing theory HOL-Hoare_Parallel.RG_Syntax ...
Processing theory Corec.Corec ...
Processing theory HOL-SET_Protocol.Message_SET ...
Processing theory Isar_Ref.HOL_Specific ...
Processing theory HOL-SET_Protocol.Event_SET ...
Processing theory HOL-SET_Protocol.Public_SET ...
Removing 5 theories ...
Processing theory Datatypes.Datatypes ...
Processing theory HOL-ex.Transfer_Debug ...
Processing theory HOL-SET_Protocol.Merchant_Registration ...
Processing theory HOL-UNITY.Project ...
Processing theory HOL-UNITY.ELT ...
Processing theory HOL-Hoare_Parallel.RG_Examples ...
Processing theory HOL-Hoare_Parallel.Hoare_Parallel ...
Processing theory HOL-SET_Protocol.Cardholder_Registration ...
Loading 138 theories ...
Processing theory HOL-SET_Protocol.Purchase ...
Processing theory HOL-SET_Protocol.SET_Protocol ...
Processing theory Tutorial.Base ...
Processing theory Locales.Examples ...
Processing theory Locales.Examples1 ...
Processing theory Locales.Examples2 ...
Processing theory Tutorial.Setup ...
Processing theory HOL-Auth.NS_Public ...
Processing theory Tutorial.CTL ...
Processing theory Tutorial.CTLind ...
Processing theory HOL-Auth.NS_Public_Bad ...
Processing theory HOL-ex.Specifications_with_bundle_mixins ...
Processing theory Locales.Examples3 ...
Processing theory HOL-Hoare.Hoare_Tac ...
Processing theory Tutorial.Message ...
Processing theory Tutorial.Event ...
Processing theory Tutorial.Public ...
Processing theory Tutorial.NS_Public ...
Processing theory HOL-Datatype_Examples.TreeFI ...
Processing theory HOL-Data_Structures.Tree23 ...
Processing theory HOL-Data_Structures.Tree234 ...
Removing 49 theories ...
Processing theory HOL-Auth.CertifiedEmail ...
Processing theory HOL-IMP.Abs_Int_Tests ...
Processing theory HOL-IMP.Hoare ...
Processing theory HOL-IMP.Hoare_Examples ...
Processing theory HOL-Isar_Examples.Hoare ...
Processing theory HOL-Isar_Examples.Hoare_Ex ...
Processing theory HOL-IMP.Hoare_Total ...
Processing theory HOL-IMP.Hoare_Sound_Complete ...
Processing theory HOL-IMP.Hoare_Total_EX ...
Processing theory HOL-IMP.ACom ...
Processing theory HOL-IMP.Sec_Type_Expr ...
Processing theory HOL-IMP.Hoare_Total_EX2 ...
Processing theory HOL-IMP.Sec_Typing ...
Processing theory HOL-IMP.VCG_Total_EX ...
Processing theory HOL-IMP.VCG ...
Processing theory HOL-IMP.Sem_Equiv ...
Processing theory HOL-IMP.Sec_TypingT ...
Processing theory HOL-IMP.Vars ...
Processing theory HOL-IMP.Fold ...
Processing theory HOL-IMP.Live ...
Processing theory HOL-IMP.Complete_Lattice ...
Processing theory HOL-IMP.VCG_Total_EX2 ...
Processing theory HOL-IMP.Collecting ...
Processing theory HOL-IMP.Collecting1 ...
Processing theory HOL-Data_Structures.Tree23_Set ...
Processing theory HOL-IMP.Collecting_Examples ...
Processing theory HOL-IMP.Small_Step ...
Processing theory HOL-IMP.Finite_Reachable ...
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 ...
Removing 26 theories ...
Processing theory HOL-IMP.Compiler2 ...
Processing theory HOL-ex.Perm_Fragments ...
Processing theory HOL-Metis_Examples.Abstraction ...
Processing theory HOL-Lattice.Orders ...
Processing theory HOL-Lattice.Bounds ...
Processing theory HOL-Lattice.Lattice ...
Processing theory HOL-Lattice.CompleteLattice ...
Processing theory HOL-Data_Structures.Tree23_Map ...
Processing theory HOL-Examples.Adhoc_Overloading_Examples ...
Processing theory HOL-Auth.TLS ...
Processing theory HOL-Auth.Auth_Public ...
Processing theory HOL-Corec_Examples.Type_Class ...
Removing 24 theories ...
Processing theory HOL-Datatype_Examples.Koenig ...
Processing theory HOL-Induct.Sexp ...
Processing theory HOL-Induct.SList ...
Processing theory HOL-Datatype_Examples.Process ...
Processing theory HOL-Datatype_Examples.Stream_Processor ...
Processing theory HOL-Codegenerator_Test.Code_Lazy_Test ...
Processing theory HOL-Codegenerator_Test.Code_Test_GHC ...
Processing theory HOL-Codegenerator_Test.Code_Test_OCaml ...
Processing theory HOL-Codegenerator_Test.Code_Test_PolyML ...
Processing theory HOL-Corec_Examples.Stream_Processor ...
Processing theory HOL-Codegenerator_Test.Code_Test_Scala ...
Processing theory HOL-Quotient_Examples.Quotient_Rat ...
Processing theory HOL-Metis_Examples.Big_O ...
Processing theory HOL-Library.Prefix_Order ...
Processing theory HOL-Data_Structures.AVL_Bal2_Set ...
Removing 25 theories ...
Processing theory HOL-Data_Structures.AA_Set ...
Processing theory HOL-IMP.Abs_Int_init ...
Processing theory HOL-Data_Structures.Interval_Tree ...
Processing theory HOL-Data_Structures.AVL_Bal_Set ...
Processing theory HOL-IMP.Abs_Int0 ...
Processing theory HOL-IMP.Abs_State ...
Processing theory HOL-IMP.Abs_Int1 ...
Processing theory HOL-Data_Structures.AA_Map ...
Processing theory HOL-IMP.Abs_Int1_const ...
Processing theory HOL-IMP.Abs_Int1_parity ...
Processing theory HOL-IMP.Abs_Int2 ...
Processing theory HOL-ex.While_Combinator_Example ...
Processing theory HOL-IMP.Live_True ...
Processing theory HOL-Metis_Examples.Tarski ...
Processing theory HOL-NanoJava.Term ...
Processing theory HOL-NanoJava.Decl ...
Processing theory HOL-NanoJava.TypeRel ...
Processing theory HOL-NanoJava.State ...
Removing 10 theories ...
Processing theory HOL-NanoJava.AxSem ...
Processing theory HOL-NanoJava.OpSem ...
Processing theory HOL-NanoJava.Equivalence ...
Processing theory HOL-NanoJava.Example ...
Processing theory HOL-Statespace.DistinctTreeProver ...
Processing theory HOL-Statespace.StateFun ...
Processing theory HOL-Statespace.StateSpaceLocale ...
Processing theory HOL-Statespace.StateSpaceSyntax ...
Processing theory HOL-Data_Structures.Height_Balanced_Tree ...
Processing theory HOL-TLA.Intensional ...
Processing theory HOL-TLA.Stfun ...
Processing theory HOL-TLA.Action ...
Processing theory HOL-TLA.Init ...
Processing theory HOL-TLA-Memory.RPCMemoryParams ...
Processing theory HOL-TLA-Memory.MemoryParameters ...
Processing theory HOL-TLA.TLA ...
Processing theory HOL-TLA-Buffer.Buffer ...
Processing theory HOL-TLA-Buffer.DBuffer ...
Processing theory HOL-TLA-Memory.ProcedureInterface ...
Processing theory HOL-TLA-Inc.Inc ...
Processing theory HOL-TLA-Memory.RPCParameters ...
Processing theory HOL-TLA-Memory.MemClerkParameters ...
Processing theory HOL-TLA-Memory.Memory ...
Processing theory HOL-TLA-Memory.RPC ...
Processing theory HOL-Data_Structures.Tree234_Set ...
Processing theory HOL-TLA-Memory.MemClerk ...
Processing theory HOL-UNITY.Token ...
Processing theory HOL-IMP.Abs_Int2_ivl ...
Processing theory HOL-Unix.Nested_Environment ...
Processing theory HOL-Statespace.StateSpaceEx ...
Removing 22 theories ...
Processing theory HOL-ex.Birthday_Paradox ...
Processing theory HOL-ex.Execute_Choice ...
Processing theory HOL-ex.Residue_Ring ...
Processing theory Haskell.Haskell ...
Processing theory HOL-TLA-Memory.MemoryImplementation ...
Processing theory HOL-Unix.Unix ...
Processing theory Haskell.Test ...
Processing theory HOL-ex.Tarski ...
Processing theory HOL-IMP.Abs_Int3 ...
Removing 44 theories ...
Processing theory HOL-Data_Structures.Tree234_Map ...
Loading 185 theories ...
Processing theory Classes.Setup ...
Processing theory Classes.Classes ...
Processing theory Eisbach.Base ...
Processing theory Eisbach.Manual ...
Processing theory Eisbach.Preface ...
Processing theory Implementation.Base ...
Processing theory Implementation.Eq ...
Processing theory Implementation.Integration ...
Processing theory Implementation.Isar ...
Processing theory Implementation.Local_Theory ...
Processing theory Implementation.Logic ...
Processing theory Implementation.ML ...
Processing theory Implementation.Prelim ...
Processing theory Implementation.Proof ...
Processing theory Implementation.Syntax ...
Processing theory Implementation.Tactic ...
Processing theory JEdit.Base ...
Processing theory JEdit.JEdit ...
Processing theory Prog_Prove.LaTeXsugar ...
Processing theory Prog_Prove.Isar ...
Processing theory Tutorial.TPrimes ...
Processing theory Tutorial.Forward ...
Processing theory Tutorial.Even ...
Processing theory Prog_Prove.Logic ...
Processing theory Tutorial.PDL ...
Processing theory Tutorial.Tree ...
Processing theory Tutorial.Tree2 ...
Processing theory Tutorial.Overloading ...
Processing theory Tutorial.Axioms ...
Processing theory HOL-Data_Structures.Queue_Spec ...
Processing theory HOL-Data_Structures.Reverse ...
Processing theory HOL-Hoare.Arith2 ...
Processing theory HOL-Data_Structures.Queue_2Lists ...
Processing theory Tutorial.Advanced ...
Processing theory HOL-Hoare.Heap ...
Processing theory HOL-Data_Structures.Tree23_of_List ...
Processing theory Tutorial.ABexpr ...
Removing 43 theories ...
Processing theory HOL-Hoare.SepLogHeap ...
Processing theory HOL-IMP.Def_Init ...
Processing theory HOL-IMP.Denotational ...
Processing theory HOL-IMP.Def_Init_Exp ...
Processing theory HOL-IMP.ASM ...
Processing theory HOL-Hoare.Hoare_Syntax ...
Processing theory Tutorial.Nested ...
Processing theory HOL-Data_Structures.Tries_Binary ...
Processing theory HOL-IMP.Def_Init_Big ...
Processing theory HOL-Hoare.Hoare_Logic ...
Processing theory HOL-Hoare.Examples ...
Processing theory HOL-Hoare.ExamplesTC ...
Processing theory HOL-Hoare.HeapSyntax ...
Processing theory HOL-Hoare.Pointers0 ...
Processing theory HOL-Hoare.Hoare_Logic_Abort ...
Processing theory HOL-Hoare.ExamplesAbort ...
Processing theory HOL-Hoare.HeapSyntaxAbort ...
Processing theory HOL-Hoare.Pointer_ExamplesAbort ...
Processing theory HOL-Hoare.Separation ...
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 ...
Processing theory HOL-IMP.Def_Init_Small ...
Processing theory HOL-IOA.Asig ...
Processing theory HOL-IOA.IOA ...
Processing theory HOL-IOA.Solve ...
Processing theory HOL-Import.Import_Setup ...
Processing theory HOL-Import.HOL_Light_Maps ...
Processing theory HOL-Induct.Sigma_Algebra ...
Processing theory HOL-Induct.Term ...
Processing theory HOL-Isar_Examples.Basic_Logic ...
Processing theory HOL-Isar_Examples.Group_Context ...
Processing theory HOL-Isar_Examples.Group_Notepad ...
Processing theory HOL-Hoare.SchorrWaite ...
Processing theory HOL-Isar_Examples.Group ...
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-Isar_Examples.Expr_Compiler ...
Processing theory HOL-Corec_Examples.LFilter ...
Removing 51 theories ...
Processing theory HOL-Hoare.Pointer_Examples ...
Processing theory HOL-Corec_Examples.Merge_A ...
Processing theory HOL-Examples.Functions ...
Processing theory HOL-Corec_Examples.Iterate_GPV ...
Processing theory HOL-Corec_Examples.GPV_Bare_Bones ...
Processing theory HOL-Corec_Examples.Merge_B ...
Processing theory HOL-Corec_Examples.Merge_C ...
Processing theory HOL-Corec_Examples.Merge_D ...
Removing 16 theories ...
Processing theory HOL-Corec_Examples.Simple_Nesting ...
Processing theory HOL-Corec_Examples.Merge_Poly ...
Removing 2 theories ...
Processing theory HOL-Corec_Examples.Stream_Friends ...
Processing theory HOL-ex.Simps_Case_Conv_Examples ...
Processing theory HOL-Library.Code_Prolog ...
Processing theory HOL-ex.Conditional_Parametricity_Examples ...
Processing theory HOL-Datatype_Examples.Cyclic_List ...
Processing theory HOL-Datatype_Examples.FAE_Sequence ...
Processing theory HOL-Datatype_Examples.Free_Idempotent_Monoid ...
Processing theory HOL-Library.Datatype_Records ...
Processing theory HOL-Datatype_Examples.Regex_ACI ...
Processing theory HOL-Corec_Examples.TLList_Friends ...
Processing theory HOL-Corec_Examples.Small_Concrete ...
Processing theory HOL-Library.List_Lenlexorder ...
Processing theory HOL-Library.Predicate_Compile_Alternative_Defs ...
Processing theory HOL-Library.Predicate_Compile_Quickcheck ...
Processing theory HOL-ex.Datatype_Record_Examples ...
Removing 16 theories ...
Processing theory HOL-ex.IArray_Examples ...
Processing theory HOL-Predicate_Compile_Examples.IMP_1 ...
Processing theory HOL-Predicate_Compile_Examples.IMP_2 ...
Processing theory HOL-Predicate_Compile_Examples.IMP_3 ...
Processing theory HOL-Datatype_Examples.Regex_ACIDZ ...
Processing theory HOL-Predicate_Compile_Examples.IMP_4 ...
Removing 13 theories ...
Processing theory HOL-Corec_Examples.Misc_Mono ...
Processing theory HOL-Examples.Rewrite_Examples ...
Processing theory HOL-Quotient_Examples.DList ...
Processing theory HOL-Quotient_Examples.Quotient_Int ...
Processing theory HOL-ex.Transitive_Closure_Table_Ex ...
Processing theory HOL-Metis_Examples.Binary_Tree ...
Processing theory HOL-Predicate_Compile_Examples.Predicate_Compile_Quickcheck_Examples ...
Processing theory HOL-Metis_Examples.Sets ...
Processing theory HOL-Metis_Examples.Type_Encodings ...
Processing theory HOL-Metis_Examples.Trans_Closure ...
Processing theory HOL-Metis_Examples.Message ...
Processing theory HOL-Predicate_Compile_Examples.Predicate_Compile_Tests ...
Removing 18 theories ...
Processing theory HOL-Corec_Examples.Misc_Poly ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Interfaces ...
Processing theory HOL-Quickcheck_Examples.Completeness ...
Processing theory HOL-ex.Refute_Examples ...
Processing theory HOL-Predicate_Compile_Examples.Specialisation_Examples ...
Processing theory HOL-Predicate_Compile_Examples.Examples ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples ...
Processing theory HOL-Metis_Examples.Proxies ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Nesting ...
Processing theory HOL-Quotient_Examples.Lift_DList ...
Processing theory HOL-Quotient_Examples.Lift_FSet ...
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-TPTP.MaSh_Export_Base ...
Processing theory HOL-TPTP.MaSh_Eval ...
Processing theory HOL-Types_To_Sets.Finite ...
Processing theory HOL-UNITY.Deadlock ...
Processing theory HOL-ex.Antiquote ...
Processing theory HOL-ex.Arith_Examples ...
Processing theory HOL-ex.CTL ...
Processing theory HOL-ex.Cartouche_Examples ...
Processing theory HOL-ex.Case_Product ...
Processing theory HOL-UNITY.Network ...
Processing theory HOL-Quotient_Examples.Quotient_Message ...
Processing theory HOL-Quickcheck_Examples.Hotel_Example ...
Processing theory HOL-ex.Classical ...
Processing theory HOL-ex.Coercion_Examples ...
Processing theory HOL-ex.Computations ...
Processing theory HOL-ex.Erdoes_Szekeres ...
Processing theory HOL-ex.Executable_Relation ...
Processing theory HOL-ex.Chinese ...
Removing 41 theories ...
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.Hebrew ...
Processing theory HOL-Quotient_Examples.Lifting_Code_Dt_Test ...
Processing theory HOL-ex.Multiquote ...
Processing theory HOL-ex.NatSum ...
Processing theory HOL-ex.MonoidGroup ...
Processing theory HOL-ex.PER ...
Processing theory HOL-ex.Peano_Axioms ...
Processing theory HOL-ex.LocaleTest2 ...
Processing theory HOL-SMT_Examples.Boogie ...
Processing theory HOL-ex.SAT_Examples ...
Processing theory HOL-ex.Primrec ...
Removing 16 theories ...
Processing theory HOL-Quickcheck_Examples.Quickcheck_Narrowing_Examples ...
Processing theory HOL-ex.Serbian ...
Processing theory HOL-ex.Set_Comprehension_Pointfree_Examples ...
Processing theory HOL-ex.Set_Theory ...
Processing theory HOL-ex.Sketch_and_Explore ...
Processing theory HOL-ex.Simproc_Tests ...
Removing 6 theories ...
Processing theory HOL-ex.ThreeDivides ...
Processing theory HOL-ex.Transfer_Int_Nat ...
Processing theory HOL-ex.veriT_Preprocessing ...
Processing theory HOL-ex.Sudoku ...
Processing theory HOL-ex.Unification ...
Removing 6 theories ...
Processing theory HOL-ex.Tree23 ...
Processing theory HOL-ex.PresburgerEx ...
Removing 2 theories ...
Processing theory HOL-ex.Meson_Test ...
Loading 84 theories ...
Processing theory Isar_Ref.Document_Preparation ...
Processing theory Isar_Ref.Framework ...
Processing theory Isar_Ref.Inner_Syntax ...
Processing theory Isar_Ref.Outer_Syntax ...
Processing theory Isar_Ref.Preface ...
Processing theory Isar_Ref.Generic ...
Processing theory Isar_Ref.Proof ...
Processing theory Isar_Ref.Proof_Script ...
Processing theory Isar_Ref.Quick_Reference ...
Processing theory Isar_Ref.Spec ...
Processing theory Isar_Ref.Symbols ...
Processing theory Main.Main_Doc ...
Processing theory Prog_Prove.Basics ...
Processing theory Tutorial.simp2 ...
Processing theory Isar_Ref.Synopsis ...
Processing theory Prog_Prove.MyList ...
Processing theory Tutorial.Fundata ...
Processing theory Tutorial.CodeGen ...
Processing theory Tutorial.fun0 ...
Processing theory Tutorial.Mutual ...
Processing theory Tutorial.Star ...
Processing theory Tutorial.Documents ...
Processing theory Tutorial.AdvancedInd ...
Processing theory Functions.Functions ...
Processing theory Prog_Prove.Types_and_funs ...
Processing theory Tutorial.Ifexpr ...
Processing theory Tutorial.Itrev ...
Processing theory Tutorial.Option2 ...
Processing theory Tutorial.Plus ...
Processing theory Tutorial.appendix ...
Processing theory Tutorial.case_exprs ...
Processing theory Tutorial.fakenat ...
Processing theory Tutorial.natsum ...
Processing theory Tutorial.pairs2 ...
Processing theory Tutorial.prime_def ...
Processing theory Tutorial.simp ...
Processing theory Tutorial.types ...
Processing theory Tutorial.Basic ...
Processing theory Tutorial.Blast ...
Processing theory Tutorial.Force ...
Processing theory Tutorial.Tacticals ...
Processing theory Tutorial.find2 ...
Processing theory Tutorial.Functions ...
Processing theory Tutorial.Recur ...
Processing theory Tutorial.Relations ...
Processing theory Tutorial.ToyList_Test ...
Processing theory Tutorial.Pairs ...
Processing theory Tutorial.unfoldnested ...
Processing theory Tutorial.ToyList ...
Removing 50 theories ...
Processing theory Tutorial.AB ...
Processing theory Tutorial.Typedefs ...
Processing theory Tutorial.Records ...
Processing theory HOL-Eisbach.Examples ...
Processing theory HOL-Eisbach.Tests ...
Processing theory HOL-Examples.Ackermann ...
Processing theory Tutorial.Trie ...
Processing theory HOL-Examples.Cantor ...
Processing theory HOL-Examples.Commands ...
Processing theory HOL-Examples.Groebner_Examples ...
Processing theory HOL-Examples.Iff_Oracle ...
Processing theory HOL-Examples.Induction_Schema ...
Processing theory HOL-Examples.Knaster_Tarski ...
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.ML ...
Processing theory HOL-Examples.Peirce ...
Processing theory HOL-Examples.Seq ...
Processing theory HOL-IMP.C_like ...
Processing theory HOL-Examples.Coherent ...
Processing theory HOL-Induct.Comb ...
Processing theory HOL-Induct.Common_Patterns ...
Processing theory HOL-Induct.Com ...
Processing theory HOL-Induct.Infinitely_Branching_Tree ...
Processing theory HOL-Induct.Ordinals ...
Processing theory HOL-Induct.Nested_Datatype ...
Processing theory HOL-Induct.PropLog ...
Processing theory HOL-Induct.ABexp ...
Processing theory HOL-Datatype_Examples.Lift_BNF ...
Processing theory HOL-Datatype_Examples.Compat ...
Processing theory HOL-Induct.QuoDataType ...
Processing theory HOL-Induct.QuoNestedDataType ...
Processing theory HOL-IMP.OO ...
Loading 234 theories ...
Removing 131 theories ...
Processing theory System.Base ...
Processing theory System.Misc ...
Processing theory System.Phabricator ...
Processing theory System.Presentation ...
Processing theory System.Server ...
Processing theory CTT.CTT ...
Processing theory CTT.Elimination ...
Processing theory CTT.Equality ...
Processing theory CTT.Synthesis ...
Processing theory CTT.Typechecking ...
Processing theory Cube.Cube ...
Processing theory Cube.Example ...
Processing theory Isar_Ref.First_Order_Logic ...
Processing theory System.Environment ...
Processing theory IFOL ...
Processing theory Logics_ZF.IFOL_examples ...
Processing theory FOL-ex.Foundation ...
Processing theory System.Scala ...
Processing theory System.Sessions ...
Processing theory FOL ...
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 Logics_ZF.FOL_examples ...
Processing theory FOL-ex.Classical ...
Processing theory FOL-ex.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.Quantifiers_Cla ...
Processing theory CCL.Wfd ...
Processing theory CCL.Nat ...
Processing theory CCL.List ...
Processing theory CCL.Flag ...
Processing theory CCL.Stream ...
Processing theory FOL-ex.Propositional_Cla ...
Processing theory Logics_ZF.If ...
Processing theory LCF.LCF ...
Processing theory LCF.Ex1 ...
Processing theory LCF.Ex2 ...
Processing theory LCF.Ex3 ...
Processing theory LCF.Ex4 ...
Processing theory ZF.ZF_Base ...
Processing theory ZF.upair ...
Processing theory ZF.pair ...
Processing theory ZF.Bool ...
Processing theory ZF.equalities ...
Processing theory ZF.Fixedpt ...
Processing theory ZF.Sum ...
Processing theory ZF.func ...
Processing theory ZF.Perm ...
Processing theory ZF.Trancl ...
Processing theory ZF.EquivClass ...
Processing theory ZF.WF ...
Processing theory ZF.Ordinal ...
Processing theory ZF.QPair ...
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.Classical ...
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.Intuitionistic ...
Processing theory FOLP-ex.Propositional_Int ...
Processing theory FOLP-ex.Quantifiers_Int ...
Processing theory HOL-Eisbach.Eisbach_Old_Appl_Syntax ...
Processing theory HOL-Eisbach.Examples_FOL ...
Processing theory Pure-Examples.First_Order_Logic ...
Processing theory Pure-Examples.Higher_Order_Logic ...
Processing theory Pure-ex.Alternative_Headings ...
Processing theory Pure-ex.Alternative_Headings_Examples ...
Processing theory Pure-ex.Def ...
Processing theory Pure-ex.Def_Examples ...
Processing theory Pure-ex.Guess ...
Processing theory Pure-ex.Guess_Examples ...
Processing theory Sequents.Sequents ...
Processing theory Sequents.ILL ...
Processing theory HOL-Prolog.HOHH ...
Processing theory FOL-ex.Locale_Test1 ...
Processing theory FOL-ex.Locale_Test2 ...
Processing theory FOL-ex.Locale_Test3 ...
Processing theory FOL-ex.Locale_Test ...
Processing theory FOLP-ex.Nat ...
Processing theory Sequents.Washing ...
Processing theory Sequents.LK0 ...
Processing theory Sequents.LK ...
Processing theory HOL-Prolog.Func ...
Processing theory ZF.Order ...
Processing theory ZF.OrdQuant ...
Processing theory ZF.Nat ...
Processing theory ZF.Epsilon ...
Processing theory ZF.OrderArith ...
Processing theory ZF.Inductive ...
Processing theory ZF.Finite ...
Processing theory ZF.OrderType ...
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 ZF.Cardinal ...
Processing theory ZF.Univ ...
Processing theory ZF.Arith ...
Processing theory ZF.ArithSimp ...
Processing theory ZF.QUniv ...
Processing theory ZF.Datatype ...
Processing theory Sequents.S43 ...
Processing theory Sequents.T ...
Processing theory HOL-Prolog.Type ...
Processing theory SML.Examples ...
Processing theory ZF.Int ...
Processing theory ZF.CardinalArith ...
Processing theory ZF.Bin ...
Processing theory HOL-Prolog.Test ...
Removing 101 theories ...
Processing theory ZF.IntDiv ...
Processing theory ZF.List ...
Processing theory ZF ...
Processing theory Logics_ZF.ZF_Isar ...
Processing theory ZF.AC ...
Processing theory ZF.Zorn ...
Processing theory ZF.Cardinal_AC ...
Processing theory ZF.InfDatatype ...
Processing theory ZF-AC.AC_Equiv ...
Processing theory ZF-AC.AC18_AC19 ...
Processing theory ZF-AC.AC7_AC9 ...
Processing theory ZF-AC.Cardinal_aux ...
Processing theory ZF-AC.WO6_WO1 ...
Processing theory ZF-AC.Hartog ...
Processing theory ZF-AC.AC16_lemmas ...
Processing theory ZF-AC.AC16_WO4 ...
Processing theory ZF-AC.DC ...
Processing theory ZF-AC.HH ...
Processing theory ZF-AC.AC15_WO6 ...
Processing theory ZF-AC.AC17_AC1 ...
Processing theory ZF-AC.WO1_AC ...
Processing theory ZF-AC.WO1_WO7 ...
Processing theory ZF-AC.WO2_AC16 ...
Processing theory ZF-Coind.Language ...
Processing theory ZF-Coind.Types ...
Processing theory ZF-Coind.Map ...
Processing theory ZF-Coind.Values ...
Processing theory ZF-Coind.Dynamic ...
Processing theory ZF-Coind.Static ...
Processing theory ZF-Coind.ECR ...
Processing theory ZF-Constructible.MetaExists ...
Processing theory ZF-Constructible.Normal ...
Processing theory ZF-Induct.Acc ...
Processing theory ZF-Constructible.Reflection ...
Processing theory ZF-Induct.Binary_Trees ...
Processing theory ZF-Induct.Comb ...
Processing theory ZF-Induct.FoldSet ...
Processing theory ZF-Induct.ListN ...
Processing theory ZF-Induct.Mutil ...
Processing theory ZF-Induct.Ntree ...
Processing theory ZF-Constructible.Formula ...
Processing theory ZF-Induct.Primrec ...
Processing theory ZF-Induct.Rmap ...
Processing theory ZF-IMP.Com ...
Processing theory ZF-IMP.Denotation ...
Processing theory ZF-IMP.Equiv ...
Processing theory ZF-Induct.PropLog ...
Processing theory ZF-Induct.Term ...
Processing theory ZF-Induct.Tree_Forest ...
Processing theory ZF-Resid.Redex ...
Processing theory ZF-Resid.Substitution ...
Processing theory ZF-Resid.Residuals ...
Processing theory ZF-Resid.Reduction ...
Processing theory ZF-UNITY.GenPrefix ...
Processing theory ZF-UNITY.State ...
Processing theory ZF-Constructible.Relative ...
Processing theory ZF-Induct.Datatypes ...
Processing theory ZF-Constructible.Wellorderings ...
Processing theory ZF-Constructible.WFrec ...
Processing theory ZF-Constructible.WF_absolute ...
Processing theory ZF-Resid.Confluence ...
Processing theory ZF-Constructible.L_axioms ...
Processing theory ZF-Constructible.Rank ...
Processing theory ZF-Constructible.Separation ...
Processing theory ZF-Constructible.AC_in_L ...
Processing theory ZF-UNITY.UNITY ...
Processing theory ZF-UNITY.Constrains ...
Processing theory ZF-UNITY.FP ...
Processing theory ZFC ...
Processing theory ZF-Induct.Brouwer ...
Processing theory ZF-Induct.Multiset ...
Processing theory ZF-UNITY.MultisetSum ...
Processing theory ZF-UNITY.Monotonicity ...
Processing theory ZF-UNITY.Increasing ...
Processing theory ZF-ex.BinEx ...
Processing theory ZF-ex.CoUnit ...
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-ex.Commutation ...
Processing theory Logics_ZF.ZF_examples ...
Processing theory ZF-UNITY.WFair ...
Processing theory ZF-UNITY.SubstAx ...
Processing theory ZF-UNITY.Follows ...
Processing theory ZF-UNITY.Mutex ...
Processing theory ZF-UNITY.Union ...
Processing theory ZF-ex.LList ...
Processing theory ZF-UNITY.Comp ...
Processing theory ZF-UNITY.Guar ...
Processing theory ZF-UNITY.AllocBase ...
Processing theory ZF-UNITY.ClientImpl ...
Processing theory ZF-UNITY.Distributor ...
Processing theory ZF-UNITY.Merge ...
Processing theory ZF-UNITY.AllocImpl ...
Processing theory ZF-ex.NatSum ...
Processing theory ZF-ex.Primes ...
Processing theory ZF-ex.Ramsey ...
Processing theory ZF-ex.misc ...
Processing theory ZF-Constructible.Satisfies_absolute ...
Processing theory ZF-Constructible.DPow_absolute ...
Processing theory ZF-ex.Group ...
Processing theory ZF-ex.Ring ...
Processing theory ZF-ex.Limit ...
Starting session Pure ...
Loading 361 theories ...
Processing theory Landau_Symbols.Group_Sort ...
Processing theory Bernoulli.Bernoulli ...
Processing theory Sturm_Tarski.PolyMisc ...
Processing theory Landau_Symbols.Landau_Real_Products ...
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 Bernoulli.Bernoulli_FPS ...
Processing theory Dirichlet_Series.Multiplicative_Function ...
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 Zeta_Function.Zeta_Library ...
Processing theory Dirichlet_Series.Arithmetic_Summatory_Asymptotics ...
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.Partial_Zeta_Bounds ...
Processing theory Prime_Distribution_Elementary.Primorial ...
Processing theory Prime_Number_Theorem.Prime_Number_Theorem ...
Processing theory Prime_Distribution_Elementary.Elementary_Prime_Bounds ...
Processing theory Prime_Number_Theorem.Mertens_Theorems ...
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 55 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 ...
Removing 9 theories ...
Processing theory Winding_Number_Eval.Winding_Number_Eval_Examples ...
Loading 13 theories ...
Processing theory Quasi_Borel_Spaces.StandardBorel ...
Processing theory Quasi_Borel_Spaces.QuasiBorel ...
Processing theory Quasi_Borel_Spaces.Measure_QuasiBorel_Adjunction ...
Processing theory Quasi_Borel_Spaces.Binary_CoProduct_QuasiBorel ...
Processing theory Quasi_Borel_Spaces.Binary_Product_QuasiBorel ...
Processing theory Quasi_Borel_Spaces.Product_QuasiBorel ...
Removing 7 theories ...
Processing theory Quasi_Borel_Spaces.CoProduct_QuasiBorel ...
Processing theory Quasi_Borel_Spaces.Exponent_QuasiBorel ...
Processing theory Quasi_Borel_Spaces.Probability_Space_QuasiBorel ...
Processing theory Quasi_Borel_Spaces.Monad_QuasiBorel ...
Processing theory Quasi_Borel_Spaces.Pair_QuasiBorel_Measure ...
Processing theory Quasi_Borel_Spaces.Measure_as_QuasiBorel_Measure ...
Processing theory Quasi_Borel_Spaces.Bayesian_Linear_Regression ...
Loading 22 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 ...
Removing 13 theories ...
Processing theory MFMC_Countable.MFMC_Reduction ...
Processing theory MFMC_Countable.MFMC_Flow_Attainability ...
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.Prob_Theory ...
Processing theory List_Update.On_Off ...
Processing theory List_Update.Competitive_Analysis ...
Processing theory List_Update.Swaps ...
Processing theory List_Update.Bit_Strings ...
Processing theory Regular-Sets.Regular_Exp ...
Processing theory Regular-Sets.NDerivative ...
Processing theory Regular-Sets.Equivalence_Checking ...
Processing theory List_Update.RExp_Var ...
Removing 3 theories ...
Processing theory List_Update.Move_to_Front ...
Processing theory List_Update.Partial_Cost_Model ...
Processing theory List_Update.OPT2 ...
Processing theory List_Update.MTF2_Effects ...
Processing theory List_Update.Phase_Partitioning ...
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 ...
Removing 18 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 ...
Processing theory Lp.Lp ...
Processing theory Fourier.Lspace ...
Processing theory Fourier.Square_Integrable ...
Processing theory Fourier.Fourier ...
Loading 9 theories ...
Processing theory Density_Compiler.Density_Predicates ...
Removing 8 theories ...
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 Regular-Sets.Relation_Interpretation ...
Processing theory VectorSpace.FunctionLemmas ...
Processing theory VectorSpace.RingModuleFacts ...
Processing theory VectorSpace.MonoidSums ...
Processing theory Jordan_Normal_Form.Missing_Misc ...
Processing theory Regular-Sets.Regexp_Method ...
Processing theory Matrix.Utility ...
Processing theory Abstract-Rewriting.Seq ...
Processing theory Polynomial_Interpolation.Missing_Unsorted ...
Processing theory Jordan_Normal_Form.Missing_Ring ...
Processing theory Abstract-Rewriting.Abstract_Rewriting ...
Processing theory Polynomial_Interpolation.Missing_Polynomial ...
Processing theory Polynomial_Factorization.Order_Polynomial ...
Processing theory Polynomial_Interpolation.Ring_Hom ...
Processing theory Jordan_Normal_Form.Conjugate ...
Processing theory Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized ...
Processing theory VectorSpace.LinearCombinations ...
Processing theory Abstract-Rewriting.SN_Orders ...
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 VectorSpace.VectorSpace ...
Processing theory Jordan_Normal_Form.Gauss_Jordan_Elimination ...
Processing theory Jordan_Normal_Form.Missing_VectorSpace ...
Processing theory Jordan_Normal_Form.Column_Operations ...
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 19 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.Hausdorff_Distance ...
Processing theory Gromov_Hyperbolicity.Eexp_Eln ...
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 ...
Loading 12 theories ...
Processing theory Gromov_Hyperbolicity.Isometries_Classification ...
Processing theory Girth_Chromatic.Girth_Chromatic_Misc ...
Processing theory Girth_Chromatic.Ugraphs ...
Processing theory Random_Graph_Subgraph_Threshold.Ugraph_Misc ...
Processing theory Ergodic_Theory.Asymptotic_Density ...
Processing theory Szemeredi_Regularity.Szemeredi ...
Processing theory Girth_Chromatic.Girth_Chromatic ...
Processing theory Random_Graph_Subgraph_Threshold.Prob_Lemmas ...
Processing theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas ...
Processing theory Random_Graph_Subgraph_Threshold.Ugraph_Properties ...
Processing theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold ...
Removing 6 theories ...
Processing theory Roth_Arithmetic_Progressions.Roth_Arithmetic_Progressions ...
Loading 15 theories ...
Processing theory Comparison_Sort_Lower_Bound.Linorder_Relations ...
Processing theory Treaps.Probability_Misc ...
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 ...
Removing 12 theories ...
Processing theory Treaps.Treap_Sort_and_BSTs ...
Processing theory Treaps.Random_Treap ...
Loading 7 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 ...
Removing 9 theories ...
Processing theory Neumann_Morgenstern_Utility.Neumann_Morgenstern_Utility_Theorem ...
Processing theory Neumann_Morgenstern_Utility.Expected_Utility ...
Processing theory MFMC_Countable.Rel_PMF_Characterisation ...
Processing theory Gromov_Hyperbolicity.Bonk_Schramm_Extension ...
Loading 5 theories ...
Removing 22 theories ...
Processing theory Monad_Normalisation.Monad_Normalisation ...
Processing theory Skip_Lists.Misc ...
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 ...
Removing 1 theories ...
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 ...
Loading 3 theories ...
Processing theory Hahn_Jordan_Decomposition.Extended_Reals_Sums_Compl ...
Processing theory Hahn_Jordan_Decomposition.Hahn_Jordan_Prelims ...
Removing 8 theories ...
Processing theory Hahn_Jordan_Decomposition.Hahn_Jordan_Decomposition ...
Processing theory Fisher_Yates.Fisher_Yates ...
Removing 4 theories ...
Processing theory Buffons_Needle.Buffons_Needle ...
Loading 7 theories ...
Processing theory Green.General_Utils ...
Processing theory Green.Derivs ...
Processing theory Green.Integrals ...
Removing 23 theories ...
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 ...
Processing theory Median_Method.Median ...
Loading 17 theories ...
Processing theory Affine_Arithmetic.Affine_Arithmetic_Auxiliarities ...
Processing theory Ordinary_Differential_Equations.Vector_Derivative_On ...
Processing theory Ordinary_Differential_Equations.Gronwall ...
Removing 18 theories ...
Processing theory Ordinary_Differential_Equations.Interval_Integral_HK ...
Processing theory Affine_Arithmetic.Executable_Euclidean_Space ...
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 Hybrid_Systems_VCs.HS_VC_Spartan ...
Loading 27 theories ...
Processing theory Matrices_for_ODEs.MTX_Flows ...
Processing theory Matrices_for_ODEs.MTX_Examples ...
Processing theory Kleene_Algebra.Signatures ...
Removing 5 theories ...
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 Order_Lattice_Props.Order_Lattice_Props ...
Processing theory Order_Lattice_Props.Galois_Connections ...
Processing theory Order_Lattice_Props.Fixpoint_Fusion ...
Processing theory KAT_and_DRA.PHL_KAT ...
Processing theory Hybrid_Systems_VCs.HS_VC_KAT ...
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 ...
Removing 2 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 ...
Processing theory Hybrid_Systems_VCs.HS_VC_PT ...
Processing theory Hybrid_Systems_VCs.HS_VC_PT_Examples ...
Loading 7 theories ...
Removing 10 theories ...
Processing theory KAD.Domain_Semiring ...
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 4 theories ...
Processing theory Laplace_Transform.Uniqueness ...
Processing theory Laplace_Transform.Laplace_Transform ...
Removing 20 theories ...
Processing theory Hyperdual.TwiceFieldDifferentiable ...
Processing theory Hyperdual.Hyperdual ...
Processing theory Hyperdual.HyperdualFunctionExtension ...
Processing theory Hyperdual.LogisticFunction ...
Processing theory Hyperdual.AnalyticTestFunction ...
Loading 2 theories ...
Processing theory Actuarial_Mathematics.Preliminaries ...
Processing theory Actuarial_Mathematics.Interest ...
Removing 7 theories ...
Processing theory Youngs_Inequality.Youngs ...
Loading 3 theories ...
Processing theory Prime_Harmonic_Series.Prime_Harmonic_Misc ...
Processing theory Prime_Harmonic_Series.Squarefree_Nat ...
Processing theory Prime_Harmonic_Series.Prime_Harmonic ...
Removing 4 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 48 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 ...
Processing theory UpDown_Scheme.Grid ...
Processing theory UpDown_Scheme.UpDown_Scheme ...
Removing 12 theories ...
Processing theory UpDown_Scheme.Triangular_Function ...
Processing theory UpDown_Scheme.Down ...
Processing theory UpDown_Scheme.Up ...
Processing theory UpDown_Scheme.Up_Down ...
Processing theory Minkowskis_Theorem.Minkowskis_Theorem ...
Loading 27 theories ...
Processing theory Deep_Learning.DL_Missing_Finite_Set ...
Processing theory Deep_Learning.DL_Concrete_Matrices ...
Processing theory Deep_Learning.DL_Flatten_Matrix ...
Processing theory Jordan_Normal_Form.DL_Missing_List ...
Processing theory Deep_Learning.Tensor ...
Processing theory Polynomials.MPoly_Type ...
Removing 15 theories ...
Processing theory Deep_Learning.Tensor_Subtensor ...
Processing theory Polynomials.More_MPoly_Type ...
Processing theory Deep_Learning.Tensor_Plus ...
Processing theory Deep_Learning.Tensor_Scalar_Mult ...
Processing theory Jordan_Normal_Form.DL_Missing_Sublist ...
Processing theory Polynomials.MPoly_Type_Univariate ...
Processing theory Deep_Learning.Tensor_Matricization ...
Processing theory Jordan_Normal_Form.DL_Submatrix ...
Processing theory Deep_Learning.Lebesgue_Functional ...
Processing theory Deep_Learning.Lebesgue_Zero_Set ...
Processing theory Jordan_Normal_Form.DL_Rank ...
Processing theory Deep_Learning.Tensor_Product ...
Processing theory Deep_Learning.Tensor_Unit_Vec ...
Processing theory Deep_Learning.Tensor_Rank ...
Processing theory Jordan_Normal_Form.DL_Rank_Submatrix ...
Processing theory Deep_Learning.DL_Rank_CP_Rank ...
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 ...
Processing theory Deep_Learning.DL_Fundamental_Theorem_Network_Capacity ...
Loading 30 theories ...
Removing 52 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 ...
Processing theory QR_Decomposition.QR_Decomposition_IArrays ...
Processing theory QR_Decomposition.QR_Efficient ...
Loading 16 theories ...
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_Instances ...
Processing theory Show.Show_Real ...
Processing theory Cauchy.CauchysMeanTheorem ...
Processing theory Sqrt_Babylonian.Log_Impl ...
Processing theory Sqrt_Babylonian.NthRoot_Impl ...
Processing theory Sqrt_Babylonian.Sqrt_Babylonian ...
Processing theory Real_Impl.Prime_Product ...
Removing 1 theories ...
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 ...
Removing 6 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 ...
Processing theory QR_Decomposition.Examples_QR_Abstract_Float ...
Loading 18 theories ...
Removing 12 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 ...
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 ...
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.Inverse_IArrays ...
Removing 20 theories ...
Processing theory Gauss_Jordan.Bases_Of_Fundamental_Subspaces_IArrays ...
Processing theory Gauss_Jordan.System_Of_Equations_IArrays ...
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 ...
Removing 29 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 ...
Processing theory Tarskis_Geometry.Projective ...
Processing theory Tarskis_Geometry.Hyperbolic_Tarski ...
Loading 10 theories ...
Removing 8 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 ...
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 45 theories ...
Processing theory Differential_Game_Logic.Differential_Game_Logic ...
Processing theory Well_Quasi_Orders.Infinite_Sequences ...
Processing theory Polynomials.Poly_Mapping_Finite_Map ...
Processing theory Well_Quasi_Orders.Least_Enum ...
Processing theory Open_Induction.Restricted_Predicates ...
Processing theory Well_Quasi_Orders.Minimal_Elements ...
Processing theory Well_Quasi_Orders.Almost_Full ...
Processing theory Well_Quasi_Orders.Minimal_Bad_Sequences ...
Processing theory Polynomials.More_Modules ...
Removing 10 theories ...
Processing theory Well_Quasi_Orders.Almost_Full_Relations ...
Processing theory Polynomials.Utils ...
Processing theory Well_Quasi_Orders.Well_Quasi_Orders ...
Processing theory Polynomials.Power_Products ...
Processing theory Polynomials.MPoly_Type_Class ...
Processing theory Polynomials.Polynomials ...
Processing theory Polynomials.Show_Polynomials ...
Processing theory Polynomials.MPoly_Type_Class_Ordered ...
Processing theory Polynomials.MPoly_Type_Class_FMap ...
Processing theory Virtual_Substitution.MPolyExtension ...
Processing theory Virtual_Substitution.ExecutiblePolyProps ...
Processing theory Virtual_Substitution.PolyAtoms ...
Processing theory Virtual_Substitution.Debruijn ...
Processing theory Virtual_Substitution.Reindex ...
Processing theory Virtual_Substitution.Optimizations ...
Processing theory Virtual_Substitution.PrettyPrinting ...
Processing theory Virtual_Substitution.OptimizationProofs ...
Processing theory Virtual_Substitution.VSAlgos ...
Processing theory Virtual_Substitution.UniAtoms ...
Processing theory Virtual_Substitution.DNF ...
Processing theory Virtual_Substitution.NegInfinity ...
Processing theory Virtual_Substitution.Heuristic ...
Processing theory Virtual_Substitution.LinearCase ...
Processing theory Virtual_Substitution.Exports ...
Processing theory Virtual_Substitution.QE ...
Processing theory Virtual_Substitution.NegInfinityUni ...
Processing theory Virtual_Substitution.QuadraticCase ...
Processing theory Virtual_Substitution.Infinitesimals ...
Processing theory Virtual_Substitution.EliminateVariable ...
Processing theory Virtual_Substitution.LuckyFind ...
Processing theory Virtual_Substitution.EqualityVS ...
Processing theory Virtual_Substitution.InfinitesimalsUni ...
Processing theory Virtual_Substitution.DNFUni ...
Processing theory Virtual_Substitution.GeneralVSProofs ...
Processing theory Virtual_Substitution.VSQuad ...
Processing theory Virtual_Substitution.HeuristicProofs ...
Processing theory Virtual_Substitution.ExportProofs ...
Loading 16 theories ...
Processing theory Separation_Logic_Imperative_HOL.Syntax_Match ...
Processing theory Separation_Logic_Imperative_HOL.Run ...
Processing theory Separation_Logic_Imperative_HOL.Imperative_HOL_Add ...
Processing theory Automatic_Refinement.Misc ...
Processing theory Separation_Logic_Imperative_HOL.Assertions ...
Removing 43 theories ...
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 ...
Processing theory Sturm_Sequences.Sturm_Theorem ...
Processing theory Sturm_Sequences.Sturm_Method ...
Processing theory Sturm_Sequences.Sturm ...
Removing 4 theories ...
Processing theory Safe_Distance.Safe_Distance ...
Processing theory Safe_Distance.Safe_Distance_Reaction ...
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 ...
Removing 10 theories ...
Processing theory First_Welfare_Theorem.Exchange_Economy ...
Processing theory First_Welfare_Theorem.Arrow_Debreu_Model ...
Processing theory QR_Decomposition.Generalizations2 ...
Loading 3 theories ...
Removing 13 theories ...
Processing theory Triangle.Angles ...
Processing theory Triangle.Triangle ...
Processing theory Stewart_Apollonius.Stewart_Apollonius ...
Processing theory Chord_Segments.Chord_Segments ...
Loading 2 theories ...
Processing theory Octonions.Cross_Product_7 ...
Removing 4 theories ...
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 ...
Processing theory Lower_Semicontinuous.Lower_Semicontinuous ...
Removing 3 theories ...
Processing theory Kuratowski_Closure_Complement.KuratowskiClosureComplementTheorem ...
Loading 2 theories ...
Processing theory Banach_Steinhaus.Banach_Steinhaus_Missing ...
Processing theory Banach_Steinhaus.Banach_Steinhaus ...
Loading 8 theories ...
Processing theory Store_Buffer_Reduction.SyntaxTweaks ...
Removing 23 theories ...
Processing theory Store_Buffer_Reduction.ReduceStoreBuffer ...
Processing theory Store_Buffer_Reduction.ReduceStoreBufferSimulation ...
Processing theory Store_Buffer_Reduction.PIMP ...
Loading 65 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 ...
Removing 8 theories ...
Processing theory Deriving.Comparator ...
Processing theory Deriving.Compare ...
Processing theory Deriving.Comparator_Generator ...
Processing theory Deriving.Equality_Generator ...
Processing theory Deriving.Equality_Instances ...
Processing theory Native_Word.Code_Int_Integer_Conversion ...
Processing theory Van_Emde_Boas_Trees.Syntax_Match ...
Processing theory Deriving.Countable_Generator ...
Processing theory Word_Lib.More_Arithmetic ...
Processing theory Deriving.Compare_Generator ...
Processing theory Van_Emde_Boas_Trees.Heap_Time_Monad ...
Processing theory Van_Emde_Boas_Trees.Array_Time ...
Processing theory Van_Emde_Boas_Trees.Ref_Time ...
Processing theory Van_Emde_Boas_Trees.Imperative_HOL_Time ...
Processing theory Deriving.Compare_Instances ...
Processing theory Van_Emde_Boas_Trees.Assertions ...
Processing theory Van_Emde_Boas_Trees.Hoare_Triple ...
Processing theory Van_Emde_Boas_Trees.Refine_Imp_Hol ...
Processing theory Van_Emde_Boas_Trees.Automation ...
Processing theory Van_Emde_Boas_Trees.Sep_Main ...
Processing theory Van_Emde_Boas_Trees.Time_Reasoning ...
Processing theory Van_Emde_Boas_Trees.Simple_TBOUND_Cond ...
Processing theory Van_Emde_Boas_Trees.VEBT_Example_Setup ...
Processing theory Van_Emde_Boas_Trees.VEBT_List_Assn ...
Processing theory Van_Emde_Boas_Trees.VEBT_Definitions ...
Processing theory Word_Lib.Bit_Comprehension ...
Processing theory Word_Lib.More_Divides ...
Processing theory Word_Lib.Signed_Division_Word ...
Processing theory Van_Emde_Boas_Trees.VEBT_Height ...
Processing theory Van_Emde_Boas_Trees.VEBT_Member ...
Processing theory Van_Emde_Boas_Trees.VEBT_Space ...
Processing theory Word_Lib.More_Word ...
Processing theory Word_Lib.Bit_Shifts_Infix_Syntax ...
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 Van_Emde_Boas_Trees.VEBT_MinMax ...
Processing theory Native_Word.Bits_Integer ...
Processing theory Native_Word.Code_Target_Word_Base ...
Processing theory Native_Word.Word_Type_Copies ...
Processing theory Van_Emde_Boas_Trees.VEBT_Insert ...
Processing theory Native_Word.Uint32 ...
Processing theory Collections.HashCode ...
Processing theory Deriving.Hash_Generator ...
Processing theory Deriving.Hash_Instances ...
Processing theory Deriving.Derive ...
Processing theory Van_Emde_Boas_Trees.VEBT_InsertCorrectness ...
Processing theory Van_Emde_Boas_Trees.VEBT_Succ ...
Processing theory Van_Emde_Boas_Trees.VEBT_Pred ...
Processing theory Van_Emde_Boas_Trees.VEBT_Delete ...
Processing theory Van_Emde_Boas_Trees.VEBT_Bounds ...
Processing theory Van_Emde_Boas_Trees.VEBT_DeleteCorrectness ...
Processing theory Van_Emde_Boas_Trees.VEBT_Uniqueness ...
Processing theory Van_Emde_Boas_Trees.VEBT_DeleteBounds ...
Processing theory Van_Emde_Boas_Trees.VEBT_Intf_Functional ...
Processing theory Van_Emde_Boas_Trees.VEBT_BuildupMemImp ...
Processing theory Van_Emde_Boas_Trees.VEBT_SuccPredImperative ...
Processing theory Van_Emde_Boas_Trees.VEBT_DelImperative ...
Loading 39 theories ...
Processing theory Van_Emde_Boas_Trees.VEBT_Intf_Imperative ...
Processing theory Van_Emde_Boas_Trees.VEBT_Example ...
Removing 38 theories ...
Processing theory Psi_Calculi.Chain ...
Processing theory Psi_Calculi.Subst_Term ...
Processing theory Psi_Calculi.Agent ...
Processing theory Psi_Calculi.Close_Subst ...
Processing theory Psi_Calculi.Frame ...
Processing theory Psi_Calculi.Structural_Congruence ...
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.Bisimulation ...
Processing theory Psi_Calculi.Weak_Simulation ...
Processing theory Psi_Calculi.Weak_Cong_Simulation ...
Processing theory Psi_Calculi.Weak_Stat_Imp_Pres ...
Processing theory Psi_Calculi.Sim_Pres ...
Processing theory Psi_Calculi.Bisim_Pres ...
Processing theory Psi_Calculi.Sim_Struct_Cong ...
Processing theory Psi_Calculi.Weak_Sim_Pres ...
Processing theory Psi_Calculi.Bisim_Struct_Cong ...
Processing theory Psi_Calculi.Bisim_Subst ...
Processing theory Psi_Calculi.Weak_Bisimulation ...
Processing theory Psi_Calculi.Weak_Bisim_Pres ...
Processing theory Psi_Calculi.Weak_Psi_Congruence ...
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.Encodings ...
Processing theory Encodability_Process_Calculi.SimulationRelations ...
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.OperationalCorrespondence ...
Processing theory Encodability_Process_Calculi.FullAbstraction ...
Processing theory Encodability_Process_Calculi.CombinedCriteria ...
Loading 19 theories ...
Processing theory Featherweight_OCL.UML_Types ...
Removing 10 theories ...
Processing theory Featherweight_OCL.UML_Logic ...
Processing theory Featherweight_OCL.UML_PropertyProfiles ...
Processing theory Featherweight_OCL.UML_Tools ...
Processing theory Featherweight_OCL.UML_Boolean ...
Processing theory Featherweight_OCL.UML_Void ...
Processing theory Featherweight_OCL.UML_String ...
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 ...
Loading 2 theories ...
Processing theory Featherweight_OCL.Analysis_OCL ...
Removing 2 theories ...
Processing theory Featherweight_OCL.Design_UML ...
Loading 5 theories ...
Processing theory Featherweight_OCL.Design_OCL ...
Removing 19 theories ...
Processing theory Native_Word.Code_Target_Bits_Int ...
Processing theory Pell.Pell ...
Processing theory Mersenne_Primes.Lucas_Lehmer_Auxiliary ...
Processing theory Mersenne_Primes.Lucas_Lehmer ...
Processing theory Mersenne_Primes.Lucas_Lehmer_Code ...
Loading 8 theories ...
Processing theory Polynomial_Factorization.Missing_List ...
Processing theory Polynomial_Factorization.Missing_Multiset ...
Processing theory Gaussian_Integers.Gaussian_Integers ...
Processing theory Gaussian_Integers.Gaussian_Integers_Pythagorean_Triples ...
Processing theory Gaussian_Integers.Gaussian_Integers_Sums_Of_Two_Squares ...
Removing 24 theories ...
Processing theory Polynomial_Factorization.Prime_Factorization ...
Processing theory Gaussian_Integers.Gaussian_Integers_Test ...
Processing theory Gaussian_Integers.Gaussian_Integers_Everything ...
Loading 6 theories ...
Processing theory Budan_Fourier.Budan_Fourier ...
Processing theory Three_Circles.RRI_Misc ...
Processing theory Three_Circles.Bernstein_01 ...
Processing theory Three_Circles.Bernstein ...
Removing 5 theories ...
Processing theory Three_Circles.Normal_Poly ...
Processing theory Three_Circles.Three_Circles ...
Loading 4 theories ...
Processing theory Pell.Efficient_Discrete_Sqrt ...
Processing theory Pell.Pell_Algorithm ...
Removing 5 theories ...
Processing theory Pell.Pell_Algorithm_Test ...
Loading 59 theories ...
Processing theory Interpreter_Optimizations.Op ...
Processing theory VeriComp.Transfer_Extras ...
Processing theory Interpreter_Optimizations.Dynamic ...
Processing theory Interpreter_Optimizations.OpInl ...
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 ...
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 9 theories ...
Processing theory Padic_Ints.Padic_Construction ...
Processing theory Padic_Ints.Extended_Int ...
Processing theory Padic_Ints.Function_Ring ...
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 ...
Processing theory Padic_Ints.Hensels_Lemma ...
Processing theory Budan_Fourier.Descartes_Roots_Test ...
Removing 5 theories ...
Processing theory Mason_Stothers.Mason_Stothers ...
Processing theory Lucas_Theorem.Lucas_Theorem ...
Loading 4 theories ...
Processing theory Lehmer.Lehmer ...
Processing theory Pratt_Certificate.Pratt_Certificate ...
Processing theory Pratt_Certificate.Pratt_Certificate_Code ...
Removing 2 theories ...
Processing theory Amicable_Numbers.Amicable_Numbers ...
Loading 21 theories ...
Processing theory Graph_Theory.Rtrancl_On ...
Processing theory Card_Partitions.Set_Partition ...
Processing theory Graph_Theory.Stuff ...
Processing theory Graph_Theory.Digraph ...
Processing theory Graph_Theory.Arc_Walk ...
Processing theory Graph_Theory.Bidirected_Digraph ...
Processing theory Graph_Theory.Pair_Digraph ...
Processing theory Nested_Multisets_Ordinals.Multiset_More ...
Processing theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset ...
Processing theory Graph_Theory.Digraph_Component ...
Removing 9 theories ...
Processing theory Design_Theory.Multisets_Extras ...
Processing theory Design_Theory.Design_Basics ...
Processing theory Design_Theory.Design_Operations ...
Processing theory Design_Theory.Sub_Designs ...
Processing theory Design_Theory.Design_Isomorphisms ...
Processing theory Design_Theory.Block_Designs ...
Processing theory Design_Theory.Designs_And_Graphs ...
Processing theory Design_Theory.BIBD ...
Processing theory Design_Theory.Resolvable_Designs ...
Processing theory Design_Theory.Group_Divisible_Designs ...
Processing theory Design_Theory.Design_Theory_Root ...
Processing theory Budan_Fourier.Sturm_Multiple_Roots ...
Loading 33 theories ...
Processing theory Containers.Extend_Partial_Order ...
Processing theory Polynomial_Interpolation.Divmod_Int ...
Processing theory Containers.Containers_Auxiliary ...
Processing theory Containers.Containers_Generator ...
Processing theory Polynomial_Interpolation.Improved_Code_Equations ...
Processing theory Polynomial_Factorization.Explicit_Roots ...
Processing theory Show.Show_Poly ...
Processing theory Polynomial_Interpolation.Neville_Aitken_Interpolation ...
Processing theory Polynomial_Factorization.Missing_Polynomial_Factorial ...
Processing theory Polynomial_Factorization.Polynomial_Divisibility ...
Processing theory Polynomial_Interpolation.Lagrange_Interpolation ...
Processing theory Containers.List_Fusion ...
Processing theory Containers.Lexicographic_Order ...
Processing theory Polynomial_Interpolation.Is_Rat_To_Rat ...
Processing theory Polynomial_Factorization.Dvd_Int_Poly ...
Processing theory Polynomial_Factorization.Gauss_Lemma ...
Processing theory Polynomial_Factorization.Gcd_Rat_Poly ...
Processing theory Polynomial_Factorization.Rational_Root_Test ...
Removing 23 theories ...
Processing theory Polynomial_Factorization.Square_Free_Factorization ...
Processing theory Polynomial_Interpolation.Newton_Interpolation ...
Processing theory Polynomial_Interpolation.Polynomial_Interpolation ...
Processing theory Containers.Set_Linorder ...
Processing theory Containers.Collection_Order ...
Processing theory Containers.RBT_ext ...
Processing theory Deriving.RBT_Comparator_Impl ...
Processing theory Containers.RBT_Mapping2 ...
Processing theory Containers.RBT_Set2 ...
Loading 3 theories ...
Processing theory Polynomial_Factorization.Precomputation ...
Processing theory Polynomial_Factorization.Kronecker_Factorization ...
Processing theory Polynomial_Factorization.Rational_Factorization ...
Processing theory Interpreter_Optimizations.Std ...
Processing theory Interpreter_Optimizations.Std_to_Inca_simulation ...
Removing 38 theories ...
Processing theory Interpreter_Optimizations.Std_to_Inca_compiler ...
Loading 3 theories ...
Processing theory Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials ...
Processing theory Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation ...
Processing theory Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities ...
Loading 14 theories ...
Removing 13 theories ...
Processing theory Timed_Automata.Timed_Automata ...
Processing theory Timed_Automata.Misc ...
Processing theory Timed_Automata.Floyd_Warshall ...
Processing theory Timed_Automata.DBM ...
Processing theory Timed_Automata.Regions ...
Processing theory Timed_Automata.Closure ...
Processing theory Timed_Automata.Paths_Cycles ...
Processing theory Timed_Automata.DBM_Basics ...
Processing theory Timed_Automata.DBM_Normalization ...
Processing theory Timed_Automata.DBM_Operations ...
Processing theory Timed_Automata.DBM_Zone_Semantics ...
Processing theory Timed_Automata.Regions_Beta ...
Processing theory Timed_Automata.Approx_Beta ...
Processing theory Timed_Automata.Normalized_Zone_Semantics ...
Loading 8 theories ...
Removing 14 theories ...
Processing theory Jacobson_Basic_Algebra.Set_Theory ...
Processing theory Grothendieck_Schemes.Set_Extras ...
Processing theory Grothendieck_Schemes.Topological_Space ...
Processing theory Jacobson_Basic_Algebra.Group_Theory ...
Processing theory Grothendieck_Schemes.Group_Extras ...
Processing theory Jacobson_Basic_Algebra.Ring_Theory ...
Processing theory Grothendieck_Schemes.Comm_Ring ...
Processing theory Grothendieck_Schemes.Scheme ...
Processing theory Interpreter_Optimizations.Op_example ...
Loading 5 theories ...
Processing theory Root_Balanced_Tree.Time_Monad ...
Removing 21 theories ...
Processing theory Amortized_Complexity.Amortized_Framework0 ...
Processing theory Root_Balanced_Tree.Root_Balanced_Tree ...
Processing theory Root_Balanced_Tree.Root_Balanced_Tree_Tab ...
Loading 18 theories ...
Processing theory Physical_Quantities.Groups_mult ...
Processing theory Physical_Quantities.Power_int ...
Processing theory Physical_Quantities.Enum_extra ...
Processing theory Physical_Quantities.ISQ_Dimensions ...
Processing theory Physical_Quantities.ISQ_Quantities ...
Processing theory Physical_Quantities.ISQ_Proof ...
Processing theory Physical_Quantities.ISQ_Algebra ...
Processing theory Physical_Quantities.ISQ_Units ...
Processing theory Physical_Quantities.ISQ_Conversion ...
Loading 20 theories ...
Processing theory Physical_Quantities.ISQ ...
Processing theory Physical_Quantities.SI_Units ...
Processing theory Physical_Quantities.SI_Constants ...
Processing theory Physical_Quantities.SI_Prefix ...
Processing theory Physical_Quantities.SI_Derived ...
Processing theory Physical_Quantities.SI_Accepted ...
Processing theory Physical_Quantities.SI_Imperial ...
Processing theory Physical_Quantities.SI ...
Processing theory Physical_Quantities.SI_Astronomical ...
Removing 9 theories ...
Processing theory Metalogic_ProofChecker.Preliminaries ...
Processing theory Metalogic_ProofChecker.Core ...
Processing theory Metalogic_ProofChecker.Term ...
Processing theory Metalogic_ProofChecker.Name ...
Processing theory Metalogic_ProofChecker.Sorts ...
Processing theory Metalogic_ProofChecker.SortConstants ...
Processing theory Metalogic_ProofChecker.SortsExe ...
Processing theory Metalogic_ProofChecker.BetaNorm ...
Processing theory Metalogic_ProofChecker.Theory ...
Processing theory Metalogic_ProofChecker.BetaNormProof ...
Processing theory Metalogic_ProofChecker.EtaNorm ...
Processing theory Metalogic_ProofChecker.EtaNormProof ...
Processing theory Metalogic_ProofChecker.Term_Subst ...
Processing theory Metalogic_ProofChecker.Instances ...
Processing theory Metalogic_ProofChecker.TheoryExe ...
Processing theory Metalogic_ProofChecker.Logic ...
Processing theory Metalogic_ProofChecker.EqualityProof ...
Processing theory Metalogic_ProofChecker.ProofTerm ...
Processing theory Metalogic_ProofChecker.CheckerExe ...
Processing theory Metalogic_ProofChecker.CodeGen ...
Processing theory Interpreter_Optimizations.Env_list ...
Removing 65 theories ...
Processing theory Padic_Ints.Zp_Compact ...
Removing 8 theories ...
Processing theory Bertrands_Postulate.Bertrand ...
Loading 2 theories ...
Removing 10 theories ...
Processing theory Fermat3_4.Quad_Form ...
Processing theory Fermat3_4.Fermat3 ...
Loading 7 theories ...
Processing theory Lambda_Free_RPOs.Lambda_Free_Util ...
Processing theory Lambda_Free_RPOs.Infinite_Chain ...
Processing theory Lambda_Free_RPOs.Lambda_Free_Term ...
Removing 2 theories ...
Processing theory Lambda_Free_RPOs.Extension_Orders ...
Processing theory Lambda_Free_EPO.Embeddings ...
Processing theory Lambda_Free_EPO.Chop ...
Processing theory Lambda_Free_EPO.Lambda_Free_EPO ...
Loading 63 theories ...
Removing 3 theories ...
Processing theory Containers.Equal ...
Processing theory Containers.Closure_Set ...
Processing theory First_Order_Terms.Option_Monad ...
Processing theory Containers.Collection_Eq ...
Processing theory Containers.AssocList ...
Processing theory Containers.Collection_Enum ...
Processing theory Regular_Tree_Relations.Horn_Inference ...
Processing theory Containers.DList_Set ...
Processing theory First_Order_Terms.Term ...
Processing theory Knuth_Bendix_Order.Subterm_and_Context ...
Processing theory Regular_Tree_Relations.Term_Context ...
Processing theory FO_Theory_Rewriting.Saturation ...
Processing theory Regular_Tree_Relations.Basic_Utils ...
Processing theory Regular_Tree_Relations.Ground_Terms ...
Processing theory Regular_Tree_Relations.Ground_Closure ...
Processing theory Regular_Tree_Relations.FSet_Utils ...
Processing theory Regular_Tree_Relations.Horn_Fset ...
Processing theory Regular_Tree_Relations.Ground_Ctxt ...
Processing theory FOL-Fitting.FOL_Fitting ...
Processing theory FO_Theory_Rewriting.Utils ...
Processing theory FO_Theory_Rewriting.Rewriting ...
Processing theory Containers.Set_Impl ...
Processing theory Containers.Mapping_Impl ...
Processing theory Containers.Map_To_Mapping ...
Processing theory Containers.Containers ...
Processing theory FO_Theory_Rewriting.Bot_Terms ...
Processing theory FO_Theory_Rewriting.Multihole_Context ...
Processing theory FO_Theory_Rewriting.FOR_Certificate ...
Processing theory FO_Theory_Rewriting.Ground_MCtxt ...
Processing theory Regular_Tree_Relations.Tree_Automata ...
Processing theory Regular_Tree_Relations.Tree_Automata_Det ...
Processing theory Regular_Tree_Relations.Tree_Automata_Complement ...
Processing theory Regular_Tree_Relations.GTT ...
Processing theory Regular_Tree_Relations.Tree_Automata_Pumping ...
Processing theory Regular_Tree_Relations.GTT_Compose ...
Processing theory FO_Theory_Rewriting.Tree_Automata_Derivation_Split ...
Processing theory Regular_Tree_Relations.Tree_Automata_Abstract_Impl ...
Processing theory FO_Theory_Rewriting.NF ...
Processing theory Regular_Tree_Relations.GTT_Transitive_Closure ...
Processing theory Regular_Tree_Relations.Pair_Automaton ...
Processing theory Regular_Tree_Relations.AGTT ...
Processing theory FO_Theory_Rewriting.LV_to_GTT ...
Processing theory FO_Theory_Rewriting.Context_Extensions ...
Processing theory Regular_Tree_Relations.Tree_Automata_Class_Instances_Impl ...
Processing theory FO_Theory_Rewriting.Lift_Root_Step ...
Processing theory FO_Theory_Rewriting.FOR_Semantics ...
Processing theory Regular_Tree_Relations.Tree_Automata_Impl ...
Processing theory FO_Theory_Rewriting.TA_Clousure_Const ...
Processing theory FO_Theory_Rewriting.Type_Instances_Impl ...
Processing theory FO_Theory_Rewriting.NF_Impl ...
Processing theory FO_Theory_Rewriting.FOL_Extra ...
Processing theory Regular_Tree_Relations.RRn_Automata ...
Processing theory FO_Theory_Rewriting.Context_RR2 ...
Processing theory FO_Theory_Rewriting.GTT_RRn ...
Processing theory Regular_Tree_Relations.RR2_Infinite ...
Processing theory Regular_Tree_Relations.RR2_Infinite_Q_infinity ...
Processing theory Regular_Tree_Relations.Regular_Relation_Abstract_Impl ...
Processing theory Regular_Tree_Relations.Regular_Relation_Impl ...
Processing theory FO_Theory_Rewriting.FOR_Check ...
Processing theory FO_Theory_Rewriting.FOR_Check_Impl ...
Loading 5 theories ...
Processing theory Lambda_Free_RPOs.Lambda_Encoding ...
Processing theory Lambda_Free_RPOs.Lambda_Free_RPO_App ...
Processing theory Lambda_Free_RPOs.Lambda_Free_RPO_Std ...
Loading 13 theories ...
Processing theory Lambda_Free_RPOs.Lambda_Free_RPO_Optim ...
Processing theory Lambda_Free_RPOs.Lambda_Free_RPOs ...
Processing theory Vickrey_Clarke_Groves.SetUtils ...
Processing theory Vickrey_Clarke_Groves.Argmax ...
Processing theory Vickrey_Clarke_Groves.Partitions ...
Processing theory Vickrey_Clarke_Groves.RelationOperators ...
Processing theory Vickrey_Clarke_Groves.RelationProperties ...
Processing theory Vickrey_Clarke_Groves.MiscTools ...
Processing theory Vickrey_Clarke_Groves.StrictCombinatorialAuction ...
Removing 47 theories ...
Processing theory Vickrey_Clarke_Groves.Universes ...
Processing theory Vickrey_Clarke_Groves.UniformTieBreaking ...
Processing theory Vickrey_Clarke_Groves.CombinatorialAuction ...
Processing theory Vickrey_Clarke_Groves.CombinatorialAuctionCodeExtraction ...
Processing theory Vickrey_Clarke_Groves.FirstPrice ...
Removing 2 theories ...
Processing theory Vickrey_Clarke_Groves.CombinatorialAuctionExamples ...
Loading 12 theories ...
Processing theory SATSolverVerification.MoreList ...
Processing theory SATSolverVerification.CNF ...
Processing theory SATSolverVerification.Trail ...
Processing theory SATSolverVerification.SatSolverVerification ...
Processing theory SATSolverVerification.SatSolverCode ...
Removing 12 theories ...
Processing theory SATSolverVerification.AssertLiteral ...
Processing theory SATSolverVerification.Decide ...
Processing theory SATSolverVerification.UnitPropagate ...
Processing theory SATSolverVerification.Initialization ...
Processing theory SATSolverVerification.ConflictAnalysis ...
Processing theory SATSolverVerification.SolveLoop ...
Loading 2 theories ...
Processing theory SATSolverVerification.FunctionalImplementation ...
Removing 8 theories ...
Processing theory Liouville_Numbers.Liouville_Numbers_Misc ...
Processing theory Liouville_Numbers.Liouville_Numbers ...
Removing 2 theories ...
Processing theory Rep_Fin_Groups.Rep_Fin_Groups ...
Removing 2 theories ...
Processing theory Descartes_Sign_Rule.Descartes_Sign_Rule ...
Loading 11 theories ...
Processing theory Finitely_Generated_Abelian_Groups.General_Auxiliary ...
Processing theory Finitely_Generated_Abelian_Groups.Set_Multiplication ...
Processing theory Finitely_Generated_Abelian_Groups.Group_Hom ...
Processing theory Finitely_Generated_Abelian_Groups.Miscellaneous_Groups ...
Processing theory Finitely_Generated_Abelian_Groups.Generated_Groups_Extend ...
Processing theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups ...
Processing theory Finitely_Generated_Abelian_Groups.IDirProds ...
Processing theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend ...
Processing theory Finitely_Generated_Abelian_Groups.DirProds ...
Processing theory Finitely_Generated_Abelian_Groups.Group_Relations ...
Processing theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups ...
Loading 20 theories ...
Removing 14 theories ...
Processing theory Collections.ICF_Tools ...
Processing theory Collections.Ord_Code_Preproc ...
Processing theory Collections.Locale_Code ...
Processing theory FOL_Seq_Calc1.Common ...
Processing theory Abstract_Completeness.Abstract_Completeness ...
Processing theory Abstract_Soundness.Finite_Proof_Soundness ...
Processing theory FOL_Seq_Calc2.SeCaV ...
Processing theory FOL_Seq_Calc2.Usemantics ...
Processing theory FOL_Seq_Calc2.Prover ...
Processing theory FOL_Seq_Calc2.Hintikka ...
Processing theory FOL_Seq_Calc2.ProverLemmas ...
Processing theory FOL_Seq_Calc2.Countermodel ...
Processing theory FOL_Seq_Calc1.Tableau ...
Processing theory FOL_Seq_Calc1.Sequent ...
Processing theory FOL_Seq_Calc2.Sequent1 ...
Processing theory FOL_Seq_Calc2.Sequent_Calculus_Verifier ...
Processing theory FOL_Seq_Calc2.EPathHintikka ...
Loading 12 theories ...
Processing theory FOL_Seq_Calc2.Completeness ...
Processing theory FOL_Seq_Calc2.Soundness ...
Processing theory FOL_Seq_Calc2.Results ...
Processing theory Safe_OCL.Transitive_Closure_Ext ...
Processing theory Safe_OCL.Errorable ...
Processing theory Safe_OCL.Finite_Map_Ext ...
Processing theory Safe_OCL.Tuple ...
Processing theory Safe_OCL.OCL_Basic_Types ...
Removing 14 theories ...
Processing theory Safe_OCL.Object_Model ...
Processing theory Safe_OCL.OCL_Types ...
Processing theory Safe_OCL.OCL_Syntax ...
Processing theory Safe_OCL.OCL_Object_Model ...
Processing theory Safe_OCL.OCL_Typing ...
Processing theory Safe_OCL.OCL_Normalization ...
Processing theory Safe_OCL.OCL_Examples ...
Processing theory SumSquares.TwoSquares ...
Processing theory SumSquares.FourSquares ...
Processing theory Lifting_the_Exponent.LTE ...
Loading 3 theories ...
Removing 15 theories ...
Processing theory Dijkstra_Shortest_Path.Graph ...
Processing theory Koenigsberg_Friendship.MoreGraph ...
Processing theory Koenigsberg_Friendship.FriendshipTheory ...
Processing theory Arith_Prog_Rel_Primes.Arith_Prog_Rel_Primes ...
Loading 13 theories ...
Processing theory Nash_Williams.Nash_Extras ...
Processing theory ZFC_in_HOL.ZFC_Library ...
Processing theory Nash_Williams.Nash_Williams ...
Removing 13 theories ...
Processing theory ZFC_in_HOL.ZFC_in_HOL ...
Processing theory ZFC_in_HOL.ZFC_Cardinals ...
Processing theory ZFC_in_HOL.ZFC_Typeclasses ...
Processing theory ZFC_in_HOL.Kirby ...
Processing theory ZFC_in_HOL.Ordinal_Exp ...
Processing theory Ordinal_Partitions.Library_Additions ...
Processing theory ZFC_in_HOL.Cantor_NF ...
Processing theory Ordinal_Partitions.Partitions ...
Processing theory Ordinal_Partitions.Erdos_Milner ...
Processing theory Ordinal_Partitions.Omega_Omega ...
Loading 20 theories ...
Removing 14 theories ...
Processing theory Incredible_Proof_Machine.Entailment ...
Processing theory Incredible_Proof_Machine.Indexed_FSet ...
Processing theory Incredible_Proof_Machine.Abstract_Formula ...
Processing theory Incredible_Proof_Machine.Incredible_Signatures ...
Processing theory Incredible_Proof_Machine.Abstract_Rules ...
Processing theory Incredible_Proof_Machine.Rose_Tree ...
Processing theory Incredible_Proof_Machine.Natural_Deduction ...
Processing theory Incredible_Proof_Machine.Propositional_Formulas ...
Processing theory Incredible_Proof_Machine.Incredible_Deduction ...
Processing theory Incredible_Proof_Machine.Predicate_Formulas ...
Processing theory Incredible_Proof_Machine.Abstract_Rules_To_Incredible ...
Processing theory Incredible_Proof_Machine.Incredible_Predicate ...
Processing theory Incredible_Proof_Machine.Incredible_Propositional ...
Processing theory Incredible_Proof_Machine.Incredible_Correctness ...
Processing theory Incredible_Proof_Machine.Incredible_Trees ...
Processing theory Incredible_Proof_Machine.Build_Incredible_Tree ...
Processing theory Incredible_Proof_Machine.Incredible_Completeness ...
Processing theory Incredible_Proof_Machine.Incredible_Predicate_Tasks ...
Loading 13 theories ...
Processing theory Incredible_Proof_Machine.Incredible_Propositional_Tasks ...
Processing theory Incredible_Proof_Machine.Incredible_Everything ...
Removing 20 theories ...
Processing theory Automatic_Refinement.Refine_Util_Bootstrap1 ...
Processing theory Automatic_Refinement.Mk_Term_Antiquot ...
Processing theory Automatic_Refinement.Mpat_Antiquot ...
Processing theory Automatic_Refinement.Refine_Util ...
Processing theory Certification_Monads.Error_Syntax ...
Processing theory Certification_Monads.Error_Monad ...
Processing theory Certification_Monads.Check_Monad ...
Processing theory AI_Planning_Languages_Semantics.Error_Monad_Add ...
Processing theory Propositional_Proof_Systems.Formulas ...
Processing theory Propositional_Proof_Systems.Sema ...
Processing theory Propositional_Proof_Systems.Consistency ...
Processing theory AI_Planning_Languages_Semantics.PDDL_STRIPS_Semantics ...
Loading 2 theories ...
Processing theory AI_Planning_Languages_Semantics.PDDL_STRIPS_Checker ...
Processing theory FOL_Seq_Calc2.Export ...
Processing theory Koenigsberg_Friendship.KoenigsbergBridge ...
Loading 32 theories ...
Processing theory Hoare_Time.AExp ...
Processing theory Hoare_Time.BExp ...
Processing theory Hoare_Time.Com ...
Processing theory Hoare_Time.Big_Step ...
Processing theory Hoare_Time.Big_StepT ...
Processing theory Hoare_Time.Vars ...
Processing theory Hoare_Time.Partial_Evaluation ...
Processing theory Separation_Algebra.Separation_Algebra ...
Processing theory Hoare_Time.Product_Separation_Algebra ...
Processing theory Separation_Algebra.Sep_Heap_Instance ...
Processing theory Hoare_Time.Sep_Algebra_Add ...
Removing 40 theories ...
Processing theory Hoare_Time.Nielson_Hoare ...
Processing theory Hoare_Time.Big_StepT_Partial ...
Processing theory Hoare_Time.QuantK_Hoare ...
Processing theory Hoare_Time.QuantK_VCG ...
Processing theory Hoare_Time.Quant_Hoare ...
Processing theory Hoare_Time.QuantK_Examples ...
Processing theory Hoare_Time.SepLog_Hoare ...
Processing theory Hoare_Time.SepLog_Examples ...
Processing theory Hoare_Time.Quant_VCG ...
Processing theory Hoare_Time.Nielson_VCG ...
Processing theory Hoare_Time.QuantK_Sqrt ...
Processing theory Hoare_Time.Discussion ...
Processing theory Hoare_Time.Quant_Examples ...
Processing theory Hoare_Time.Nielson_Examples ...
Processing theory Hoare_Time.SepLogK_Hoare ...
Processing theory Hoare_Time.DiscussionO ...
Processing theory Hoare_Time.Nielson_VCGi ...
Processing theory Hoare_Time.Nielson_VCGi_complete ...
Processing theory Hoare_Time.Nielson_Sqrt ...
Processing theory Hoare_Time.SepLogK_VCG ...
Processing theory Hoare_Time.Hoare_Time ...
Loading 23 theories ...
Processing theory Category3.Category ...
Processing theory Category3.DiscreteCategory ...
Processing theory Category3.DualCategory ...
Processing theory Category3.EpiMonoIso ...
Processing theory Category3.InitialTerminal ...
Processing theory HereditarilyFinite.HF ...
Processing theory Category3.ConcreteCategory ...
Removing 30 theories ...
Processing theory Category3.ProductCategory ...
Processing theory Category3.FreeCategory ...
Processing theory Category3.Functor ...
Processing theory Category3.NaturalTransformation ...
Processing theory Category3.BinaryFunctor ...
Processing theory Category3.SetCategory ...
Processing theory Category3.FunctorCategory ...
Processing theory Category3.SetCat ...
Processing theory Category3.Yoneda ...
Processing theory Category3.Adjunction ...
Processing theory Category3.Limit ...
Processing theory Category3.CategoryWithPullbacks ...
Processing theory Category3.CartesianCategory ...
Processing theory Category3.CartesianClosedCategory ...
Processing theory Category3.CategoryWithFiniteLimits ...
Processing theory Category3.HFSetCat ...
Loading 8 theories ...
Processing theory Datatype_Order_Generator.Derive_Aux ...
Processing theory Datatype_Order_Generator.Order_Generator ...
Processing theory Higher_Order_Terms.Term_Utils ...
Processing theory Higher_Order_Terms.Name ...
Processing theory Higher_Order_Terms.Term_Class ...
Loading 3 theories ...
Processing theory Higher_Order_Terms.Unification_Compat ...
Processing theory Higher_Order_Terms.Lambda_Free_Compat ...
Removing 12 theories ...
Processing theory Category3.EquivalenceOfCategories ...
Processing theory MonoidalCategory.MonoidalCategory ...
Processing theory MonoidalCategory.CartesianMonoidalCategory ...
Loading 12 theories ...
Processing theory RSAPSS.Mod ...
Processing theory RSAPSS.Crypt ...
Processing theory RSAPSS.Pdifference ...
Processing theory RSAPSS.Productdivides ...
Processing theory RSAPSS.Cryptinverts ...
Processing theory RSAPSS.Word ...
Processing theory RSAPSS.WordOperations ...
Processing theory RSAPSS.SHA1Padding ...
Processing theory RSAPSS.SHA1 ...
Processing theory RSAPSS.Wordarith ...
Processing theory RSAPSS.EMSAPSS ...
Removing 5 theories ...
Processing theory RSAPSS.RSAPSS ...
Loading 8 theories ...
Processing theory Integration.MonConv ...
Processing theory Integration.Sigma_Algebra ...
Processing theory Integration.Measure ...
Processing theory Integration.RealRandVar ...
Processing theory Integration.Failure ...
Processing theory Password_Authentication_Protocol.Propaedeutics ...
Removing 13 theories ...
Processing theory Integration.Integral ...
Removing 5 theories ...
Processing theory Password_Authentication_Protocol.Protocol ...
Loading 6 theories ...
Removing 2 theories ...
Processing theory Elliptic_Curves_Group_Law.Elliptic_Locale ...
Processing theory Elliptic_Curves_Group_Law.Elliptic_Test ...
Loading 12 theories ...
Processing theory Physical_Quantities.SI_Pretty ...
Processing theory Randomised_Social_Choice.Order_Predicates ...
Processing theory Randomised_Social_Choice.Preference_Profiles ...
Processing theory Randomised_Social_Choice.Elections ...
Processing theory Randomised_Social_Choice.Preference_Profile_Cmd ...
Removing 17 theories ...
Processing theory Fishburn_Impossibility.Social_Choice_Functions ...
Processing theory Priority_Queue_Braun.Priority_Queue_Braun ...
Processing theory Fishburn_Impossibility.Fishburn_Impossibility ...
Processing theory Priority_Queue_Braun.Priority_Queue_Braun2 ...
Processing theory Priority_Queue_Braun.Sorting_Braun ...
Loading 3 theories ...
Removing 11 theories ...
Processing theory Category3.Subcategory ...
Processing theory MonoidalCategory.MonoidalFunctor ...
Processing theory MonoidalCategory.FreeMonoidalCategory ...
Loading 31 theories ...
Processing theory Verified_SAT_Based_AI_Planning.List_Supplement ...
Processing theory Verified_SAT_Based_AI_Planning.Map_Supplement ...
Processing theory AI_Planning_Languages_Semantics.SASP_Semantics ...
Processing theory AI_Planning_Languages_Semantics.SASP_Checker ...
Processing theory Propositional_Proof_Systems.CNF ...
Processing theory Propositional_Proof_Systems.CNF_Sema ...
Processing theory Verified_SAT_Based_AI_Planning.State_Variable_Representation ...
Processing theory Verified_SAT_Based_AI_Planning.SAS_Plus_Representation ...
Processing theory Verified_SAT_Based_AI_Planning.STRIPS_Representation ...
Removing 19 theories ...
Processing theory Verified_SAT_Based_AI_Planning.SAS_Plus_Semantics ...
Processing theory Verified_SAT_Based_AI_Planning.STRIPS_Semantics ...
Processing theory Propositional_Proof_Systems.CNF_Formulas ...
Processing theory Propositional_Proof_Systems.CNF_Formulas_Sema ...
Processing theory Verified_SAT_Based_AI_Planning.CNF_Supplement ...
Processing theory Verified_SAT_Based_AI_Planning.CNF_Semantics_Supplement ...
Processing theory Verified_SAT_Based_AI_Planning.AST_SAS_Plus_Equivalence ...
Processing theory Verified_SAT_Based_AI_Planning.SAS_Plus_STRIPS ...
Processing theory Verified_SAT_Based_AI_Planning.SAT_Plan_Base ...
Processing theory Verified_SAT_Based_AI_Planning.SAT_Plan_Extensions ...
Processing theory Verified_SAT_Based_AI_Planning.SAT_Solve_SAS_Plus ...
Processing theory Verified_SAT_Based_AI_Planning.Set2_Join_RBT ...
Processing theory Verified_SAT_Based_AI_Planning.Solve_SASP ...
Loading 39 theories ...
Processing theory Case_Labeling.Case_Labeling ...
Processing theory Discrete_Summation.Discrete_Summation ...
Processing theory Card_Partitions.Injectivity_Solver ...
Processing theory Physical_Quantities.CGS ...
Processing theory Physical_Quantities.BIS ...
Processing theory Case_Labeling.Conditionals ...
Processing theory Case_Labeling.Monadic_Language ...
Processing theory Discrete_Summation.Factorials ...
Processing theory Discrete_Summation.Summation_Conversion ...
Processing theory Discrete_Summation.Examples ...
Processing theory Van_der_Waerden.Digits ...
Processing theory LinearQuantifierElim.Logic ...
Processing theory Falling_Factorial_Sum.Falling_Factorial_Sum_Combinatorics ...
Processing theory Falling_Factorial_Sum.Falling_Factorial_Sum_Induction ...
Processing theory Falling_Factorial_Sum.Falling_Factorial_Sum_Vandermonde ...
Processing theory Case_Labeling.Labeled_Hoare ...
Processing theory Case_Labeling.Labeled_Hoare_Examples ...
Processing theory LinearQuantifierElim.QE ...
Processing theory Case_Labeling.Case_Labeling_Examples ...
Processing theory Van_der_Waerden.Van_der_Waerden ...
Processing theory Efficient-Mergesort.Natural_Mergesort ...
Processing theory LinearQuantifierElim.DLO ...
Processing theory LinearQuantifierElim.QEdlo ...
Processing theory LinearQuantifierElim.CertDlo ...
Processing theory LinearQuantifierElim.QEdlo_fr ...
Processing theory LinearQuantifierElim.QEdlo_inf ...
Processing theory Universal_Turing_Machine.Recs ...
Removing 60 theories ...
Processing theory LinearQuantifierElim.LinArith ...
Processing theory LinearQuantifierElim.CertLin ...
Processing theory LinearQuantifierElim.QEdlo_ex ...
Processing theory LinearQuantifierElim.QElin ...
Processing theory LinearQuantifierElim.QElin_opt ...
Processing theory LinearQuantifierElim.QElin_inf ...
Processing theory LinearQuantifierElim.FRE ...
Loading 17 theories ...
Processing theory General-Triangle.GeneralTriangle ...
Processing theory Weight_Balanced_Trees.Weight_Balanced_Trees_log ...
Processing theory PLM.TAO_1_Embedding ...
Processing theory PLM.TAO_2_Semantics ...
Processing theory PLM.TAO_3_Quantifiable ...
Processing theory PLM.TAO_4_BasicDefinitions ...
Processing theory PLM.TAO_5_MetaSolver ...
Removing 11 theories ...
Processing theory PLM.TAO_6_Identifiable ...
Processing theory PLM.TAO_7_Axioms ...
Processing theory PLM.TAO_8_Definitions ...
Processing theory PLM.TAO_98_ArtificialTheorems ...
Processing theory PLM.TAO_99_SanityTests ...
Processing theory Impossible_Geometry.Impossible_Geometry ...
Processing theory PLM.TAO_9_PLM ...
Loading 16 theories ...
Processing theory PLM.TAO_10_PossibleWorlds ...
Processing theory PLM.TAO_99_Paradox ...
Processing theory PLM.Thesis ...
Processing theory FileRefinement.CArrays ...
Processing theory FileRefinement.ResizableArrays ...
Processing theory Approximation_Algorithms.Approx_SC_Hoare ...
Processing theory Approximation_Algorithms.Center_Selection ...
Processing theory ArrowImpossibilityGS.Arrow_Utility ...
Processing theory Approximation_Algorithms.Approx_LB_Hoare ...
Removing 20 theories ...
Processing theory Derangements.Derangements ...
Processing theory FFT.FFT ...
Processing theory FunWithFunctions.FunWithFunctions ...
Processing theory ClockSynchInst.ICAInstance ...
Processing theory ClockSynchInst.LynchInstance ...
Processing theory Efficient-Mergesort.Efficient_Sort ...
Processing theory Efficient-Mergesort.Mergesort_Complexity ...
Processing theory FileRefinement.FileRefinement ...
Processing theory GenClock.GenClock ...
Loading 24 theories ...
Processing theory Approximation_Algorithms.Approx_BP_Hoare ...
Processing theory WebAssembly.Wasm_Type_Abs ...
Processing theory Word_Lib.Even_More_List ...
Processing theory Word_Lib.Legacy_Aliases ...
Processing theory Word_Lib.Singleton_Bit_Shifts ...
Processing theory Word_Lib.Aligned ...
Processing theory Native_Word.Uint8 ...
Processing theory Word_Lib.Bits_Int ...
Processing theory Word_Lib.Typedef_Morphisms ...
Removing 17 theories ...
Processing theory Word_Lib.Reversed_Bit_Lists ...
Processing theory WebAssembly.Wasm_Ast ...
Processing theory WebAssembly.Wasm_Base_Defs ...
Processing theory WebAssembly.Wasm ...
Processing theory WebAssembly.Wasm_Axioms ...
Processing theory WebAssembly.Wasm_Type_Abs_Printing ...
Processing theory WebAssembly.Wasm_Checker_Types ...
Processing theory WebAssembly.Wasm_Checker ...
Processing theory WebAssembly.Wasm_Checker_Printing ...
Processing theory WebAssembly.Wasm_Interpreter ...
Processing theory WebAssembly.Wasm_Properties_Aux ...
Processing theory WebAssembly.Wasm_Properties ...
Processing theory WebAssembly.Wasm_Interpreter_Properties ...
Loading 13 theories ...
Processing theory WebAssembly.Wasm_Interpreter_Printing ...
Processing theory WebAssembly.Wasm_Interpreter_Printing_Pure ...
Processing theory WebAssembly.Wasm_Printing ...
Processing theory Binding_Syntax_Theory.Pick ...
Processing theory WebAssembly.Wasm_Soundness ...
Processing theory Binding_Syntax_Theory.Preliminaries ...
Processing theory Binding_Syntax_Theory.Equiv_Relation2 ...
Removing 8 theories ...
Processing theory Binding_Syntax_Theory.QuasiTerms_Swap_Fresh ...
Processing theory Binding_Syntax_Theory.QuasiTerms_PickFresh_Alpha ...
Processing theory Binding_Syntax_Theory.QuasiTerms_Environments_Substitution ...
Processing theory Binding_Syntax_Theory.Transition_QuasiTerms_Terms ...
Processing theory Binding_Syntax_Theory.Terms ...
Processing theory Binding_Syntax_Theory.Well_Sorted_Terms ...
Processing theory Binding_Syntax_Theory.Iteration ...
Processing theory Binding_Syntax_Theory.Semantic_Domains ...
Removing 1 theories ...
Processing theory Binding_Syntax_Theory.Recursion ...
Processing theory WebAssembly.Wasm_Checker_Properties ...
Loading 57 theories ...
Removing 22 theories ...
Processing theory Real_Power.RatPower ...
Processing theory CSP_RefTK.Fix_ind_ext ...
Processing theory Real_Power.RealPower ...
Processing theory Real_Power.Log ...
Processing theory HOL-CSP.Process ...
Processing theory HOL-CSP.Bot ...
Processing theory HOL-CSP.Det ...
Processing theory HOL-CSP.Mprefix ...
Processing theory HOL-CSP.Ndet ...
Processing theory HOL-CSP.Skip ...
Processing theory HOL-CSP.Stop ...
Removing 11 theories ...
Processing theory HOL-CSP.Mndet ...
Processing theory HOL-CSP.Seq ...
Processing theory HOL-CSP.Hide ...
Processing theory HOL-CSP.Sync ...
Processing theory HOL-CSP.CSP ...
Processing theory HOL-CSP.Assertions ...
Processing theory HOL-CSP.CopyBuffer ...
Processing theory CSP_RefTK.Assertions_ext ...
Processing theory CSP_RefTK.Properties ...
Processing theory CSP_RefTK.Process_norm ...
Processing theory CSP_RefTK.CopyBuffer_props ...
Processing theory CSP_RefTK.DiningPhilosophers ...
Loading 12 theories ...
Removing 7 theories ...
Processing theory HOL-CSP.Conclusion ...
Processing theory Word_Lib.Syntax_Bundles ...
Processing theory Word_Lib.Bitwise ...
Processing theory X86_Semantics.BitByte ...
Processing theory X86_Semantics.Memory ...
Processing theory X86_Semantics.State ...
Processing theory X86_Semantics.StateCleanUp ...
Removing 14 theories ...
Processing theory X86_Semantics.X86_InstructionSemantics ...
Processing theory X86_Semantics.SymbolicExecution ...
Processing theory X86_Semantics.X86_Parse ...
Processing theory X86_Semantics.Examples ...
Removing 1 theories ...
Processing theory X86_Semantics.Example_WC ...
Loading 46 theories ...
Processing theory Flyspeck-Tame.Quasi_Order ...
Processing theory Flyspeck-Tame.RTranCl ...
Processing theory SPARCv8.Lib ...
Processing theory SPARCv8.DetMonad ...
Processing theory SPARCv8.DetMonadLemmas ...
Processing theory Trie.Trie ...
Processing theory Flyspeck-Tame.Arch ...
Processing theory Flyspeck-Tame.IArray_Syntax ...
Processing theory SPARCv8.WordDecl ...
Processing theory SPARCv8.RegistersOps ...
Processing theory Flyspeck-Tame.ListAux ...
Processing theory Flyspeck-Tame.ListSum ...
Processing theory Flyspeck-Tame.Worklist ...
Removing 17 theories ...
Processing theory Trie.Tries ...
Processing theory Flyspeck-Tame.Maps ...
Processing theory Flyspeck-Tame.PlaneGraphIso ...
Processing theory Flyspeck-Tame.Rotation ...
Processing theory Flyspeck-Tame.Graph ...
Processing theory Flyspeck-Tame.FaceDivision ...
Processing theory Flyspeck-Tame.Tame ...
Processing theory Flyspeck-Tame.TameProps ...
Processing theory Flyspeck-Tame.Enumerator ...
Processing theory Flyspeck-Tame.Plane ...
Processing theory Flyspeck-Tame.Plane1 ...
Processing theory Flyspeck-Tame.Generator ...
Processing theory Flyspeck-Tame.TameEnum ...
Processing theory Flyspeck-Tame.ArchCompAux ...
Processing theory Flyspeck-Tame.GraphProps ...
Processing theory Flyspeck-Tame.EnumeratorProps ...
Processing theory SPARCv8.Sparc_Types ...
Processing theory SPARCv8.MMU ...
Processing theory SPARCv8.Sparc_State ...
Processing theory SPARCv8.Sparc_Instruction ...
Processing theory SPARCv8.Sparc_Execution ...
Processing theory SPARCv8.Sparc_Init_State ...
Processing theory SPARCv8.Sparc_Code_Gen ...
Removing 2 theories ...
Processing theory Flyspeck-Tame.FaceDivisionProps ...
Processing theory Flyspeck-Tame.Invariants ...
Processing theory Flyspeck-Tame.PlaneProps ...
Processing theory Flyspeck-Tame.ScoreProps ...
Processing theory Flyspeck-Tame.LowerBound ...
Processing theory Flyspeck-Tame.Plane1Props ...
Processing theory Flyspeck-Tame.GeneratorProps ...
Loading 7 theories ...
Processing theory Flyspeck-Tame.TameEnumProps ...
Processing theory Flyspeck-Tame.ArchCompProps ...
Processing theory Flyspeck-Tame.Relative_Completeness ...
Processing theory Buildings.Prelim ...
Processing theory Buildings.Simplicial ...
Removing 34 theories ...
Processing theory Buildings.Algebra ...
Processing theory Buildings.Chamber ...
Processing theory Buildings.Coxeter ...
Processing theory Buildings.Building ...
Removing 7 theories ...
Processing theory SPARCv8.Sparc_Properties ...
Loading 70 theories ...
Processing theory JinjaDCI.Auxiliary ...
Processing theory JinjaDCI.Hidden ...
Processing theory Jinja.Semilat ...
Processing theory JinjaDCI.Type ...
Processing theory JinjaDCI.Decl ...
Processing theory JinjaDCI.TypeRel ...
Processing theory JinjaDCI.Value ...
Processing theory JinjaDCI.Objects ...
Processing theory JinjaDCI.Exceptions ...
Processing theory JinjaDCI.Conform ...
Processing theory JinjaDCI.SystemClasses ...
Processing theory JinjaDCI.State ...
Processing theory JinjaDCI.WellForm ...
Processing theory JinjaDCI.JVMState ...
Processing theory JinjaDCI.JVMInstructions ...
Processing theory JinjaDCI.PCompiler ...
Processing theory JinjaDCI.JVMExceptions ...
Processing theory Jinja.Err ...
Processing theory Jinja.Listn ...
Processing theory Jinja.Opt ...
Processing theory Jinja.Product ...
Processing theory Jinja.Semilattices ...
Processing theory Jinja.Typing_Framework_1 ...
Processing theory Jinja.SemilatAlg ...
Processing theory Jinja.Kildall_1 ...
Processing theory JinjaDCI.SemiType ...
Removing 11 theories ...
Processing theory Jinja.Typing_Framework_err ...
Processing theory Jinja.Typing_Framework_2 ...
Processing theory JinjaDCI.JVM_SemiType ...
Processing theory Jinja.LBVSpec ...
Processing theory Jinja.LBVComplete ...
Processing theory Jinja.LBVCorrect ...
Processing theory JinjaDCI.JVMExecInstr ...
Processing theory JinjaDCI.JVMExec ...
Processing theory JinjaDCI.JVMDefensive ...
Processing theory JinjaDCI.Expr ...
Processing theory JinjaDCI.WWellForm ...
Processing theory JinjaDCI.WellType ...
Processing theory JinjaDCI.Annotate ...
Processing theory JinjaDCI.WellTypeRT ...
Processing theory JinjaDCI.Effect ...
Processing theory JinjaDCI.BVSpec ...
Processing theory Jinja.Kildall_2 ...
Processing theory Jinja.Abstract_BV ...
Processing theory JinjaDCI.EffectMono ...
Processing theory JinjaDCI.BVConform ...
Processing theory JinjaDCI.ClassAdd ...
Processing theory JinjaDCI.TF_JVM ...
Processing theory JinjaDCI.BigStep ...
Processing theory JinjaDCI.DefAss ...
Processing theory JinjaDCI.JWellForm ...
Processing theory JinjaDCI.SmallStep ...
Processing theory JinjaDCI.StartProg ...
Processing theory JinjaDCI.EConform ...
Processing theory JinjaDCI.BVExec ...
Processing theory JinjaDCI.LBVJVM ...
Processing theory JinjaDCI.Progress ...
Processing theory JinjaDCI.J1 ...
Processing theory JinjaDCI.Compiler1 ...
Processing theory JinjaDCI.Compiler2 ...
Processing theory JinjaDCI.J1WellForm ...
Processing theory JinjaDCI.Correctness1 ...
Processing theory JinjaDCI.TypeSafe ...
Processing theory JinjaDCI.BVSpecTypeSafe ...
Processing theory JinjaDCI.BVNoTypeError ...
Processing theory JinjaDCI.Equivalence ...
Processing theory JinjaDCI.Correctness2 ...
Processing theory JinjaDCI.Compiler ...
Processing theory JinjaDCI.TypeComp ...
Loading 34 theories ...
Processing theory JinjaDCI.JinjaDCI ...
Processing theory Factored_Transition_System_Bounding.HoArithUtils ...
Processing theory Factored_Transition_System_Bounding.RelUtils ...
Processing theory Factored_Transition_System_Bounding.SetUtils ...
Processing theory Collections.Partial_Equivalence_Relation ...
Processing theory Factored_Transition_System_Bounding.FactoredSystemLib ...
Processing theory Factored_Transition_System_Bounding.FmapUtils ...
Processing theory Collections.Code_Target_ICF ...
Processing theory Factored_Transition_System_Bounding.Acyclicity ...
Processing theory Separation_Logic_Imperative_HOL.Imp_List_Spec ...
Processing theory Separation_Logic_Imperative_HOL.Imp_Map_Spec ...
Processing theory Separation_Logic_Imperative_HOL.Imp_Set_Spec ...
Processing theory Separation_Logic_Imperative_HOL.List_Seg ...
Processing theory Separation_Logic_Imperative_HOL.Hash_Table ...
Processing theory Separation_Logic_Imperative_HOL.Array_Blit ...
Processing theory Factored_Transition_System_Bounding.ListUtils ...
Processing theory Separation_Logic_Imperative_HOL.Array_Map_Impl ...
Processing theory Separation_Logic_Imperative_HOL.Array_Set_Impl ...
Processing theory Separation_Logic_Imperative_HOL.Union_Find ...
Processing theory Separation_Logic_Imperative_HOL.Circ_List ...
Processing theory Separation_Logic_Imperative_HOL.Open_List ...
Processing theory Factored_Transition_System_Bounding.FSSublist ...
Processing theory Separation_Logic_Imperative_HOL.Hash_Map ...
Processing theory Separation_Logic_Imperative_HOL.Hash_Map_Impl ...
Removing 38 theories ...
Processing theory Separation_Logic_Imperative_HOL.Hash_Set_Impl ...
Processing theory Separation_Logic_Imperative_HOL.From_List_GA ...
Processing theory Separation_Logic_Imperative_HOL.Idioms ...
Processing theory Separation_Logic_Imperative_HOL.To_List_GA ...
Processing theory Separation_Logic_Imperative_HOL.Sep_Examples ...
Processing theory Factored_Transition_System_Bounding.FactoredSystem ...
Processing theory Factored_Transition_System_Bounding.ActionSeqProcess ...
Processing theory Factored_Transition_System_Bounding.Dependency ...
Processing theory Factored_Transition_System_Bounding.TopologicalProps ...
Removing 45 theories ...
Processing theory Factored_Transition_System_Bounding.SystemAbstraction ...
Loading 34 theories ...
Processing theory Factored_Transition_System_Bounding.AcycSspace ...
Processing theory LocalLexing.InductRules ...
Processing theory LocalLexing.ListTools ...
Processing theory LocalLexing.CFG ...
Processing theory Jordan_Hoelder.GroupIsoClasses ...
Processing theory Secondary_Sylow.GroupAction ...
Processing theory Secondary_Sylow.SubgroupConjugation ...
Processing theory LocalLexing.LocalLexing ...
Processing theory LocalLexing.LLEarleyParsing ...
Processing theory LocalLexing.Limit ...
Processing theory LocalLexing.LocalLexingLemmas ...
Processing theory Jordan_Hoelder.SndIsomorphismGrp ...
Processing theory Secondary_Sylow.SndSylow ...
Processing theory Jordan_Hoelder.SubgroupsAndNormalSubgroups ...
Processing theory Jordan_Hoelder.SimpleGroups ...
Processing theory Jordan_Hoelder.MaximalNormalSubgroups ...
Processing theory Jordan_Hoelder.CompositionSeries ...
Processing theory LocalLexing.Derivations ...
Processing theory LocalLexing.Validity ...
Removing 8 theories ...
Processing theory LocalLexing.TheoremD2 ...
Processing theory Jordan_Hoelder.JordanHolder ...
Processing theory LocalLexing.TheoremD4 ...
Processing theory LocalLexing.TheoremD5 ...
Removing 11 theories ...
Processing theory LocalLexing.TheoremD6 ...
Processing theory LocalLexing.TheoremD7 ...
Processing theory LocalLexing.TheoremD8 ...
Processing theory LocalLexing.TheoremD9 ...
Processing theory LocalLexing.Ladder ...
Processing theory LocalLexing.TheoremD10 ...
Loading 20 theories ...
Processing theory LocalLexing.TheoremD11 ...
Processing theory LocalLexing.TheoremD12 ...
Processing theory LocalLexing.TheoremD13 ...
Processing theory LocalLexing.TheoremD14 ...
Processing theory LocalLexing.PathLemmas ...
Processing theory LocalLexing.MainTheorems ...
Processing theory Modular_Assembly_Kit_Security.Prefix ...
Processing theory Modular_Assembly_Kit_Security.Projection ...
Processing theory Modular_Assembly_Kit_Security.EventSystems ...
Processing theory Modular_Assembly_Kit_Security.Views ...
Processing theory Modular_Assembly_Kit_Security.BasicSecurityPredicates ...
Processing theory Modular_Assembly_Kit_Security.BSPTaxonomy ...
Processing theory Modular_Assembly_Kit_Security.CompositionBase ...
Processing theory Modular_Assembly_Kit_Security.CompositionSupport ...
Processing theory Inductive_Inference.Partial_Recursive ...
Removing 24 theories ...
Processing theory Modular_Assembly_Kit_Security.GeneralizedZippingLemma ...
Processing theory Modular_Assembly_Kit_Security.CompositionalityResults ...
Removing 4 theories ...
Processing theory Inductive_Inference.Universal ...
Processing theory Inductive_Inference.Standard_Results ...
Processing theory Inductive_Inference.Inductive_Inference_Basics ...
Processing theory Inductive_Inference.CONS_LIM ...
Processing theory Inductive_Inference.CP_FIN_NUM ...
Processing theory Inductive_Inference.Lemma_R ...
Processing theory Inductive_Inference.R1_BC ...
Processing theory Inductive_Inference.TOTAL_CONS ...
Loading 42 theories ...
Processing theory Inductive_Inference.Union ...
Processing theory Automatic_Refinement.Prio_List ...
Processing theory Automatic_Refinement.Anti_Unification ...
Processing theory Automatic_Refinement.Attr_Comb ...
Processing theory Automatic_Refinement.Named_Sorted_Thms ...
Processing theory Automatic_Refinement.Indep_Vars ...
Processing theory Automatic_Refinement.Foldi ...
Processing theory Automatic_Refinement.Mk_Record_Simp ...
Processing theory Automatic_Refinement.Tagged_Solver ...
Processing theory Automatic_Refinement.Select_Solve ...
Processing theory Automatic_Refinement.Refine_Lib ...
Processing theory Automatic_Refinement.Relators ...
Processing theory Automatic_Refinement.Param_Tool ...
Processing theory Collections.SetIterator ...
Processing theory Collections.SetIteratorOperations ...
Processing theory Collections.Assoc_List ...
Processing theory Automatic_Refinement.Param_HOL ...
Processing theory Automatic_Refinement.Parametricity ...
Processing theory Pi_Calculus.Agent ...
Processing theory Pi_Calculus.Rel ...
Removing 5 theories ...
Processing theory Collections.Diff_Array ...
Processing theory Pi_Calculus.Late_Semantics ...
Processing theory Pi_Calculus.Late_Semantics1 ...
Processing theory Pi_Calculus.Late_Tau_Chain ...
Processing theory Pi_Calculus.Strong_Late_Sim ...
Processing theory Pi_Calculus.Strong_Late_Bisim ...
Processing theory Pi_Calculus.Weak_Late_Step_Semantics ...
Processing theory Pi_Calculus.Weak_Late_Semantics ...
Processing theory Pi_Calculus.Strong_Late_Sim_Pres ...
Processing theory Pi_Calculus.Strong_Late_Bisim_Pres ...
Processing theory Pi_Calculus.Weak_Late_Sim ...
Processing theory Pi_Calculus.Weak_Late_Bisim ...
Processing theory Pi_Calculus.Weak_Late_Sim_Pres ...
Processing theory Pi_Calculus.Weak_Late_Step_Sim ...
Processing theory Pi_Calculus.Weak_Late_Cong ...
Processing theory Pi_Calculus.Weak_Late_Step_Sim_Pres ...
Processing theory Pi_Calculus.Strong_Late_Sim_SC ...
Processing theory Pi_Calculus.Strong_Late_Bisim_SC ...
Processing theory Pi_Calculus.Weak_Late_Bisim_SC ...
Processing theory Pi_Calculus.Weak_Late_Bisim_Pres ...
Processing theory Pi_Calculus.Weak_Late_Cong_Pres ...
Processing theory Gale_Shapley.Gale_Shapley1 ...
Loading 19 theories ...
Processing theory Gale_Shapley.Gale_Shapley2 ...
Removing 25 theories ...
Processing theory Regression_Test_Selection.ClassesChanged ...
Processing theory Regression_Test_Selection.RTS_safe ...
Processing theory Regression_Test_Selection.Semantics ...
Processing theory Regression_Test_Selection.CollectionSemantics ...
Processing theory Regression_Test_Selection.CollectionBasedRTS ...
Processing theory Free-Groups.C2 ...
Processing theory Free-Groups.Generators ...
Processing theory Free-Groups.UnitGroup ...
Processing theory Regression_Test_Selection.JVMSemantics ...
Processing theory Regression_Test_Selection.Subcls ...
Processing theory Regression_Test_Selection.ClassesAbove ...
Processing theory Free-Groups.Cancelation ...
Processing theory Free-Groups.FreeGroups ...
Processing theory Free-Groups.Isomorphisms ...
Processing theory Regression_Test_Selection.JVMCollectionSemantics ...
Removing 7 theories ...
Processing theory Regression_Test_Selection.JVMExecStepInductive ...
Processing theory Regression_Test_Selection.JVMCollectionBasedRTS ...
Loading 41 theories ...
Processing theory Regression_Test_Selection.RTS ...
Processing theory Pi_Calculus.Strong_Late_Bisim_Subst ...
Processing theory Program-Conflict-Analysis.LTS ...
Processing theory Pi_Calculus.Strong_Late_Bisim_Subst_Pres ...
Processing theory Pi_Calculus.Strong_Late_Bisim_Subst_SC ...
Processing theory SATSolverVerification.BasicDPLL ...
Processing theory SATSolverVerification.NieuwenhuisOliverasTinelli ...
Processing theory SATSolverVerification.KrsticGoel ...
Processing theory Program-Conflict-Analysis.Misc ...
Processing theory Program-Conflict-Analysis.Interleave ...
Processing theory Program-Conflict-Analysis.ThreadTracking ...
Processing theory Pi_Calculus.Early_Semantics ...
Processing theory Pi_Calculus.Early_Tau_Chain ...
Processing theory Pi_Calculus.Strong_Early_Sim ...
Processing theory Pi_Calculus.Strong_Early_Bisim ...
Processing theory Pi_Calculus.Strong_Early_Bisim_Subst ...
Processing theory Program-Conflict-Analysis.Flowgraph ...
Removing 43 theories ...
Processing theory Pi_Calculus.Strong_Early_Sim_Pres ...
Processing theory Pi_Calculus.Strong_Early_Bisim_Pres ...
Processing theory Pi_Calculus.Strong_Early_Late_Comp ...
Processing theory Pi_Calculus.Strong_Early_Bisim_SC ...
Processing theory Program-Conflict-Analysis.ConsInterleave ...
Processing theory Program-Conflict-Analysis.AcquisitionHistory ...
Processing theory Pi_Calculus.Weak_Early_Step_Semantics ...
Processing theory Pi_Calculus.Weak_Early_Semantics ...
Processing theory Pi_Calculus.Weak_Early_Sim ...
Processing theory Pi_Calculus.Weak_Early_Bisim ...
Processing theory Pi_Calculus.Weak_Early_Bisim_Subst ...
Processing theory Pi_Calculus.Weak_Early_Step_Sim ...
Processing theory Pi_Calculus.Weak_Early_Cong ...
Processing theory Pi_Calculus.Weak_Early_Cong_Subst ...
Processing theory Pi_Calculus.Weak_Early_Bisim_SC ...
Processing theory Pi_Calculus.Weak_Early_Sim_Pres ...
Processing theory Pi_Calculus.Weak_Early_Step_Sim_Pres ...
Processing theory Pi_Calculus.Weak_Early_Bisim_Pres ...
Processing theory Pi_Calculus.Weak_Early_Cong_Pres ...
Processing theory Pi_Calculus.Weak_Early_Cong_Subst_Pres ...
Processing theory Program-Conflict-Analysis.Semantics ...
Processing theory Program-Conflict-Analysis.Normalization ...
Processing theory Program-Conflict-Analysis.ConstraintSystems ...
Loading 16 theories ...
Processing theory Program-Conflict-Analysis.MainResult ...
Removing 29 theories ...
Processing theory Pi_Calculus.Weak_Late_Bisim_Subst ...
Processing theory Pi_Calculus.Weak_Late_Cong_Subst ...
Processing theory Pi_Calculus.Weak_Late_Cong_Subst_SC ...
Processing theory Universal_Turing_Machine.Rec_Def ...
Processing theory Universal_Turing_Machine.Turing ...
Processing theory Universal_Turing_Machine.Turing_Hoare ...
Processing theory Pi_Calculus.Strong_Late_Expansion_Law ...
Removing 13 theories ...
Processing theory Inductive_Inference.LIM_BC ...
Processing theory Pi_Calculus.Strong_Late_Axiomatisation ...
Processing theory Universal_Turing_Machine.Uncomputable ...
Processing theory Universal_Turing_Machine.Abacus_Mopup ...
Removing 16 theories ...
Processing theory Universal_Turing_Machine.Abacus ...
Processing theory Universal_Turing_Machine.Abacus_Hoare ...
Processing theory Universal_Turing_Machine.UF ...
Processing theory Universal_Turing_Machine.Recursive ...
Processing theory Universal_Turing_Machine.UTM ...
Loading 3 theories ...
Processing theory Regular_Tree_Relations.Myhill_Nerode ...
Processing theory AI_Planning_Languages_Semantics.Lifschitz_Consistency ...
Processing theory Elliptic_Curves_Group_Law.Elliptic_Axclass ...
Loading 27 theories ...
Processing theory Card_Multisets.Card_Multisets ...
Processing theory Card_Number_Partitions.Additions_to_Main ...
Processing theory Card_Number_Partitions.Number_Partition ...
Processing theory Card_Number_Partitions.Card_Number_Partitions ...
Processing theory Card_Partitions.Card_Partitions ...
Removing 22 theories ...
Processing theory Bell_Numbers_Spivey.Bell_Numbers ...
Processing theory Twelvefold_Way.Preliminaries ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry1 ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry2 ...
Processing theory Twelvefold_Way.Twelvefold_Way_Core ...
Processing theory Twelvefold_Way.Equiv_Relations_on_Functions ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry10 ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry11 ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry4 ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry6 ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry5 ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry7 ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry8 ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry9 ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry12 ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry3 ...
Processing theory Twelvefold_Way.Card_Bijections ...
Processing theory IFC_Tracking.IFC ...
Processing theory IFC_Tracking.PDG ...
Removing 2 theories ...
Processing theory Twelvefold_Way.Card_Bijections_Direct ...
Loading 78 theories ...
Processing theory Twelvefold_Way.Twelvefold_Way ...
Processing theory Network_Security_Policy_Verification.ML_GraphViz ...
Processing theory Network_Security_Policy_Verification.FiniteGraph ...
Processing theory Network_Security_Policy_Verification.TopoS_Util ...
Processing theory Transitive-Closure.Transitive_Closure_Impl ...
Processing theory Transitive-Closure.Transitive_Closure_List_Impl ...
Processing theory Network_Security_Policy_Verification.FiniteListGraph ...
Processing theory Network_Security_Policy_Verification.TopoS_Vertices ...
Processing theory Network_Security_Policy_Verification.TopoS_Interface ...
Processing theory Network_Security_Policy_Verification.vertex_example_simps ...
Processing theory Network_Security_Policy_Verification.Efficient_Distinct ...
Processing theory PCF.Basis ...
Processing theory Network_Security_Policy_Verification.TopoS_withOffendingFlows ...
Processing theory Network_Security_Policy_Verification.TopoS_ENF ...
Processing theory Network_Security_Policy_Verification.TopoS_Helper ...
Processing theory Network_Security_Policy_Verification.SINVAR_ACLcommunicateWith ...
Processing theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith ...
Processing theory Network_Security_Policy_Verification.SINVAR_BLPbasic ...
Processing theory Network_Security_Policy_Verification.SINVAR_BLPtrusted ...
Processing theory Network_Security_Policy_Verification.SINVAR_Dependability ...
Processing theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl ...
Processing theory Network_Security_Policy_Verification.FiniteListGraph_Impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_NoRefl ...
Processing theory PCF.Logical_Relations ...
Processing theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners ...
Removing 21 theories ...
Processing theory Network_Security_Policy_Verification.SINVAR_Tainting ...
Processing theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted ...
Processing theory Network_Security_Policy_Verification.SINVAR_NonInterference ...
Processing theory Network_Security_Policy_Verification.SINVAR_Sink ...
Processing theory Network_Security_Policy_Verification.SINVAR_Subnets ...
Processing theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW ...
Processing theory Network_Security_Policy_Verification.SINVAR_SecGwExt ...
Processing theory Network_Security_Policy_Verification.TopoS_Composition_Theory ...
Processing theory Network_Security_Policy_Verification.TopoS_Stateful_Policy ...
Processing theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_Algorithm ...
Processing theory Network_Security_Policy_Verification.TopoS_Interface_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_ACLcommunicateWith_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_BLPbasic_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_BLPtrusted_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_Dependability_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_NoRefl_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_NonInterference_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_SecGwExt_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_Sink_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_Subnets_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_Tainting_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG ...
Processing theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG_impl ...
Processing theory PCF.PCF ...
Processing theory Network_Security_Policy_Verification.TopoS_Composition_Theory_impl ...
Processing theory Network_Security_Policy_Verification.METASINVAR_SystemBoundary ...
Processing theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted_impl ...
Processing theory Network_Security_Policy_Verification.TopoS_Library ...
Processing theory Network_Security_Policy_Verification.TopoS_Impl ...
Processing theory PCF.OpSem ...
Processing theory PCF.SmallStep ...
Processing theory Network_Security_Policy_Verification.Example_Forte14 ...
Processing theory Network_Security_Policy_Verification.I8_SSH_Landscape ...
Processing theory Network_Security_Policy_Verification.Impl_List_Playground ...
Processing theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork ...
Processing theory Network_Security_Policy_Verification.Distributed_WebApp ...
Removing 6 theories ...
Processing theory Network_Security_Policy_Verification.Impl_List_Playground_statefulpolicycompliance ...
Processing theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork_statefulpolicy_example ...
Processing theory Network_Security_Policy_Verification.CryptoDB ...
Processing theory Network_Security_Policy_Verification.IDEM ...
Processing theory Network_Security_Policy_Verification.Network_Security_Policy_Verification ...
Removing 6 theories ...
Processing theory Network_Security_Policy_Verification.MeasrDroid ...
Processing theory Network_Security_Policy_Verification.SINVAR_Examples ...
Removing 2 theories ...
Processing theory Network_Security_Policy_Verification.Imaginary_Factory_Network ...
Loading 47 theories ...
Processing theory Isabelle_Meta_Model.Antiquote_Setup ...
Processing theory Isabelle_Meta_Model.Isabelle_Cartouche_Examples ...
Processing theory Isabelle_Meta_Model.Isabelle_Main0 ...
Processing theory Isabelle_Meta_Model.Isabelle_typedecl ...
Processing theory Isabelle_Meta_Model.Isabelle_Main2 ...
Processing theory Isabelle_Meta_Model.Isabelle_code_runtime ...
Processing theory Isabelle_Meta_Model.Isabelle_code_target ...
Processing theory Isabelle_Meta_Model.Isabelle_Main1 ...
Processing theory Isabelle_Meta_Model.Toy_Library ...
Processing theory Isabelle_Meta_Model.Toy_Library_Static ...
Processing theory Network_Security_Policy_Verification.Example_BLP ...
Processing theory Network_Security_Policy_Verification.Example ...
Processing theory Network_Security_Policy_Verification.TopoS_generateCode ...
Processing theory Isabelle_Meta_Model.Init ...
Processing theory Isabelle_Meta_Model.Meta_Pure ...
Processing theory Isabelle_Meta_Model.Parser_init ...
Processing theory Isabelle_Meta_Model.Parser_Pure ...
Processing theory Isabelle_Meta_Model.Printer_init ...
Processing theory Isabelle_Meta_Model.Printer_Pure ...
Processing theory Isabelle_Meta_Model.Init_rbt ...
Processing theory Isabelle_Meta_Model.Meta_SML ...
Processing theory Isabelle_Meta_Model.Printer_SML ...
Processing theory Isabelle_Meta_Model.Meta_Toy_extended ...
Processing theory Isabelle_Meta_Model.Parser_Toy_extended ...
Processing theory Isabelle_Meta_Model.Meta_Toy ...
Processing theory Isabelle_Meta_Model.Parser_Toy ...
Processing theory Isabelle_Meta_Model.Printer_Toy ...
Processing theory Isabelle_Meta_Model.Printer_Toy_extended ...
Removing 50 theories ...
Processing theory Isabelle_Meta_Model.Meta_Isabelle ...
Processing theory Isabelle_Meta_Model.Printer_Isabelle ...
Processing theory Isabelle_Meta_Model.Meta_META ...
Processing theory Isabelle_Meta_Model.Core_init ...
Processing theory Isabelle_Meta_Model.Floor1_access ...
Processing theory Isabelle_Meta_Model.Floor1_ctxt ...
Processing theory Isabelle_Meta_Model.Floor1_examp ...
Processing theory Isabelle_Meta_Model.Floor2_examp ...
Processing theory Isabelle_Meta_Model.Floor1_infra ...
Processing theory Isabelle_Meta_Model.Core ...
Processing theory Isabelle_Meta_Model.Parser_META ...
Processing theory Isabelle_Meta_Model.Printer_META ...
Processing theory Isabelle_Meta_Model.Printer ...
Processing theory Localization_Ring.Localization ...
Processing theory Isabelle_Meta_Model.Generator_dynamic_sequential ...
Processing theory Isabelle_Meta_Model.Rail ...
Processing theory Isabelle_Meta_Model.Design_deep ...
Removing 6 theories ...
Processing theory Isabelle_Meta_Model.Design_generated ...
Processing theory Isabelle_Meta_Model.Design_shallow ...
Loading 35 theories ...
Processing theory LatticeProperties.Conj_Disj ...
Processing theory LatticeProperties.WellFoundedTransitive ...
Processing theory LatticeProperties.Complete_Lattice_Prop ...
Processing theory MonoBoolTranAlgebra.Mono_Bool_Tran ...
Removing 5 theories ...
Processing theory MonoBoolTranAlgebra.Mono_Bool_Tran_Algebra ...
Processing theory MonoBoolTranAlgebra.Assertion_Algebra ...
Processing theory SequentInvertibility.MultiSequents ...
Processing theory SequentInvertibility.SRCTransforms ...
Processing theory SequentInvertibility.SingleSuccedent ...
Processing theory Stone_Algebras.Lattice_Basics ...
Processing theory Factored_Transition_System_Bounding.Invariants ...
Processing theory Stone_Relation_Algebras.Fixpoints ...
Processing theory SequentInvertibility.NominalSequents ...
Removing 7 theories ...
Processing theory SequentInvertibility.ModalSequents ...
Processing theory SequentInvertibility.SequentInvertibility ...
Processing theory Stone_Relation_Algebras.Semirings ...
Processing theory Correctness_Algebras.Base ...
Processing theory Correctness_Algebras.Monotonic_Boolean_Transformers ...
Processing theory Stone_Algebras.P_Algebras ...
Removing 6 theories ...
Processing theory Stone_Kleene_Relation_Algebras.Iterings ...
Processing theory Stone_Kleene_Relation_Algebras.Kleene_Algebras ...
Processing theory Correctness_Algebras.Omega_Algebras ...
Processing theory Subset_Boolean_Algebras.Subset_Boolean_Algebras ...
Processing theory Correctness_Algebras.Tests ...
Processing theory Correctness_Algebras.Complete_Tests ...
Processing theory Correctness_Algebras.Preconditions ...
Processing theory Correctness_Algebras.General_Refinement_Algebras ...
Processing theory Correctness_Algebras.Relative_Domain ...
Processing theory Correctness_Algebras.Complete_Domain ...
Processing theory Correctness_Algebras.Pre_Post ...
Processing theory Correctness_Algebras.Relative_Modal ...
Processing theory Correctness_Algebras.Hoare ...
Processing theory Correctness_Algebras.Hoare_Modal ...
Processing theory Correctness_Algebras.Pre_Post_Modal ...
Processing theory Correctness_Algebras.Monotonic_Boolean_Transformers_Instances ...
Loading 22 theories ...
Processing theory Circus.Var ...
Processing theory Circus.Var_list ...
Processing theory Perfect-Number-Thm.PerfectBasics ...
Processing theory Orbit_Stabiliser.Left_Coset ...
Processing theory Orbit_Stabiliser.Orbit_Stabiliser ...
Processing theory Circus.Relations ...
Processing theory Circus.Designs ...
Removing 12 theories ...
Processing theory Perfect-Number-Thm.Sigma ...
Processing theory Perfect-Number-Thm.Perfect ...
Processing theory Fermat3_4.Fermat4 ...
Processing theory Circus.Reactive_Processes ...
Processing theory Orbit_Stabiliser.Tetrahedron ...
Processing theory Circus.CSP_Processes ...
Processing theory Correctness_Algebras.Test_Iterings ...
Processing theory Circus.Circus_Actions ...
Removing 9 theories ...
Processing theory Correctness_Algebras.N_Semirings ...
Processing theory Circus.Denotational_Semantics ...
Processing theory Circus.Circus_Syntax ...
Processing theory Circus.Refinement ...
Processing theory Correctness_Algebras.N_Semirings_Boolean ...
Processing theory Circus.Refinement_Example ...
Processing theory Correctness_Algebras.N_Semirings_Modal ...
Loading 32 theories ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Cars ...
Processing theory Clean.Lens_Laws ...
Processing theory Clean.Optics ...
Processing theory Clean.MonadSE ...
Processing theory Clean.Seq_MonadSE ...
Processing theory Clean.Symbex_MonadSE ...
Processing theory Clean.Clean ...
Processing theory Clean.Hoare_MonadSE ...
Processing theory Correctness_Algebras.Approximation ...
Removing 13 theories ...
Processing theory Clean.Hoare_Clean ...
Processing theory Clean.Clean_Symbex ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.NatInt ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.RealInt ...
Processing theory Clean.IsPrime ...
Processing theory Generalized_Counting_Sort.Algorithm ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Views ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Traffic ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Move ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Sensors ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Restriction ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Length ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Perfect_Sensors ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Regular_Sensors ...
Processing theory Correctness_Algebras.Recursion_Strict ...
Removing 7 theories ...
Processing theory Generalized_Counting_Sort.Conservation ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.HMLSL ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.HMLSL_Perfect ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.HMLSL_Regular ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Safety_Perfect ...
Processing theory Generalized_Counting_Sort.Sorting ...
Removing 3 theories ...
Processing theory Generalized_Counting_Sort.Stability ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Safety_Regular ...
Loading 44 theories ...
Processing theory AWN.Lib ...
Processing theory Pi_Calculus.Strong_Early_Bisim_Subst_Pres ...
Processing theory AWN.TransitionSystems ...
Processing theory AWN.Invariants ...
Processing theory AWN.OInvariants ...
Processing theory Sort_Encodings.Preliminaries ...
Processing theory Sort_Encodings.Sig ...
Processing theory Sort_Encodings.TermsAndClauses ...
Processing theory Sort_Encodings.M ...
Processing theory Sort_Encodings.U ...
Processing theory Sort_Encodings.CU ...
Removing 26 theories ...
Processing theory Sort_Encodings.CM ...
Processing theory PCF.Continuations ...
Processing theory AWN.AWN ...
Processing theory AWN.AWN_SOS ...
Processing theory AWN.AWN_Cterms ...
Processing theory AWN.AWN_Labels ...
Processing theory Sort_Encodings.Mono ...
Processing theory Sort_Encodings.Mcalc ...
Processing theory AWN.Inv_Cterms ...
Processing theory AWN.AWN_SOS_Labels ...
Processing theory AWN.AWN_Invariants ...
Processing theory AWN.Qmsg ...
Processing theory AWN.Pnet ...
Processing theory AWN.Closed ...
Processing theory AWN.OAWN_SOS ...
Processing theory AWN.OAWN_SOS_Labels ...
Processing theory AWN.OPnet ...
Processing theory Sort_Encodings.T_G_Prelim ...
Processing theory AWN.ONode_Lifting ...
Processing theory AWN.OAWN_Invariants ...
Processing theory AWN.OAWN_Convert ...
Processing theory AWN.Qmsg_Lifting ...
Processing theory Sort_Encodings.Mcalc2 ...
Removing 5 theories ...
Processing theory AWN.OPnet_Lifting ...
Processing theory Sort_Encodings.Mcalc2C ...
Processing theory Sort_Encodings.T ...
Processing theory AWN.OClosed_Lifting ...
Processing theory Sort_Encodings.E ...
Processing theory AWN.OClosed_Transfer ...
Processing theory AWN.AWN_Main ...
Processing theory Sort_Encodings.G ...
Processing theory Sort_Encodings.Encodings ...
Removing 17 theories ...
Processing theory AWN.Toy ...
Loading 44 theories ...
Processing theory MSO_Regex_Equivalence.List_More ...
Processing theory KBPs.Extra ...
Processing theory MSO_Regex_Equivalence.Pi_Regular_Set ...
Processing theory Isabelle_Meta_Model.Generator_static ...
Processing theory KBPs.MapOps ...
Processing theory KBPs.Traces ...
Processing theory KBPs.DFS ...
Processing theory KBPs.Kripke ...
Removing 60 theories ...
Processing theory Stable_Matching.Basis ...
Processing theory KBPs.KBPs ...
Processing theory KBPs.KBPsAuto ...
Processing theory KBPs.SPRView ...
Processing theory KBPs.List_local ...
Processing theory KBPs.ODList ...
Processing theory KBPs.Eval ...
Processing theory KBPs.Trie2 ...
Processing theory Stable_Matching.Choice_Functions ...
Processing theory KBPs.KBPsAlg ...
Processing theory KBPs.SPRViewNonDet ...
Processing theory KBPs.SPRViewNonDetIndInit ...
Processing theory MSO_Regex_Equivalence.Pi_Regular_Exp ...
Processing theory MSO_Regex_Equivalence.Pi_Derivatives ...
Processing theory KBPs.ClockView ...
Processing theory KBPs.SPRViewSingle ...
Processing theory MSO_Regex_Equivalence.Init_Normalization ...
Processing theory KBPs.SPRViewDet ...
Processing theory KBPs.Views ...
Processing theory KBPs.Robot ...
Processing theory KBPs.MuddyChildren ...
Processing theory KBPs.Examples ...
Processing theory KBPs.KBPs_Main ...
Removing 28 theories ...
Processing theory MSO_Regex_Equivalence.Pi_Regular_Operators ...
Processing theory MSO_Regex_Equivalence.Pi_Equivalence_Checking ...
Processing theory MSO_Regex_Equivalence.PNormalization ...
Processing theory MSO_Regex_Equivalence.Formula ...
Processing theory MSO_Regex_Equivalence.WS1S ...
Processing theory MSO_Regex_Equivalence.WS1S_Normalization ...
Processing theory Stable_Matching.Contracts ...
Processing theory Stable_Matching.COP ...
Processing theory Stable_Matching.Bossiness ...
Processing theory Stable_Matching.Strategic ...
Removing 10 theories ...
Processing theory MSO_Regex_Equivalence.Pi_Regular_Exp_Dual ...
Processing theory MSO_Regex_Equivalence.WS1S_Equivalence_Checking ...
Processing theory MSO_Regex_Equivalence.WS1S_Examples ...
Loading 47 theories ...
Processing theory Key_Agreement_Strong_Adversaries.Infra ...
Processing theory Optics.Interp ...
Processing theory Optics.Two ...
Processing theory Key_Agreement_Strong_Adversaries.Refinement ...
Processing theory Optics.Lens_Laws ...
Processing theory Optics.Lens_Algebra ...
Processing theory Key_Agreement_Strong_Adversaries.Messages ...
Processing theory Key_Agreement_Strong_Adversaries.AuthenticationN ...
Processing theory Key_Agreement_Strong_Adversaries.AuthenticationI ...
Processing theory Key_Agreement_Strong_Adversaries.Message_derivation ...
Processing theory Key_Agreement_Strong_Adversaries.Channels ...
Processing theory Key_Agreement_Strong_Adversaries.IK ...
Processing theory Key_Agreement_Strong_Adversaries.Secrecy ...
Processing theory Higher_Order_Terms.Find_First ...
Processing theory Higher_Order_Terms.Fresh_Monad ...
Processing theory Key_Agreement_Strong_Adversaries.Runs ...
Processing theory Higher_Order_Terms.Fresh_Class ...
Processing theory Correctness_Algebras.Domain ...
Removing 4 theories ...
Processing theory Optics.Lens_Order ...
Processing theory Optics.Lens_Symmetric ...
Processing theory Optics.Lens_Instances ...
Processing theory Optics.Lenses ...
Processing theory Optics.Prisms ...
Processing theory Optics.Channel_Type ...
Processing theory Optics.Dataspace ...
Processing theory Higher_Order_Terms.Nterm ...
Processing theory Higher_Order_Terms.Term ...
Processing theory Higher_Order_Terms.Pats ...
Processing theory Key_Agreement_Strong_Adversaries.Payloads ...
Processing theory Key_Agreement_Strong_Adversaries.Implem ...
Processing theory Optics.Scenes ...
Processing theory Optics.Optics ...
Processing theory Free-Groups.PingPongLemma ...
Processing theory Optics.Lens_Record_Example ...
Processing theory Higher_Order_Terms.Term_to_Nterm ...
Processing theory Key_Agreement_Strong_Adversaries.Implem_lemmas ...
Processing theory Key_Agreement_Strong_Adversaries.Implem_asymmetric ...
Processing theory Key_Agreement_Strong_Adversaries.Implem_symmetric ...
Removing 31 theories ...
Processing theory Key_Agreement_Strong_Adversaries.dhlvl1 ...
Processing theory Correctness_Algebras.Lattice_Ordered_Semirings ...
Processing theory Correctness_Algebras.Domain_Iterings ...
Processing theory Key_Agreement_Strong_Adversaries.sklvl1 ...
Processing theory Correctness_Algebras.Domain_Recursion ...
Removing 2 theories ...
Processing theory Key_Agreement_Strong_Adversaries.sklvl2 ...
Processing theory Key_Agreement_Strong_Adversaries.sklvl3 ...
Loading 41 theories ...
Processing theory Key_Agreement_Strong_Adversaries.sklvl3_asymmetric ...
Processing theory Key_Agreement_Strong_Adversaries.sklvl3_symmetric ...
Removing 5 theories ...
Processing theory Isabelle_C.C_Lexer_Language ...
Processing theory Isabelle_C.C_Lexer_Annotation ...
Processing theory Presburger-Automata.DFS ...
Processing theory Binomial-Heaps.BinomialHeap ...
Processing theory Tycon.Coerce ...
Processing theory Tycon.TypeApp ...
Processing theory Tycon.Functor ...
Processing theory Tycon.Monad ...
Processing theory Tycon.Binary_Tree_Monad ...
Processing theory Tycon.Lift_Monad ...
Processing theory Tycon.Monad_Plus ...
Processing theory Tycon.Error_Monad ...
Processing theory Tycon.Error_Transformer ...
Processing theory Tycon.Monad_Zero ...
Processing theory Tycon.Resumption_Transformer ...
Processing theory Tycon.Monad_Zero_Plus ...
Processing theory Tycon.Lazy_List_Monad ...
Processing theory Tycon.Maybe_Monad ...
Processing theory Tycon.State_Transformer ...
Processing theory Tycon.Writer_Monad ...
Processing theory Binomial-Heaps.SkewBinomialHeap ...
Processing theory Isabelle_C.C_Ast ...
Processing theory Isabelle_C.C_Environment ...
Processing theory Isabelle_C.C_Parser_Annotation ...
Processing theory Binomial-Heaps.Test ...
Processing theory Tycon.Writer_Transformer ...
Processing theory Tycon.Monad_Transformer ...
### Ignored report message: int
### Ignored report message: array\ int
### Ignored report message: redefining\ this\isactrlhere 
### Ignored report message: int
Processing theory Isabelle_C.C_Parser_Language ...
Removing 24 theories ...
Processing theory Isabelle_C.C_Eval ...
Processing theory Isabelle_C.C_Command ...
Processing theory Isabelle_C.C_Document ...
Processing theory Isabelle_C.C_Main ...
Processing theory Isabelle_C.C1 ...
Processing theory Isabelle_C.C_Appendices ...
Processing theory Presburger-Automata.Presburger_Automata ...
Processing theory Presburger-Automata.Exec ...
Removing 3 theories ...
Processing theory MSO_Regex_Equivalence.M2L ...
Processing theory MSO_Regex_Equivalence.M2L_Normalization ...
Processing theory MSO_Regex_Equivalence.M2L_Equivalence_Checking ...
Processing theory MSO_Regex_Equivalence.M2L_Examples ...
Loading 37 theories ...
Processing theory Isabelle_C.C0 ...
Processing theory Isabelle_C.C4 ...
Processing theory Isabelle_C.C_paper ...
Processing theory Separation_Algebra.Sep_Tactics ...
Processing theory Separation_Algebra.Map_Extra ...
Processing theory Universal_Turing_Machine.Abacus_Defs ...
Processing theory WorkerWrapper.FixedPointTheorems ...
Processing theory WorkerWrapper.Maybe ...
Processing theory WorkerWrapper.Nats ...
Processing theory WorkerWrapper.WorkerWrapper ...
Processing theory WorkerWrapper.WorkerWrapperNew ...
Processing theory WorkerWrapper.LList ...
Processing theory WorkerWrapper.Last ...
Processing theory WorkerWrapper.Accumulator ...
Processing theory WorkerWrapper.Nub ...
Processing theory Separation_Algebra.Types_D ...
Processing theory Isabelle_C.C2 ...
Processing theory Isabelle_C.C3 ...
Processing theory Separation_Algebra.Abstract_Separation_D ...
Processing theory Separation_Algebra.Separation_D ...
Removing 49 theories ...
Processing theory RIPEMD-160-SPARK.RIPEMD_160_SPARK ...
Processing theory Correctness_Algebras.Extended_Designs ...
Loading 47 theories ...
Processing theory Shivers-CFA.Utils ...
Processing theory Locally-Nameless-Sigma.ListPre ...
Processing theory Shivers-CFA.SetMap ...
Processing theory Shivers-CFA.MapSets ...
Processing theory Completeness.Tree ...
Processing theory Locally-Nameless-Sigma.FMap ...
Processing theory Completeness.PermutationLemmas ...
Processing theory Completeness.Base ...
Processing theory Locally-Nameless-Sigma.Environments ...
Processing theory Completeness.Formula ...
Processing theory Completeness.Sequents ...
Processing theory Completeness.Completeness ...
Processing theory Completeness.Soundness ...
Processing theory Category2.Category ...
Processing theory Category2.Functors ...
Processing theory Shivers-CFA.CPSScheme ...
Removing 29 theories ...
Processing theory Shivers-CFA.FixTransform ...
Processing theory Shivers-CFA.HOLCFUtils ...
Processing theory Category2.NatTrans ...
Processing theory List_Inversions.List_Inversions ...
Processing theory Shivers-CFA.CPSUtils ...
Processing theory Locally-Nameless-Sigma.Sigma ...
Processing theory LightweightJava.Lightweight_Java_Definition ...
Processing theory LightweightJava.Lightweight_Java_Equivalence ...
Processing theory Shivers-CFA.Computability ...
Processing theory Locally-Nameless-Sigma.TypedSigma ...
Processing theory Shivers-CFA.ExCF ...
Processing theory MuchAdoAboutTwo.MuchAdoAboutTwo ...
Processing theory Shivers-CFA.AbsCF ...
Processing theory Shivers-CFA.ExCFSV ...
Processing theory WorkerWrapper.CounterExample ...
Processing theory Shivers-CFA.AbsCFComp ...
Processing theory Shivers-CFA.AbsCFCorrect ...
Processing theory WorkerWrapper.Streams ...
Processing theory WorkerWrapper.UnboxedNats ...
Processing theory WorkerWrapper.Backtracking ...
Processing theory WorkerWrapper.Continuations ...
Processing theory Category2.Universe ...
Processing theory Category2.SetCat ...
Processing theory Category2.Yoneda ...
Removing 28 theories ...
Processing theory Locally-Nameless-Sigma.ParRed ...
Processing theory Locally-Nameless-Sigma.Locally_Nameless_Sigma ...
Processing theory LightweightJava.Lightweight_Java_Proof ...
Loading 41 theories ...
Processing theory Dominance_CHK.Sorted_Less2 ...
Processing theory First_Order_Terms.Unifiers ...
Processing theory Dominance_CHK.Sorted_List_Operations2 ...
Processing theory First_Order_Terms.Term_Pair_Multiset ...
Processing theory Propositional_Proof_Systems.Compactness ...
Processing theory Dominance_CHK.Cfg ...
Processing theory Stream-Fusion.LazyList ...
Processing theory DiskPaxos.DiskPaxos_Model ...
Processing theory DiskPaxos.DiskPaxos_Inv1 ...
Processing theory Resolution_FOL.Tree ...
Processing theory Shivers-CFA.Eval ...
Processing theory Stream-Fusion.Stream ...
Processing theory Dominance_CHK.Dom_Semi_List ...
Processing theory Propositional_Proof_Systems.SC ...
Processing theory Stream-Fusion.StreamFusion ...
Processing theory Resolution_FOL.TermsAndLiterals ...
Removing 18 theories ...
Processing theory Dominance_CHK.Dom_Kildall ...
Processing theory Propositional_Proof_Systems.SC_Cut ...
Processing theory DiskPaxos.DiskPaxos_Inv2 ...
Processing theory Propositional_Proof_Systems.LSC ...
Processing theory Propositional_Proof_Systems.SC_Sema ...
Processing theory DiskPaxos.DiskPaxos_Inv3 ...
Processing theory Propositional_Proof_Systems.Resolution ...
Processing theory Propositional_Proof_Systems.LSC_Resolution ...
Processing theory Propositional_Proof_Systems.Resolution_Compl_SC_Full ...
Processing theory Propositional_Proof_Systems.Resolution_Compl_SC_Small ...
Processing theory First_Order_Terms.Abstract_Unification ...
Processing theory First_Order_Terms.Unification ...
Processing theory DiskPaxos.DiskPaxos_Inv4 ...
Processing theory DiskPaxos.DiskPaxos_Inv5 ...
Processing theory DiskPaxos.DiskPaxos_Chosen ...
Processing theory DiskPaxos.DiskPaxos_Inv6 ...
Processing theory DiskPaxos.DiskPaxos_Invariant ...
Processing theory Dominance_CHK.Dom_Kildall_Property ...
Processing theory Dominance_CHK.Dom_Kildall_Correct ...
Removing 20 theories ...
Processing theory DiskPaxos.DiskPaxos ...
Processing theory Resolution_FOL.Resolution ...
Processing theory Resolution_FOL.Completeness ...
Loading 41 theories ...
Processing theory Resolution_FOL.Unification_Theorem ...
Processing theory Resolution_FOL.Completeness_Instance ...
Processing theory CISC-Kernel.Step_configuration ...
Processing theory CISC-Kernel.Step_policies ...
Processing theory CISC-Kernel.List_Theorems ...
Processing theory CISC-Kernel.Option_Binders ...
Processing theory CISC-Kernel.K ...
Processing theory Modular_Assembly_Kit_Security.StateEventSystems ...
Processing theory Modular_Assembly_Kit_Security.UnwindingConditions ...
Processing theory Modular_Assembly_Kit_Security.AuxiliaryLemmas ...
Processing theory Modular_Assembly_Kit_Security.UnwindingResults ...
Processing theory CISC-Kernel.Step ...
Processing theory CISC-Kernel.Step_invariants ...
Processing theory CISC-Kernel.Step_vpeq ...
Processing theory CISC-Kernel.Step_vpeq_locally_respects ...
Processing theory CISC-Kernel.Step_vpeq_weakly_step_consistent ...
Removing 23 theories ...
Processing theory CISC-Kernel.SK ...
Processing theory CISC-Kernel.ISK ...
Processing theory Correctness_Algebras.Binary_Iterings ...
Processing theory CISC-Kernel.CISK ...
Processing theory CISC-Kernel.Separation_kernel_model ...
Processing theory CISC-Kernel.Link_separation_kernel_model_to_CISK ...
Processing theory Correctness_Algebras.Binary_Iterings_Strict ...
Processing theory TESL_Language.TESL ...
Processing theory TESL_Language.Run ...
Processing theory TESL_Language.Denotational ...
Processing theory TESL_Language.SymbolicPrimitive ...
Processing theory TESL_Language.Operational ...
Processing theory CSP_RefTK.Conclusion ...
Processing theory CSP_RefTK.Introduction ...
Processing theory HOL-CSP.Introduction ...
Processing theory TESL_Language.Corecursive_Prop ...
Processing theory Propositional_Proof_Systems.SC_Depth ...
Processing theory Propositional_Proof_Systems.SC_Gentzen ...
Processing theory Propositional_Proof_Systems.SC_Depth_Limit ...
Removing 55 theories ...
Processing theory TESL_Language.Hygge_Theory ...
Processing theory TESL_Language.Config_Morphisms ...
Processing theory Correctness_Algebras.N_Algebras ...
Processing theory Correctness_Algebras.Recursion ...
Processing theory Stone_Relation_Algebras.Relation_Algebras ...
Removing 5 theories ...
Processing theory Correctness_Algebras.N_Omega_Algebras ...
Processing theory Correctness_Algebras.N_Relation_Algebras ...
Removing 2 theories ...
Processing theory Correctness_Algebras.N_Omega_Binary_Iterings ...
Loading 58 theories ...
Processing theory Modular_Assembly_Kit_Security.InformationFlowProperties ...
Processing theory Possibilistic_Noninterference.MyTactics ...
Processing theory Possibilistic_Noninterference.Interface ...
Processing theory Possibilistic_Noninterference.Bisim ...
Processing theory Modular_Assembly_Kit_Security.PropertyLibrary ...
Processing theory Ribbon_Proofs.JHelper ...
Processing theory Decl_Sem_Fun_PL.Lambda ...
Processing theory Decl_Sem_Fun_PL.SmallStepLam ...
Processing theory Ribbon_Proofs.Proofchain ...
Processing theory Ribbon_Proofs.Ribbons_Basic ...
Processing theory Resolution_FOL.Examples ...
Processing theory Decl_Sem_Fun_PL.ValuesFSet ...
Processing theory Decl_Sem_Fun_PL.DeclSemAsDenotFSet ...
Processing theory Decl_Sem_Fun_PL.ValuesFSetProps ...
Processing theory Decl_Sem_Fun_PL.BigStepLam ...
Processing theory Decl_Sem_Fun_PL.ChangeEnv ...
Processing theory Possibilistic_Noninterference.Language_Semantics ...
Removing 13 theories ...
Processing theory Decl_Sem_Fun_PL.DenotSoundFSet ...
Processing theory Decl_Sem_Fun_PL.DenotCompleteFSet ...
Processing theory Possibilistic_Noninterference.During_Execution ...
Processing theory Decl_Sem_Fun_PL.DenotCongruenceFSet ...
Processing theory Kleene_Algebra.Dioid_Models ...
Processing theory Decl_Sem_Fun_PL.DenotEqualitiesFSet ...
Processing theory Possibilistic_Noninterference.After_Execution ...
Processing theory Decl_Sem_Fun_PL.Optimizer ...
Processing theory Ribbon_Proofs.Ribbons_Interfaces ...
Processing theory Kleene_Algebra.Kleene_Algebra_Models ...
Processing theory Finite-Map-Extras.Finite_Map_Extras ...
Processing theory Ribbon_Proofs.More_Finite_Map ...
Processing theory Key_Agreement_Strong_Adversaries.dhlvl2 ...
Processing theory Ribbon_Proofs.Ribbons_Graphical ...
Processing theory KAD.Modal_Kleene_Algebra_Models ...
Processing theory Possibilistic_Noninterference.Compositionality ...
Processing theory Ribbon_Proofs.Ribbons_Graphical_Soundness ...
Processing theory CCS.Agent ...
Processing theory CCS.Strong_Sim ...
Processing theory CCS.Strong_Bisim ...
Processing theory CCS.Strong_Sim_Pres ...
Processing theory CCS.Strong_Bisim_Pres ...
Processing theory CCS.Struct_Cong ...
Processing theory CCS.Tau_Chain ...
Processing theory CCS.Weak_Cong_Semantics ...
Processing theory CCS.Weak_Semantics ...
Removing 19 theories ...
Processing theory CCS.Strong_Sim_SC ...
Processing theory CCS.Strong_Bisim_SC ...
Processing theory CCS.Weak_Sim ...
Processing theory CCS.Weak_Bisim ...
Processing theory CCS.Weak_Cong_Sim ...
Processing theory CCS.Weak_Cong_Sim_Pres ...
Processing theory CCS.Weak_Sim_Pres ...
Processing theory Possibilistic_Noninterference.Syntactic_Criteria ...
Processing theory Possibilistic_Noninterference.Concrete ...
Processing theory CCS.Weak_Bisim_Pres ...
Processing theory CCS.Weak_Cong ...
Processing theory CCS.Weak_Cong_Pres ...
Processing theory Key_Agreement_Strong_Adversaries.dhlvl3 ...
Processing theory Key_Agreement_Strong_Adversaries.dhlvl3_asymmetric ...
Processing theory Key_Agreement_Strong_Adversaries.dhlvl3_symmetric ...
Loading 37 theories ...
Removing 33 theories ...
Processing theory Security_Protocol_Refinement.Agents ...
Processing theory Security_Protocol_Refinement.Infra ...
Processing theory Security_Protocol_Refinement.Keys ...
Processing theory Security_Protocol_Refinement.Atoms ...
Processing theory Security_Protocol_Refinement.Runs ...
Processing theory SuperCalc.well_founded_continued ...
Processing theory Security_Protocol_Refinement.Channels ...
Processing theory Security_Protocol_Refinement.Refinement ...
Processing theory Security_Protocol_Refinement.Message ...
Processing theory Security_Protocol_Refinement.a0n_agree ...
Processing theory Security_Protocol_Refinement.a0i_agree ...
Processing theory SuperCalc.multisets_continued ...
Processing theory Well_Quasi_Orders.Multiset_Extension ...
Processing theory Security_Protocol_Refinement.s0g_secrecy ...
Processing theory Correctness_Algebras.Capped_Omega_Algebras ...
Processing theory Propositional_Proof_Systems.HC ...
Processing theory Propositional_Proof_Systems.ND ...
Processing theory Propositional_Proof_Systems.NDHC ...
Processing theory Propositional_Proof_Systems.SCND ...
Processing theory Propositional_Proof_Systems.HCSC ...
Processing theory Propositional_Proof_Systems.HCSCND ...
Processing theory Security_Protocol_Refinement.m1_keydist ...
Processing theory Well_Quasi_Orders.Wqo_Multiset ...
Processing theory SuperCalc.terms ...
Removing 6 theories ...
Processing theory SuperCalc.equational_clausal_logic ...
Processing theory Security_Protocol_Refinement.m1_keydist_iirn ...
Processing theory Security_Protocol_Refinement.m1_nssk ...
Processing theory SuperCalc.superposition ...
Processing theory Correctness_Algebras.Binary_Iterings_Nonstrict ...
Removing 12 theories ...
Processing theory Security_Protocol_Refinement.m1_kerberos ...
Processing theory Security_Protocol_Refinement.m2_nssk ...
Processing theory Security_Protocol_Refinement.m3_nssk ...
Processing theory Security_Protocol_Refinement.m3_nssk_par ...
Processing theory Security_Protocol_Refinement.m2_kerberos ...
Removing 4 theories ...
Processing theory Security_Protocol_Refinement.m3_kerberos5 ...
Processing theory Security_Protocol_Refinement.m3_kerberos_par ...
Removing 2 theories ...
Processing theory Security_Protocol_Refinement.m3_kerberos4 ...
Loading 34 theories ...
Processing theory Allen_Calculus.xor_cal ...
Processing theory Allen_Calculus.axioms ...
Processing theory Probabilistic_System_Zoo.Bool_Bounded_Set ...
Processing theory Noninterference_CSP.CSPNoninterference ...
Processing theory List_Interleaving.ListInterleaving ...
Processing theory Key_Agreement_Strong_Adversaries.pfslvl1 ...
Processing theory Optics.Lens_State ...
Processing theory Noninterference_Ipurge_Unwinding.IpurgeUnwinding ...
Processing theory Noninterference_Ipurge_Unwinding.DeterministicProcesses ...
Processing theory Noninterference_Inductive_Unwinding.InductiveUnwinding ...
Processing theory Euler_Partition.Euler_Partition ...
Processing theory Selection_Heap_Sort.Sort ...
Processing theory Selection_Heap_Sort.RemoveMax ...
Processing theory Propositional_Proof_Systems.MiniFormulas ...
Processing theory Probabilistic_System_Zoo.Finitely_Bounded_Set_Counterexample ...
Processing theory Selection_Heap_Sort.Heap ...
Processing theory Propositional_Proof_Systems.MiniSC ...
Processing theory Selection_Heap_Sort.HeapFunctional ...
Removing 26 theories ...
Processing theory Selection_Heap_Sort.HeapImperative ...
Processing theory Propositional_Proof_Systems.MiniSC_HC ...
Processing theory Propositional_Proof_Systems.ND_Sound ...
Processing theory Allen_Calculus.allen ...
Processing theory Allen_Calculus.jointly_exhaustive ...
Processing theory Propositional_Proof_Systems.ND_Compl_SC ...
Processing theory Propositional_Proof_Systems.SC_Compl_Consistency ...
Processing theory Allen_Calculus.disjoint_relations ...
Processing theory Propositional_Proof_Systems.MiniSC_Craig ...
Processing theory Key_Agreement_Strong_Adversaries.pfslvl2 ...
Processing theory Category2.MonadicEquationalTheory ...
Removing 18 theories ...
Processing theory Key_Agreement_Strong_Adversaries.pfslvl3 ...
Processing theory Key_Agreement_Strong_Adversaries.pfslvl3_asymmetric ...
Processing theory Key_Agreement_Strong_Adversaries.pfslvl3_symmetric ...
Removing 20 theories ...
Processing theory Allen_Calculus.examples ...
Processing theory Allen_Calculus.nest ...
Loading 55 theories ...
Processing theory SpecCheck.SpecCheck_Show ...
Processing theory SpecCheck.SpecCheck_Base ...
Processing theory SpecCheck.SpecCheck_Generators ...
Processing theory SpecCheck.SpecCheck_Shrink ...
Processing theory SpecCheck.SpecCheck_Output_Style ...
Processing theory SpecCheck.SpecCheck ...
Processing theory Clean.Test_Clean ...
Processing theory Clean.SquareRoot_concept ...
Processing theory Clean.Clean_Main ...
Processing theory Recursion-Theory-I.CPair ...
Processing theory Recursion-Theory-I.PRecFun ...
Processing theory Clean.Quicksort ...
Processing theory Clean.Quicksort_concept ...
Removing 14 theories ...
Processing theory Recursion-Theory-I.PRecFinSet ...
Processing theory Regular-Sets.Derivatives ...
Processing theory TLA.Intensional ...
Processing theory TLA.Sequence ...
Processing theory Recursion-Theory-I.PRecList ...
Processing theory TLA.Semantics ...
Processing theory TLA.PreFormulas ...
Processing theory Recursion-Theory-I.PRecFun2 ...
Processing theory Relational_Method.Definitions ...
Processing theory TLA.Rules ...
Processing theory TLA.Liveness ...
Processing theory TLA.State ...
Processing theory TLA.Even ...
Processing theory Recursion-Theory-I.PRecUnGr ...
Processing theory Recursion-Theory-I.RecEnSet ...
Processing theory Ordinals_and_Cardinals.Cardinal_Order_Relation_discontinued ...
Processing theory Selection_Heap_Sort.SelectionSort_Functional ...
Processing theory TLA.Buffer ...
Processing theory Regex_Equivalence.Derivatives_Finite ...
Processing theory TLA.Inc ...
Removing 29 theories ...
Processing theory Imperative_Insertion_Sort.Imperative_Loops ...
Processing theory Separata.Separata ...
Processing theory Pairing_Heap.Pairing_Heap_Tree ...
Processing theory Regex_Equivalence.Deriv_PDeriv ...
Processing theory Skew_Heap.Skew_Heap ...
Processing theory Pairing_Heap.Pairing_Heap_List2 ...
Processing theory Pairing_Heap.Pairing_Heap_List1 ...
Processing theory Tail_Recursive_Functions.CaseStudy2 ...
Processing theory Regex_Equivalence.Automaton ...
Processing theory Imperative_Insertion_Sort.Imperative_Insertion_Sort ...
Processing theory Splay_Tree.Splay_Heap ...
Processing theory Regex_Equivalence.Deriv_Autos ...
Processing theory Regex_Equivalence.Position_Autos ...
Processing theory Regex_Equivalence.After2 ...
Processing theory Regex_Equivalence.Before2 ...
Processing theory Regex_Equivalence.Regex_Equivalence ...
Processing theory Regex_Equivalence.Benchmark ...
Removing 15 theories ...
Processing theory Regex_Equivalence.Examples ...
Removing 12 theories ...
Processing theory Relational_Method.Authentication ...
Processing theory Relational_Method.Anonymity ...
Processing theory Relational_Method.Possibility ...
Loading 62 theories ...
Processing theory BNF_CC.Preliminaries ...
Processing theory FLP.ListUtilities ...
Processing theory FLP.Multiset ...
Processing theory Graph_Saturation.MissingRelation ...
Processing theory Statecharts.Contrib ...
Processing theory Coinductive_Languages.Coinductive_Language ...
Processing theory Graph_Saturation.LabeledGraphs ...
Processing theory Graph_Saturation.RulesAndChains ...
Processing theory FLP.AsynchronousSystem ...
Processing theory Graph_Saturation.LabeledGraphSemantics ...
Processing theory Graph_Saturation.StandardModels ...
Removing 4 theories ...
Processing theory Statecharts.DataSpace ...
Processing theory Statecharts.Data ...
Processing theory FLP.Execution ...
Processing theory FLP.FLPSystem ...
Processing theory Statecharts.Update ...
Processing theory Statecharts.Expr ...
Processing theory Statecharts.SA ...
Processing theory Graph_Saturation.RuleSemanticsConnection ...
Processing theory WOOT_Strong_Eventual_Consistency.ErrorMonad ...
Processing theory FLP.FLPTheorem ...
Processing theory FLP.FLPExistingSystem ...
Processing theory WOOT_Strong_Eventual_Consistency.Data ...
Processing theory KAD.Modal_Kleene_Algebra_Applications ...
Processing theory Statecharts.Kripke ...
Processing theory WOOT_Strong_Eventual_Consistency.BasicAlgorithms ...
Processing theory WOOT_Strong_Eventual_Consistency.CreateAlgorithms ...
Processing theory Graph_Saturation.GraphRewriting ...
Processing theory Graph_Saturation.StandardRules ...
Processing theory Statecharts.HA ...
Processing theory WOOT_Strong_Eventual_Consistency.IntegrateAlgorithm ...
Processing theory Network_Security_Policy_Verification.Analysis_Tainting ...
Processing theory Van_Emde_Boas_Trees.Imperative_HOL_Add ...
Processing theory Decl_Sem_Fun_PL.MutableRef ...
Processing theory Graph_Saturation.CombinedCorrectness ...
Processing theory Decl_Sem_Fun_PL.MutableRefProps ...
Processing theory Decl_Sem_Fun_PL.RelationalSemFSet ...
Processing theory Decl_Sem_Fun_PL.EquivRelationalDenotFSet ...
Processing theory Decl_Sem_Fun_PL.DeclSemAsNDInterpFSet ...
Processing theory Coinductive_Languages.Context_Free_Grammar ...
Processing theory Decl_Sem_Fun_PL.SystemF ...
Removing 43 theories ...
Processing theory WOOT_Strong_Eventual_Consistency.SortKeys ...
Processing theory Ribbon_Proofs.Ribbons_Stratified ...
Processing theory WOOT_Strong_Eventual_Consistency.DistributedExecution ...
Processing theory WOOT_Strong_Eventual_Consistency.Sorting ...
Processing theory Well_Quasi_Orders.Kruskal ...
Processing theory Well_Quasi_Orders.Wqo_Instances ...
Processing theory Statecharts.HAOps ...
Processing theory BNF_CC.Concrete_Examples ...
Processing theory BNF_CC.DDS ...
Processing theory Lam-ml-Normalization.Lam_ml ...
Processing theory Well_Quasi_Orders.Kruskal_Examples ...
Processing theory WOOT_Strong_Eventual_Consistency.Psi ...
Processing theory WOOT_Strong_Eventual_Consistency.Consistency ...
Processing theory WOOT_Strong_Eventual_Consistency.CreateConsistent ...
Processing theory Statecharts.HASem ...
Processing theory Statecharts.HAKripke ...
Processing theory Statecharts.CarAudioSystem ...
Removing 25 theories ...
Processing theory WOOT_Strong_Eventual_Consistency.IntegrateInsertCommute ...
Processing theory WOOT_Strong_Eventual_Consistency.StrongConvergence ...
Processing theory WOOT_Strong_Eventual_Consistency.SEC ...
Processing theory WOOT_Strong_Eventual_Consistency.Example ...
Loading 49 theories ...
Processing theory Consensus_Refined.Consensus_Types ...
Processing theory Consensus_Refined.Quorums ...
Processing theory Consensus_Refined.Infra ...
Processing theory Consensus_Refined.Consensus_Misc ...
Processing theory Consensus_Refined.Two_Steps ...
Processing theory Clean.LinearSearch ...
Processing theory Consensus_Refined.Refinement ...
Processing theory Consensus_Refined.Voting ...
Processing theory Consensus_Refined.Same_Vote ...
Processing theory Heard_Of.Majorities ...
Processing theory POPLmark-deBruijn.Basis ...
Processing theory Heard_Of.HOModel ...
Processing theory Consensus_Refined.HO_Transition_System ...
Processing theory Consensus_Refined.BenOr_Defs ...
Processing theory Consensus_Refined.Uv_Defs ...
Processing theory Foundation_of_geometry.Incidence ...
Processing theory Heard_Of.AteDefs ...
Processing theory Heard_Of.EigbyzDefs ...
Processing theory Consensus_Refined.Observing_Quorums ...
Processing theory Consensus_Refined.Observing_Quorums_Opt ...
Processing theory Consensus_Refined.Two_Step_Observing ...
Processing theory Heard_Of.OneThirdRuleDefs ...
Processing theory Stuttering_Equivalence.Samplers ...
Processing theory Stuttering_Equivalence.StutterEquivalence ...
Processing theory Foundation_of_geometry.Order ...
Processing theory Heard_Of.UteDefs ...
Processing theory Heard_Of.LastVotingDefs ...
Processing theory Heard_Of.UvDefs ...
Removing 26 theories ...
Processing theory Heard_Of.Reduction ...
Processing theory Consensus_Refined.BenOr_Proofs ...
Processing theory POPLmark-deBruijn.POPLmarkRecord ...
Processing theory POPLmark-deBruijn.POPLmarkRecordCtxt ...
Processing theory POPLmark-deBruijn.Execute ...
Processing theory Heard_Of.OneThirdRuleProof ...
Processing theory Consensus_Refined.Uv_Proofs ...
Processing theory Heard_Of.AteProof ...
Processing theory Heard_Of.EigbyzProof ...
Processing theory PropResPI.Propositional_Resolution ...
Processing theory PropResPI.Prime_Implicates ...
Processing theory Propositional_Proof_Systems.Compactness_Consistency ...
Processing theory Heard_Of.LastVotingProof ...
Processing theory Heard_Of.UteProof ...
Processing theory Heard_Of.UvProof ...
Processing theory Network_Security_Policy_Verification.Example_NetModel ...
Processing theory Propositional_Proof_Systems.Resolution_Compl_Consistency ...
Processing theory Network_Security_Policy_Verification.SINVAR_BLPstrict ...
Processing theory Network_Security_Policy_Verification.SINVAR_Subnets2 ...
Removing 41 theories ...
Processing theory Propositional_Proof_Systems.HC_Compl_Consistency ...
Processing theory Foundation_of_geometry.Congruence ...
Loading 62 theories ...
Processing theory ConcurrentIMP.CIMP_pred ...
Processing theory ConcurrentIMP.Infinite_Sequences ...
Processing theory ConcurrentIMP.LTL ...
Processing theory Diophantine_Eqns_Lin_Hom.List_Vector ...
Removing 6 theories ...
Processing theory Complete_Non_Orders.Binary_Relations ...
Processing theory Complete_Non_Orders.Complete_Relations ...
Processing theory Complete_Non_Orders.Kleene_Fixed_Point ...
Processing theory Complete_Non_Orders.Fixed_Points ...
Processing theory Diophantine_Eqns_Lin_Hom.Linear_Diophantine_Equations ...
Processing theory Diophantine_Eqns_Lin_Hom.Sorted_Wrt ...
Processing theory Diophantine_Eqns_Lin_Hom.Minimize_Wrt ...
Processing theory Myhill-Nerode.Folds ...
Processing theory SIFUM_Type_Systems.Preliminaries ...
Processing theory ConcurrentIMP.CIMP_lang ...
Processing theory Concurrent_Revisions.Data ...
Processing theory Concurrent_Revisions.Occurrences ...
Processing theory Concurrent_Revisions.Renaming ...
Processing theory Concurrent_Revisions.Substitution ...
Processing theory Diophantine_Eqns_Lin_Hom.Simple_Algorithm ...
Processing theory SIFUM_Type_Systems.Security ...
Processing theory ConcurrentIMP.CIMP_vcg ...
Processing theory ConcurrentIMP.CIMP_vcg_rules ...
Processing theory ConcurrentIMP.CIMP ...
Processing theory ConcurrentIMP.CIMP_locales ...
Processing theory SIFUM_Type_Systems.Language ...
Processing theory Concurrent_Revisions.OperationalSemantics ...
Processing theory Concurrent_Revisions.Executions ...
Processing theory ConcurrentIMP.CIMP_one_place_buffer ...
Removing 6 theories ...
Processing theory Security_Protocol_Refinement.m1_keydist_inrn ...
Processing theory Diophantine_Eqns_Lin_Hom.Algorithm ...
Processing theory Diophantine_Eqns_Lin_Hom.Solver_Code ...
Processing theory Topological_Semantics.sse_boolean_algebra ...
Processing theory Topological_Semantics.sse_boolean_algebra_quantification ...
Processing theory Security_Protocol_Refinement.m1_ds ...
Processing theory SIFUM_Type_Systems.Compositionality ...
Processing theory Topological_Semantics.sse_operation_positive ...
Processing theory Concurrent_Revisions.Determinacy ...
Removing 14 theories ...
Processing theory Topological_Semantics.sse_operation_positive_quantification ...
Processing theory Security_Protocol_Refinement.m2_ds ...
Processing theory SIFUM_Type_Systems.TypeSystem ...
Processing theory Topological_Semantics.sse_operation_negative ...
Processing theory Topological_Semantics.topo_operators_basic ...
Processing theory Topological_Semantics.sse_operation_negative_quantification ...
Processing theory Card_Equiv_Relations.Card_Equiv_Relations ...
Processing theory Propositional_Proof_Systems.ND_Compl_Truthtable ...
Processing theory Propositional_Proof_Systems.ND_Compl_Truthtable_Compact ...
Processing theory Security_Protocol_Refinement.m3_ds ...
Processing theory Security_Protocol_Refinement.m3_ds_par ...
Processing theory Topological_Semantics.topo_frontier_algebra ...
Removing 13 theories ...
Processing theory Topological_Semantics.topo_strict_implication ...
Processing theory Propositional_Proof_Systems.Tseytin ...
Processing theory Propositional_Proof_Systems.Tseytin_Sema ...
Processing theory Equivalence_Relation_Enumeration.Equivalence_Relation_Enumeration ...
Processing theory Myhill-Nerode.Myhill_1 ...
Processing theory Myhill-Nerode.Myhill_2 ...
Processing theory Myhill-Nerode.Myhill ...
Processing theory ConcurrentIMP.CIMP_unbounded_buffer ...
Processing theory Myhill-Nerode.Closures ...
Processing theory Myhill-Nerode.Closures2 ...
Removing 23 theories ...
Processing theory Topological_Semantics.topo_negation_conditions ...
Processing theory Topological_Semantics.ex_LFIs ...
Processing theory Topological_Semantics.ex_subminimal_logics ...
Loading 79 theories ...
Removing 4 theories ...
Processing theory FocusStreamsCaseStudies.ListExtras ...
Processing theory FocusStreamsCaseStudies.ArithExtras ...
Processing theory Attack_Trees.MC ...
Processing theory JiveDataStoreModel.TypeIds ...
Processing theory FocusStreamsCaseStudies.stream ...
Processing theory FocusStreamsCaseStudies.BitBoolTS ...
Processing theory FocusStreamsCaseStudies.Gateway_types ...
Processing theory FocusStreamsCaseStudies.Gateway ...
Processing theory JiveDataStoreModel.JavaType ...
Processing theory JiveDataStoreModel.DirectSubtypes ...
Processing theory JiveDataStoreModel.Subtype ...
Processing theory JiveDataStoreModel.Attributes ...
Processing theory JiveDataStoreModel.AttributesIndep ...
Processing theory Attack_Trees.AT ...
Processing theory Attack_Trees.Infrastructure ...
Processing theory Attack_Trees.GDPRhealthcare ...
Processing theory JiveDataStoreModel.Value ...
Processing theory JiveDataStoreModel.Location ...
Processing theory JiveDataStoreModel.Store ...
Processing theory LatticeProperties.Lattice_Prop ...
Processing theory JiveDataStoreModel.StoreProperties ...
Processing theory JiveDataStoreModel.JML ...
Processing theory JiveDataStoreModel.UnivSpec ...
Processing theory PseudoHoops.Operations ...
Processing theory FocusStreamsCaseStudies.Gateway_proof_aux ...
Processing theory LatticeProperties.Modular_Distrib_Lattice ...
Processing theory LatticeProperties.Lattice_Ordered_Group ...
Processing theory PseudoHoops.LeftComplementedMonoid ...
Processing theory PseudoHoops.RightComplementedMonoid ...
Processing theory SIFPL.OBJ ...
Processing theory SIFPL.PBIJ ...
Processing theory PseudoHoops.PseudoWaisbergAlgebra ...
Processing theory Finger-Trees.FingerTree ...
Processing theory Strong_Security.Types ...
Processing theory FocusStreamsCaseStudies.Gateway_proof ...
Processing theory WHATandWHERE_Security.WHATWHERE_Security ...
Processing theory SIFPL.VDM_OBJ ...
Processing theory Strong_Security.Expr ...
Processing theory Strong_Security.Domain_example ...
Processing theory WHATandWHERE_Security.MWLs ...
Removing 20 theories ...
Processing theory WHATandWHERE_Security.Up_To_Technique ...
Processing theory WHATandWHERE_Security.Parallel_Composition ...
Processing theory WHATandWHERE_Security.WHATWHERE_Secure_Skip_Assign ...
Processing theory PseudoHoops.PseudoHoops ...
Processing theory PseudoHoops.PseudoHoopFilters ...
Processing theory SIFPL.VS_OBJ ...
Processing theory WHATandWHERE_Security.Language_Composition ...
Processing theory TESL_Language.StutteringDefs ...
Processing theory WHATandWHERE_Security.Type_System ...
Processing theory WHATandWHERE_Security.Type_System_example ...
Processing theory SIFPL.ContextOBJ ...
Processing theory HyperCTL.Prelim ...
Processing theory Topological_Semantics.topo_operators_derivative ...
Processing theory Finger-Trees.Test ...
Processing theory TESL_Language.StutteringLemmas ...
Processing theory TESL_Language.Stuttering ...
Processing theory Topological_Semantics.topo_derivative_algebra ...
Processing theory HyperCTL.Shallow ...
Processing theory HyperCTL.Deep ...
Processing theory Propositional_Proof_Systems.MiniFormulas_Sema ...
Processing theory Topological_Semantics.ex_LFUs ...
Processing theory Propositional_Proof_Systems.CNF_To_Formula ...
Processing theory Propositional_Proof_Systems.ND_FiniteAssms ...
Processing theory Propositional_Proof_Systems.Substitution ...
Processing theory Propositional_Proof_Systems.Substitution_Sema ...
Processing theory Propositional_Proof_Systems.Sema_Craig ...
Processing theory Propositional_Proof_Systems.Resolution_Sound ...
Processing theory BNF_CC.Axiomatised_BNF_CC ...
Processing theory HyperCTL.Noninterference ...
Removing 41 theories ...
Processing theory PseudoHoops.SpecialPseudoHoops ...
Processing theory Correctness_Algebras.Boolean_Semirings ...
Processing theory BNF_CC.Quotient_Preservation ...
Processing theory BNF_CC.Subtypes ...
Processing theory HyperCTL.Finite_Noninterference ...
Processing theory HyperCTL.HyperCTL ...
Processing theory BNF_CC.Composition ...
Processing theory BNF_CC.Fixpoints ...
Processing theory BNF_CC.Operation_Examples ...
Processing theory PseudoHoops.Examples ...
Loading 48 theories ...
Processing theory Dict_Construction.Dict_Construction ...
Processing theory Consensus_Refined.Three_Steps ...
Processing theory Consensus_Refined.MRU_Vote ...
Processing theory Belief_Revision.AGM_Logic ...
Processing theory Belief_Revision.AGM_Remainder ...
Processing theory Consensus_Refined.MRU_Vote_Opt ...
Processing theory Consensus_Refined.Three_Step_MRU ...
Processing theory Consensus_Refined.New_Algorithm_Defs ...
Processing theory Consensus_Refined.CT_Defs ...
Processing theory Consensus_Refined.Paxos_Defs ...
Processing theory FeatherweightJava.FJDefs ...
Processing theory AWN.AWN_Term_Graph ...
Removing 36 theories ...
Processing theory Consensus_Refined.New_Algorithm_Proofs ...
Processing theory Consensus_Refined.Paxos_Proofs ...
Processing theory Lazy_Case.Lazy_Case ...
Processing theory Mereology.PM ...
Processing theory Mereology.M ...
Processing theory FeatherweightJava.FJAux ...
Processing theory FeatherweightJava.FJSound ...
Processing theory Consensus_Refined.CT_Proofs ...
Processing theory Mereology.CM ...
Processing theory Mereology.GM ...
Processing theory Mereology.MM ...
Processing theory Mereology.EM ...
Processing theory Mereology.CEM ...
Processing theory Mereology.GMM ...
Processing theory Open_Induction.Open_Induction ...
Processing theory Mereology.GEM ...
Processing theory Topological_Semantics.topo_negation_fixedpoints ...
Processing theory Belief_Revision.AGM_Contraction ...
Processing theory Belief_Revision.AGM_Revision ...
Processing theory FeatherweightJava.Execute ...
Processing theory FeatherweightJava.Featherweight_Java ...
Processing theory ADS_Functor.Merkle_Interface ...
Processing theory HereditarilyFinite.Ordinal ...
Processing theory FOL_Axiomatic.FOL_Axiomatic ...
Processing theory Dict_Construction.Test_Lazy_Case ...
Processing theory Boolean_Expression_Checkers.Boolean_Expression_Checkers ...
Processing theory Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping ...
Processing theory ADS_Functor.ADS_Construction ...
Processing theory FinFun.FinFunPred ...
Processing theory ADS_Functor.Inclusion_Proof_Construction ...
Processing theory Finite_Automata_HF.Finite_Automata_HF ...
Processing theory Van_Emde_Boas_Trees.Heap ...
Removing 44 theories ...
Processing theory Boolean_Expression_Checkers.Boolean_Expression_Example ...
Processing theory Well_Quasi_Orders.Higman_OI ...
Processing theory ADS_Functor.Canton_Transaction_Tree ...
Processing theory Hybrid_Logic.Hybrid_Logic ...
Loading 103 theories ...
Processing theory Abs_Int_ITP2012.Complete_Lattice_ix ...
Processing theory Functional-Automata.AutoProj ...
Processing theory Functional-Automata.DA ...
Processing theory Functional-Automata.NA ...
Processing theory Functional-Automata.NAe ...
Processing theory Consensus_Refined.Voting_Opt ...
Processing theory Functional-Automata.Automata ...
Processing theory GraphMarkingIBP.Graph ...
Processing theory Consensus_Refined.Ate_Defs ...
Processing theory Consensus_Refined.OneThirdRule_Defs ...
Processing theory Consensus_Refined.Ate_Proofs ...
Processing theory InfPathElimination.Aexp ...
Processing theory InfPathElimination.Bexp ...
Processing theory Consensus_Refined.OneThirdRule_Proofs ...
Processing theory InfPathElimination.Store ...
Processing theory InfPathElimination.Conf ...
Processing theory DataRefinementIBP.Preliminaries ...
Processing theory DataRefinementIBP.Statements ...
Processing theory DataRefinementIBP.Hoare ...
Processing theory DataRefinementIBP.Diagram ...
Processing theory InfPathElimination.Graph ...
Processing theory DataRefinementIBP.DataRefinement ...
Processing theory InfPathElimination.Labels ...
Removing 35 theories ...
Processing theory Inductive_Confidentiality.Message ...
Processing theory Inductive_Confidentiality.Event ...
Processing theory Inductive_Confidentiality.Public ...
Processing theory Inductive_Confidentiality.NS_Public_Bad ...
Processing theory Inductive_Confidentiality.ConfidentialityDY ...
Processing theory GraphMarkingIBP.SetMark ...
Processing theory GraphMarkingIBP.StackMark ...
Processing theory MonoBoolTranAlgebra.Statements ...
Processing theory InfPathElimination.SymExec ...
Processing theory InfPathElimination.LTS ...
Processing theory InfPathElimination.SubRel ...
Processing theory InfPathElimination.ArcExt ...
Processing theory GraphMarkingIBP.LinkMark ...
Processing theory Menger.Helpers ...
Processing theory Menger.Graph ...
Processing theory Menger.Separations ...
Processing theory Menger.DisjointPaths ...
Processing theory Menger.MengerInduction ...
Processing theory Menger.Y_eq_new_last ...
Processing theory Partial_Function_MR.Partial_Function_MR ...
Processing theory Functional-Automata.RegSet_of_nat_DA ...
Processing theory InfPathElimination.SubExt ...
Processing theory OpSets.OpSet ...
Processing theory Functional-Automata.RegExp2NA ...
Processing theory GraphMarkingIBP.DSWMark ...
Processing theory Menger.Y_neq_new_last ...
Processing theory Menger.Menger ...
Processing theory Security_Protocol_Refinement.m1_auth ...
Processing theory OpSets.Insert_Spec ...
Processing theory Functional-Automata.RegExp2NAe ...
Processing theory Functional-Automata.AutoRegExp ...
Processing theory Functional-Automata.Execute ...
Processing theory Security_Protocol_Refinement.m2_auth_chan ...
Processing theory OpSets.List_Spec ...
Removing 31 theories ...
Processing theory OpSets.Interleaving ...
Processing theory OpSets.RGA ...
Processing theory Security_Protocol_Refinement.m3_sig ...
Processing theory Strong_Security.Strong_Security ...
Processing theory Strong_Security.Up_To_Technique ...
Processing theory Strong_Security.MWLf ...
Processing theory Strong_Security.Parallel_Composition ...
Processing theory Strong_Security.Strongly_Secure_Skip_Assign ...
Processing theory Topological_Semantics.topo_border_algebra ...
Processing theory Topological_Semantics.topo_closure_algebra ...
Processing theory Strong_Security.Language_Composition ...
Processing theory Topological_Semantics.topo_interior_algebra ...
Processing theory Security_Protocol_Refinement.m2_confid_chan ...
Processing theory Strong_Security.Type_System ...
Processing theory Strong_Security.Type_System_example ...
Removing 21 theories ...
Processing theory Security_Protocol_Refinement.m3_enc ...
Processing theory VolpanoSmith.Semantics ...
Processing theory VolpanoSmith.secTypes ...
Processing theory VolpanoSmith.Execute ...
Processing theory Abs_Int_ITP2012.ACom ...
Processing theory Certification_Monads.Parser_Monad ...
Processing theory Certification_Monads.Strict_Sum ...
Processing theory Functional-Automata.MaxPrefix ...
Processing theory Abs_Int_ITP2012.Collecting ...
Processing theory XML.Xml ...
Processing theory Partial_Function_MR.Partial_Function_MR_Examples ...
Processing theory LinearQuantifierElim.PresArith ...
Processing theory Functional-Automata.MaxChop ...
Processing theory Functional-Automata.AutoMaxChop ...
Processing theory Functional-Automata.Functional_Automata ...
Processing theory Myhill-Nerode.Non_Regular_Languages ...
Processing theory LinearQuantifierElim.Cooper ...
Processing theory XML.Xmlt ...
Processing theory LinearQuantifierElim.QEpres ...
Processing theory Abs_Int_ITP2012.Abs_Int0 ...
Processing theory Abs_Int_ITP2012.Abs_State ...
Processing theory Abs_Int_ITP2012.Abs_Int1 ...
Removing 55 theories ...
Processing theory Abs_Int_ITP2012.Abs_Int2 ...
Processing theory Abs_Int_ITP2012.Abs_Int2_ivl ...
Processing theory Abs_Int_ITP2012.Abs_Int3 ...
Removing 4 theories ...
Processing theory InfPathElimination.RB ...
Loading 94 theories ...
Processing theory BytecodeLogicJmlTypes.AssocLists ...
Processing theory Dict_Construction.Test_Side_Conditions ...
Processing theory CryptoBasedCompositionalProperties.ListExtras ...
Processing theory Concurrent_Ref_Alg.Refinement_Lattice ...
Processing theory Concurrent_Ref_Alg.Conjunction ...
Processing theory Concurrent_Ref_Alg.Galois_Connections ...
Processing theory Concurrent_Ref_Alg.Infimum_Nat ...
Processing theory Concurrent_Ref_Alg.Parallel ...
Processing theory Concurrent_Ref_Alg.Sequential ...
Processing theory Concurrent_Ref_Alg.CRA ...
Processing theory Concurrent_Ref_Alg.Iteration ...
Processing theory Concurrent_Ref_Alg.Conjunctive_Sequential ...
Processing theory Dict_Construction.Termination ...
Processing theory FocusStreamsCaseStudies.FR_types ...
Processing theory FocusStreamsCaseStudies.FR ...
Processing theory FocusStreamsCaseStudies.SteamBoiler ...
Processing theory FocusStreamsCaseStudies.FR_proof ...
Processing theory Concurrent_Ref_Alg.Conjunctive_Iteration ...
Processing theory Concurrent_Ref_Alg.Rely_Quotient ...
Processing theory FocusStreamsCaseStudies.SteamBoiler_proof ...
Processing theory CryptoBasedCompositionalProperties.Secrecy_types ...
Processing theory CryptoBasedCompositionalProperties.inout ...
Processing theory CryptoBasedCompositionalProperties.Secrecy ...
Processing theory CryptoBasedCompositionalProperties.CompLocalSecrets ...
Processing theory CryptoBasedCompositionalProperties.KnowledgeKeysSecrets ...
Processing theory MiniML.Maybe ...
Processing theory Inductive_Confidentiality.MessageGA ...
Processing theory Inductive_Confidentiality.EventGA ...
Processing theory Inductive_Confidentiality.PublicGA ...
Processing theory Inductive_Confidentiality.NS_Public_Bad_GA ...
Processing theory Inductive_Confidentiality.ConfidentialityGA ...
Processing theory MiniML.Type ...
Processing theory Logging_Independent_Anonymity.Definitions ...
Processing theory BytecodeLogicJmlTypes.Language ...
Processing theory BytecodeLogicJmlTypes.Logic ...
Processing theory BytecodeLogicJmlTypes.MultiStep ...
Processing theory BytecodeLogicJmlTypes.Reachability ...
Removing 38 theories ...
Processing theory Inductive_Confidentiality.Knowledge ...
Processing theory MiniML.Instance ...
Processing theory MiniML.Generalize ...
Processing theory Modular_Assembly_Kit_Security.SecureSystems ...
Processing theory Name_Carrying_Type_Inference.Fresh ...
Processing theory MiniML.MiniML ...
Processing theory MiniML.W ...
Processing theory Name_Carrying_Type_Inference.Permutation ...
Processing theory Name_Carrying_Type_Inference.PreSimplyTyped ...
Processing theory Logging_Independent_Anonymity.Anonymity ...
Removing 18 theories ...
Processing theory No_FTL_observers.SomeFunc ...
Processing theory Logging_Independent_Anonymity.Possibility ...
Processing theory BytecodeLogicJmlTypes.Sound ...
Processing theory Name_Carrying_Type_Inference.SimplyTyped ...
Processing theory Projective_Geometry.Projective_Plane_Axioms ...
Processing theory PSemigroupsConvolution.Partial_Semigroups ...
Processing theory SIFPL.IMP ...
Processing theory BytecodeLogicJmlTypes.Cachera ...
Removing 14 theories ...
Processing theory Projective_Geometry.Pappus_Property ...
Processing theory Schutz_Spacetime.Util ...
Processing theory SIFPL.VDM ...
Processing theory Schutz_Spacetime.TernaryOrdering ...
Processing theory SIFPL.VS ...
Processing theory Tree_Decomposition.Graph ...
Processing theory SIFPL.ContextVS ...
Processing theory PSemigroupsConvolution.Quantales ...
Processing theory PSemigroupsConvolution.Binary_Modalities ...
Processing theory PSemigroupsConvolution.Partial_Semigroup_Lifting ...
Processing theory PSemigroupsConvolution.Unary_Modalities ...
Processing theory Projective_Geometry.Pascal_Property ...
Processing theory Projective_Geometry.Desargues_Property ...
Processing theory Tree_Decomposition.Tree ...
Processing theory VeriComp.Fixpoint ...
Processing theory Tree_Decomposition.TreeDecomposition ...
Processing theory Tree_Decomposition.TreewidthCompleteGraph ...
Processing theory Tree_Decomposition.TreewidthTree ...
Processing theory Schutz_Spacetime.Minkowski ...
Processing theory Tree_Decomposition.ExampleInstantiations ...
Removing 21 theories ...
Processing theory ArrowImpossibilityGS.Arrow_Order ...
Processing theory ArrowImpossibilityGS.GS ...
Processing theory Sunflowers.Sunflower ...
Processing theory Sunflowers.Erdos_Rado_Sunflower ...
Processing theory Category.Cat ...
Processing theory Category.Functors ...
Processing theory Category.NatTrans ...
Processing theory Category.SetCat ...
Processing theory Category.HomFunctors ...
Processing theory Category.Yoneda ...
Processing theory Approximation_Algorithms.Approx_MIS_Hoare ...
Removing 13 theories ...
Processing theory Dict_Construction.Test_Dict_Construction ...
Removing 7 theories ...
Processing theory Abs_Int_ITP2012.Abs_Int1_const ...
Processing theory Abs_Int_ITP2012.Abs_Int1_parity ...
Processing theory No_FTL_observers.SpaceTime ...
Removing 11 theories ...
Processing theory Schutz_Spacetime.TemporalOrderOnPath ...
Processing theory Projective_Geometry.Pappus_Desargues ...
Removing 9 theories ...
Processing theory No_FTL_observers.Axioms ...
Processing theory No_FTL_observers.SpecRel ...
Loading 109 theories ...
Removing 4 theories ...
Processing theory Abstract-Hoare-Logics.PLang ...
Processing theory Abstract-Hoare-Logics.PHoare ...
Processing theory Abstract-Hoare-Logics.PTermi ...
Processing theory BinarySearchTree.BinaryTree ...
Processing theory Binomial-Queues.PQ ...
Processing theory Abortable_Linearizable_Modules.Sequences ...
Processing theory Binomial-Queues.Binomial_Queue ...
Processing theory BinarySearchTree.BinaryTree_Map ...
Processing theory C2KA_DistributedSystems.Stimuli ...
Processing theory Abstract-Hoare-Logics.PHoareTotal ...
Processing theory Binomial-Queues.PQ_Implementation ...
Processing theory C2KA_DistributedSystems.CKA ...
Processing theory C2KA_DistributedSystems.C2KA ...
Processing theory C2KA_DistributedSystems.Topology_C2KA ...
Processing theory C2KA_DistributedSystems.Communication_C2KA ...
Processing theory Decl_Sem_Fun_PL.Values ...
Processing theory Decl_Sem_Fun_PL.DeclSemAsDenot ...
Processing theory Decl_Sem_Fun_PL.ValueProps ...
Processing theory Decl_Sem_Fun_PL.DenotLam5 ...
Processing theory FocusStreamsCaseStudies.arith_hints ...
Processing theory FocusStreamsCaseStudies.JoinSplitTime ...
Processing theory Decl_Sem_Fun_PL.InterTypeSystem ...
Processing theory Decl_Sem_Fun_PL.EquivDenotInterTypes ...
Processing theory GPU_Kernel_PL.Misc ...
Processing theory Abortable_Linearizable_Modules.IOA ...
Processing theory Abortable_Linearizable_Modules.Simulations ...
Processing theory GPU_Kernel_PL.KPL_syntax ...
Processing theory GPU_Kernel_PL.KPL_state ...
Processing theory GPU_Kernel_PL.KPL_execution_thread ...
Processing theory GPU_Kernel_PL.KPL_execution_group ...
Processing theory GPU_Kernel_PL.KPL_wellformedness ...
Processing theory Abortable_Linearizable_Modules.RDR ...
Processing theory GPU_Kernel_PL.KPL_execution_kernel ...
Processing theory GPU_Kernel_PL.Kernel_programming_language ...
Processing theory LambdaMu.Syntax ...
Processing theory LambdaMu.DeBruijn ...
Processing theory LambdaMu.Substitution ...
Processing theory LambdaMu.Reduction ...
Processing theory LambdaMu.Types ...
Processing theory LambdaMu.ContextFacts ...
Processing theory Abortable_Linearizable_Modules.SLin ...
Removing 34 theories ...
Processing theory GewirthPGCProof.CJDDLplus ...
Processing theory LambdaMu.TypePreservation ...
Processing theory LambdaMu.Progress ...
Processing theory GewirthPGCProof.ExtendedDDL ...
Processing theory MFOTL_Monitor.Table ...
Processing theory Generic_Join.Generic_Join ...
Processing theory GewirthPGCProof.GewirthArgument ...
Processing theory Matroids.Indep_System ...
Processing theory Generic_Join.Examples_Join ...
Removing 10 theories ...
Processing theory ComponentDependencies.DataDependenciesConcreteValues ...
Processing theory ComponentDependencies.DataDependencies ...
Processing theory Network_Security_Policy_Verification.attic ...
Processing theory RefinementReactive.Refinement ...
Processing theory Coinductive_Languages.Coinductive_Regular_Set ...
Processing theory SIFPL.Lattice ...
Processing theory Matroids.Matroid ...
Processing theory RefinementReactive.Temporal ...
Processing theory Generic_Join.Generic_Join_Correctness ...
Processing theory PSemigroupsConvolution.Partial_Semigroup_Models ...
Processing theory SenSocialChoice.FSext ...
Processing theory SenSocialChoice.RPRs ...
Processing theory SenSocialChoice.SCFs ...
Processing theory RefinementReactive.Reactive ...
Processing theory SIFPL.HuntSands ...
Processing theory Abortable_Linearizable_Modules.Idempotence ...
Processing theory SenSocialChoice.May ...
Processing theory SenSocialChoice.Sen ...
Processing theory Separation_Algebra.Sep_Tactics_Test ...
Processing theory Separation_Algebra.Separation_Algebra_Alt ...
Processing theory Types_Tableaus_and_Goedels_God.Relations ...
Processing theory Separation_Algebra.Sep_Eq ...
Processing theory SIFUM_Type_Systems.LocallySoundModeUse ...
Processing theory Separation_Algebra.VM_Example ...
Removing 33 theories ...
Processing theory SenSocialChoice.Arrow ...
Processing theory Topological_Semantics.topo_alexandrov ...
Processing theory Types_Tableaus_and_Goedels_God.IHOML ...
Processing theory Types_Tableaus_and_Goedels_God.AndersonProof ...
Processing theory Types_Tableaus_and_Goedels_God.FittingProof ...
Processing theory Types_Tableaus_and_Goedels_God.GoedelProof_P1 ...
Processing theory Types_Tableaus_and_Goedels_God.GoedelProof_P2 ...
Processing theory Types_Tableaus_and_Goedels_God.IHOML_Examples ...
Processing theory Separation_Algebra.Simple_Separation_Example ...
Processing theory Hello_World.IO ...
Processing theory Hello_World.HelloWorld ...
Processing theory Hello_World.HelloWorld_Proof ...
Processing theory ComponentDependencies.DataDependenciesCaseStudy ...
Processing theory IMP_Compiler.Compiler ...
Processing theory Hello_World.RunningCodeFromIsabelle ...
Processing theory Ramsey-Infinite.Ramsey ...
Processing theory HotelKeyCards.Notation ...
Processing theory HotelKeyCards.Basis ...
Processing theory Relational-Incorrectness-Logic.RelationalIncorrectness ...
Processing theory HotelKeyCards.State ...
Processing theory HotelKeyCards.Trace ...
Processing theory HotelKeyCards.Equivalence ...
Processing theory ADS_Functor.Generic_ADS_Construction ...
Processing theory Propositional_Proof_Systems.Resolution_Compl ...
Processing theory Transitive-Closure-II.RTrancl ...
Processing theory TortoiseHare.Basis ...
Processing theory TortoiseHare.Brent ...
Processing theory TortoiseHare.TortoiseHare ...
Processing theory Splay_Tree.Splay_Tree ...
Removing 58 theories ...
Processing theory Weight_Balanced_Trees.Weight_Balanced_Trees ...
Processing theory Splay_Tree.Splay_Map ...
Processing theory IMP_Compiler.Compiler2 ...
Loading 112 theories ...
Processing theory Abortable_Linearizable_Modules.Consensus ...
Processing theory Conditional_Simplification.CS_Tools ...
Processing theory Conditional_Simplification.IHOL_CS ...
Processing theory Constructor_Funs.Constructor_Funs ...
Processing theory DPT-SAT-Solver.DPT_SAT_Solver ...
Processing theory Fresh_Identifiers.Fresh ...
Processing theory Fresh_Identifiers.Fresh_Infinite ...
Processing theory Fresh_Identifiers.Fresh_Nat ...
Processing theory Abstract-Hoare-Logics.Lang ...
Processing theory Abstract-Hoare-Logics.Hoare ...
Processing theory Abstract-Hoare-Logics.Termi ...
Processing theory Abstract-Hoare-Logics.HoareTotal ...
Processing theory Abstract-Hoare-Logics.PsLang ...
Processing theory Abstract-Hoare-Logics.PsHoare ...
Processing theory Abstract-Hoare-Logics.PsTermi ...
Removing 27 theories ...
Processing theory DPT-SAT-Solver.DPT_SAT_Tests ...
Processing theory Fresh_Identifiers.Fresh_String ...
Processing theory Intro_Dest_Elim.IDE_Tools ...
Processing theory Intro_Dest_Elim.IHOL_IDE ...
Processing theory Isabelle_C.README ...
Processing theory Abstract-Hoare-Logics.PsHoareTotal ...
Processing theory Generic_Deriving.Tagged_Prod_Sum ...
Processing theory Constructor_Funs.Test_Constructor_Funs ...
Processing theory Generic_Deriving.Derive ...
Processing theory LambdaMu.Peirce ...
Processing theory Lifting_Definition_Option.Lifting_Definition_Option_Examples ...
Processing theory Lazy_Case.Test_Lazy_Case ...
Processing theory Generic_Deriving.Derive_Datatypes ...
Processing theory Generic_Deriving.Derive_Algebra_Laws ...
Processing theory Generic_Deriving.Derive_Algebra ...
Processing theory Generic_Deriving.Derive_Encode ...
Processing theory Generic_Deriving.Derive_Eq ...
Processing theory Lowe_Ontological_Argument.Relations ...
Processing theory Lowe_Ontological_Argument.QML ...
Processing theory Lowe_Ontological_Argument.LoweOntologicalArgument_1 ...
Processing theory Lowe_Ontological_Argument.LoweOntologicalArgument_2 ...
Processing theory Lowe_Ontological_Argument.LoweOntologicalArgument_3 ...
Processing theory Lowe_Ontological_Argument.LoweOntologicalArgument_4 ...
Processing theory Generic_Deriving.Derive_Eq_Laws ...
Processing theory Isabelle_Meta_Model.Design_generated_generated ...
Removing 29 theories ...
Processing theory Lowe_Ontological_Argument.LoweOntologicalArgument_5 ...
Processing theory Lowe_Ontological_Argument.LoweOntologicalArgument_6 ...
Processing theory Lowe_Ontological_Argument.LoweOntologicalArgument_7 ...
Processing theory Marriage.Marriage ...
Processing theory Network_Security_Policy_Verification.ML_GraphViz_Disable ...
Processing theory Max-Card-Matching.Matching ...
Processing theory Modular_Assembly_Kit_Security.FlowPolicies ...
Processing theory Latin_Square.Latin_Square ...
Processing theory Generic_Deriving.Derive_Show ...
Processing theory PAL.PAL ...
Processing theory Pop_Refinement.Definition ...
Processing theory Pop_Refinement.Future_Work ...
Processing theory Pop_Refinement.General_Remarks ...
Processing theory Pop_Refinement.Related_Work ...
Processing theory Pop_Refinement.First_Example ...
Processing theory POPLmark-deBruijn.POPLmark ...
Processing theory Projective_Geometry.Higher_Projective_Space_Axioms ...
Processing theory Projective_Geometry.Higher_Projective_Space_Rank_Axioms ...
Processing theory Pop_Refinement.Second_Example ...
Removing 26 theories ...
Processing theory Projective_Geometry.Matroid_Rank_Properties ...
Processing theory Projective_Geometry.Desargues_3D ...
Processing theory Projective_Geometry.Projective_Space_Axioms ...
Processing theory Proof_Strategy_Language.Try_Hard ...
Processing theory Proof_Strategy_Language.PSL ...
Processing theory NormByEval.NBE ...
Processing theory Roy_Floyd_Warshall.Roy_Floyd_Warshall ...
Processing theory Projective_Geometry.Desargues_2D ...
Processing theory Regular_Tree_Relations.Horn_List ...
Processing theory Separation_Logic_Imperative_HOL.Default_Insts ...
Processing theory SimplifiedOntologicalArgument.DisableKodkodScala ...
Processing theory SimplifiedOntologicalArgument.HOML ...
Processing theory SimplifiedOntologicalArgument.BaseDefs ...
Processing theory SimplifiedOntologicalArgument.MFilter ...
Processing theory Knights_Tour.KnightsTour ...
Processing theory SimplifiedOntologicalArgument.KanckosLethenNo2Possibilist ...
Processing theory Robbins-Conjecture.Robbins_Conjecture ...
Removing 13 theories ...
Processing theory SimplifiedOntologicalArgument.SimpleVariant ...
Processing theory SimplifiedOntologicalArgument.SimpleVariantHF ...
Processing theory SimplifiedOntologicalArgument.SimpleVariantPG ...
Processing theory SimplifiedOntologicalArgument.SimpleVariantSE ...
Processing theory SimplifiedOntologicalArgument.SimpleVariantSEinT ...
Processing theory SimplifiedOntologicalArgument.SimplifiedOntologicalArgument ...
Processing theory SimplifiedOntologicalArgument.UFilterVariant ...
Removing 8 theories ...
Processing theory SimplifiedOntologicalArgument.ScottVariant ...
Processing theory Stable_Matching.Sotomayor ...
Processing theory Sliding_Window_Algorithm.SWA ...
Removing 6 theories ...
Processing theory TESL_Language.Introduction ...
Processing theory Tail_Recursive_Functions.Method ...
Processing theory Szpilrajn.Szpilrajn ...
Processing theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun ...
Processing theory Blue_Eyes.Blue_Eyes ...
Processing theory Tail_Recursive_Functions.CaseStudy1 ...
Processing theory Paraconsistency.Paraconsistency ...
Processing theory Approximation_Algorithms.Approx_VC_Hoare ...
Processing theory AI_Planning_Languages_Semantics.Option_Monad_Add ...
Processing theory BNF_Operations.Kill ...
Processing theory BNF_Operations.Lift ...
Processing theory Stellar_Quorums.Stellar_Quorums ...
Processing theory BNF_Operations.Compose ...
Processing theory Verified-Prover.Prover ...
Processing theory BNF_Operations.LFP ...
Processing theory BNF_Operations.GFP ...
Processing theory Conditional_Simplification.Reference_Prerequisites ...
Processing theory Conditional_Simplification.CS_Reference ...
Processing theory Intro_Dest_Elim.Reference_Prerequisites ...
Processing theory Intro_Dest_Elim.IDE_Reference ...
Processing theory CofGroups.CofGroups ...
Processing theory BNF_Operations.Permute ...
Removing 34 theories ...
Processing theory BNF_Operations.N2M ...
Removing 2 theories ...
Processing theory Hood_Melville_Queue.Hood_Melville_Queue ...
Removing 2 theories ...
Processing theory Proof_Strategy_Language.Example ...
Loading 22 theories ...
Removing 4 theories ...
Processing theory AnselmGod.AnselmGod ...
Processing theory Aristotles_Assertoric_Syllogistic.AristotlesAssertoric ...
Processing theory Certification_Monads.Misc ...
Processing theory Bondy.Bondy ...
Processing theory BinarySearchTree.BinaryTree_TacticStyle ...
Processing theory Depth-First-Search.DFS ...
Processing theory Dict_Construction.Impossibility ...
Processing theory Example-Submission.Submission ...
Processing theory Dict_Construction.Introduction ...
Processing theory CYK.CYK ...
Processing theory AVL-Trees.AVL2 ...
Processing theory Compiling-Exceptions-Correctly.Exceptions ...
Processing theory Free-Boolean-Algebra.Free_Boolean_Algebra ...
Processing theory AVL-Trees.AVL ...
Removing 14 theories ...
Processing theory GoedelGod.GoedelGod ...
Processing theory AxiomaticCategoryTheory.AxiomaticCategoryTheory ...
Processing theory FunWithTilings.Tilings ...
Processing theory HotelKeyCards.NewCard ...
Processing theory Goodstein_Lambda.Goodstein_Lambda ...
Processing theory FOL_Harrison.FOL_Harrison ...
Processing theory Huffman.Huffman ...
Removing 7 theories ...
Processing theory IsaGeoCoq.Tarski_Neutral ...
Loading 98 theories ...
Processing theory SpecCheck.SpecCheck_Dynamic ...
Processing theory SpecCheck.SpecCheck_Examples ...
Processing theory Forcing.Recursion_Thms ...
Removing 106 theories ...
Processing theory Forcing.Nat_Miscellanea ...
Processing theory Forcing.Pointed_DC ...
Processing theory Recursion-Addition.recursion ...
Processing theory Forcing.Utils ...
Processing theory Forcing.Synthetic_Definition ...
Removing 1 theories ...
Processing theory Forcing.Renaming ...
Processing theory Forcing.Renaming_Auto ...
Processing theory Delta_System_Lemma.ZF_Library ...
Processing theory Delta_System_Lemma.Cardinal_Library ...
Processing theory Delta_System_Lemma.Delta_System ...
Processing theory Delta_System_Lemma.Cohen_Posets ...
Processing theory Forcing.Forcing_Notions ...
Processing theory Forcing.Rasiowa_Sikorski ...
Processing theory Delta_System_Lemma.Cofinality ...
Processing theory Delta_System_Lemma.Konig ...
Processing theory Forcing.Internalizations ...
Processing theory Forcing.Relative_Univ ...
Processing theory Forcing.Interface ...
Processing theory Forcing.Forcing_Data ...
Processing theory Forcing.Internal_ZFC_Axioms ...
Processing theory Forcing.Names ...
Processing theory Forcing.Separation_Rename ...
Processing theory Forcing.Extensionality_Axiom ...
Processing theory Forcing.Foundation_Axiom ...
Processing theory Forcing.FrecR ...
Processing theory Forcing.Arities ...
Processing theory Forcing.Least ...
Processing theory Forcing.Pairing_Axiom ...
Processing theory Forcing.Proper_Extension ...
Processing theory Forcing.Succession_Poset ...
Processing theory Forcing.Union_Axiom ...
Processing theory Forcing.Forces_Definition ...
Removing 11 theories ...
Processing theory Forcing.Forcing_Theorems ...
Processing theory Forcing.Separation_Axiom ...
Processing theory Forcing.Infinity_Axiom ...
Processing theory Forcing.Powerset_Axiom ...
Processing theory Forcing.Ordinals_In_MG ...
Processing theory Forcing.Replacement_Axiom ...
Processing theory Forcing.Choice_Axiom ...
Processing theory Forcing.Forcing_Main ...
Exception in thread "Isabelle.process_manager" java.nio.file.NoSuchFileException: /tmp/isabelle-jenkins/process11533083202489363878/export261076972/StdIO.hs
	at java.base/sun.nio.fs.UnixException.translateToIOException(UnixException.java:92)
	at java.base/sun.nio.fs.UnixException.rethrowAsIOException(UnixException.java:106)
	at java.base/sun.nio.fs.UnixException.rethrowAsIOException(UnixException.java:111)
	at java.base/sun.nio.fs.UnixFileAttributeViews$Basic.readAttributes(UnixFileAttributeViews.java:55)
	at java.base/sun.nio.fs.UnixFileSystemProvider.readAttributes(UnixFileSystemProvider.java:148)
	at java.base/sun.nio.fs.LinuxFileSystemProvider.readAttributes(LinuxFileSystemProvider.java:99)
	at java.base/java.nio.file.Files.readAttributes(Files.java:1851)
	at java.base/java.nio.file.FileTreeWalker.getAttributes(FileTreeWalker.java:220)
	at java.base/java.nio.file.FileTreeWalker.visit(FileTreeWalker.java:277)
	at java.base/java.nio.file.FileTreeWalker.next(FileTreeWalker.java:374)
	at java.base/java.nio.file.Files.walkFileTree(Files.java:2845)
	at java.base/java.nio.file.Files.walkFileTree(Files.java:2882)
	at isabelle.Isabelle_System$.rm_tree(isabelle_system.scala:323)
	at isabelle.ML_Process$.$anonfun$apply$9(ml_process.scala:138)
	at isabelle.Bash$Process.do_cleanup(bash.scala:189)
	at isabelle.Bash$Process.join(bash.scala:198)
	at isabelle.Prover.$anonfun$process_result$1(prover.scala:113)
	at isabelle.Exn$.capture(exn.scala:61)
	at isabelle.Thread_Future.$anonfun$thread$1(future.scala:156)
	at isabelle.Isabelle_Thread$.$anonfun$fork$2(isabelle_thread.scala:65)
	at isabelle.Isabelle_Thread.run(isabelle_thread.scala:141)
Cancelling nested steps due to timeout
Sending interrupt signal to process
+ true
[Pipeline] }
[Pipeline] // stage
[Pipeline] stage
[Pipeline] { (Store)
[Pipeline] zip
Compress /media/data/jenkins/workspace/isabelle-dump/dump to /media/data/jenkins/workspace/isabelle-dump/dump.zip
Body did not finish within grace period; terminating with extreme prejudice
[Pipeline] }
[Pipeline] // stage
[Pipeline] }
[Pipeline] // timeout
[Pipeline] }
[Pipeline] // node
[Pipeline] End of Pipeline
Timeout has been exceeded
Finished: ABORTED