Skipping 129 KB.. Full Log

Processing theory Separation_Logic_Imperative_HOL.Automation ...
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 ...
Removing 9 theories ...
Processing theory First_Welfare_Theorem.Argmax ...
Processing theory First_Welfare_Theorem.Consumers ...
Processing theory First_Welfare_Theorem.Common ...
Processing theory First_Welfare_Theorem.Private_Ownership_Economy ...
Processing theory First_Welfare_Theorem.Exchange_Economy ...
Processing theory First_Welfare_Theorem.Arrow_Debreu_Model ...
Processing theory QR_Decomposition.Generalizations2 ...
Loading 3 theories ...
Removing 14 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 8 theories ...
Removing 21 theories ...
Processing theory Store_Buffer_Reduction.SyntaxTweaks ...
Processing theory Store_Buffer_Reduction.ReduceStoreBuffer ...
Processing theory Store_Buffer_Reduction.ReduceStoreBufferSimulation ...
Processing theory Store_Buffer_Reduction.PIMP ...
Loading 39 theories ...
Processing theory Store_Buffer_Reduction.Abbrevs ...
Processing theory Store_Buffer_Reduction.Preliminaries ...
Processing theory Store_Buffer_Reduction.Variants ...
Processing theory Store_Buffer_Reduction.Text ...
Removing 8 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.Structural_Congruence ...
Processing theory Psi_Calculi.Frame ...
Processing theory Psi_Calculi.Semantics ...
Processing theory Psi_Calculi.Simulation ...
Processing theory Psi_Calculi.Sum ...
Processing theory Psi_Calculi.Tau_Chain ...
Processing theory Psi_Calculi.Weak_Stat_Imp ...
Processing theory Psi_Calculi.Weak_Stat_Imp_Pres ...
Processing theory Psi_Calculi.Bisimulation ...
Processing theory Psi_Calculi.Weak_Simulation ...
Processing theory Psi_Calculi.Weak_Cong_Simulation ...
Processing theory Psi_Calculi.Sim_Pres ...
Processing theory Psi_Calculi.Bisim_Pres ...
Processing theory Psi_Calculi.Sim_Struct_Cong ...
Processing theory Psi_Calculi.Bisim_Struct_Cong ...
Processing theory Psi_Calculi.Bisim_Subst ...
Processing theory Psi_Calculi.Weak_Sim_Pres ...
Processing theory Psi_Calculi.Weak_Bisimulation ...
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.Weak_Bisim_Pres ...
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 ...
Processing theory FinFun.FinFun ...
Removing 17 theories ...
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++.TypeRel ...
Processing theory CoreC++.State ...
Processing theory CoreC++.Syntax ...
Processing theory CoreC++.SystemClasses ...
Processing theory CoreC++.WellType ...
Processing theory CoreC++.Annotate ...
Processing theory CoreC++.WellTypeRT ...
Processing theory CoreC++.Conform ...
Processing theory CoreC++.WellForm ...
Processing theory CoreC++.WWellForm ...
Processing theory CoreC++.BigStep ...
Processing theory CoreC++.DefAss ...
Processing theory CoreC++.CWellForm ...
Processing theory CoreC++.SmallStep ...
Processing theory CoreC++.Equivalence ...
Processing theory CoreC++.Progress ...
Processing theory CoreC++.HeapExtension ...
Processing theory CoreC++.TypeSafe ...
Processing theory CoreC++.Determinism ...
Processing theory CoreC++.Execute ...
Loading 12 theories ...
Processing theory CoreC++.CoreC++ ...
Processing theory Encodability_Process_Calculi.Relations ...
Processing theory Encodability_Process_Calculi.ProcessCalculi ...
Processing theory Encodability_Process_Calculi.SimulationRelations ...
Processing theory Encodability_Process_Calculi.Encodings ...
Removing 30 theories ...
Processing theory Encodability_Process_Calculi.SourceTargetRelation ...
Processing theory Encodability_Process_Calculi.DivergenceReflection ...
Processing theory Encodability_Process_Calculi.SuccessSensitiveness ...
Processing theory Encodability_Process_Calculi.OperationalCorrespondence ...
Processing theory Encodability_Process_Calculi.FullAbstraction ...
Processing theory Encodability_Process_Calculi.CombinedCriteria ...
Loading 21 theories ...
Processing theory Featherweight_OCL.UML_Types ...
Removing 10 theories ...
Processing theory Featherweight_OCL.UML_Logic ...
Processing theory Featherweight_OCL.UML_PropertyProfiles ...
Processing theory Featherweight_OCL.UML_Tools ...
Processing theory Featherweight_OCL.UML_Boolean ...
Processing theory Featherweight_OCL.UML_Void ...
Processing theory Featherweight_OCL.UML_Pair ...
Processing theory Featherweight_OCL.UML_String ...
Processing theory Featherweight_OCL.UML_Integer ...
Processing theory Featherweight_OCL.UML_Sequence ...
Processing theory Featherweight_OCL.UML_Real ...
Processing theory Featherweight_OCL.UML_Bag ...
Processing theory Featherweight_OCL.UML_Set ...
Processing theory Featherweight_OCL.UML_Library ...
Processing theory Featherweight_OCL.UML_State ...
Processing theory Featherweight_OCL.UML_Contracts ...
Processing theory Featherweight_OCL.UML_Main ...
Processing theory Featherweight_OCL.Analysis_UML ...
Processing theory Featherweight_OCL.Analysis_OCL ...
Processing theory Featherweight_OCL.Design_UML ...
Loading 18 theories ...
Processing theory Featherweight_OCL.Design_OCL ...
Processing theory Native_Word.Code_Int_Integer_Conversion ...
Processing theory Word_Lib.More_Arithmetic ...
Processing theory Pell.Pell ...
Removing 21 theories ...
Processing theory Mersenne_Primes.Lucas_Lehmer_Auxiliary ...
Processing theory Mersenne_Primes.Lucas_Lehmer ...
Processing theory Word_Lib.Bit_Comprehension ...
Processing theory Word_Lib.More_Divides ...
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 Native_Word.Bits_Integer ...
Processing theory Native_Word.Code_Target_Bits_Int ...
Processing theory Mersenne_Primes.Lucas_Lehmer_Code ...
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 ...
Processing theory Three_Circles.Normal_Poly ...
Removing 30 theories ...
Processing theory Three_Circles.Three_Circles ...
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 5 theories ...
Processing theory Polynomial_Factorization.Prime_Factorization ...
Processing theory Gaussian_Integers.Gaussian_Integers_Test ...
Processing theory Gaussian_Integers.Gaussian_Integers_Everything ...
Loading 4 theories ...
Removing 5 theories ...
Processing theory Pell.Efficient_Discrete_Sqrt ...
Processing theory Pell.Pell_Algorithm ...
Processing theory Pell.Pell_Algorithm_Test ...
Loading 60 theories ...
Processing theory Interpreter_Optimizations.Dynamic ...
Processing theory Interpreter_Optimizations.Op ...
Processing theory Interpreter_Optimizations.OpInl ...
Processing theory VeriComp.Transfer_Extras ...
Processing theory Interpreter_Optimizations.List_util ...
Processing theory Interpreter_Optimizations.Option_Extra ...
Processing theory VeriComp.Well_founded ...
Processing theory VeriComp.Inf ...
Processing theory Interpreter_Optimizations.AList_Extra ...
Processing theory VeriComp.Behaviour ...
Processing theory VeriComp.Semantics ...
Processing theory VeriComp.Language ...
Processing theory Interpreter_Optimizations.Result ...
Removing 4 theories ...
Processing theory VeriComp.Simulation ...
Processing theory VeriComp.Compiler ...
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.Unboxed_lemmas ...
Processing theory Interpreter_Optimizations.OpUbx ...
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 ...
Removing 5 theories ...
Processing theory Formal_Puiseux_Series.FPS_Hensel ...
Loading 9 theories ...
Processing theory Formal_Puiseux_Series.Formal_Puiseux_Series ...
Processing theory Padic_Ints.Supplementary_Ring_Facts ...
Processing theory Padic_Ints.Extended_Int ...
Processing theory Padic_Ints.Padic_Construction ...
Processing theory Padic_Ints.Function_Ring ...
Removing 4 theories ...
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 ...
Processing theory Mason_Stothers.Mason_Stothers ...
Removing 6 theories ...
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 1 theories ...
Processing theory Amicable_Numbers.Amicable_Numbers ...
Loading 21 theories ...
Processing theory Graph_Theory.Rtrancl_On ...
Processing theory Graph_Theory.Stuff ...
Processing theory Card_Partitions.Set_Partition ...
Processing theory Nested_Multisets_Ordinals.Multiset_More ...
Processing theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset ...
Processing theory Graph_Theory.Digraph ...
Processing theory Graph_Theory.Arc_Walk ...
Processing theory Graph_Theory.Bidirected_Digraph ...
Processing theory Design_Theory.Multisets_Extras ...
Processing theory Graph_Theory.Pair_Digraph ...
Processing theory Design_Theory.Design_Basics ...
Processing theory Design_Theory.Design_Operations ...
Processing theory Design_Theory.Sub_Designs ...
Processing theory Graph_Theory.Digraph_Component ...
Removing 9 theories ...
Processing theory Design_Theory.Block_Designs ...
Processing theory Design_Theory.Design_Isomorphisms ...
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 ...
Removing 19 theories ...
Processing theory Budan_Fourier.Sturm_Multiple_Roots ...
Loading 21 theories ...
Processing theory Polynomial_Interpolation.Divmod_Int ...
Processing theory Polynomial_Interpolation.Improved_Code_Equations ...
Processing theory Polynomial_Factorization.Explicit_Roots ...
Processing theory Polynomial_Factorization.Precomputation ...
Processing theory Show.Show_Poly ...
Processing theory Polynomial_Factorization.Missing_Polynomial_Factorial ...
Processing theory Polynomial_Factorization.Polynomial_Divisibility ...
Processing theory Polynomial_Interpolation.Lagrange_Interpolation ...
Processing theory Polynomial_Interpolation.Neville_Aitken_Interpolation ...
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 ...
Processing theory Polynomial_Interpolation.Newton_Interpolation ...
Processing theory Polynomial_Interpolation.Polynomial_Interpolation ...
Processing theory Polynomial_Factorization.Kronecker_Factorization ...
Processing theory Polynomial_Factorization.Square_Free_Factorization ...
Removing 4 theories ...
Processing theory Polynomial_Factorization.Rational_Factorization ...
Loading 3 theories ...
Processing theory Interpreter_Optimizations.Std ...
Processing theory Interpreter_Optimizations.Std_to_Inca_simulation ...
Processing theory Interpreter_Optimizations.Std_to_Inca_compiler ...
Loading 14 theories ...
Removing 44 theories ...
Processing theory Timed_Automata.Misc ...
Processing theory Timed_Automata.Timed_Automata ...
Processing theory Timed_Automata.Floyd_Warshall ...
Processing theory Timed_Automata.Regions ...
Processing theory Timed_Automata.DBM ...
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 ...
Removing 21 theories ...
Processing theory Root_Balanced_Tree.Time_Monad ...
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.Power_int ...
Processing theory Physical_Quantities.Enum_extra ...
Processing theory Physical_Quantities.Groups_mult ...
Processing theory Physical_Quantities.ISQ_Dimensions ...
Processing theory Physical_Quantities.ISQ_Quantities ...
Loading 20 theories ...
Processing theory Physical_Quantities.ISQ_Proof ...
Processing theory Physical_Quantities.ISQ_Algebra ...
Processing theory Physical_Quantities.ISQ_Units ...
Processing theory Physical_Quantities.ISQ_Conversion ...
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 66 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 12 theories ...
Processing theory Lambda_Free_RPOs.Lambda_Free_Util ...
Processing theory Lambda_Free_RPOs.Infinite_Chain ...
Removing 2 theories ...
Processing theory Lambda_Free_RPOs.Extension_Orders ...
Processing theory Lambda_Free_RPOs.Lambda_Free_Term ...
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 ...
Processing theory Lambda_Free_RPOs.Lambda_Free_RPO_Optim ...
Processing theory Lambda_Free_RPOs.Lambda_Free_RPOs ...
Processing theory Lambda_Free_EPO.Embeddings ...
Processing theory Lambda_Free_EPO.Chop ...
Processing theory Lambda_Free_EPO.Lambda_Free_EPO ...
Loading 13 theories ...
Removing 11 theories ...
Processing theory Vickrey_Clarke_Groves.Argmax ...
Processing theory Vickrey_Clarke_Groves.SetUtils ...
Processing theory Vickrey_Clarke_Groves.RelationOperators ...
Processing theory Vickrey_Clarke_Groves.RelationProperties ...
Processing theory Vickrey_Clarke_Groves.Partitions ...
Processing theory Vickrey_Clarke_Groves.MiscTools ...
Processing theory Vickrey_Clarke_Groves.StrictCombinatorialAuction ...
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.Trail ...
Removing 12 theories ...
Processing theory SATSolverVerification.CNF ...
Processing theory SATSolverVerification.SatSolverVerification ...
Processing theory SATSolverVerification.SatSolverCode ...
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 ...
Processing theory Liouville_Numbers.Liouville_Numbers_Misc ...
Processing theory Liouville_Numbers.Liouville_Numbers ...
Removing 10 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.IDirProds ...
Processing theory Finitely_Generated_Abelian_Groups.Finite_Product_Extend ...
Processing theory Finitely_Generated_Abelian_Groups.Group_Relations ...
Processing theory Finitely_Generated_Abelian_Groups.Finite_And_Cyclic_Groups ...
Processing theory Finitely_Generated_Abelian_Groups.DirProds ...
Loading 12 theories ...
Removing 14 theories ...
Processing theory Finitely_Generated_Abelian_Groups.Finitely_Generated_Abelian_Groups ...
Processing theory Safe_OCL.Transitive_Closure_Ext ...
Processing theory Safe_OCL.Errorable ...
Processing theory Safe_OCL.Finite_Map_Ext ...
Processing theory Safe_OCL.OCL_Basic_Types ...
Processing theory Safe_OCL.Tuple ...
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 ...
Removing 14 theories ...
Processing theory Lifting_the_Exponent.LTE ...
Loading 3 theories ...
Processing theory Dijkstra_Shortest_Path.Graph ...
Removing 1 theories ...
Processing theory Koenigsberg_Friendship.MoreGraph ...
Processing theory Koenigsberg_Friendship.FriendshipTheory ...
Processing theory Arith_Prog_Rel_Primes.Arith_Prog_Rel_Primes ...
Loading 14 theories ...
Removing 13 theories ...
Processing theory Nash_Williams.Nash_Extras ...
Processing theory ZFC_in_HOL.ZFC_Library ...
Processing theory Nash_Williams.Nash_Williams ...
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 24 theories ...
Processing theory Collections.ICF_Tools ...
Processing theory Collections.Ord_Code_Preproc ...
Processing theory Collections.Locale_Code ...
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.Incredible_Deduction ...
Processing theory Incredible_Proof_Machine.Propositional_Formulas ...
Processing theory Abstract_Completeness.Abstract_Completeness ...
Processing theory Incredible_Proof_Machine.Natural_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 ...
Removing 14 theories ...
Processing theory Incredible_Proof_Machine.Incredible_Trees ...
Processing theory Incredible_Proof_Machine.Build_Incredible_Tree ...
Processing theory Incredible_Proof_Machine.Incredible_Completeness ...
Loading 18 theories ...
Processing theory Incredible_Proof_Machine.Incredible_Predicate_Tasks ...
Processing theory Incredible_Proof_Machine.Incredible_Propositional_Tasks ...
Processing theory Incredible_Proof_Machine.Incredible_Everything ...
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 Containers.AssocList ...
Processing theory Certification_Monads.Error_Monad ...
Processing theory Certification_Monads.Check_Monad ...
Processing theory AI_Planning_Languages_Semantics.Error_Monad_Add ...
Processing theory Containers.Mapping_Impl ...
Processing theory Containers.Map_To_Mapping ...
Processing theory Containers.Containers ...
Processing theory Propositional_Proof_Systems.Formulas ...
Processing theory Propositional_Proof_Systems.Sema ...
Processing theory Propositional_Proof_Systems.Consistency ...
Removing 25 theories ...
Processing theory AI_Planning_Languages_Semantics.PDDL_STRIPS_Semantics ...
Processing theory AI_Planning_Languages_Semantics.PDDL_STRIPS_Checker ...
Removing 27 theories ...
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.Vars ...
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 3 theories ...
Processing theory Hoare_Time.Big_Step ...
Processing theory Hoare_Time.Big_StepT ...
Processing theory Hoare_Time.Quant_Hoare ...
Processing theory Hoare_Time.Nielson_Hoare ...
Processing theory Hoare_Time.Partial_Evaluation ...
Processing theory Hoare_Time.QuantK_Hoare ...
Processing theory Hoare_Time.Big_StepT_Partial ...
Processing theory Hoare_Time.SepLog_Hoare ...
Processing theory Hoare_Time.SepLog_Examples ...
Processing theory Hoare_Time.QuantK_VCG ...
Processing theory Hoare_Time.QuantK_Examples ...
Processing theory Hoare_Time.Nielson_VCG ...
Processing theory Hoare_Time.Discussion ...
Processing theory Hoare_Time.QuantK_Sqrt ...
Processing theory Hoare_Time.Nielson_Examples ...
Processing theory Hoare_Time.SepLogK_Hoare ...
Processing theory Hoare_Time.DiscussionO ...
Processing theory Hoare_Time.Quant_VCG ...
Processing theory Hoare_Time.Quant_Examples ...
Processing theory Hoare_Time.Nielson_VCGi ...
Processing theory Hoare_Time.Nielson_VCGi_complete ...
Processing theory Hoare_Time.SepLogK_VCG ...
Processing theory Hoare_Time.Nielson_Sqrt ...
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 HereditarilyFinite.HF ...
Processing theory Category3.InitialTerminal ...
Processing theory Category3.ConcreteCategory ...
Processing theory Category3.ProductCategory ...
Processing theory Category3.Functor ...
Processing theory Category3.FreeCategory ...
Removing 30 theories ...
Processing theory Category3.NaturalTransformation ...
Processing theory Category3.SetCategory ...
Processing theory Category3.BinaryFunctor ...
Processing theory Category3.SetCat ...
Processing theory Category3.FunctorCategory ...
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.Name ...
Processing theory Higher_Order_Terms.Term_Utils ...
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.Sigma_Algebra ...
Processing theory Integration.MonConv ...
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 Priority_Queue_Braun.Priority_Queue_Braun2 ...
Processing theory Fishburn_Impossibility.Fishburn_Impossibility ...
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 ...
Removing 19 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.SAS_Plus_Semantics ...
Processing theory Verified_SAT_Based_AI_Planning.STRIPS_Representation ...
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 Card_Partitions.Injectivity_Solver ...
Processing theory Discrete_Summation.Discrete_Summation ...
Processing theory Physical_Quantities.CGS ...
Processing theory Case_Labeling.Conditionals ...
Processing theory Physical_Quantities.BIS ...
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 ...
Removing 51 theories ...
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.QEdlo_fr ...
Processing theory LinearQuantifierElim.CertDlo ...
Processing theory LinearQuantifierElim.QEdlo_inf ...
Processing theory LinearQuantifierElim.LinArith ...
Processing theory LinearQuantifierElim.CertLin ...
Processing theory Universal_Turing_Machine.Recs ...
Processing theory LinearQuantifierElim.QEdlo_ex ...
Processing theory LinearQuantifierElim.QElin ...
Processing theory LinearQuantifierElim.QElin_opt ...
Processing theory LinearQuantifierElim.QElin_inf ...
Removing 16 theories ...
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 ...
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 ...
Removing 5 theories ...
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 ...
Processing theory ClockSynchInst.ICAInstance ...
Processing theory Derangements.Derangements ...
Processing theory FFT.FFT ...
Processing theory FunWithFunctions.FunWithFunctions ...
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 27 theories ...
Processing theory Approximation_Algorithms.Approx_BP_Hoare ...
Removing 44 theories ...
Processing theory WebAssembly.Wasm_Type_Abs ...
Processing theory Word_Lib.Even_More_List ...
Processing theory Word_Lib.Singleton_Bit_Shifts ...
Processing theory Word_Lib.Legacy_Aliases ...
Processing theory Word_Lib.Aligned ...
Processing theory Word_Lib.Signed_Division_Word ...
Processing theory Native_Word.Code_Target_Word_Base ...
Processing theory Native_Word.Word_Type_Copies ...
Processing theory Native_Word.Uint8 ...
Processing theory Word_Lib.Bits_Int ...
Processing theory Word_Lib.Typedef_Morphisms ...
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_Interpreter ...
Processing theory WebAssembly.Wasm_Checker ...
Processing theory WebAssembly.Wasm_Checker_Printing ...
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 ...
Removing 7 theories ...
Processing theory Binding_Syntax_Theory.Pick ...
Processing theory WebAssembly.Wasm_Soundness ...
Processing theory Binding_Syntax_Theory.Preliminaries ...
Processing theory Binding_Syntax_Theory.Equiv_Relation2 ...
Processing theory Binding_Syntax_Theory.QuasiTerms_Swap_Fresh ...
Processing theory Binding_Syntax_Theory.QuasiTerms_PickFresh_Alpha ...
Processing theory Binding_Syntax_Theory.QuasiTerms_Environments_Substitution ...
Removing 1 theories ...
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 ...
Processing theory Binding_Syntax_Theory.Recursion ...
Removing 12 theories ...
Processing theory WebAssembly.Wasm_Checker_Properties ...
Loading 66 theories ...
Processing theory Word_Lib.Syntax_Bundles ...
Processing theory Word_Lib.Bitwise ...
Processing theory X86_Semantics.BitByte ...
Processing theory X86_Semantics.Memory ...
Processing theory CSP_RefTK.Fix_ind_ext ...
Processing theory HOL-CSP.Process ...
Processing theory HOL-CSP.Bot ...
Processing theory X86_Semantics.State ...
Processing theory X86_Semantics.StateCleanUp ...
Removing 11 theories ...
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 ...
Processing theory HOL-CSP.Mndet ...
Processing theory X86_Semantics.X86_InstructionSemantics ...
Processing theory X86_Semantics.SymbolicExecution ...
Processing theory X86_Semantics.X86_Parse ...
Processing theory X86_Semantics.Examples ...
Processing theory HOL-CSP.Hide ...
Processing theory HOL-CSP.Seq ...
Processing theory HOL-CSP.Sync ...
Removing 1 theories ...
Processing theory HOL-CSP.CSP ...
Processing theory HOL-CSP.Assertions ...
Processing theory HOL-CSP.Conclusion ...
Processing theory HOL-CSP.CopyBuffer ...
Removing 1 theories ...
Processing theory CSP_RefTK.Assertions_ext ...
Processing theory CSP_RefTK.Properties ...
Processing theory CSP_RefTK.Process_norm ...
Processing theory CSP_RefTK.CopyBuffer_props ...
Removing 2 theories ...
Processing theory CSP_RefTK.DiningPhilosophers ...
Removing 18 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 ...
Removing 17 theories ...
Processing theory Flyspeck-Tame.Worklist ...
Processing theory Flyspeck-Tame.Maps ...
Processing theory Trie.Tries ...
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.Enumerator ...
Processing theory Flyspeck-Tame.GraphProps ...
Processing theory Flyspeck-Tame.TameProps ...
Processing theory Flyspeck-Tame.EnumeratorProps ...
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 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.Plane1Props ...
Processing theory Flyspeck-Tame.ScoreProps ...
Processing theory Flyspeck-Tame.LowerBound ...
Processing theory Flyspeck-Tame.GeneratorProps ...
Processing theory Flyspeck-Tame.TameEnumProps ...
Processing theory Flyspeck-Tame.ArchCompProps ...
Processing theory Flyspeck-Tame.Relative_Completeness ...
Removing 34 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 ...
Removing 11 theories ...
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.JVMState ...
Processing theory JinjaDCI.WellForm ...
Processing theory JinjaDCI.PCompiler ...
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 JinjaDCI.JVMInstructions ...
Processing theory JinjaDCI.JVMExceptions ...
Processing theory Jinja.SemilatAlg ...
Processing theory Jinja.Kildall_1 ...
Processing theory Jinja.LBVSpec ...
Processing theory Jinja.LBVComplete ...
Processing theory Jinja.LBVCorrect ...
Processing theory Jinja.Typing_Framework_err ...
Processing theory Jinja.Typing_Framework_2 ...
Processing theory JinjaDCI.SemiType ...
Processing theory JinjaDCI.JVM_SemiType ...
Processing theory JinjaDCI.JVMExecInstr ...
Processing theory JinjaDCI.JVMExec ...
Processing theory JinjaDCI.Expr ...
Processing theory JinjaDCI.WWellForm ...
Processing theory JinjaDCI.WellType ...
Processing theory JinjaDCI.Annotate ...
Processing theory JinjaDCI.JVMDefensive ...
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.BigStep ...
Processing theory JinjaDCI.DefAss ...
Processing theory JinjaDCI.JWellForm ...
Processing theory JinjaDCI.SmallStep ...
Processing theory JinjaDCI.StartProg ...
Processing theory JinjaDCI.TF_JVM ...
Processing theory JinjaDCI.EConform ...
Processing theory JinjaDCI.BVExec ...
Processing theory JinjaDCI.Progress ...
Processing theory JinjaDCI.LBVJVM ...
Processing theory JinjaDCI.J1 ...
Processing theory JinjaDCI.Compiler1 ...
Processing theory JinjaDCI.Compiler2 ...
Processing theory JinjaDCI.J1WellForm ...
Processing theory JinjaDCI.TypeSafe ...
Processing theory JinjaDCI.Correctness1 ...
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 20 theories ...
Processing theory JinjaDCI.JinjaDCI ...
Removing 38 theories ...
Processing theory Factored_Transition_System_Bounding.HoArithUtils ...
Processing theory Factored_Transition_System_Bounding.RelUtils ...
Processing theory Factored_Transition_System_Bounding.FactoredSystemLib ...
Processing theory Factored_Transition_System_Bounding.FmapUtils ...
Processing theory Factored_Transition_System_Bounding.ListUtils ...
Processing theory Factored_Transition_System_Bounding.SetUtils ...
Processing theory Factored_Transition_System_Bounding.Acyclicity ...
Processing theory Factored_Transition_System_Bounding.FSSublist ...
Processing theory Buildings.Prelim ...
Processing theory Buildings.Simplicial ...
Processing theory Buildings.Algebra ...
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 ...
Processing theory Factored_Transition_System_Bounding.SystemAbstraction ...
Processing theory Factored_Transition_System_Bounding.AcycSspace ...
Processing theory Buildings.Chamber ...
Removing 8 theories ...
Processing theory Buildings.Coxeter ...
Processing theory Buildings.Building ...
Loading 46 theories ...
Processing theory Collections.Partial_Equivalence_Relation ...
Processing theory LocalLexing.CFG ...
Processing theory LocalLexing.InductRules ...
Processing theory LocalLexing.ListTools ...
Processing theory Separation_Logic_Imperative_HOL.Imp_List_Spec ...
Processing theory Separation_Logic_Imperative_HOL.Imp_Map_Spec ...
Processing theory LocalLexing.LocalLexing ...
Processing theory LocalLexing.LLEarleyParsing ...
Processing theory Separation_Logic_Imperative_HOL.Imp_Set_Spec ...
Processing theory Separation_Logic_Imperative_HOL.List_Seg ...
Processing theory LocalLexing.Limit ...
Processing theory LocalLexing.LocalLexingLemmas ...
Processing theory Separation_Logic_Imperative_HOL.Array_Blit ...
Processing theory Separation_Logic_Imperative_HOL.Array_Map_Impl ...
Processing theory Separation_Logic_Imperative_HOL.Array_Set_Impl ...
Processing theory Collections.Code_Target_ICF ...
Processing theory Separation_Logic_Imperative_HOL.Open_List ...
Processing theory Separation_Logic_Imperative_HOL.Circ_List ...
Processing theory Separation_Logic_Imperative_HOL.Union_Find ...
Processing theory LocalLexing.Derivations ...
Processing theory LocalLexing.Validity ...
Processing theory Native_Word.Uint32 ...
Processing theory Collections.HashCode ...
Processing theory Separation_Logic_Imperative_HOL.Hash_Table ...
Removing 7 theories ...
Processing theory LocalLexing.TheoremD2 ...
Processing theory Separation_Logic_Imperative_HOL.Hash_Map ...
Processing theory Separation_Logic_Imperative_HOL.Hash_Map_Impl ...
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 LocalLexing.TheoremD4 ...
Processing theory Separation_Logic_Imperative_HOL.To_List_GA ...
Processing theory Separation_Logic_Imperative_HOL.Sep_Examples ...
Processing theory LocalLexing.TheoremD5 ...
Processing theory LocalLexing.TheoremD6 ...
Processing theory LocalLexing.TheoremD7 ...
Processing theory LocalLexing.TheoremD8 ...
Processing theory LocalLexing.TheoremD9 ...
Removing 45 theories ...
Processing theory LocalLexing.Ladder ...
Processing theory LocalLexing.TheoremD10 ...
Processing theory LocalLexing.TheoremD11 ...
Processing theory LocalLexing.TheoremD12 ...
Loading 20 theories ...
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 Jordan_Hoelder.GroupIsoClasses ...
Processing theory Modular_Assembly_Kit_Security.Projection ...
Processing theory Modular_Assembly_Kit_Security.Views ...
Processing theory Modular_Assembly_Kit_Security.EventSystems ...
Processing theory Modular_Assembly_Kit_Security.BasicSecurityPredicates ...
Processing theory Secondary_Sylow.GroupAction ...
Processing theory Secondary_Sylow.SubgroupConjugation ...
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 Modular_Assembly_Kit_Security.BSPTaxonomy ...
Processing theory Modular_Assembly_Kit_Security.CompositionBase ...
Processing theory Modular_Assembly_Kit_Security.CompositionSupport ...
Processing theory Jordan_Hoelder.CompositionSeries ...
Processing theory Jordan_Hoelder.JordanHolder ...
Removing 35 theories ...
Processing theory Modular_Assembly_Kit_Security.GeneralizedZippingLemma ...
Processing theory Modular_Assembly_Kit_Security.CompositionalityResults ...
Loading 44 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.Subcls ...
Processing theory Regression_Test_Selection.CollectionSemantics ...
Processing theory Regression_Test_Selection.CollectionBasedRTS ...
Processing theory Regression_Test_Selection.JVMSemantics ...
Removing 4 theories ...
Processing theory Regression_Test_Selection.ClassesAbove ...
Processing theory Pi_Calculus.Agent ...
Processing theory Pi_Calculus.Rel ...
Processing theory Regression_Test_Selection.JVMCollectionSemantics ...
Processing theory Inductive_Inference.Partial_Recursive ...
Processing theory Pi_Calculus.Late_Semantics ...
Processing theory Pi_Calculus.Late_Semantics1 ...
Processing theory Pi_Calculus.Late_Tau_Chain ...
Processing theory Pi_Calculus.Weak_Late_Step_Semantics ...
Processing theory Pi_Calculus.Weak_Late_Semantics ...
Processing theory Pi_Calculus.Strong_Late_Sim ...
Processing theory Pi_Calculus.Strong_Late_Bisim ...
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_Step_Sim ...
Processing theory Pi_Calculus.Weak_Late_Cong ...
Processing theory Pi_Calculus.Weak_Late_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_Step_Sim_Pres ...
Processing theory Pi_Calculus.Weak_Late_Cong_Pres ...
Processing theory Regression_Test_Selection.JVMExecStepInductive ...
Removing 5 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 ...
Processing theory Inductive_Inference.Union ...
Processing theory Regression_Test_Selection.JVMCollectionBasedRTS ...
Loading 33 theories ...
Processing theory Regression_Test_Selection.RTS ...
Processing theory Free-Groups.C2 ...
Processing theory Pi_Calculus.Strong_Late_Bisim_Subst ...
Processing theory Pi_Calculus.Strong_Late_Bisim_Subst_Pres ...
Processing theory Free-Groups.Generators ...
Processing theory Free-Groups.UnitGroup ...
Processing theory Pi_Calculus.Strong_Late_Bisim_Subst_SC ...
Processing theory Free-Groups.Cancelation ...
Processing theory Free-Groups.FreeGroups ...
Removing 41 theories ...
Processing theory Free-Groups.Isomorphisms ...
Processing theory Pi_Calculus.Early_Semantics ...
Processing theory Pi_Calculus.Early_Tau_Chain ...
Processing theory Pi_Calculus.Weak_Early_Step_Semantics ...
Processing theory Pi_Calculus.Weak_Early_Semantics ...
Processing theory Pi_Calculus.Strong_Early_Sim ...
Processing theory Pi_Calculus.Strong_Early_Bisim ...
Processing theory Pi_Calculus.Strong_Early_Bisim_Subst ...
Processing theory Pi_Calculus.Strong_Early_Sim_Pres ...
Processing theory Pi_Calculus.Strong_Early_Late_Comp ...
Processing theory Pi_Calculus.Strong_Early_Bisim_SC ...
Processing theory Pi_Calculus.Strong_Early_Bisim_Pres ...
Processing theory Pi_Calculus.Weak_Early_Sim ...
Loading 16 theories ...
Processing theory Pi_Calculus.Weak_Early_Bisim ...
Processing theory Pi_Calculus.Weak_Early_Bisim_Subst ...
Processing theory Pi_Calculus.Weak_Early_Sim_Pres ...
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_Step_Sim_Pres ...
Processing theory Pi_Calculus.Weak_Early_Bisim_SC ...
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.LTS ...
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.ConsInterleave ...
Processing theory Program-Conflict-Analysis.AcquisitionHistory ...
Processing theory Program-Conflict-Analysis.ThreadTracking ...
Processing theory Program-Conflict-Analysis.Flowgraph ...
Removing 31 theories ...
Processing theory Inductive_Inference.LIM_BC ...
Processing theory Program-Conflict-Analysis.Semantics ...
Processing theory Program-Conflict-Analysis.Normalization ...
Processing theory Program-Conflict-Analysis.ConstraintSystems ...
Loading 15 theories ...
Processing theory Program-Conflict-Analysis.MainResult ...
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 ...
Removing 31 theories ...
Processing theory Pi_Calculus.Strong_Late_Expansion_Law ...
Processing theory Universal_Turing_Machine.Turing ...
Processing theory Universal_Turing_Machine.Turing_Hoare ...
Processing theory Universal_Turing_Machine.Uncomputable ...
Processing theory Pi_Calculus.Strong_Late_Axiomatisation ...
Processing theory Universal_Turing_Machine.Abacus_Mopup ...
Removing 10 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 29 theories ...
Processing theory Card_Multisets.Card_Multisets ...
Processing theory Card_Number_Partitions.Additions_to_Main ...
Processing theory Card_Partitions.Card_Partitions ...
Removing 5 theories ...
Processing theory Card_Number_Partitions.Number_Partition ...
Processing theory Card_Number_Partitions.Card_Number_Partitions ...
Processing theory AI_Planning_Languages_Semantics.Lifschitz_Consistency ...
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 Elliptic_Curves_Group_Law.Elliptic_Axclass ...
Processing theory Twelvefold_Way.Twelvefold_Way_Core ...
Processing theory Twelvefold_Way.Equiv_Relations_on_Functions ...
Removing 7 theories ...
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_Entry7 ...
Processing theory Twelvefold_Way.Twelvefold_Way_Entry5 ...
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 IFC_Tracking.IFC ...
Processing theory IFC_Tracking.PDG ...
Processing theory Twelvefold_Way.Card_Bijections ...
Removing 2 theories ...
Processing theory Twelvefold_Way.Card_Bijections_Direct ...
Loading 79 theories ...
Processing theory Twelvefold_Way.Twelvefold_Way ...
Processing theory Network_Security_Policy_Verification.ML_GraphViz ...
Processing theory Network_Security_Policy_Verification.TopoS_Util ...
Processing theory Network_Security_Policy_Verification.TopoS_Vertices ...
Processing theory Network_Security_Policy_Verification.FiniteGraph ...
Processing theory Transitive-Closure.Transitive_Closure_Impl ...
Processing theory Transitive-Closure.Transitive_Closure_List_Impl ...
Processing theory Network_Security_Policy_Verification.vertex_example_simps ...
Processing theory PCF.Basis ...
Processing theory Network_Security_Policy_Verification.TopoS_Interface ...
Processing theory Network_Security_Policy_Verification.Efficient_Distinct ...
Processing theory Network_Security_Policy_Verification.FiniteListGraph ...
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_BLPbasic ...
Processing theory Network_Security_Policy_Verification.SINVAR_BLPtrusted ...
Processing theory PCF.Logical_Relations ...
Processing theory Network_Security_Policy_Verification.FiniteListGraph_Impl ...
Removing 26 theories ...
Processing theory Network_Security_Policy_Verification.SINVAR_ACLnotCommunicateWith ...
Processing theory Network_Security_Policy_Verification.SINVAR_Dependability ...
Processing theory Network_Security_Policy_Verification.SINVAR_Dependability_norefl ...
Processing theory Network_Security_Policy_Verification.SINVAR_NoRefl ...
Processing theory Network_Security_Policy_Verification.SINVAR_Tainting ...
Processing theory Network_Security_Policy_Verification.SINVAR_NonInterference ...
Processing theory Network_Security_Policy_Verification.SINVAR_Sink ...
Processing theory Network_Security_Policy_Verification.SINVAR_SecGwExt ...
Processing theory Network_Security_Policy_Verification.SINVAR_Subnets ...
Processing theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted ...
Processing theory Network_Security_Policy_Verification.SINVAR_SubnetsInGW ...
Processing theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners ...
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_BLPtrusted_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_CommunicationPartners_impl ...
Processing theory Network_Security_Policy_Verification.SINVAR_BLPbasic_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.TopoS_Composition_Theory ...
Processing theory Network_Security_Policy_Verification.TopoS_Stateful_Policy ...
Processing theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG ...
Processing theory Network_Security_Policy_Verification.SINVAR_DomainHierarchyNG_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.TopoS_Stateful_Policy_Algorithm ...
Processing theory Network_Security_Policy_Verification.TopoS_Composition_Theory_impl ...
Processing theory PCF.PCF ...
Processing theory Network_Security_Policy_Verification.SINVAR_TaintingTrusted_impl ...
Processing theory Network_Security_Policy_Verification.TopoS_Library ...
Processing theory Network_Security_Policy_Verification.METASINVAR_SystemBoundary ...
Processing theory Network_Security_Policy_Verification.TopoS_Stateful_Policy_impl ...
Processing theory Network_Security_Policy_Verification.TopoS_Impl ...
Processing theory Network_Security_Policy_Verification.Example_Forte14 ...
Processing theory PCF.OpSem ...
Processing theory PCF.SmallStep ...
Processing theory Network_Security_Policy_Verification.I8_SSH_Landscape ...
Processing theory Network_Security_Policy_Verification.Impl_List_Playground ...
Removing 5 theories ...
Processing theory Network_Security_Policy_Verification.Distributed_WebApp ...
Processing theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork ...
Processing theory Network_Security_Policy_Verification.Impl_List_Playground_ChairNetwork_statefulpolicy_example ...
Processing theory Network_Security_Policy_Verification.Impl_List_Playground_statefulpolicycompliance ...
Processing theory Network_Security_Policy_Verification.CryptoDB ...
Processing theory Network_Security_Policy_Verification.IDEM ...
Removing 6 theories ...
Processing theory Network_Security_Policy_Verification.Network_Security_Policy_Verification ...
Processing theory Network_Security_Policy_Verification.MeasrDroid ...
Processing theory Network_Security_Policy_Verification.SINVAR_Examples ...
Removing 3 theories ...
Processing theory Network_Security_Policy_Verification.Imaginary_Factory_Network ...
Loading 47 theories ...
Processing theory Isabelle_Meta_Model.Isabelle_Cartouche_Examples ...
Processing theory Isabelle_Meta_Model.Isabelle_Main0 ...
Processing theory Isabelle_Meta_Model.Antiquote_Setup ...
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_Static ...
Processing theory Isabelle_Meta_Model.Toy_Library ...
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 ...
Removing 50 theories ...
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 ...
Processing theory Isabelle_Meta_Model.Meta_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_infra ...
Processing theory Isabelle_Meta_Model.Parser_META ...
Processing theory Isabelle_Meta_Model.Printer_Isabelle ...
Processing theory Isabelle_Meta_Model.Printer_META ...
Processing theory Isabelle_Meta_Model.Floor1_examp ...
Processing theory Isabelle_Meta_Model.Floor2_examp ...
Processing theory Isabelle_Meta_Model.Core ...
Processing theory Isabelle_Meta_Model.Printer ...
Processing theory Localization_Ring.Localization ...
Processing theory Isabelle_Meta_Model.Generator_dynamic_sequential ...
Processing theory Isabelle_Meta_Model.Design_deep ...
Processing theory Isabelle_Meta_Model.Rail ...
Removing 6 theories ...
Processing theory Isabelle_Meta_Model.Design_shallow ...
Processing theory Isabelle_Meta_Model.Design_generated ...
Loading 35 theories ...
Processing theory LatticeProperties.Conj_Disj ...
Processing theory LatticeProperties.WellFoundedTransitive ...
Processing theory LatticeProperties.Complete_Lattice_Prop ...
Processing theory MonoBoolTranAlgebra.Mono_Bool_Tran ...
Processing theory MonoBoolTranAlgebra.Mono_Bool_Tran_Algebra ...
Processing theory MonoBoolTranAlgebra.Assertion_Algebra ...
Processing theory SequentInvertibility.MultiSequents ...
Removing 5 theories ...
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 ...
Processing theory SequentInvertibility.ModalSequents ...
Processing theory SequentInvertibility.SequentInvertibility ...
Processing theory Stone_Relation_Algebras.Semirings ...
Processing theory Correctness_Algebras.Base ...
Removing 13 theories ...
Processing theory Stone_Algebras.P_Algebras ...
Processing theory Correctness_Algebras.Monotonic_Boolean_Transformers ...
Processing theory Stone_Kleene_Relation_Algebras.Iterings ...
Processing theory Stone_Kleene_Relation_Algebras.Kleene_Algebras ...
Processing theory Correctness_Algebras.Omega_Algebras ...
Processing theory Correctness_Algebras.General_Refinement_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.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 21 theories ...
Processing theory Circus.Var_list ...
Processing theory Circus.Var ...
Processing theory Perfect-Number-Thm.PerfectBasics ...
Processing theory Orbit_Stabiliser.Left_Coset ...
Processing theory Circus.Relations ...
Processing theory Circus.Designs ...
Processing theory Orbit_Stabiliser.Orbit_Stabiliser ...
Processing theory Perfect-Number-Thm.Sigma ...
Processing theory Perfect-Number-Thm.Perfect ...
Removing 16 theories ...
Processing theory Orbit_Stabiliser.Tetrahedron ...
Processing theory Circus.Reactive_Processes ...
Processing theory Correctness_Algebras.Test_Iterings ...
Processing theory Circus.CSP_Processes ...
Processing theory Circus.Circus_Actions ...
Processing theory Correctness_Algebras.N_Semirings ...
Removing 4 theories ...
Processing theory Circus.Denotational_Semantics ...
Processing theory Circus.Circus_Syntax ...
Processing theory Circus.Refinement ...
Processing theory Circus.Refinement_Example ...
Processing theory Correctness_Algebras.N_Semirings_Boolean ...
Removing 11 theories ...
Processing theory Correctness_Algebras.N_Semirings_Modal ...
Loading 33 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 Correctness_Algebras.Approximation ...
Processing theory Clean.Hoare_MonadSE ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.NatInt ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.RealInt ...
Processing theory Clean.Clean ...
Processing theory Clean.Clean_Symbex ...
Processing theory Clean.Hoare_Clean ...
Processing theory Generalized_Counting_Sort.Algorithm ...
Processing theory Clean.IsPrime ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Traffic ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Views ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Move ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Restriction ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Sensors ...
Processing theory Fermat3_4.Fermat4 ...
Removing 7 theories ...
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 Generalized_Counting_Sort.Conservation ...
Processing theory Correctness_Algebras.Recursion_Strict ...
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 ...
Removing 3 theories ...
Processing theory Generalized_Counting_Sort.Sorting ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Safety_Perfect ...
Processing theory Generalized_Counting_Sort.Stability ...
Processing theory Hybrid_Multi_Lane_Spatial_Logic.Safety_Regular ...
Loading 44 theories ...
Removing 20 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.CM ...
Processing theory Sort_Encodings.U ...
Processing theory Sort_Encodings.CU ...
Processing theory PCF.Continuations ...
Processing theory Sort_Encodings.Mono ...
Processing theory AWN.AWN ...
Removing 14 theories ...
Processing theory AWN.AWN_SOS ...
Processing theory AWN.AWN_Cterms ...
Processing theory AWN.AWN_Labels ...
Processing theory AWN.Inv_Cterms ...
Processing theory Sort_Encodings.Mcalc ...
Processing theory Sort_Encodings.T_G_Prelim ...
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_Invariants ...
Processing theory AWN.OAWN_SOS_Labels ...
Processing theory AWN.OPnet ...
Processing theory Sort_Encodings.Mcalc2 ...
Processing theory AWN.OAWN_Convert ...
Processing theory AWN.ONode_Lifting ...
Processing theory AWN.Qmsg_Lifting ...
Processing theory Sort_Encodings.Mcalc2C ...
Processing theory Sort_Encodings.T ...
Processing theory AWN.OPnet_Lifting ...
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 ...
Processing theory AWN.Toy ...
Loading 44 theories ...
Processing theory KBPs.Extra ...
Processing theory MSO_Regex_Equivalence.List_More ...
Processing theory Isabelle_Meta_Model.Generator_static ...
Processing theory KBPs.MapOps ...
Processing theory MSO_Regex_Equivalence.Pi_Regular_Set ...
Processing theory KBPs.Traces ...
Processing theory KBPs.Kripke ...
Processing theory KBPs.DFS ...
Processing theory Stable_Matching.Basis ...
Removing 77 theories ...
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.PNormalization ...
Processing theory MSO_Regex_Equivalence.Pi_Equivalence_Checking ...
Processing theory MSO_Regex_Equivalence.Formula ...
Processing theory Stable_Matching.Contracts ...
Processing theory MSO_Regex_Equivalence.WS1S ...
Processing theory MSO_Regex_Equivalence.WS1S_Normalization ...
Processing theory Stable_Matching.COP ...
Processing theory Stable_Matching.Strategic ...
Processing theory Stable_Matching.Bossiness ...
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 33 theories ...
Processing theory Key_Agreement_Strong_Adversaries.Infra ...
Processing theory Higher_Order_Terms.Find_First ...
Processing theory Higher_Order_Terms.Fresh_Monad ...
Processing theory Key_Agreement_Strong_Adversaries.Refinement ...
Processing theory Key_Agreement_Strong_Adversaries.Messages ...
Processing theory Key_Agreement_Strong_Adversaries.Message_derivation ...
Processing theory Key_Agreement_Strong_Adversaries.IK ...
Processing theory Key_Agreement_Strong_Adversaries.Secrecy ...
Processing theory Key_Agreement_Strong_Adversaries.AuthenticationN ...
Processing theory Key_Agreement_Strong_Adversaries.AuthenticationI ...
Processing theory Key_Agreement_Strong_Adversaries.Runs ...
Processing theory Higher_Order_Terms.Fresh_Class ...
Processing theory Higher_Order_Terms.Nterm ...
Processing theory Higher_Order_Terms.Term ...
Processing theory Higher_Order_Terms.Pats ...
Processing theory Correctness_Algebras.Domain ...
Removing 5 theories ...
Processing theory Free-Groups.PingPongLemma ...
Processing theory Key_Agreement_Strong_Adversaries.Channels ...
Processing theory Higher_Order_Terms.Term_to_Nterm ...
Processing theory Key_Agreement_Strong_Adversaries.Payloads ...
Processing theory Key_Agreement_Strong_Adversaries.Implem ...
Processing theory Key_Agreement_Strong_Adversaries.Implem_lemmas ...
Processing theory Key_Agreement_Strong_Adversaries.Implem_asymmetric ...
Processing theory Key_Agreement_Strong_Adversaries.Implem_symmetric ...
Processing theory Correctness_Algebras.Lattice_Ordered_Semirings ...
Removing 20 theories ...
Processing theory Key_Agreement_Strong_Adversaries.dhlvl1 ...
Processing theory Correctness_Algebras.Domain_Iterings ...
Processing theory Correctness_Algebras.Domain_Recursion ...
Removing 2 theories ...
Processing theory Key_Agreement_Strong_Adversaries.sklvl1 ...
Processing theory Key_Agreement_Strong_Adversaries.sklvl2 ...
Processing theory Key_Agreement_Strong_Adversaries.sklvl3 ...
Loading 53 theories ...
Processing theory Key_Agreement_Strong_Adversaries.sklvl3_asymmetric ...
Processing theory Key_Agreement_Strong_Adversaries.sklvl3_symmetric ...
Processing theory Optics.Interp ...
Processing theory Presburger-Automata.DFS ...
Processing theory Optics.Two ...
Processing theory Tycon.Coerce ...
Processing theory Isabelle_C.C_Lexer_Language ...
Processing theory Isabelle_C.C_Lexer_Annotation ...
Processing theory Optics.Lens_Laws ...
Processing theory Optics.Lens_Algebra ...
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.Monad_Zero ...
Processing theory Tycon.Error_Monad ...
Processing theory Tycon.Resumption_Transformer ...
Processing theory Tycon.Error_Transformer ...
Processing theory Optics.Lens_Order ...
Processing theory Optics.Lens_Symmetric ...
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 Tycon.Writer_Transformer ...
Processing theory Tycon.Monad_Transformer ...
Removing 23 theories ...
Processing theory Optics.Lens_Instances ...
Processing theory Optics.Lenses ...
Processing theory Isabelle_C.C_Ast ...
Processing theory Isabelle_C.C_Environment ...
Processing theory Isabelle_C.C_Parser_Annotation ...
Processing theory Optics.Scenes ...
Processing theory Optics.Prisms ...
Processing theory Optics.Channel_Type ...
Processing theory Optics.Dataspace ...
Processing theory Optics.Optics ...
Processing theory Optics.Lens_Record_Example ...
Processing theory Isabelle_C.C_Parser_Language ...
Processing theory Isabelle_C.C_Eval ...
Processing theory Isabelle_C.C_Command ...
### Ignored report message: \freeify{}\isacommand{}
### Ignored report message: \freeify{}\isacommand{}
### Ignored report message: \freeify{}\isacommand{}
### Ignored report message: \freeify{}
### Ignored report message: \freeify{}\freeify{}
### Ignored report message: \freeify{}int
### Ignored report message: \freeify{}array\ int
### Ignored report message: \freeify{}\isacommand{}
### Ignored report message: \freeify{}\isacommand{}
### Ignored report message: \freeify{}
### Ignored report message: \freeify{}
### Ignored report message: \freeify{}
### Ignored report message: \freeify{}\freeify{}\freeify{}
### Ignored report message: \freeify{}int\freeify{}\isacommand{}
### Ignored report message: \freeify{}
### Ignored report message: \freeify{}\isacommand{}
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 17 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 45 theories ...
Processing theory Separation_Algebra.Sep_Tactics ...
Processing theory Shivers-CFA.Utils ...
Processing theory Shivers-CFA.SetMap ...
Processing theory Separation_Algebra.Map_Extra ...
Processing theory Universal_Turing_Machine.Abacus_Defs ...
Processing theory Shivers-CFA.HOLCFUtils ...
Processing theory WorkerWrapper.FixedPointTheorems ...
Processing theory WorkerWrapper.Maybe ...
Processing theory WorkerWrapper.Nats ...
Processing theory WorkerWrapper.WorkerWrapper ...
Processing theory WorkerWrapper.LList ...
Processing theory Shivers-CFA.CPSScheme ...
Processing theory Binomial-Heaps.BinomialHeap ...
Processing theory Shivers-CFA.AbsCF ...
Processing theory Shivers-CFA.ExCF ...
Removing 26 theories ...
Processing theory WorkerWrapper.WorkerWrapperNew ...
Processing theory WorkerWrapper.Last ...
Processing theory Shivers-CFA.ExCFSV ...
Processing theory WorkerWrapper.Accumulator ...
Processing theory Shivers-CFA.AbsCFCorrect ...
Processing theory WorkerWrapper.Nub ...
Processing theory WorkerWrapper.UnboxedNats ...
Processing theory WorkerWrapper.Continuations ...
Processing theory WorkerWrapper.Backtracking ...
Processing theory Separation_Algebra.Types_D ...
Processing theory Correctness_Algebras.Extended_Designs ...
Processing theory Binomial-Heaps.SkewBinomialHeap ...
Processing theory Binomial-Heaps.Test ...
Processing theory Separation_Algebra.Abstract_Separation_D ...
Processing theory Separation_Algebra.Separation_D ...
Processing theory RIPEMD-160-SPARK.RIPEMD_160_SPARK ...
Loading 34 theories ...
Removing 40 theories ...
Processing theory Completeness.PermutationLemmas ...
Processing theory Completeness.Tree ...
Processing theory Locally-Nameless-Sigma.ListPre ...
Processing theory Locally-Nameless-Sigma.FMap ...
Processing theory Shivers-CFA.MapSets ...
Processing theory Completeness.Base ...
Processing theory Locally-Nameless-Sigma.Environments ...
Processing theory Shivers-CFA.CPSUtils ...
Processing theory Completeness.Formula ...
Processing theory Completeness.Sequents ...
Processing theory Shivers-CFA.FixTransform ...
Processing theory Shivers-CFA.Computability ...
Processing theory Completeness.Completeness ...
Processing theory Completeness.Soundness ...
Processing theory Category2.Category ...
Processing theory Category2.Functors ...
Processing theory Category2.NatTrans ...
Processing theory WorkerWrapper.CounterExample ...
Processing theory WorkerWrapper.Streams ...
Processing theory Shivers-CFA.AbsCFComp ...
Processing theory Category2.Universe ...
Processing theory Category2.SetCat ...
Processing theory Category2.Yoneda ...
Processing theory Locally-Nameless-Sigma.Sigma ...
Processing theory LightweightJava.Lightweight_Java_Definition ...
Processing theory LightweightJava.Lightweight_Java_Equivalence ...
Processing theory Locally-Nameless-Sigma.TypedSigma ...
Removing 24 theories ...
Processing theory Locally-Nameless-Sigma.ParRed ...
Processing theory Locally-Nameless-Sigma.Locally_Nameless_Sigma ...
Processing theory LightweightJava.Lightweight_Java_Proof ...
Loading 38 theories ...
Processing theory First_Order_Terms.Option_Monad ...
Processing theory DiskPaxos.DiskPaxos_Model ...
Processing theory DiskPaxos.DiskPaxos_Inv1 ...
Processing theory First_Order_Terms.Term ...
Processing theory First_Order_Terms.Unifiers ...
Processing theory Resolution_FOL.Tree ...
Processing theory First_Order_Terms.Term_Pair_Multiset ...
Processing theory List_Inversions.List_Inversions ...
Removing 12 theories ...
Processing theory Propositional_Proof_Systems.SC ...
Processing theory Propositional_Proof_Systems.Compactness ...
Processing theory Stream-Fusion.LazyList ...
Processing theory Shivers-CFA.Eval ...
Processing theory Stream-Fusion.Stream ...
Processing theory MuchAdoAboutTwo.MuchAdoAboutTwo ...
Processing theory Resolution_FOL.TermsAndLiterals ...
Processing theory Propositional_Proof_Systems.SC_Cut ...
Processing theory DiskPaxos.DiskPaxos_Inv2 ...
Processing theory Propositional_Proof_Systems.SC_Sema ...
Processing theory Stream-Fusion.StreamFusion ...
Processing theory DiskPaxos.DiskPaxos_Inv3 ...
Processing theory Propositional_Proof_Systems.LSC ...
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 ...
Removing 13 theories ...
Processing theory DiskPaxos.DiskPaxos_Inv5 ...
Processing theory DiskPaxos.DiskPaxos_Chosen ...
Processing theory DiskPaxos.DiskPaxos_Inv6 ...
Processing theory DiskPaxos.DiskPaxos_Invariant ...
Processing theory DiskPaxos.DiskPaxos ...
Processing theory Resolution_FOL.Resolution ...
Processing theory Resolution_FOL.Unification_Theorem ...
Removing 10 theories ...
Processing theory Resolution_FOL.Completeness ...
Loading 25 theories ...
Processing theory Resolution_FOL.Completeness_Instance ...
### Ignored report message: \freeify{}
### Ignored report message: \freeify{}
Processing theory Isabelle_C.C_paper ...
Processing theory Isabelle_C.C0 ...
Processing theory Isabelle_C.C2 ...
Processing theory Dominance_CHK.Sorted_Less2 ...
Processing theory Dominance_CHK.Sorted_List_Operations2 ...
Processing theory CSP_RefTK.Conclusion ...
Processing theory CSP_RefTK.Introduction ...
Processing theory HOL-CSP.Introduction ...
Processing theory Dominance_CHK.Cfg ...
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 Dominance_CHK.Dom_Semi_List ...
Processing theory Dominance_CHK.Dom_Kildall ...
Processing theory Correctness_Algebras.Binary_Iterings ...
Processing theory Correctness_Algebras.Binary_Iterings_Strict ...
Removing 63 theories ...
Processing theory Correctness_Algebras.N_Algebras ...
Processing theory Dominance_CHK.Dom_Kildall_Property ...
Processing theory Dominance_CHK.Dom_Kildall_Correct ...
Processing theory Correctness_Algebras.Recursion ...
Removing 16 theories ...
Processing theory Stone_Relation_Algebras.Relation_Algebras ...
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 78 theories ...
Processing theory CISC-Kernel.List_Theorems ...
Processing theory CISC-Kernel.Option_Binders ...
Processing theory CISC-Kernel.K ...
Processing theory CISC-Kernel.Step_configuration ...
Processing theory CISC-Kernel.Step_policies ...
Processing theory Decl_Sem_Fun_PL.Lambda ...
Processing theory Decl_Sem_Fun_PL.SmallStepLam ...
Processing theory CISC-Kernel.Step ...
Removing 6 theories ...
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 ...
Processing theory CISC-Kernel.SK ...
Processing theory Decl_Sem_Fun_PL.BigStepLam ...
Processing theory Possibilistic_Noninterference.MyTactics ...
Processing theory Possibilistic_Noninterference.Interface ...
Processing theory Possibilistic_Noninterference.Bisim ...
Processing theory Possibilistic_Noninterference.Language_Semantics ...
Processing theory Ribbon_Proofs.JHelper ...
Processing theory Ribbon_Proofs.Proofchain ...
Processing theory Ribbon_Proofs.Ribbons_Basic ...
Processing theory CISC-Kernel.ISK ...
Processing theory TESL_Language.TESL ...
Processing theory TESL_Language.Run ...
Processing theory TESL_Language.Denotational ...
Processing theory CISC-Kernel.CISK ...
Processing theory CISC-Kernel.Separation_kernel_model ...
Processing theory CISC-Kernel.Link_separation_kernel_model_to_CISK ...
Processing theory Possibilistic_Noninterference.During_Execution ...
Processing theory Possibilistic_Noninterference.After_Execution ...
Processing theory TESL_Language.SymbolicPrimitive ...
Processing theory TESL_Language.Operational ...
Processing theory Key_Agreement_Strong_Adversaries.dhlvl2 ...
Processing theory TESL_Language.Corecursive_Prop ...
Processing theory TESL_Language.Hygge_Theory ...
Processing theory TESL_Language.Config_Morphisms ...
Processing theory Decl_Sem_Fun_PL.ValuesFSet ...
Processing theory Decl_Sem_Fun_PL.ValuesFSetProps ...
Processing theory Propositional_Proof_Systems.SC_Depth ...
Removing 23 theories ...
Processing theory Propositional_Proof_Systems.SC_Gentzen ...
Processing theory Propositional_Proof_Systems.SC_Depth_Limit ...
Processing theory Decl_Sem_Fun_PL.DeclSemAsDenotFSet ...
Processing theory Decl_Sem_Fun_PL.ChangeEnv ...
Processing theory Decl_Sem_Fun_PL.DenotSoundFSet ...
Processing theory Decl_Sem_Fun_PL.DenotCompleteFSet ...
Processing theory Ribbon_Proofs.Ribbons_Interfaces ...
Processing theory Ribbon_Proofs.Ribbons_Graphical ...
Processing theory Ribbon_Proofs.More_Finite_Map ...
Processing theory Finite-Map-Extras.Finite_Map_Extras ...
Processing theory Possibilistic_Noninterference.Compositionality ...
Processing theory Decl_Sem_Fun_PL.DenotCongruenceFSet ...
Processing theory Decl_Sem_Fun_PL.DenotEqualitiesFSet ...
Processing theory Decl_Sem_Fun_PL.Optimizer ...
Processing theory Possibilistic_Noninterference.Syntactic_Criteria ...
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.Strong_Sim_SC ...
Processing theory CCS.Tau_Chain ...
Processing theory CCS.Struct_Cong ...
Processing theory CCS.Weak_Cong_Semantics ...
Processing theory CCS.Weak_Semantics ...
Processing theory CCS.Weak_Sim ...
Processing theory CCS.Weak_Sim_Pres ...
Processing theory Ribbon_Proofs.Ribbons_Graphical_Soundness ...
Processing theory Possibilistic_Noninterference.Concrete ...
Removing 23 theories ...
Processing theory CCS.Strong_Bisim_SC ...
Processing theory CCS.Weak_Cong_Sim ...
Processing theory CCS.Weak_Cong_Sim_Pres ...
Processing theory CCS.Weak_Bisim ...
Processing theory CCS.Weak_Cong ...
Processing theory CCS.Weak_Bisim_Pres ...
Processing theory CCS.Weak_Cong_Pres ...
Processing theory Key_Agreement_Strong_Adversaries.dhlvl3 ...
Loading 33 theories ...
Processing theory Key_Agreement_Strong_Adversaries.dhlvl3_asymmetric ...
Processing theory Key_Agreement_Strong_Adversaries.dhlvl3_symmetric ...
Processing theory Modular_Assembly_Kit_Security.InformationFlowProperties ...
Processing theory Modular_Assembly_Kit_Security.PropertyLibrary ...
Processing theory Security_Protocol_Refinement.Infra ...
Processing theory Security_Protocol_Refinement.Agents ...
Processing theory Security_Protocol_Refinement.Keys ...
Processing theory Security_Protocol_Refinement.Atoms ...
Processing theory Security_Protocol_Refinement.Channels ...
Processing theory Security_Protocol_Refinement.Runs ...
Processing theory SuperCalc.well_founded_continued ...
Processing theory SuperCalc.multisets_continued ...
Processing theory Resolution_FOL.Examples ...
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 Security_Protocol_Refinement.s0g_secrecy ...
Processing theory SuperCalc.terms ...
Processing theory SuperCalc.equational_clausal_logic ...
Processing theory Kleene_Algebra.Dioid_Models ...
Processing theory Security_Protocol_Refinement.m1_keydist ...
Processing theory Kleene_Algebra.Kleene_Algebra_Models ...
Removing 31 theories ...
Processing theory KAD.Modal_Kleene_Algebra_Models ...
Processing theory Security_Protocol_Refinement.m1_keydist_iirn ...
Processing theory SuperCalc.superposition ...
Removing 11 theories ...
Processing theory Security_Protocol_Refinement.m1_nssk ...
Processing theory Security_Protocol_Refinement.m1_kerberos ...
Processing theory Security_Protocol_Refinement.m2_nssk ...
Processing theory Security_Protocol_Refinement.m3_nssk_par ...
Processing theory Security_Protocol_Refinement.m3_nssk ...
Processing theory Security_Protocol_Refinement.m2_kerberos ...
Removing 4 theories ...
Processing theory Security_Protocol_Refinement.m3_kerberos_par ...
Removing 1 theories ...
Processing theory Security_Protocol_Refinement.m3_kerberos5 ...
Processing theory Security_Protocol_Refinement.m3_kerberos4 ...
Loading 31 theories ...
Processing theory Allen_Calculus.xor_cal ...
Processing theory Allen_Calculus.axioms ...
Processing theory Noninterference_CSP.CSPNoninterference ...
Processing theory List_Interleaving.ListInterleaving ...
Processing theory Probabilistic_System_Zoo.Bool_Bounded_Set ...
Processing theory Optics.Lens_State ...
Processing theory Euler_Partition.Euler_Partition ...
Processing theory Well_Quasi_Orders.Multiset_Extension ...
Processing theory Noninterference_Ipurge_Unwinding.IpurgeUnwinding ...
Processing theory Noninterference_Ipurge_Unwinding.DeterministicProcesses ...
Processing theory Noninterference_Inductive_Unwinding.InductiveUnwinding ...
Processing theory Probabilistic_System_Zoo.Finitely_Bounded_Set_Counterexample ...
Processing theory Correctness_Algebras.Capped_Omega_Algebras ...
Removing 27 theories ...
Processing theory Propositional_Proof_Systems.ND ...
Processing theory Propositional_Proof_Systems.HC ...
Processing theory Propositional_Proof_Systems.MiniFormulas ...
Processing theory Propositional_Proof_Systems.NDHC ...
Processing theory Propositional_Proof_Systems.SCND ...
Processing theory Propositional_Proof_Systems.HCSC ...
Processing theory Allen_Calculus.allen ...
Processing theory Allen_Calculus.jointly_exhaustive ...
Processing theory Allen_Calculus.disjoint_relations ...
Processing theory Propositional_Proof_Systems.MiniSC ...
Processing theory Propositional_Proof_Systems.MiniSC_HC ...
Processing theory Propositional_Proof_Systems.HCSCND ...
Processing theory Propositional_Proof_Systems.SC_Compl_Consistency ...
Processing theory Well_Quasi_Orders.Wqo_Multiset ...
Removing 8 theories ...
Processing theory Propositional_Proof_Systems.MiniSC_Craig ...
Processing theory Correctness_Algebras.Binary_Iterings_Nonstrict ...
Removing 8 theories ...
Processing theory Allen_Calculus.examples ...
Processing theory Allen_Calculus.nest ...
Loading 54 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 Recursion-Theory-I.CPair ...
Processing theory Regular-Sets.Derivatives ...
Processing theory Recursion-Theory-I.PRecFun ...
Processing theory Recursion-Theory-I.PRecFinSet ...
Processing theory Recursion-Theory-I.PRecList ...
Processing theory Recursion-Theory-I.PRecFun2 ...
Processing theory Relational_Method.Definitions ...
Removing 7 theories ...
Processing theory TLA.Intensional ...
Processing theory Key_Agreement_Strong_Adversaries.pfslvl1 ...
Processing theory Recursion-Theory-I.PRecUnGr ...
Processing theory Recursion-Theory-I.RecEnSet ...
Processing theory TLA.Sequence ...
Processing theory TLA.Semantics ...
Processing theory Regex_Equivalence.Derivatives_Finite ...
Processing theory TLA.PreFormulas ...
Processing theory TLA.Rules ...
Processing theory TLA.Liveness ...
Processing theory TLA.State ...
Processing theory TLA.Even ...
Processing theory Selection_Heap_Sort.Sort ...
Processing theory TLA.Buffer ...
Processing theory Selection_Heap_Sort.RemoveMax ...
Processing theory Regex_Equivalence.Deriv_PDeriv ...
Processing theory Selection_Heap_Sort.Heap ...
Removing 9 theories ...
Processing theory Selection_Heap_Sort.SelectionSort_Functional ...
Processing theory Propositional_Proof_Systems.ND_Sound ...
Processing theory Selection_Heap_Sort.HeapFunctional ...
Processing theory Key_Agreement_Strong_Adversaries.pfslvl2 ...
Processing theory TLA.Inc ...
Processing theory Selection_Heap_Sort.HeapImperative ...
Processing theory Propositional_Proof_Systems.ND_Compl_SC ...
Processing theory Skew_Heap.Skew_Heap ...
Processing theory Regex_Equivalence.Automaton ...
Processing theory Regex_Equivalence.Deriv_Autos ...
Processing theory Regex_Equivalence.Position_Autos ...
Processing theory Category2.MonadicEquationalTheory ...
Processing theory Regex_Equivalence.Before2 ...
Processing theory Regex_Equivalence.After2 ...
Processing theory Regex_Equivalence.Regex_Equivalence ...
Processing theory Regex_Equivalence.Benchmark ...
Processing theory Key_Agreement_Strong_Adversaries.pfslvl3 ...
Processing theory Key_Agreement_Strong_Adversaries.pfslvl3_asymmetric ...
Processing theory Key_Agreement_Strong_Adversaries.pfslvl3_symmetric ...
Removing 48 theories ...
Processing theory Regex_Equivalence.Examples ...
Removing 10 theories ...
Processing theory Relational_Method.Authentication ...
Processing theory Relational_Method.Anonymity ...
Processing theory Relational_Method.Possibility ...
Loading 50 theories ...
Processing theory Clean.Test_Clean ...
Processing theory Clean.SquareRoot_concept ...
Processing theory Clean.Clean_Main ...
Processing theory FLP.ListUtilities ...
Processing theory FLP.Multiset ...
Processing theory Graph_Saturation.MissingRelation ...
Processing theory Statecharts.Contrib ...
Processing theory Statecharts.DataSpace ...
Processing theory Clean.Quicksort ...
Processing theory Graph_Saturation.LabeledGraphs ...
Processing theory Statecharts.Data ...
Processing theory Statecharts.Update ...
Processing theory Clean.Quicksort_concept ...
Removing 11 theories ...
Processing theory Graph_Saturation.RulesAndChains ...
Processing theory FLP.AsynchronousSystem ...
Processing theory FLP.Execution ...
Processing theory FLP.FLPSystem ...
Processing theory Graph_Saturation.LabeledGraphSemantics ...
Processing theory Graph_Saturation.StandardModels ...
Processing theory Statecharts.Expr ...
Processing theory Statecharts.SA ...
Processing theory Graph_Saturation.RuleSemanticsConnection ...
Processing theory FLP.FLPTheorem ...
Processing theory FLP.FLPExistingSystem ...
Processing theory Ordinals_and_Cardinals.Cardinal_Order_Relation_discontinued ...
Processing theory Statecharts.HA ...
Processing theory Pairing_Heap.Pairing_Heap_List2 ...
Processing theory Tail_Recursive_Functions.CaseStudy2 ...
Processing theory KAD.Modal_Kleene_Algebra_Applications ...
Processing theory Statecharts.Kripke ...
Processing theory Graph_Saturation.StandardRules ...
Processing theory Separata.Separata ...
Processing theory Graph_Saturation.GraphRewriting ...
Processing theory Imperative_Insertion_Sort.Imperative_Loops ...
Removing 27 theories ...
Processing theory Decl_Sem_Fun_PL.RelationalSemFSet ...
Processing theory Graph_Saturation.CombinedCorrectness ...
Processing theory Decl_Sem_Fun_PL.EquivRelationalDenotFSet ...
Processing theory Imperative_Insertion_Sort.Imperative_Insertion_Sort ...
Processing theory Decl_Sem_Fun_PL.DeclSemAsNDInterpFSet ...
Processing theory Statecharts.HAOps ...
Processing theory Splay_Tree.Splay_Heap ...
Processing theory Pairing_Heap.Pairing_Heap_Tree ...
Processing theory Pairing_Heap.Pairing_Heap_List1 ...
Processing theory Ribbon_Proofs.Ribbons_Stratified ...
Processing theory Lam-ml-Normalization.Lam_ml ...
Processing theory Decl_Sem_Fun_PL.MutableRef ...
Processing theory Decl_Sem_Fun_PL.MutableRefProps ...
Processing theory Statecharts.HASem ...
Loading 69 theories ...
Processing theory Statecharts.HAKripke ...
Processing theory Statecharts.CarAudioSystem ...
Removing 50 theories ...
Processing theory BNF_CC.Preliminaries ...
Processing theory Consensus_Refined.Consensus_Misc ...
Processing theory Consensus_Refined.Two_Steps ...
Processing theory Consensus_Refined.Consensus_Types ...
Processing theory Consensus_Refined.Quorums ...
Processing theory Consensus_Refined.Infra ...
Processing theory Clean.LinearSearch ...
Processing theory Coinductive_Languages.Coinductive_Language ...
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 Heard_Of.AteDefs ...
Processing theory Heard_Of.EigbyzDefs ...
Processing theory Heard_Of.OneThirdRuleDefs ...
Processing theory WOOT_Strong_Eventual_Consistency.ErrorMonad ...
Processing theory Consensus_Refined.Observing_Quorums ...
Processing theory Consensus_Refined.Observing_Quorums_Opt ...
Processing theory Consensus_Refined.Two_Step_Observing ...
Processing theory Stuttering_Equivalence.Samplers ...
Processing theory Stuttering_Equivalence.StutterEquivalence ...
Processing theory Heard_Of.UteDefs ...
Processing theory Network_Security_Policy_Verification.Example_NetModel ...
Processing theory Heard_Of.UvDefs ...
Processing theory Heard_Of.LastVotingDefs ...
Processing theory Network_Security_Policy_Verification.SINVAR_BLPstrict ...
Processing theory WOOT_Strong_Eventual_Consistency.Data ...
Processing theory WOOT_Strong_Eventual_Consistency.BasicAlgorithms ...
Processing theory WOOT_Strong_Eventual_Consistency.CreateAlgorithms ...
Processing theory WOOT_Strong_Eventual_Consistency.IntegrateAlgorithm ...
Processing theory Heard_Of.Reduction ...
Processing theory Consensus_Refined.BenOr_Proofs ...
Processing theory Consensus_Refined.Uv_Proofs ...
Processing theory Heard_Of.AteProof ...
Processing theory Heard_Of.EigbyzProof ...
Processing theory Heard_Of.OneThirdRuleProof ...
Processing theory Network_Security_Policy_Verification.Analysis_Tainting ...
Processing theory Propositional_Proof_Systems.Compactness_Consistency ...
Processing theory Network_Security_Policy_Verification.SINVAR_Subnets2 ...
Processing theory POPLmark-deBruijn.POPLmarkRecord ...
Processing theory POPLmark-deBruijn.POPLmarkRecordCtxt ...
Processing theory POPLmark-deBruijn.Execute ...
Processing theory Propositional_Proof_Systems.HC_Compl_Consistency ...
Processing theory Heard_Of.LastVotingProof ...
Processing theory Heard_Of.UteProof ...
Processing theory Heard_Of.UvProof ...
Processing theory WOOT_Strong_Eventual_Consistency.SortKeys ...
Processing theory WOOT_Strong_Eventual_Consistency.DistributedExecution ...
Removing 53 theories ...
Processing theory WOOT_Strong_Eventual_Consistency.Sorting ...
Processing theory Propositional_Proof_Systems.Resolution_Compl_Consistency ...
Processing theory Well_Quasi_Orders.Kruskal ...
Processing theory Well_Quasi_Orders.Wqo_Instances ...
Processing theory BNF_CC.Concrete_Examples ...
Processing theory Coinductive_Languages.Context_Free_Grammar ...
Processing theory BNF_CC.DDS ...
Processing theory Decl_Sem_Fun_PL.SystemF ...
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 WOOT_Strong_Eventual_Consistency.IntegrateInsertCommute ...
Removing 10 theories ...
Processing theory WOOT_Strong_Eventual_Consistency.StrongConvergence ...
Processing theory WOOT_Strong_Eventual_Consistency.SEC ...
Processing theory WOOT_Strong_Eventual_Consistency.Example ...
Loading 55 theories ...
Processing theory ConcurrentIMP.CIMP_pred ...
Processing theory Diophantine_Eqns_Lin_Hom.Sorted_Wrt ...
Processing theory ConcurrentIMP.Infinite_Sequences ...
Processing theory Diophantine_Eqns_Lin_Hom.Minimize_Wrt ...
Processing theory ConcurrentIMP.LTL ...
Processing theory Diophantine_Eqns_Lin_Hom.List_Vector ...
Processing theory Complete_Non_Orders.Binary_Relations ...
Processing theory Complete_Non_Orders.Complete_Relations ...
Processing theory ConcurrentIMP.CIMP_lang ...
Removing 18 theories ...
Processing theory Myhill-Nerode.Folds ...
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.Simple_Algorithm ...
Processing theory SIFUM_Type_Systems.Preliminaries ...
Processing theory PropResPI.Propositional_Resolution ...
Processing theory PropResPI.Prime_Implicates ...
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 Topological_Semantics.sse_boolean_algebra ...
Processing theory Security_Protocol_Refinement.m1_keydist_inrn ...
Processing theory Security_Protocol_Refinement.m1_ds ...
Processing theory ConcurrentIMP.CIMP_one_place_buffer ...
Processing theory Diophantine_Eqns_Lin_Hom.Algorithm ...
Processing theory Diophantine_Eqns_Lin_Hom.Solver_Code ...
Processing theory Topological_Semantics.sse_boolean_algebra_quantification ...
Removing 15 theories ...
Processing theory Topological_Semantics.sse_operation_positive ...
Processing theory Topological_Semantics.sse_operation_positive_quantification ...
Processing theory SIFUM_Type_Systems.Compositionality ...
Processing theory Topological_Semantics.topo_operators_basic ...
Processing theory Security_Protocol_Refinement.m2_ds ...
Processing theory SIFUM_Type_Systems.TypeSystem ...
Removing 2 theories ...
Processing theory Propositional_Proof_Systems.ND_Compl_Truthtable ...
Processing theory Propositional_Proof_Systems.ND_Compl_Truthtable_Compact ...
Processing theory Propositional_Proof_Systems.Tseytin ...
Processing theory Security_Protocol_Refinement.m3_ds_par ...
Processing theory Topological_Semantics.topo_frontier_algebra ...
Processing theory Security_Protocol_Refinement.m3_ds ...
Processing theory Propositional_Proof_Systems.Tseytin_Sema ...
Processing theory ConcurrentIMP.CIMP_unbounded_buffer ...
Processing theory Myhill-Nerode.Myhill_1 ...
Processing theory Myhill-Nerode.Myhill_2 ...
Processing theory Myhill-Nerode.Myhill ...
Processing theory Myhill-Nerode.Closures ...
Processing theory Myhill-Nerode.Closures2 ...
Removing 27 theories ...
FAILED to process theory Topological_Semantics.sse_operation_negative
*** Error (line 260 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/sse_operation_negative.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 261 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/sse_operation_negative.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 262 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/sse_operation_negative.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 263 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/sse_operation_negative.thy"):
*** Unexpected outcome: "unknown"
Processing theory Topological_Semantics.sse_operation_negative_quantification ...
FAILED to process theory Topological_Semantics.topo_strict_implication
*** Error (line 106 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_strict_implication.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 107 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_strict_implication.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 112 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_strict_implication.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 113 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_strict_implication.thy"):
*** Unexpected outcome: "unknown"
FAILED to process theory Topological_Semantics.topo_negation_conditions
*** Error (line 55 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_negation_conditions.thy"):
*** Unexpected outcome: "unknown"
FAILED to process theory Topological_Semantics.ex_LFIs
*** Error (line 127 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 128 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 137 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 138 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 143 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 148 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 149 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 153 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFIs.thy"):
*** Unexpected outcome: "unknown"
FAILED to process theory Topological_Semantics.ex_subminimal_logics
*** Error (line 82 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 85 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 109 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 180 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 199 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 201 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 208 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_subminimal_logics.thy"):
*** Unexpected outcome: "unknown"
Loading 78 theories ...
Processing theory Attack_Trees.MC ...
Processing theory JiveDataStoreModel.TypeIds ...
Processing theory JiveDataStoreModel.JavaType ...
Removing 4 theories ...
Processing theory JiveDataStoreModel.DirectSubtypes ...
Processing theory JiveDataStoreModel.Subtype ...
Processing theory JiveDataStoreModel.Attributes ...
Processing theory JiveDataStoreModel.AttributesIndep ...
Processing theory LatticeProperties.Lattice_Prop ...
Processing theory PseudoHoops.Operations ...
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 JiveDataStoreModel.StoreProperties ...
Processing theory JiveDataStoreModel.JML ...
Processing theory JiveDataStoreModel.UnivSpec ...
Processing theory Concurrent_Revisions.Data ...
Processing theory Concurrent_Revisions.Occurrences ...
Processing theory Concurrent_Revisions.Renaming ...
Processing theory Concurrent_Revisions.Substitution ...
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 SIFPL.VDM_OBJ ...
Processing theory PseudoHoops.PseudoWaisbergAlgebra ...
Processing theory Finger-Trees.FingerTree ...
Removing 16 theories ...
Processing theory Concurrent_Revisions.OperationalSemantics ...
Processing theory Concurrent_Revisions.Executions ...
Processing theory PseudoHoops.PseudoHoops ...
Processing theory SIFPL.VS_OBJ ...
Processing theory PseudoHoops.PseudoHoopFilters ...
Processing theory Strong_Security.Types ...
Processing theory WHATandWHERE_Security.WHATWHERE_Security ...
Processing theory Concurrent_Revisions.Determinacy ...
Processing theory Strong_Security.Expr ...
Processing theory Strong_Security.Domain_example ...
Processing theory SIFPL.ContextOBJ ...
Processing theory WHATandWHERE_Security.Up_To_Technique ...
Processing theory TESL_Language.StutteringDefs ...
Processing theory WHATandWHERE_Security.MWLs ...
Processing theory WHATandWHERE_Security.Parallel_Composition ...
Processing theory WHATandWHERE_Security.WHATWHERE_Secure_Skip_Assign ...
Processing theory TESL_Language.StutteringLemmas ...
Processing theory TESL_Language.Stuttering ...
Processing theory Finger-Trees.Test ...
Processing theory HyperCTL.Prelim ...
Processing theory PseudoHoops.SpecialPseudoHoops ...
Processing theory Correctness_Algebras.Boolean_Semirings ...
Removing 30 theories ...
Processing theory HyperCTL.Shallow ...
Processing theory HyperCTL.Deep ...
Processing theory WHATandWHERE_Security.Language_Composition ...
Processing theory Propositional_Proof_Systems.CNF_To_Formula ...
Processing theory Propositional_Proof_Systems.ND_FiniteAssms ...
Processing theory Propositional_Proof_Systems.MiniFormulas_Sema ...
Processing theory Propositional_Proof_Systems.Substitution ...
Processing theory WHATandWHERE_Security.Type_System ...
Processing theory WHATandWHERE_Security.Type_System_example ...
Processing theory HyperCTL.Noninterference ...
Processing theory HyperCTL.Finite_Noninterference ...
Processing theory HyperCTL.HyperCTL ...
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 BNF_CC.Composition ...
Processing theory BNF_CC.Quotient_Preservation ...
Processing theory BNF_CC.Subtypes ...
Processing theory PseudoHoops.Examples ...
Processing theory BNF_CC.Fixpoints ...
Processing theory BNF_CC.Operation_Examples ...
FAILED to process theory Topological_Semantics.topo_operators_derivative
*** Error (line 97 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_operators_derivative.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 114 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_operators_derivative.thy"):
*** Unexpected outcome: "unknown"
Removing 47 theories ...
FAILED to process theory Topological_Semantics.topo_derivative_algebra
*** Error (line 90 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_derivative_algebra.thy"):
*** Unexpected outcome: "unknown"
FAILED to process theory Topological_Semantics.ex_LFUs
*** Error (line 56 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFUs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 59 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFUs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 66 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFUs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 72 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFUs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 74 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFUs.thy"):
*** Unexpected outcome: "unknown"
*** Error (line 81 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/ex_LFUs.thy"):
*** Unexpected outcome: "unknown"
Loading 53 theories ...
Removing 3 theories ...
Processing theory Dict_Construction.Dict_Construction ...
Processing theory Consensus_Refined.Three_Steps ...
Processing theory Consensus_Refined.MRU_Vote ...
Processing theory FocusStreamsCaseStudies.ListExtras ...
Processing theory Belief_Revision.AGM_Logic ...
Processing theory Consensus_Refined.MRU_Vote_Opt ...
Processing theory Consensus_Refined.Three_Step_MRU ...
Processing theory FocusStreamsCaseStudies.ArithExtras ...
Processing theory Consensus_Refined.CT_Defs ...
Processing theory AWN.AWN_Term_Graph ...
Processing theory FeatherweightJava.FJDefs ...
Processing theory Belief_Revision.AGM_Remainder ...
Processing theory FeatherweightJava.FJAux ...
Processing theory FeatherweightJava.FJSound ...
Processing theory Consensus_Refined.CT_Proofs ...
Processing theory Consensus_Refined.New_Algorithm_Defs ...
Processing theory Consensus_Refined.New_Algorithm_Proofs ...
Processing theory FocusStreamsCaseStudies.stream ...
Processing theory FocusStreamsCaseStudies.BitBoolTS ...
Processing theory FocusStreamsCaseStudies.Gateway_types ...
Processing theory FocusStreamsCaseStudies.Gateway ...
Processing theory Consensus_Refined.Paxos_Defs ...
Processing theory FeatherweightJava.Execute ...
Processing theory FeatherweightJava.Featherweight_Java ...
Processing theory FocusStreamsCaseStudies.Gateway_proof_aux ...
Processing theory Consensus_Refined.Paxos_Proofs ...
Processing theory Lazy_Case.Lazy_Case ...
Processing theory Belief_Revision.AGM_Contraction ...
Processing theory Belief_Revision.AGM_Revision ...
Processing theory Mereology.PM ...
Processing theory Mereology.M ...
Processing theory Mereology.CM ...
Processing theory Mereology.GM ...
Processing theory Mereology.MM ...
Processing theory Mereology.EM ...
Processing theory Mereology.CEM ...
Processing theory Open_Induction.Open_Induction ...
Processing theory Mereology.GMM ...
Processing theory Topological_Semantics.topo_negation_fixedpoints ...
Processing theory FocusStreamsCaseStudies.Gateway_proof ...
Processing theory ADS_Functor.Merkle_Interface ...
Processing theory Mereology.GEM ...
Removing 41 theories ...
Processing theory Dict_Construction.Test_Lazy_Case ...
Processing theory FinFun.FinFunPred ...
Processing theory Well_Quasi_Orders.Higman_OI ...
Processing theory FOL_Axiomatic.FOL_Axiomatic ...
Processing theory Boolean_Expression_Checkers.Boolean_Expression_Checkers ...
Processing theory Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping ...
Processing theory Boolean_Expression_Checkers.Boolean_Expression_Example ...
Processing theory ADS_Functor.ADS_Construction ...
Processing theory ADS_Functor.Inclusion_Proof_Construction ...
Processing theory ADS_Functor.Canton_Transaction_Tree ...
Processing theory Hybrid_Logic.Hybrid_Logic ...
Loading 100 theories ...
Removing 28 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 Functional-Automata.Automata ...
Processing theory GraphMarkingIBP.Graph ...
Processing theory InfPathElimination.Aexp ...
Processing theory InfPathElimination.Bexp ...
Processing theory DataRefinementIBP.Preliminaries ...
Processing theory InfPathElimination.Store ...
Processing theory InfPathElimination.Conf ...
Processing theory DataRefinementIBP.Statements ...
Processing theory InfPathElimination.Labels ...
Processing theory InfPathElimination.Graph ...
Processing theory DataRefinementIBP.Hoare ...
Processing theory DataRefinementIBP.Diagram ...
Processing theory DataRefinementIBP.DataRefinement ...
Processing theory Inductive_Confidentiality.Message ...
Processing theory Inductive_Confidentiality.Event ...
Processing theory Inductive_Confidentiality.Public ...
Processing theory Inductive_Confidentiality.NS_Public_Bad ...
Processing theory MonoBoolTranAlgebra.Statements ...
Processing theory GraphMarkingIBP.SetMark ...
Processing theory GraphMarkingIBP.StackMark ...
Processing theory Inductive_Confidentiality.ConfidentialityDY ...
Processing theory InfPathElimination.SubRel ...
Processing theory InfPathElimination.ArcExt ...
Processing theory Menger.Graph ...
Processing theory Menger.Helpers ...
Processing theory Menger.Separations ...
Processing theory InfPathElimination.SubExt ...
Processing theory InfPathElimination.SymExec ...
Processing theory InfPathElimination.LTS ...
Processing theory GraphMarkingIBP.LinkMark ...
Processing theory Menger.DisjointPaths ...
Processing theory Partial_Function_MR.Partial_Function_MR ...
Processing theory Menger.MengerInduction ...
Processing theory Menger.Y_eq_new_last ...
Processing theory Menger.Y_neq_new_last ...
Processing theory Menger.Menger ...
Removing 17 theories ...
Processing theory Functional-Automata.RegSet_of_nat_DA ...
Processing theory Functional-Automata.RegExp2NA ...
Processing theory OpSets.OpSet ...
Processing theory Functional-Automata.RegExp2NAe ...
Processing theory Security_Protocol_Refinement.m1_auth ...
Processing theory GraphMarkingIBP.DSWMark ...
Processing theory OpSets.Insert_Spec ...
Processing theory OpSets.RGA ...
Processing theory Functional-Automata.AutoRegExp ...
Processing theory Functional-Automata.Execute ...
Processing theory OpSets.Interleaving ...
Processing theory Security_Protocol_Refinement.m2_auth_chan ...
Processing theory OpSets.List_Spec ...
Processing theory Strong_Security.MWLf ...
Processing theory Strong_Security.Strong_Security ...
Processing theory Strong_Security.Up_To_Technique ...
Processing theory Strong_Security.Parallel_Composition ...
Processing theory Security_Protocol_Refinement.m3_sig ...
Processing theory Strong_Security.Strongly_Secure_Skip_Assign ...
Processing theory Strong_Security.Language_Composition ...
Processing theory Security_Protocol_Refinement.m2_confid_chan ...
Processing theory Strong_Security.Type_System ...
Processing theory Strong_Security.Type_System_example ...
Removing 31 theories ...
FAILED to process theory Topological_Semantics.topo_border_algebra
*** Error (line 47 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_border_algebra.thy"):
*** Unexpected outcome: "unknown"
Processing theory Security_Protocol_Refinement.m3_enc ...
Processing theory VolpanoSmith.Semantics ...
Processing theory VolpanoSmith.secTypes ...
Processing theory VolpanoSmith.Execute ...
FAILED to process theory Topological_Semantics.topo_closure_algebra
*** Error (line 46 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_closure_algebra.thy"):
*** Unexpected outcome: "unknown"
FAILED to process theory Topological_Semantics.topo_interior_algebra
*** Error (line 46 of "/media/data/jenkins/workspace/isabelle-dump/afp/thys/Topological_Semantics/topo_interior_algebra.thy"):
*** Unexpected outcome: "unknown"
Processing theory Certification_Monads.Parser_Monad ...
Processing theory Certification_Monads.Strict_Sum ...
Processing theory Abs_Int_ITP2012.ACom ...
Processing theory Abs_Int_ITP2012.Collecting ...
Processing theory Partial_Function_MR.Partial_Function_MR_Examples ...
Processing theory LinearQuantifierElim.PresArith ...
Removing 21 theories ...
Processing theory XML.Xml ...
Processing theory LinearQuantifierElim.Cooper ...
Processing theory HereditarilyFinite.Ordinal ...
Processing theory Functional-Automata.MaxPrefix ...
Processing theory Functional-Automata.MaxChop ...
Processing theory Functional-Automata.AutoMaxChop ...
Processing theory Functional-Automata.Functional_Automata ...
Processing theory LinearQuantifierElim.QEpres ...
Processing theory Myhill-Nerode.Non_Regular_Languages ...
Processing theory Finite_Automata_HF.Finite_Automata_HF ...
Processing theory XML.Xmlt ...
Processing theory Abs_Int_ITP2012.Abs_Int0 ...
Processing theory Abs_Int_ITP2012.Abs_State ...
Processing theory Abs_Int_ITP2012.Abs_Int1 ...
Processing theory Abs_Int_ITP2012.Abs_Int2 ...
Removing 41 theories ...
Processing theory Abs_Int_ITP2012.Abs_Int2_ivl ...
Processing theory Abs_Int_ITP2012.Abs_Int3 ...
Processing theory InfPathElimination.RB ...
Loading 94 theories ...
Removing 16 theories ...
Processing theory Dict_Construction.Test_Side_Conditions ...
Processing theory BytecodeLogicJmlTypes.AssocLists ...
Processing theory CryptoBasedCompositionalProperties.ListExtras ...
Processing theory Dict_Construction.Termination ...
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 Consensus_Refined.Voting_Opt ...
Processing theory FocusStreamsCaseStudies.FR_types ...
Processing theory FocusStreamsCaseStudies.FR ...
Processing theory Concurrent_Ref_Alg.Conjunctive_Iteration ...
Processing theory Concurrent_Ref_Alg.Rely_Quotient ...
Processing theory FocusStreamsCaseStudies.SteamBoiler ...
Processing theory FocusStreamsCaseStudies.FR_proof ...
Processing theory FocusStreamsCaseStudies.SteamBoiler_proof ...
Processing theory Consensus_Refined.Ate_Defs ...
Processing theory Consensus_Refined.OneThirdRule_Defs ...
Processing theory Consensus_Refined.Ate_Proofs ...
Processing theory Consensus_Refined.OneThirdRule_Proofs ...
Processing theory CryptoBasedCompositionalProperties.Secrecy_types ...
Processing theory CryptoBasedCompositionalProperties.inout ...
Processing theory CryptoBasedCompositionalProperties.Secrecy ...
Processing theory CryptoBasedCompositionalProperties.CompLocalSecrets ...
Processing theory CryptoBasedCompositionalProperties.KnowledgeKeysSecrets ...
Processing theory BytecodeLogicJmlTypes.Language ...
Processing theory BytecodeLogicJmlTypes.Reachability ...
Processing theory BytecodeLogicJmlTypes.MultiStep ...
Processing theory MiniML.Maybe ...
Processing theory BytecodeLogicJmlTypes.Logic ...
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 Inductive_Confidentiality.Knowledge ...
Processing theory MiniML.Instance ...
Processing theory MiniML.Generalize ...
Processing theory MiniML.MiniML ...
Removing 45 theories ...
Processing theory Modular_Assembly_Kit_Security.SecureSystems ...
Processing theory Name_Carrying_Type_Inference.Fresh ...
Processing theory MiniML.W ...
Processing theory Name_Carrying_Type_Inference.Permutation ...
Processing theory Logging_Independent_Anonymity.Anonymity ...
Processing theory Name_Carrying_Type_Inference.PreSimplyTyped ...
Processing theory BytecodeLogicJmlTypes.Sound ...
Processing theory Logging_Independent_Anonymity.Possibility ...
Processing theory Projective_Geometry.Projective_Plane_Axioms ...
Processing theory SIFPL.IMP ...
Processing theory Name_Carrying_Type_Inference.SimplyTyped ...
Processing theory PSemigroupsConvolution.Partial_Semigroups ...
Removing 23 theories ...
Processing theory Projective_Geometry.Pappus_Property ...
Processing theory SIFPL.VDM ...
Processing theory Schutz_Spacetime.Util ...
Processing theory SIFPL.VS ...
Processing theory BytecodeLogicJmlTypes.Cachera ...
Processing theory PSemigroupsConvolution.Quantales ...
Processing theory Projective_Geometry.Pascal_Property ...
Processing theory Projective_Geometry.Desargues_Property ...
Processing theory PSemigroupsConvolution.Binary_Modalities ...
Processing theory PSemigroupsConvolution.Unary_Modalities ...
Processing theory Schutz_Spacetime.TernaryOrdering ...
Processing theory PSemigroupsConvolution.Partial_Semigroup_Lifting ...
Processing theory Tree_Decomposition.Graph ...
Processing theory Tree_Decomposition.Tree ...
Processing theory SIFPL.ContextVS ...
Processing theory Tree_Decomposition.TreeDecomposition ...
Processing theory ArrowImpossibilityGS.Arrow_Order ...
Processing theory ArrowImpossibilityGS.GS ...
Processing theory Schutz_Spacetime.Minkowski ...
Processing theory Category.Cat ...
Processing theory Category.Functors ...
Processing theory Category.NatTrans ...
Processing theory Category.SetCat ...
Processing theory Category.HomFunctors ...
Processing theory Tree_Decomposition.TreewidthCompleteGraph ...
Processing theory Tree_Decomposition.TreewidthTree ...
Processing theory Sunflowers.Sunflower ...
Processing theory Category.Yoneda ...
Processing theory Sunflowers.Erdos_Rado_Sunflower ...
Processing theory Approximation_Algorithms.Approx_MIS_Hoare ...
Processing theory Tree_Decomposition.ExampleInstantiations ...
Processing theory Abs_Int_ITP2012.Abs_Int1_const ...
Removing 31 theories ...
Processing theory Abs_Int_ITP2012.Abs_Int1_parity ...
Processing theory Dict_Construction.Test_Dict_Construction ...
Removing 16 theories ...
Processing theory Projective_Geometry.Pappus_Desargues ...
Processing theory Schutz_Spacetime.TemporalOrderOnPath ...
Loading 112 theories ...
Processing theory Binomial-Queues.PQ ...
Processing theory Abstract-Hoare-Logics.PLang ...
Processing theory Abstract-Hoare-Logics.PHoare ...
Processing theory Abstract-Hoare-Logics.PTermi ...
Processing theory Abortable_Linearizable_Modules.Sequences ...
Processing theory BinarySearchTree.BinaryTree ...
Processing theory BinarySearchTree.BinaryTree_Map ...
Processing theory Binomial-Queues.Binomial_Queue ...
Processing theory C2KA_DistributedSystems.Stimuli ...
Processing theory Abstract-Hoare-Logics.PHoareTotal ...
Processing theory Binomial-Queues.PQ_Implementation ...
Processing theory Decl_Sem_Fun_PL.Values ...
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.DeclSemAsDenot ...
Processing theory Decl_Sem_Fun_PL.ValueProps ...
Processing theory FocusStreamsCaseStudies.arith_hints ...
Processing theory FocusStreamsCaseStudies.JoinSplitTime ...
Processing theory GPU_Kernel_PL.Misc ...
Processing theory Decl_Sem_Fun_PL.InterTypeSystem ...
Processing theory Abortable_Linearizable_Modules.IOA ...
Removing 28 theories ...
Processing theory Abortable_Linearizable_Modules.RDR ...
Processing theory Decl_Sem_Fun_PL.DenotLam5 ...
Processing theory Abortable_Linearizable_Modules.Simulations ...
Processing theory Decl_Sem_Fun_PL.EquivDenotInterTypes ...
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 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 Abortable_Linearizable_Modules.SLin ...
Processing theory LambdaMu.ContextFacts ...
Processing theory LambdaMu.TypePreservation ...
Processing theory LambdaMu.Progress ...
Removing 21 theories ...
Processing theory MFOTL_Monitor.Table ...
Processing theory Generic_Join.Generic_Join ...
Processing theory Generic_Join.Examples_Join ...
Processing theory GewirthPGCProof.CJDDLplus ...
Processing theory ComponentDependencies.DataDependenciesConcreteValues ...
Processing theory ComponentDependencies.DataDependencies ...
Removing 1 theories ...
Processing theory GewirthPGCProof.ExtendedDDL ...
Processing theory No_FTL_observers.SomeFunc ...
Processing theory Matroids.Indep_System ...
Processing theory Generic_Join.Generic_Join_Correctness ...
Processing theory Abortable_Linearizable_Modules.Idempotence ...
Processing theory Matroids.Matroid ...
Processing theory RefinementReactive.Refinement ...
Processing theory PSemigroupsConvolution.Partial_Semigroup_Models ...
Processing theory RefinementReactive.Temporal ...
Removing 11 theories ...
Processing theory GewirthPGCProof.GewirthArgument ...
Processing theory Coinductive_Languages.Coinductive_Regular_Set ...
Processing theory SIFPL.Lattice ...
Processing theory RefinementReactive.Reactive ...
Processing theory SIFPL.HuntSands ...
Processing theory SenSocialChoice.FSext ...
Processing theory Separation_Algebra.Sep_Tactics_Test ...
Processing theory SenSocialChoice.RPRs ...
Processing theory SenSocialChoice.SCFs ...
Processing theory SenSocialChoice.May ...
Processing theory Separation_Algebra.VM_Example ...
Processing theory ComponentDependencies.DataDependenciesCaseStudy ...
Processing theory SenSocialChoice.Sen ...
Processing theory Separation_Algebra.Separation_Algebra_Alt ...
Processing theory SenSocialChoice.Arrow ...
Processing theory Separation_Algebra.Sep_Eq ...
Processing theory Types_Tableaus_and_Goedels_God.Relations ...
Processing theory Types_Tableaus_and_Goedels_God.IHOML ...
Processing theory SIFUM_Type_Systems.LocallySoundModeUse ...
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 VeriComp.Fixpoint ...
Processing theory Topological_Semantics.topo_alexandrov ...
Processing theory Hello_World.IO ...
Processing theory Separation_Algebra.Simple_Separation_Example ...
Removing 56 theories ...
Processing theory Hello_World.HelloWorld ...
Processing theory Hello_World.RunningCodeFromIsabelle ...
Processing theory Ramsey-Infinite.Ramsey ...
Processing theory Hello_World.HelloWorld_Proof ...
Processing theory HotelKeyCards.Notation ...
Processing theory HotelKeyCards.Basis ...
Processing theory Relational-Incorrectness-Logic.RelationalIncorrectness ...
Processing theory HotelKeyCards.State ...
Processing theory HotelKeyCards.Trace ...
Processing theory IMP_Compiler.Compiler ...
Processing theory HotelKeyCards.Equivalence ...
Processing theory Splay_Tree.Splay_Tree ...
Processing theory Weight_Balanced_Trees.Weight_Balanced_Trees ...
Processing theory Propositional_Proof_Systems.Resolution_Compl ...
Processing theory TortoiseHare.Basis ...
Processing theory Transitive-Closure-II.RTrancl ...
Processing theory TortoiseHare.Brent ...
Processing theory Splay_Tree.Splay_Map ...
Removing 41 theories ...
Processing theory IMP_Compiler.Compiler2 ...
Processing theory TortoiseHare.TortoiseHare ...
Processing theory No_FTL_observers.SpaceTime ...
Removing 8 theories ...
Processing theory No_FTL_observers.Axioms ...
Processing theory No_FTL_observers.SpecRel ...
Loading 98 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.PsLang ...
Processing theory Abstract-Hoare-Logics.PsHoare ...
Processing theory Abstract-Hoare-Logics.PsTermi ...
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 DPT-SAT-Solver.DPT_SAT_Tests ...
Processing theory Intro_Dest_Elim.IDE_Tools ...
Processing theory Fresh_Identifiers.Fresh_String ...
Processing theory Intro_Dest_Elim.IHOL_IDE ...
Processing theory Isabelle_C.README ...
Processing theory LambdaMu.Peirce ...
Processing theory Lowe_Ontological_Argument.Relations ...
Processing theory Lowe_Ontological_Argument.QML ...
Processing theory Abstract-Hoare-Logics.PsHoareTotal ...
Processing theory Lifting_Definition_Option.Lifting_Definition_Option_Examples ...
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.Tagged_Prod_Sum ...
Processing theory Generic_Deriving.Derive ...
Processing theory Lazy_Case.Test_Lazy_Case ...
Processing theory Constructor_Funs.Test_Constructor_Funs ...
Processing theory Generic_Deriving.Derive_Datatypes ...
Processing theory Generic_Deriving.Derive_Algebra_Laws ...
Processing theory Generic_Deriving.Derive_Eq ...
Processing theory Generic_Deriving.Derive_Encode ...
Processing theory Generic_Deriving.Derive_Algebra ...
Removing 38 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 Max-Card-Matching.Matching ...
Processing theory Network_Security_Policy_Verification.ML_GraphViz_Disable ...
Processing theory Network_Security_Policy_Verification.attic ...
Processing theory Modular_Assembly_Kit_Security.FlowPolicies ...
Processing theory Generic_Deriving.Derive_Eq_Laws ...
Processing theory Isabelle_Meta_Model.Design_generated_generated ...
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 Latin_Square.Latin_Square ...
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 Projective_Geometry.Projective_Space_Axioms ...
Processing theory Pop_Refinement.Second_Example ...
Processing theory Generic_Deriving.Derive_Show ...
Processing theory Proof_Strategy_Language.Try_Hard ...
Processing theory Proof_Strategy_Language.PSL ...
Processing theory Projective_Geometry.Matroid_Rank_Properties ...
Processing theory Projective_Geometry.Desargues_3D ...
Removing 33 theories ...
Processing theory NormByEval.NBE ...
Processing theory Projective_Geometry.Desargues_2D ...
Processing theory Roy_Floyd_Warshall.Roy_Floyd_Warshall ...
Processing theory Separation_Logic_Imperative_HOL.Default_Insts ...
Processing theory Robbins-Conjecture.Robbins_Conjecture ...
Processing theory Stable_Matching.Sotomayor ...
Removing 8 theories ...
Processing theory Szpilrajn.Szpilrajn ...
Processing theory TESL_Language.Introduction ...
Processing theory Stellar_Quorums.Stellar_Quorums ...
Processing theory Tail_Recursive_Functions.CaseStudy1 ...
Processing theory Tail_Recursive_Functions.Method ...
Processing theory Blue_Eyes.Blue_Eyes ...
Processing theory Sliding_Window_Algorithm.SWA ...
Removing 7 theories ...
Processing theory Approximation_Algorithms.Approx_VC_Hoare ...
Processing theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun ...
Processing theory AI_Planning_Languages_Semantics.Option_Monad_Add ...
Processing theory Verified-Prover.Prover ...
Processing theory BNF_Operations.Kill ...
Processing theory BNF_Operations.Compose ...
Processing theory BNF_Operations.LFP ...
Processing theory BNF_Operations.GFP ...
Removing 12 theories ...
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 BNF_Operations.Lift ...
Processing theory BNF_Operations.Permute ...
Processing theory CofGroups.CofGroups ...
Processing theory Paraconsistency.Paraconsistency ...
Processing theory ADS_Functor.Generic_ADS_Construction ...
Processing theory BNF_Operations.N2M ...
Processing theory Hood_Melville_Queue.Hood_Melville_Queue ...
Removing 23 theories ...
Processing theory Proof_Strategy_Language.Example ...
Loading 22 theories ...
Processing theory AnselmGod.AnselmGod ...
Processing theory Aristotles_Assertoric_Syllogistic.AristotlesAssertoric ...
Processing theory Bondy.Bondy ...
Processing theory BinarySearchTree.BinaryTree_TacticStyle ...
Processing theory Certification_Monads.Misc ...
Processing theory Depth-First-Search.DFS ...
Processing theory Dict_Construction.Impossibility ...
Processing theory Dict_Construction.Introduction ...
Processing theory Example-Submission.Submission ...
Processing theory Free-Boolean-Algebra.Free_Boolean_Algebra ...
Processing theory AVL-Trees.AVL2 ...
Processing theory CYK.CYK ...
Processing theory Compiling-Exceptions-Correctly.Exceptions ...
Removing 17 theories ...
Processing theory GoedelGod.GoedelGod ...
Processing theory FunWithTilings.Tilings ...
Processing theory AxiomaticCategoryTheory.AxiomaticCategoryTheory ...
Processing theory HotelKeyCards.NewCard ...
Processing theory AVL-Trees.AVL ...
Processing theory Goodstein_Lambda.Goodstein_Lambda ...
Processing theory FOL_Harrison.FOL_Harrison ...
Processing theory Huffman.Huffman ...
Removing 8 theories ...
Processing theory IsaGeoCoq.Tarski_Neutral ...
Loading 98 theories ...
Removing 98 theories ...
Processing theory SpecCheck.SpecCheck_Dynamic ...
Processing theory SpecCheck.SpecCheck_Examples ...
Processing theory Forcing.Recursion_Thms ...
Processing theory Forcing.Nat_Miscellanea ...
Processing theory Forcing.Pointed_DC ...
Processing theory Recursion-Addition.recursion ...
Processing theory Delta_System_Lemma.ZF_Library ...
Processing theory Forcing.Renaming ...
Processing theory Forcing.Utils ...
Processing theory Forcing.Renaming_Auto ...
Processing theory Forcing.Synthetic_Definition ...
Processing theory Forcing.Forcing_Notions ...
Processing theory Forcing.Rasiowa_Sikorski ...
Processing theory Delta_System_Lemma.Cardinal_Library ...
Processing theory Delta_System_Lemma.Delta_System ...
Processing theory Delta_System_Lemma.Cohen_Posets ...
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.Separation_Rename ...
Processing theory Forcing.Names ...
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 ...
Removing 20 theories ...
Processing theory Forcing.Forces_Definition ...
Processing theory Forcing.Forcing_Theorems ...
Processing theory Forcing.Ordinals_In_MG ...
Processing theory Forcing.Separation_Axiom ...
Processing theory Forcing.Infinity_Axiom ...
Processing theory Forcing.Powerset_Axiom ...
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/process2749754976390610746/export251621680/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:149)
	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
Writing zip file of /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