Console Output

Skipping 216 KB.. Full Log

y Zeta_Function.Zeta_Laurent_Expansion ...
Processing theory Zeta_Function.Hadjicostas_Chapman ...
Loading 3 theories ...
Processing theory Multi_Party_Computation.DH_Ext ...
Processing theory Multi_Party_Computation.Malicious_Defs ...
Removing 10 theories ...
Processing theory Multi_Party_Computation.Malicious_OT ...
Loading 2 theories ...
Removing 8 theories ...
Processing theory Game_Based_Crypto.CryptHOL_Tutorial ...
Loading 24 theories ...
Processing theory Linear_Recurrences.Linear_Recurrences_Common ...
Processing theory Linear_Recurrences.Pochhammer_Polynomials ...
Processing theory Linear_Recurrences.Eulerian_Polynomials ...
Processing theory Linear_Recurrences.Linear_Recurrences_Misc ...
Processing theory Linear_Recurrences.Factorizations ...
Processing theory Count_Complex_Roots.More_Polynomials ...
Processing theory Linear_Recurrences.Partial_Fraction_Decomposition ...
Processing theory Linear_Recurrences.RatFPS ...
Processing theory Linear_Recurrences.Rational_FPS_Solver ...
Processing theory Linear_Recurrences.Linear_Homogenous_Recurrences ...
Processing theory Linear_Recurrences.Linear_Inhomogenous_Recurrences ...
Removing 19 theories ...
Processing theory Polynomial_Factorization.Polynomial_Divisibility ...
Processing theory Count_Complex_Roots.Extended_Sturm ...
Processing theory Polynomial_Factorization.Square_Free_Factorization ...
Processing theory Count_Complex_Roots.Count_Complex_Roots ...
Processing theory Linear_Recurrences.Rational_FPS_Asymptotics ...
Removing 1 theories ...
Processing theory Count_Complex_Roots.Count_Complex_Roots_Examples ...
Loading 218 theories ...
Removing 12 theories ...
Processing theory LLL_Basis_Reduction.List_Representation ...
Processing theory Subresultants.Binary_Exponentiation ...
Processing theory LLL_Basis_Reduction.More_IArray ...
Processing theory Perron_Frobenius.Bij_Nat ...
Processing theory Berlekamp_Zassenhaus.More_Missing_Multiset ...
Processing theory Berlekamp_Zassenhaus.Arithmetic_Record_Based ...
Processing theory Berlekamp_Zassenhaus.Sublist_Iteration ...
Processing theory Perron_Frobenius.Cancel_Card_Constraint ...
Processing theory Show.Show_Poly ...
Processing theory Berlekamp_Zassenhaus.Karatsuba_Multiplication ...
Processing theory Abstract-Rewriting.SN_Order_Carrier ...
Processing theory Polynomial_Factorization.Missing_Polynomial_Factorial ...
Processing theory Polynomial_Factorization.Explicit_Roots ...
Processing theory Subresultants.Dichotomous_Lazard ...
Processing theory Polynomial_Factorization.Dvd_Int_Poly ...
Processing theory Berlekamp_Zassenhaus.Polynomial_Record_Based ...
Processing theory Polynomial_Factorization.Gauss_Lemma ...
Processing theory Polynomial_Factorization.Gcd_Rat_Poly ...
Processing theory Jordan_Normal_Form.Show_Matrix ...
Processing theory Polynomial_Factorization.Rational_Root_Test ...
Processing theory Subresultants.Coeff_Int ...
Processing theory Berlekamp_Zassenhaus.Unique_Factorization ...
Processing theory Berlekamp_Zassenhaus.Chinese_Remainder_Poly ...
Processing theory Berlekamp_Zassenhaus.Finite_Field ...
Processing theory Smith_Normal_Form.Finite_Field_Mod_Type_Connection ...
Processing theory Subresultants.More_Homomorphisms ...
Processing theory Echelon_Form.Rings2 ...
Processing theory Subresultants.Resultant_Prelim ...
Processing theory Native_Word.Uint64 ...
Processing theory Berlekamp_Zassenhaus.Unique_Factorization_Poly ...
Processing theory Algebraic_Numbers.Bivariate_Polynomials ...
Processing theory Berlekamp_Zassenhaus.Poly_Mod ...
Processing theory Modular_arithmetic_LLL_and_HNF_algorithms.Signed_Modulo ...
Processing theory Echelon_Form.Cayley_Hamilton_Compatible ...
Processing theory Echelon_Form.Code_Cayley_Hamilton ...
Processing theory Algebraic_Numbers.Resultant ...
Processing theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field ...
Processing theory Berlekamp_Zassenhaus.Finite_Field_Record_Based ...
Processing theory Jordan_Normal_Form.Determinant_Impl ...
Processing theory Berlekamp_Zassenhaus.Poly_Mod_Finite_Field_Record_Based ...
Processing theory Jordan_Normal_Form.Matrix_Kernel ...
Processing theory Smith_Normal_Form.Rings2_Extended ...
Processing theory Echelon_Form.Echelon_Form ...
Processing theory Echelon_Form.Echelon_Form_Det ...
Processing theory Echelon_Form.Echelon_Form_Inverse ...
Processing theory Berlekamp_Zassenhaus.Hensel_Lifting ...
Processing theory Berlekamp_Zassenhaus.Berlekamp_Type_Based ...
Processing theory Berlekamp_Zassenhaus.Distinct_Degree_Factorization ...
Processing theory Subresultants.Subresultant ...
Processing theory Berlekamp_Zassenhaus.Finite_Field_Factorization ...
Processing theory Subresultants.Subresultant_Gcd ...
Processing theory Polynomial_Factorization.Precomputation ...
Processing theory Jordan_Normal_Form.Spectral_Radius ...
Processing theory Polynomial_Factorization.Kronecker_Factorization ...
Processing theory Echelon_Form.Examples_Echelon_Form_Abstract ...
Processing theory Perron_Frobenius.HMA_Connect ...
Processing theory Polynomial_Factorization.Rational_Factorization ...
Processing theory Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp ...
Processing theory Smith_Normal_Form.Mod_Type_Connect ...
Processing theory Jordan_Normal_Form.Matrix_IArray_Impl ...
Processing theory Modular_arithmetic_LLL_and_HNF_algorithms.Matrix_Change_Row ...
Processing theory Jordan_Normal_Form.Gauss_Jordan_IArray_Impl ...
Processing theory Berlekamp_Zassenhaus.Matrix_Record_Based ...
Processing theory Hermite.Hermite ...
Processing theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite ...
Processing theory Smith_Normal_Form.Smith_Normal_Form ...
Processing theory Jordan_Normal_Form.Matrix_Impl ...
Processing theory Smith_Normal_Form.SNF_Missing_Lemmas ...
Processing theory Berlekamp_Zassenhaus.Finite_Field_Factorization_Record_Based ...
Processing theory Smith_Normal_Form.Smith_Normal_Form_JNF ...
Processing theory Berlekamp_Zassenhaus.Berlekamp_Hensel ...
Processing theory Modular_arithmetic_LLL_and_HNF_algorithms.Uniqueness_Hermite_JNF ...
Processing theory LLL_Basis_Reduction.Missing_Lemmas ...
Processing theory LLL_Basis_Reduction.Norms ...
Processing theory LLL_Basis_Reduction.Int_Rat_Operations ...
Processing theory Smith_Normal_Form.Diagonal_To_Smith ...
Processing theory Smith_Normal_Form.Admits_SNF_From_Diagonal_Iff_Bezout_Ring ...
Processing theory Smith_Normal_Form.Diagonal_To_Smith_JNF ...
Processing theory LLL_Basis_Reduction.Gram_Schmidt_2 ...
Processing theory Smith_Normal_Form.SNF_Algorithm ...
Processing theory Smith_Normal_Form.Elementary_Divisor_Rings ...
Processing theory LLL_Basis_Reduction.Gram_Schmidt_Int ...
Processing theory LLL_Basis_Reduction.LLL ...
Processing theory Smith_Normal_Form.SNF_Algorithm_Euclidean_Domain ...
Processing theory LLL_Basis_Reduction.LLL_Impl ...
Processing theory LLL_Basis_Reduction.LLL_Certification ...
Processing theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Algorithm ...
Processing theory Modular_arithmetic_LLL_and_HNF_algorithms.HNF_Mod_Det_Soundness ...
Processing theory Modular_arithmetic_LLL_and_HNF_algorithms.LLL_Certification_via_HNF ...
Loading 9 theories ...
Removing 6 theories ...
Processing theory Ergodic_Theory.Asymptotic_Density ...
Processing theory Ergodic_Theory.Measure_Preserving_Transformations ...
Processing theory Ergodic_Theory.Recurrence ...
Processing theory Ergodic_Theory.Invariants ...
Processing theory Ergodic_Theory.Ergodicity ...
Processing theory Ergodic_Theory.Kingman ...
Processing theory Ergodic_Theory.Gouezel_Karlsson ...
Loading 39 theories ...
Removing 2 theories ...
Processing theory Differential_Dynamic_Logic.Ids ...
Processing theory Ordinary_Differential_Equations.Bounded_Linear_Operator ...
Processing theory Differential_Dynamic_Logic.Syntax ...
Processing theory Ordinary_Differential_Equations.Multivariate_Taylor ...
Processing theory Ordinary_Differential_Equations.Cones ...
Processing theory Ordinary_Differential_Equations.MVT_Ex ...
Processing theory Ordinary_Differential_Equations.Flow ...
Processing theory Ordinary_Differential_Equations.Linear_ODE ...
Processing theory Ordinary_Differential_Equations.Upper_Lower_Solution ...
Processing theory Ordinary_Differential_Equations.Poincare_Map ...
Processing theory Ordinary_Differential_Equations.Reachability_Analysis ...
Processing theory Ordinary_Differential_Equations.Flow_Congs ...
Processing theory Ordinary_Differential_Equations.ODE_Analysis ...
Processing theory Differential_Dynamic_Logic.Lib ...
Processing theory Differential_Dynamic_Logic.Denotational_Semantics ...
Processing theory Differential_Dynamic_Logic.Axioms ...
Processing theory Differential_Dynamic_Logic.Frechet_Correctness ...
Processing theory Differential_Dynamic_Logic.Static_Semantics ...
Processing theory Differential_Dynamic_Logic.USubst ...
Processing theory Differential_Dynamic_Logic.Pretty_Printer ...
Processing theory Differential_Dynamic_Logic.Coincidence ...
Processing theory Differential_Dynamic_Logic.Bound_Effect ...
Processing theory Differential_Dynamic_Logic.Uniform_Renaming ...
Processing theory Differential_Dynamic_Logic.Differential_Axioms ...
Processing theory Differential_Dynamic_Logic.USubst_Lemma ...
Processing theory Differential_Dynamic_Logic.Proof_Checker ...
Loading 147 theories ...
Processing theory Differential_Dynamic_Logic.Differential_Dynamic_Logic ...
Removing 16 theories ...
Processing theory Automatic_Refinement.Foldi ...
Processing theory Automatic_Refinement.Prio_List ...
Processing theory Automatic_Refinement.Anti_Unification ...
Processing theory Automatic_Refinement.Attr_Comb ...
Processing theory Automatic_Refinement.Named_Sorted_Thms ...
Processing theory Automatic_Refinement.Indep_Vars ...
Processing theory Automatic_Refinement.Mk_Record_Simp ...
Processing theory Automatic_Refinement.Tagged_Solver ...
Processing theory Automatic_Refinement.Select_Solve ...
Processing theory Automatic_Refinement.Autoref_Data ...
Processing theory Refine_Monadic.Refine_Chapter ...
Processing theory Deriving.Countable_Generator ...
Processing theory Affine_Arithmetic.Optimize_Integer ...
Processing theory Affine_Arithmetic.Optimize_Float ...
Processing theory Affine_Arithmetic.Float_Real ...
Processing theory HOL-ODE-Numerics.Transfer_Analysis ...
Processing theory HOL-ODE-Numerics.Transfer_ODE ...
Processing theory Deriving.Hash_Generator ...
Processing theory Deriving.Hash_Instances ...
Processing theory Deriving.Derive ...
Processing theory HOL-ODE-Numerics.One_Step_Method ...
Processing theory Native_Word.Uint ...
Processing theory Affine_Arithmetic.Affine_Form ...
Processing theory HOL-ODE-Numerics.Runge_Kutta ...
Processing theory Affine_Arithmetic.Counterclockwise ...
Processing theory Affine_Arithmetic.Counterclockwise_Vector ...
Processing theory Automatic_Refinement.Refine_Lib ...
Processing theory Automatic_Refinement.Autoref_Phases ...
Processing theory Automatic_Refinement.Autoref_Tagging ...
Processing theory Refine_Monadic.Refine_Mono_Prover ...
Processing theory Collections.SetIterator ...
Processing theory Automatic_Refinement.Relators ...
Processing theory Automatic_Refinement.Param_Tool ...
Processing theory Affine_Arithmetic.Counterclockwise_2D_Strict ...
Processing theory Automatic_Refinement.Param_HOL ...
Processing theory Automatic_Refinement.Parametricity ...
Processing theory Automatic_Refinement.Autoref_Id_Ops ...
Processing theory Automatic_Refinement.Autoref_Fix_Rel ...
Processing theory Automatic_Refinement.Autoref_Translate ...
Processing theory Automatic_Refinement.Autoref_Gen_Algo ...
Processing theory Automatic_Refinement.Autoref_Relator_Interface ...
Processing theory Automatic_Refinement.Autoref_Tool ...
Processing theory Collections.SetIteratorOperations ...
Processing theory Collections.Proper_Iterator ...
Processing theory Collections.It_to_It ...
Processing theory Collections.Assoc_List ...
Processing theory Collections.SetIteratorGA ...
Processing theory Affine_Arithmetic.Polygon ...
Processing theory Automatic_Refinement.Autoref_Bindings_HOL ...
Processing theory Automatic_Refinement.Automatic_Refinement ...
Processing theory Refine_Monadic.Refine_Misc ...
Processing theory Refine_Monadic.RefineG_Transfer ...
Processing theory Refine_Monadic.RefineG_Assert ...
Processing theory Collections.Idx_Iterator ...
Processing theory Collections.Intf_Hash ...
Processing theory Collections.Gen_Hash ...
Processing theory Collections.Diff_Array ...
Processing theory Collections.Impl_Array_Stack ...
Processing theory Refine_Monadic.RefineG_Domain ...
Processing theory Refine_Monadic.RefineG_Recursion ...
Processing theory Refine_Monadic.RefineG_While ...
Processing theory Collections.Intf_Comp ...
Processing theory Refine_Monadic.Refine_Det ...
Processing theory Refine_Monadic.Refine_Basic ...
Processing theory Refine_Monadic.Refine_Heuristics ...
Processing theory Refine_Monadic.Refine_Leof ...
Processing theory Refine_Monadic.Refine_More_Comb ...
Processing theory Refine_Monadic.Refine_Pfun ...
Processing theory Refine_Monadic.Refine_While ...
Processing theory Refine_Monadic.Refine_Transfer ...
Processing theory Affine_Arithmetic.Floatarith_Expression ...
Processing theory Refine_Monadic.Autoref_Monadic ...
Processing theory Refine_Monadic.Refine_Automation ...
Processing theory Affine_Arithmetic.Counterclockwise_2D_Arbitrary ...
Processing theory Refine_Monadic.Refine_Foreach ...
Processing theory Refine_Monadic.Refine_Monadic ...
Processing theory Collections.Intf_Map ...
Processing theory Collections.Intf_Set ...
Processing theory Collections.Impl_Cfun_Set ...
Processing theory Collections.Gen_Iterator ...
Processing theory Collections.Iterator ...
Processing theory Collections.Array_Iterator ...
Processing theory Collections.Gen_Map2Set ...
Processing theory Collections.Impl_Bit_Set ...
Processing theory Collections.Impl_List_Set ...
Processing theory Collections.Gen_Map ...
Processing theory Collections.Gen_Set ...
Processing theory Collections.RBT_add ...
Processing theory Collections.Impl_Array_Map ...
Processing theory Collections.Impl_List_Map ...
Processing theory Collections.Impl_Uv_Set ...
Processing theory Collections.Impl_Array_Hash_Map ...
Processing theory Affine_Arithmetic.Intersection ...
Processing theory Affine_Arithmetic.Straight_Line_Program ...
Processing theory Collections.Impl_RBT_Map ...
Processing theory HOL-ODE-Numerics.GenCF_No_Comp ...
Processing theory HOL-ODE-Numerics.Refine_Dflt_No_Comp ...
Processing theory HOL-ODE-Numerics.Autoref_Misc ...
Processing theory Affine_Arithmetic.Affine_Approximation ...
Processing theory HOL-ODE-Numerics.Refine_String ...
Processing theory HOL-ODE-Numerics.Refine_Folds ...
Processing theory HOL-ODE-Numerics.Weak_Set ...
Processing theory HOL-ODE-Numerics.Refine_Parallel ...
Processing theory Affine_Arithmetic.Affine_Code ...
Processing theory Affine_Arithmetic.Print ...
Processing theory HOL-ODE-Numerics.Enclosure_Operations ...
Processing theory HOL-ODE-Numerics.Refine_Default ...
Processing theory HOL-ODE-Numerics.Refine_Unions ...
Processing theory HOL-ODE-Numerics.Refine_Intersection ...
Processing theory HOL-ODE-Numerics.Refine_Phantom ...
Processing theory HOL-ODE-Numerics.Refine_Vector_List ...
Processing theory Affine_Arithmetic.Ex_Inter ...
Processing theory Affine_Arithmetic.Ex_Affine_Approximation ...
Processing theory HOL-ODE-Numerics.Refine_Invar ...
Processing theory HOL-ODE-Numerics.Refine_Hyperplane ...
Processing theory HOL-ODE-Numerics.Refine_Info ...
Processing theory HOL-ODE-Numerics.Transfer_Euclidean_Space_Vector ...
Processing theory Affine_Arithmetic.Ex_Ineqs ...
Processing theory Affine_Arithmetic.Affine_Arithmetic ...
Processing theory HOL-ODE-Numerics.Refine_Interval ...
Processing theory HOL-ODE-Numerics.Abstract_Rigorous_Numerics ...
Processing theory HOL-ODE-Numerics.Refine_Rigorous_Numerics ...
Processing theory HOL-ODE-Numerics.Refine_ScaleR2 ...
Processing theory HOL-ODE-Numerics.Concrete_Rigorous_Numerics ...
Processing theory HOL-ODE-Numerics.Abstract_Reachability_Analysis ...
Processing theory HOL-ODE-Numerics.Refine_Rigorous_Numerics_Aform ...
Processing theory HOL-ODE-Numerics.Abstract_Reachability_Analysis_C1 ...
Processing theory HOL-ODE-Numerics.Concrete_Reachability_Analysis ...
Processing theory HOL-ODE-Numerics.Refine_Reachability_Analysis ...
Processing theory HOL-ODE-Numerics.Concrete_Reachability_Analysis_C1 ...
Processing theory HOL-ODE-Numerics.Refine_Reachability_Analysis_C1 ...
Processing theory HOL-ODE-Numerics.Init_ODE_Solver ...
Processing theory HOL-ODE-Numerics.Example_Utilities ...
Processing theory HOL-ODE-Numerics.ODE_Numerics ...
Processing theory Lorenz_Approximation.Result_Elements ...
Processing theory Lorenz_Approximation.Result_File_Coarse ...
Processing theory Lorenz_Approximation.Lorenz_Approximation ...
Loading 8 theories ...
Processing theory Poincare_Bendixson.Affine_Arithmetic_Misc ...
Processing theory Poincare_Bendixson.Analysis_Misc ...
Removing 3 theories ...
Processing theory Poincare_Bendixson.ODE_Misc ...
Processing theory Poincare_Bendixson.Invariance ...
Processing theory Poincare_Bendixson.Limit_Set ...
Processing theory Poincare_Bendixson.Periodic_Orbit ...
Processing theory Poincare_Bendixson.Poincare_Bendixson ...
Processing theory Poincare_Bendixson.Examples ...
Loading 4 theories ...
Processing theory Ergodic_Theory.ME_Library_Complement ...
Processing theory Ergodic_Theory.Shift_Operator ...
Processing theory Laws_of_Large_Numbers.Laws_of_Large_Numbers ...
Processing theory Laws_of_Large_Numbers.Laws_of_Large_Numbers_Example ...
Removing 14 theories ...
Processing theory HOL-ODE-ARCH-COMP.Examples_ARCH_COMP ...
Loading 2 theories ...
Processing theory Ergodic_Theory.Transfer_Operator ...
Removing 57 theories ...
Processing theory Ergodic_Theory.Normalizing_Sequences ...
Loading 29 theories ...
Processing theory Probabilistic_Timed_Automata.Instantiate_Existentials ...
Processing theory Probabilistic_Timed_Automata.Basic ...
Processing theory Probabilistic_Timed_Automata.Finiteness ...
Removing 6 theories ...
Processing theory Probabilistic_Timed_Automata.Sequence ...
Processing theory Probabilistic_Timed_Automata.More_List ...
Processing theory Probabilistic_Timed_Automata.Sequence_LTL ...
Processing theory Probabilistic_Timed_Automata.Stream_More ...
Processing theory Markov_Models.Markov_Decision_Process ...
Processing theory Probabilistic_Timed_Automata.MDP_Aux ...
Processing theory Probabilistic_Timed_Automata.Graphs ...
Processing theory Probabilistic_Timed_Automata.Lib ...
Processing theory Probabilistic_Timed_Automata.PTA ...
Processing theory Probabilistic_Timed_Automata.PTA_Reachability ...
Loading 20 theories ...
Removing 25 theories ...
Processing theory Symmetric_Polynomials.Vieta ...
Processing theory Pi_Transcendental.Pi_Transcendental_Polynomial_Library ...
Processing theory Algebraic_Numbers.Algebraic_Numbers_Prelim ...
Processing theory Hermite_Lindemann.Complex_Lexorder ...
Processing theory Hermite_Lindemann.Misc_HLW ...
Processing theory Algebraic_Numbers.Algebraic_Numbers ...
Processing theory Hermite_Lindemann.Algebraic_Integer_Divisibility ...
Processing theory Hermite_Lindemann.More_Algebraic_Numbers_HLW ...
Processing theory Symmetric_Polynomials.Symmetric_Polynomials ...
Processing theory Power_Sum_Polynomials.Power_Sum_Polynomials_Library ...
Processing theory Hermite_Lindemann.More_Multivariate_Polynomial_HLW ...
Processing theory Hermite_Lindemann.More_Polynomial_HLW ...
Processing theory Hermite_Lindemann.Min_Int_Poly ...
Processing theory Pi_Transcendental.Pi_Transcendental ...
Processing theory Hermite_Lindemann.Hermite_Lindemann ...
Loading 11 theories ...
Removing 11 theories ...
Processing theory Perron_Frobenius.Perron_Frobenius_Aux ...
Processing theory Stochastic_Matrices.Stochastic_Matrix ...
Processing theory Jordan_Normal_Form.Jordan_Normal_Form_Uniqueness ...
Processing theory Stochastic_Matrices.Eigenspace ...
Processing theory Perron_Frobenius.Perron_Frobenius ...
Processing theory Stochastic_Matrices.Stochastic_Vector_PMF ...
Processing theory Perron_Frobenius.Roots_Unity ...
Processing theory Perron_Frobenius.Perron_Frobenius_Irreducible ...
Processing theory Markov_Models.Classifying_Markov_Chain_States ...
Loading 6 theories ...
Processing theory Stochastic_Matrices.Stochastic_Matrix_Markov_Models ...
Processing theory Stochastic_Matrices.Stochastic_Matrix_Perron_Frobenius ...
Processing theory Markov_Models.Discrete_Time_Markov_Process ...
Processing theory Markov_Models.Trace_Space_Equals_Markov_Processes ...
Processing theory Markov_Models.MDP_Reachability_Problem ...
Processing theory Markov_Models.Continuous_Time_Markov_Chain ...
Processing theory Markov_Models.Markov_Models ...
Removing 5 theories ...
Processing theory Markov_Models.MDP_RP ...
Processing theory Markov_Models.Example_B ...
Processing theory Markov_Models.Example_A ...
Processing theory Markov_Models.MDP_RP_Certification ...
Removing 10 theories ...
Processing theory Stirling_Formula.Gamma_Asymptotics ...
Removing 13 theories ...
Processing theory Markov_Models.PGCL ...
Loading 20 theories ...
Processing theory Monad_Memo_DP.Pure_Monad ...
Processing theory Monad_Memo_DP.State_Heap_Misc ...
Processing theory Hidden_Markov_Models.Auxiliary ...
Processing theory Monad_Memo_DP.State_Monad_Ext ...
Processing theory Monad_Memo_DP.DP_CRelVS ...
Processing theory Monad_Memo_DP.Memory ...
Processing theory Monad_Memo_DP.Heap_Monad_Ext ...
Processing theory Monad_Memo_DP.State_Heap ...
Processing theory Monad_Memo_DP.DP_CRelVH ...
Processing theory Monad_Memo_DP.Transform_Cmd ...
Processing theory Monad_Memo_DP.State_Main ...
Removing 2 theories ...
Processing theory Hidden_Markov_Models.Hidden_Markov_Model ...
Processing theory Hidden_Markov_Models.HMM_Implementation ...
Processing theory Hidden_Markov_Models.HMM_Example ...
Processing theory Markov_Models.Zeroconf_Analysis ...
Loading 2 theories ...
Processing theory Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun ...
Removing 5 theories ...
Processing theory Markov_Models.PCTL ...
Processing theory Markov_Models.Gossip_Broadcast ...
Removing 3 theories ...
Processing theory Markov_Models.Crowds_Protocol ...
Processing theory Probabilistic_While.Resampling ...
Loading 2 theories ...
Processing theory Probabilistic_While.Bernoulli ...
Processing theory Probabilistic_While.Geometric ...
Processing theory Probabilistic_While.Fast_Dice_Roll ...
Loading 16 theories ...
Removing 13 theories ...
Processing theory Randomised_Social_Choice.QSOpt_Exact ...
Processing theory Randomised_Social_Choice.Lotteries ...
Processing theory Randomised_Social_Choice.Utility_Functions ...
Processing theory Randomised_Social_Choice.Stochastic_Dominance ...
Processing theory Randomised_Social_Choice.SD_Efficiency ...
Processing theory Randomised_Social_Choice.Social_Decision_Schemes ...
Processing theory Randomised_Social_Choice.Random_Dictatorship ...
Processing theory Randomised_Social_Choice.Random_Serial_Dictatorship ...
Processing theory Randomised_Social_Choice.SDS_Automation ...
Processing theory Randomised_Social_Choice.SDS_Lowering ...
Processing theory Randomised_Social_Choice.Randomised_Social_Choice ...
Processing theory SDS_Impossibility.SDS_Impossibility ...
Loading 11 theories ...
Removing 16 theories ...
Processing theory Randomised_BSTs.Randomised_BSTs ...
Loading 8 theories ...
Processing theory Girth_Chromatic.Girth_Chromatic_Misc ...
Processing theory Girth_Chromatic.Ugraphs ...
Processing theory Random_Graph_Subgraph_Threshold.Ugraph_Misc ...
Processing theory Girth_Chromatic.Girth_Chromatic ...
Processing theory Random_Graph_Subgraph_Threshold.Prob_Lemmas ...
Processing theory Random_Graph_Subgraph_Threshold.Ugraph_Lemmas ...
Processing theory Random_Graph_Subgraph_Threshold.Ugraph_Properties ...
Processing theory Random_Graph_Subgraph_Threshold.Subgraph_Threshold ...
Removing 13 theories ...
Processing theory Smith_Normal_Form.Smith_Certified ...
Loading 8 theories ...
Processing theory Applicative_Lifting.Applicative_Option ...
Processing theory Applicative_Lifting.Applicative_State ...
Processing theory Applicative_Lifting.Applicative_Environment_Algebra ...
Processing theory Applicative_Lifting.Applicative_Stream ...
Processing theory Applicative_Lifting.Stream_Algebra ...
Processing theory Applicative_Lifting.Tree_Relabelling ...
Loading 15 theories ...
Processing theory Applicative_Lifting.Applicative_Examples ...
Processing theory Applicative_Lifting.Applicative_Open_State ...
Processing theory Applicative_Lifting.Applicative_List ...
Processing theory Applicative_Lifting.Applicative_Filter ...
Processing theory Applicative_Lifting.Applicative_Vector ...
Processing theory Applicative_Lifting.Applicative_Probability_List ...
Processing theory Applicative_Lifting.Applicative_Sum ...
Processing theory Applicative_Lifting.Applicative_Star ...
Processing theory Applicative_Lifting.Applicative_DNEList ...
Processing theory Applicative_Lifting.Applicative_Monoid ...
Processing theory Applicative_Lifting.Applicative_Functor ...
Removing 50 theories ...
Processing theory Smith_Normal_Form.SNF_Algorithm_HOL_Analysis ...
Loading 2 theories ...
Processing theory Smith_Normal_Form.Diagonalize ...
Loading 2 theories ...
Processing theory Smith_Normal_Form.SNF_Algorithm_Two_Steps_JNF ...
Removing 4 theories ...
Processing theory Smith_Normal_Form.Cauchy_Binet ...
Processing theory Smith_Normal_Form.SNF_Uniqueness ...
Processing theory Smith_Normal_Form.Cauchy_Binet_HOL_Analysis ...
Processing theory Smith_Normal_Form.SNF_Algorithm_Two_Steps ...
Loading 5 theories ...
Removing 15 theories ...
Processing theory Echelon_Form.Echelon_Form_IArrays ...
Processing theory Hermite.Hermite_IArrays ...
Loading 6 theories ...
Processing theory Echelon_Form.Echelon_Form_Det_IArrays ...
Processing theory Echelon_Form.Code_Cayley_Hamilton_IArrays ...
Processing theory Echelon_Form.Echelon_Form_Inverse_IArrays ...
Removing 2 theories ...
Processing theory Echelon_Form.Examples_Echelon_Form_IArrays ...
Loading 7 theories ...
Processing theory Gauss_Sums.Periodic_Arithmetic ...
Processing theory Gauss_Sums.Gauss_Sums_Auxiliary ...
Processing theory Gauss_Sums.Complex_Roots_Of_Unity ...
Processing theory Gauss_Sums.Finite_Fourier_Series ...
Processing theory Gauss_Sums.Ramanujan_Sums ...
Removing 36 theories ...
Processing theory Gauss_Sums.Gauss_Sums ...
Processing theory Gauss_Sums.Polya_Vinogradov ...
Loading 2 theories ...
Processing theory Lambert_W.Lambert_W ...
Removing 10 theories ...
Processing theory Lambert_W.Lambert_W_MacLaurin_Series ...
Processing theory Comparison_Sort_Lower_Bound.Comparison_Sort_Lower_Bound ...
Loading 11 theories ...
Processing theory Akra_Bazzi.Akra_Bazzi_Library ...
Processing theory Akra_Bazzi.Akra_Bazzi_Asymptotics ...
Processing theory Akra_Bazzi.Eval_Numeral ...
Processing theory Akra_Bazzi.Akra_Bazzi_Real ...
Removing 42 theories ...
Processing theory Akra_Bazzi.Akra_Bazzi ...
Processing theory Akra_Bazzi.Master_Theorem ...
Processing theory Akra_Bazzi.Akra_Bazzi_Method ...
Processing theory Akra_Bazzi.Akra_Bazzi_Approximation ...
Processing theory Closest_Pair_Points.Common ...
Processing theory Closest_Pair_Points.Closest_Pair_Alternative ...
Removing 1 theories ...
Processing theory Closest_Pair_Points.Closest_Pair ...
Processing theory Akra_Bazzi.Master_Theorem_Examples ...
Loading 9 theories ...
Processing theory Perron_Frobenius.Hom_Gauss_Jordan ...
Processing theory Perron_Frobenius.Perron_Frobenius_General ...
Removing 33 theories ...
Processing theory Perron_Frobenius.Spectral_Radius_Largest_Jordan_Block ...
Loading 12 theories ...
Processing theory Perron_Frobenius.Spectral_Radius_Theory_2 ...
Processing theory Perron_Frobenius.Check_Matrix_Growth ...
Removing 18 theories ...
Processing theory Group-Ring-Module.Algebra1 ...
Processing theory Group-Ring-Module.Algebra2 ...
Processing theory Group-Ring-Module.Algebra3 ...
Processing theory Group-Ring-Module.Algebra4 ...
Processing theory Group-Ring-Module.Algebra5 ...
Processing theory Group-Ring-Module.Algebra6 ...
Processing theory Group-Ring-Module.Algebra7 ...
Processing theory Group-Ring-Module.Algebra8 ...
Processing theory Group-Ring-Module.Algebra9 ...
Processing theory Valuation.Valuation1 ...
Processing theory Valuation.Valuation2 ...
Processing theory Valuation.Valuation3 ...
Processing theory Perron_Frobenius.Spectral_Radius_Theory ...
Loading 8 theories ...
Removing 25 theories ...
Processing theory Taylor_Models.Horner_Eval ...
Processing theory Taylor_Models.Taylor_Models_Misc ...
Processing theory Taylor_Models.Polynomial_Expression ...
Processing theory Taylor_Models.Polynomial_Expression_Additional ...
Processing theory Taylor_Models.Taylor_Models ...
Processing theory Taylor_Models.Experiments ...
Loading 4 theories ...
Removing 35 theories ...
Processing theory LLL_Basis_Reduction.LLL_Number_Bounds ...
Processing theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Mod_Operation ...
Processing theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann ...
Processing theory Modular_arithmetic_LLL_and_HNF_algorithms.Storjohann_Impl ...
Loading 18 theories ...
Processing theory LLL_Factorization.Sub_Sums ...
Processing theory Berlekamp_Zassenhaus.Code_Abort_Gcd ...
Removing 5 theories ...
Processing theory Berlekamp_Zassenhaus.Suitable_Prime ...
Processing theory LLL_Factorization.Missing_Dvd_Int_Poly ...
Processing theory Berlekamp_Zassenhaus.Degree_Bound ...
Processing theory Berlekamp_Zassenhaus.Mahler_Measure ...
Processing theory Berlekamp_Zassenhaus.Factor_Bound ...
Processing theory LLL_Factorization.Factor_Bound_2 ...
Processing theory Berlekamp_Zassenhaus.Gcd_Finite_Field_Impl ...
Processing theory Berlekamp_Zassenhaus.Reconstruction ...
Processing theory Berlekamp_Zassenhaus.Berlekamp_Zassenhaus ...
Processing theory Berlekamp_Zassenhaus.Square_Free_Factorization_Int ...
Processing theory Berlekamp_Zassenhaus.Factorize_Int_Poly ...
Processing theory LLL_Factorization.LLL_Factorization_Impl ...
Processing theory LLL_Factorization.LLL_Factorization ...
Processing theory LLL_Factorization.Factorization_Algorithm_16_22 ...
Processing theory LLL_Factorization.Modern_Computer_Algebra_Problem ...
Loading 33 theories ...
Processing theory Polynomials.More_Modules ...
Processing theory Groebner_Bases.Code_Target_Rat ...
Processing theory Groebner_Bases.Confluence ...
Processing theory Polynomials.Utils ...
Removing 8 theories ...
Processing theory Groebner_Bases.General ...
Processing theory Signature_Groebner.Prelims ...
Processing theory Polynomials.Power_Products ...
Processing theory Polynomials.OAlist ...
Processing theory Polynomials.PP_Type ...
Processing theory Polynomials.MPoly_Type_Class ...
Processing theory Polynomials.MPoly_Type_Class_Ordered ...
Processing theory Groebner_Bases.More_MPoly_Type_Class ...
Processing theory Polynomials.Quasi_PM_Power_Products ...
Processing theory Signature_Groebner.More_MPoly ...
Processing theory Groebner_Bases.Reduction ...
Processing theory Polynomials.OAlist_Poly_Mapping ...
Processing theory Polynomials.Term_Order ...
Processing theory Groebner_Bases.Groebner_Bases ...
Processing theory Groebner_Bases.Syzygy ...
Processing theory Polynomials.MPoly_Type_Class_OAlist ...
Processing theory Groebner_Bases.Benchmarks ...
Processing theory Signature_Groebner.Signature_Groebner ...
Processing theory Signature_Groebner.Signature_Examples ...
Loading 15 theories ...
Processing theory Deriving.Compare_Rat ...
Processing theory Deriving.Compare_Real ...
Processing theory Algebraic_Numbers.Factors_of_Int_Poly ...
Processing theory Berlekamp_Zassenhaus.Factorize_Rat_Poly ...
Processing theory Algebraic_Numbers.Sturm_Rat ...
Removing 4 theories ...
Processing theory BenOr_Kozen_Reif.More_Matrix ...
Processing theory BenOr_Kozen_Reif.BKR_Algorithm ...
Processing theory BenOr_Kozen_Reif.Renegar_Algorithm ...
Processing theory BenOr_Kozen_Reif.Matrix_Equation_Construction ...
Processing theory Algebraic_Numbers.Real_Algebraic_Numbers ...
Processing theory Algebraic_Numbers.Real_Roots ...
Processing theory BenOr_Kozen_Reif.BKR_Proofs ...
Processing theory BenOr_Kozen_Reif.Renegar_Proofs ...
Processing theory BenOr_Kozen_Reif.BKR_Decision ...
Processing theory BenOr_Kozen_Reif.Renegar_Decision ...
Removing 12 theories ...
Processing theory LLL_Basis_Reduction.FPLLL_Solver ...
Loading 11 theories ...
Processing theory Show.Show_Complex ...
Processing theory Algebraic_Numbers.Compare_Complex ...
Processing theory Algebraic_Numbers.Show_Real_Alg ...
Processing theory Algebraic_Numbers.Complex_Roots_Real_Poly ...
Processing theory Algebraic_Numbers.Show_Real_Precise ...
Processing theory Algebraic_Numbers.Interval_Arithmetic ...
Processing theory Algebraic_Numbers.Complex_Algebraic_Numbers ...
Processing theory Algebraic_Numbers.Real_Factorization ...
Removing 2 theories ...
Processing theory Algebraic_Numbers.Algebraic_Number_Tests ...
Processing theory Algebraic_Numbers.Algebraic_Numbers_External_Code ...
Loading 40 theories ...
Processing theory Automated_Stateful_Protocol_Verification.Eisbach_Protocol_Verification ...
Processing theory Automated_Stateful_Protocol_Verification.ml_yacc_lib ...
Processing theory Automated_Stateful_Protocol_Verification.trac_term ...
Processing theory Automated_Stateful_Protocol_Verification.trac_fp_parser ...
Processing theory Automated_Stateful_Protocol_Verification.trac_protocol_parser ...
Processing theory Automated_Stateful_Protocol_Verification.trac ...
Processing theory Stateful_Protocol_Composition_and_Typing.Miscellaneous ...
Processing theory Stateful_Protocol_Composition_and_Typing.Messages ...
Removing 4 theories ...
Processing theory Stateful_Protocol_Composition_and_Typing.More_Unification ...
Processing theory Stateful_Protocol_Composition_and_Typing.Intruder_Deduction ...
Processing theory Automated_Stateful_Protocol_Verification.Term_Variants ...
Processing theory Stateful_Protocol_Composition_and_Typing.Strands_and_Constraints ...
Processing theory Stateful_Protocol_Composition_and_Typing.Labeled_Strands ...
Processing theory Stateful_Protocol_Composition_and_Typing.Lazy_Intruder ...
Processing theory Stateful_Protocol_Composition_and_Typing.Stateful_Strands ...
Processing theory Stateful_Protocol_Composition_and_Typing.Typed_Model ...
Processing theory Stateful_Protocol_Composition_and_Typing.Labeled_Stateful_Strands ...
Processing theory Automated_Stateful_Protocol_Verification.Transactions ...
Processing theory Automated_Stateful_Protocol_Verification.Term_Abstraction ...
Processing theory Stateful_Protocol_Composition_and_Typing.Typing_Result ...
Processing theory Stateful_Protocol_Composition_and_Typing.Parallel_Compositionality ...
Processing theory Stateful_Protocol_Composition_and_Typing.Stateful_Typing ...
Processing theory Stateful_Protocol_Composition_and_Typing.Stateful_Compositionality ...
Processing theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Model ...
Processing theory Automated_Stateful_Protocol_Verification.Term_Implication ...
Processing theory Automated_Stateful_Protocol_Verification.Stateful_Protocol_Verification ...
Processing theory Automated_Stateful_Protocol_Verification.PSPSP ...
Processing theory Automated_Stateful_Protocol_Verification.PKCS_Model09 ...
Processing theory Automated_Stateful_Protocol_Verification.PKCS_Model07 ...
Processing theory Automated_Stateful_Protocol_Verification.PKCS_Model03 ...
Processing theory Automated_Stateful_Protocol_Verification.Keyserver_Composition ...
Processing theory Automated_Stateful_Protocol_Verification.Keyserver ...
Processing theory Automated_Stateful_Protocol_Verification.Keyserver2 ...
Loading 14 theories ...
Processing theory Automated_Stateful_Protocol_Verification.Examples ...
Processing theory Linear_Inequalities.Missing_Matrix ...
Processing theory Linear_Inequalities.Sum_Vec_Set ...
Processing theory Linear_Inequalities.Missing_VS_Connect ...
Processing theory Linear_Inequalities.Dim_Span ...
Processing theory Linear_Inequalities.Basis_Extension ...
Removing 20 theories ...
Processing theory Linear_Inequalities.Integral_Bounded_Vectors ...
Processing theory Linear_Inequalities.Normal_Vector ...
Processing theory Linear_Inequalities.Cone ...
Processing theory Linear_Inequalities.Convex_Hull ...
Processing theory Linear_Inequalities.Fundamental_Theorem_Linear_Inequalities ...
Processing theory Linear_Inequalities.Farkas_Minkowsky_Weyl ...
Processing theory Linear_Inequalities.Decomposition_Theorem ...
Processing theory Linear_Inequalities.Mixed_Integer_Solutions ...
Processing theory Linear_Inequalities.Integer_Hull ...
Loading 4 theories ...
Removing 5 theories ...
Processing theory Linear_Recurrences_Solver.Show_RatFPS ...
Processing theory Linear_Recurrences_Solver.Linear_Recurrences_Solver ...
Processing theory Linear_Recurrences_Solver.Linear_Recurrences_Pretty ...
Processing theory Linear_Recurrences_Solver.Linear_Recurrences_Test ...
Loading 32 theories ...
Processing theory Core_SC_DOM.Core_DOM_Basic_Datatypes ...
Processing theory Core_SC_DOM.Hiding_Type_Variables ...
Processing theory Core_SC_DOM.Ref ...
Processing theory Core_SC_DOM.ObjectPointer ...
Processing theory Core_SC_DOM.NodePointer ...
Processing theory Core_SC_DOM.BaseClass ...
Processing theory Core_SC_DOM.ObjectClass ...
Processing theory Core_SC_DOM.NodeClass ...
Processing theory Core_SC_DOM.ElementPointer ...
Processing theory Core_SC_DOM.CharacterDataPointer ...
Processing theory Core_SC_DOM.DocumentPointer ...
Processing theory Core_SC_DOM.ShadowRootPointer ...
Removing 21 theories ...
Processing theory Core_SC_DOM.ElementClass ...
Processing theory Core_SC_DOM.CharacterDataClass ...
Processing theory Core_SC_DOM.DocumentClass ...
Processing theory Core_SC_DOM.Heap_Error_Monad ...
Processing theory Core_SC_DOM.BaseMonad ...
Processing theory Core_SC_DOM.ObjectMonad ...
Processing theory Core_SC_DOM.NodeMonad ...
Processing theory Shadow_SC_DOM.ShadowRootClass ...
Processing theory Core_SC_DOM.ElementMonad ...
Processing theory Core_SC_DOM.CharacterDataMonad ...
Processing theory Core_SC_DOM.DocumentMonad ...
Processing theory Shadow_SC_DOM.ShadowRootMonad ...
Processing theory Core_SC_DOM.Core_DOM_Functions ...
Processing theory Core_SC_DOM.Core_DOM_Heap_WF ...
Processing theory Core_SC_DOM.Core_DOM ...
Processing theory SC_DOM_Components.Core_DOM_DOM_Components ...
Processing theory SC_DOM_Components.Core_DOM_SC_DOM_Components ...
Processing theory Shadow_SC_DOM.Shadow_DOM ...
Processing theory SC_DOM_Components.Shadow_DOM_DOM_Components ...
Processing theory SC_DOM_Components.Shadow_DOM_SC_DOM_Components ...
Loading 2 theories ...
Processing theory LLL_Basis_Reduction.Cost ...
Processing theory LLL_Basis_Reduction.LLL_Complexity ...
Processing theory Ergodic_Theory.Kohlberg_Neyman_Karlsson ...
Loading 8 theories ...
Removing 13 theories ...
Processing theory Shadow_SC_DOM.Shadow_DOM_BaseTest ...
Processing theory Shadow_SC_DOM.Shadow_DOM_Document_adoptNode ...
Processing theory Shadow_SC_DOM.Shadow_DOM_Node_insertBefore ...
Processing theory Shadow_SC_DOM.Shadow_DOM_Node_removeChild ...
Processing theory Shadow_SC_DOM.Shadow_DOM_Document_getElementById ...
Processing theory Shadow_SC_DOM.slots_fallback ...
Processing theory Shadow_SC_DOM.slots ...
Processing theory Shadow_SC_DOM.Shadow_DOM_Tests ...
Processing theory Taylor_Models.Float_Topology ...
Removing 31 theories ...
Processing theory Linear_Inequalities.Farkas_Lemma ...
Loading 11 theories ...
Removing 15 theories ...
Processing theory QHLProver.Matrix_Limit ...
Processing theory QHLProver.Quantum_Program ...
Processing theory QHLProver.Partial_State ...
Processing theory QHLProver.Quantum_Hoare ...
Processing theory QHLProver.Grover ...
Processing theory Algebraic_Numbers.Show_Real_Approx ...
Loading 16 theories ...
Processing theory Groebner_Macaulay.Dube_Prelims ...
Processing theory Groebner_Macaulay.Binomial_Int ...
Processing theory Groebner_Macaulay.Poly_Fun ...
Removing 63 theories ...
Processing theory Groebner_Bases.Auto_Reduction ...
Processing theory Groebner_Bases.Reduced_GB ...
Processing theory Groebner_Bases.Macaulay_Matrix ...
Processing theory Groebner_Macaulay.Monomial_Module ...
Processing theory Polynomials.MPoly_PM ...
Processing theory Groebner_Macaulay.Degree_Section ...
Processing theory Groebner_Bases.Groebner_PM ...
Processing theory Groebner_Macaulay.Degree_Bound_Utils ...
Processing theory Groebner_Macaulay.Groebner_Macaulay ...
Processing theory Groebner_Macaulay.Hilbert_Function ...
Processing theory Groebner_Macaulay.Cone_Decomposition ...
Processing theory Groebner_Macaulay.Dube_Bound ...
Processing theory Groebner_Macaulay.Groebner_Macaulay_Examples ...
Loading 4 theories ...
Removing 11 theories ...
Processing theory Groebner_Bases.Algorithm_Schema ...
Processing theory Groebner_Bases.Algorithm_Schema_Impl ...
Processing theory Groebner_Bases.F4 ...
Processing theory Groebner_Bases.F4_Examples ...
Loading 36 theories ...
Removing 3 theories ...
Processing theory Core_DOM.Core_DOM_Basic_Datatypes ...
Processing theory Core_DOM.Hiding_Type_Variables ...
Processing theory Core_DOM.Ref ...
Processing theory Core_DOM.ObjectPointer ...
Processing theory Core_DOM.NodePointer ...
Processing theory Core_DOM.BaseClass ...
Processing theory Core_DOM.ObjectClass ...
Processing theory Core_DOM.NodeClass ...
Processing theory Core_DOM.ElementPointer ...
Processing theory Core_DOM.CharacterDataPointer ...
Processing theory Core_DOM.DocumentPointer ...
Processing theory Core_DOM.ShadowRootPointer ...
Processing theory Core_DOM.ElementClass ...
Processing theory Core_DOM.CharacterDataClass ...
Processing theory Core_DOM.DocumentClass ...
Processing theory Core_DOM.Heap_Error_Monad ...
Processing theory Shadow_DOM.ShadowRootClass ...
Processing theory Core_DOM.BaseMonad ...
Processing theory Core_DOM.ObjectMonad ...
Processing theory Core_DOM.NodeMonad ...
Processing theory Core_DOM.ElementMonad ...
Processing theory Core_DOM.CharacterDataMonad ...
Processing theory Core_DOM.DocumentMonad ...
Processing theory Shadow_DOM.ShadowRootMonad ...
Processing theory Core_DOM.Core_DOM_Functions ...
Processing theory Core_DOM.Core_DOM_Heap_WF ...
Processing theory Core_DOM.Core_DOM ...
Processing theory Shadow_DOM.Shadow_DOM ...
Processing theory Shadow_DOM.Shadow_DOM_BaseTest ...
Processing theory Shadow_DOM.Shadow_DOM_Document_adoptNode ...
Processing theory Shadow_DOM.Shadow_DOM_Node_insertBefore ...
Processing theory Shadow_DOM.Shadow_DOM_Node_removeChild ...
Processing theory Shadow_DOM.Shadow_DOM_Document_getElementById ...
Processing theory Shadow_DOM.slots_fallback ...
Processing theory Shadow_DOM.slots ...
Loading 2 theories ...
Processing theory Shadow_DOM.Shadow_DOM_Tests ...
Processing theory Groebner_Bases.Buchberger ...
Removing 8 theories ...
Processing theory Groebner_Bases.Syzygy_Examples ...
Removing 2 theories ...
Processing theory Groebner_Bases.Reduced_GB_Examples ...
Removing 1 theories ...
Processing theory Groebner_Bases.Buchberger_Examples ...
Processing theory DOM_Components.fancy_tabs ...
Loading 2 theories ...
Removing 12 theories ...
Processing theory DOM_Components.Core_DOM_Components ...
Processing theory DOM_Components.Shadow_DOM_Components ...
Loading 30 theories ...
Processing theory Word_Lib.Type_Syntax ...
Processing theory MFOTL_Monitor.Interval ...
Processing theory Word_Lib.Enumeration ...
Processing theory Word_Lib.Enumeration_Word ...
Processing theory MFOTL_Monitor.Trace ...
Processing theory MFOTL_Monitor.Table ...
Processing theory MFOTL_Monitor.Abstract_Monitor ...
Processing theory MFODL_Monitor_Optimized.Regex ...
Removing 5 theories ...
Processing theory Word_Lib.Word_Lemmas ...
Processing theory Generic_Join.Generic_Join ...
Processing theory IEEE_Floating_Point.IEEE ...
Processing theory IEEE_Floating_Point.IEEE_Properties ...
Processing theory Generic_Join.Generic_Join_Correctness ...
Processing theory MFODL_Monitor_Optimized.Optimized_Join ...
Processing theory MFODL_Monitor_Optimized.Code_Double ...
Processing theory MFODL_Monitor_Optimized.Event_Data ...
Processing theory MFODL_Monitor_Optimized.Formula ...
Processing theory MFODL_Monitor_Optimized.Monitor ...
Processing theory MFODL_Monitor_Optimized.Optimized_MTL ...
Processing theory MFODL_Monitor_Optimized.Monitor_Impl ...
Processing theory MFODL_Monitor_Optimized.Monitor_Code ...
Loading 11 theories ...
Processing theory Coinductive.Coinductive_List_Prefix ...
Processing theory Coinductive.Koenigslemma ...
Processing theory Coinductive.LMirror ...
Processing theory Coinductive.CCPO_Topology ...
Processing theory Coinductive.Resumption ...
Removing 11 theories ...
Processing theory Coinductive.TLList_CCPO ...
Processing theory Coinductive.TLList_CCPO_Examples ...
Processing theory Coinductive.LList_CCPO_Topology ...
Loading 5 theories ...
Processing theory Coinductive.Hamming_Stream ...
Processing theory Coinductive.Coinductive_Examples ...
Processing theory Nullstellensatz.Lex_Order_PP ...
Processing theory Nullstellensatz.Univariate_PM ...
Processing theory Nullstellensatz.Algebraically_Closed_Fields ...
Processing theory Nullstellensatz.Nullstellensatz ...
Loading 29 theories ...
Processing theory Nullstellensatz.Nullstellensatz_Field ...
Removing 40 theories ...
Processing theory Complex_Geometry.Linear_Systems ...
Processing theory Poincare_Disc.Tarski ...
Processing theory Complex_Geometry.More_Transcendental ...
Processing theory Complex_Geometry.Canonical_Angle ...
Processing theory Complex_Geometry.More_Set ...
Processing theory Complex_Geometry.More_Complex ...
Processing theory Poincare_Disc.Hyperbolic_Functions ...
Processing theory Complex_Geometry.Quadratic ...
Processing theory Complex_Geometry.Angles ...
Processing theory Complex_Geometry.Elementary_Complex_Geometry ...
Processing theory Complex_Geometry.Matrices ...
Processing theory Complex_Geometry.Unitary_Matrices ...
Processing theory Complex_Geometry.Unitary11_Matrices ...
Processing theory Complex_Geometry.Hermitean_Matrices ...
Processing theory Complex_Geometry.Homogeneous_Coordinates ...
Processing theory Complex_Geometry.Moebius ...
Processing theory Complex_Geometry.Circlines ...
Processing theory Complex_Geometry.Oriented_Circlines ...
Processing theory Complex_Geometry.Circlines_Angle ...
Processing theory Complex_Geometry.Unit_Circle_Preserving_Moebius ...
Processing theory Poincare_Disc.Poincare_Lines ...
Processing theory Poincare_Disc.Poincare_Lines_Ideal_Points ...
Processing theory Poincare_Disc.Poincare_Distance ...
Processing theory Poincare_Disc.Poincare_Circles ...
Processing theory Poincare_Disc.Poincare_Between ...
Processing theory Poincare_Disc.Poincare ...
Processing theory Poincare_Disc.Poincare_Lines_Axis_Intersections ...
Processing theory Poincare_Disc.Poincare_Tarski ...
Removing 4 theories ...
Processing theory Poincare_Disc.Poincare_Perpendicular ...
Loading 15 theories ...
Processing theory Simplex.Simplex_Auxiliary ...
Processing theory Simplex.Rel_Chain ...
Processing theory Linear_Programming.More_Jordan_Normal_Forms ...
Processing theory Simplex.Simplex_Algebra ...
Processing theory Simplex.Abstract_Linear_Poly ...
Processing theory Simplex.Linear_Poly_Maps ...
Processing theory Simplex.QDelta ...
Removing 10 theories ...
Processing theory Simplex.Simplex ...
Processing theory Simplex.Simplex_Incremental ...
Processing theory Farkas.Farkas ...
Processing theory Farkas.Simplex_for_Reals ...
Processing theory Farkas.Matrix_Farkas ...
Processing theory Linear_Programming.Matrix_LinPoly ...
Processing theory Linear_Programming.LP_Preliminaries ...
Processing theory Linear_Programming.Linear_Programming ...
Loading 114 theories ...
Removing 25 theories ...
Processing theory LEM.Lem_bool ...
Processing theory Constructor_Funs.Constructor_Funs ...
Processing theory Lazy_Case.Lazy_Case ...
Processing theory Word_Lib.More_Misc ...
Processing theory Word_Lib.Word_Names ...
Processing theory Word_Lib.Word_Syntax ...
Processing theory Dict_Construction.Dict_Construction ...
Processing theory CakeML_Codegen.ML_Utils ...
Processing theory CakeML_Codegen.Code_Utils ...
Processing theory Word_Lib.Rsplit ...
Processing theory LEM.Lem_basic_classes ...
Processing theory LEM.Lem_tuple ...
Processing theory LEM.Lem_function ...
Processing theory LEM.Lem_maybe ...
Processing theory CakeML_Codegen.Compiler_Utils ...
Processing theory LEM.LemExtraDefs ...
Processing theory LEM.Lem_num ...
Processing theory LEM.Lem_set_helpers ...
Processing theory LEM.Lem ...
Processing theory LEM.Lem_assert_extra ...
Processing theory LEM.Lem_maybe_extra ...
Processing theory LEM.Lem_function_extra ...
Processing theory CakeML_Codegen.Terms_Extras ...
Processing theory CakeML_Codegen.General_Rewriting ...
Processing theory CakeML_Codegen.HOL_Datatype ...
Processing theory CakeML_Codegen.Constructors ...
Processing theory LEM.Lem_list ...
Processing theory LEM.Lem_either ...
Processing theory LEM.Lem_string ...
Processing theory LEM.Lem_list_extra ...
Processing theory LEM.Lem_num_extra ...
Processing theory LEM.Lem_set ...
Processing theory LEM.Lem_map ...
Processing theory LEM.Lem_map_extra ...
Processing theory LEM.Lem_relation ...
Processing theory LEM.Lem_show ...
Processing theory LEM.Lem_machine_word ...
Processing theory LEM.Lem_sorting ...
Processing theory LEM.Lem_set_extra ...
Processing theory LEM.Lem_string_extra ...
Processing theory LEM.Lem_show_extra ...
Processing theory CakeML_Codegen.Consts ...
Processing theory Word_Lib.More_Word_Operations ...
Processing theory CakeML_Codegen.Strong_Term ...
Processing theory LEM.Lem_word ...
Processing theory LEM.Lem_pervasives ...
Processing theory LEM.Lem_pervasives_extra ...
Processing theory CakeML_Codegen.Rewriting_Term ...
Processing theory CakeML_Codegen.Eval_Class ...
Processing theory Word_Lib.Word_64 ...
Processing theory IEEE_Floating_Point.FP64 ...
Processing theory CakeML_Codegen.Embed ...
Processing theory CakeML.Lib ...
Processing theory CakeML.Namespace ...
Processing theory CakeML_Codegen.Eval_Instances ...
Processing theory CakeML.FpSem ...
Processing theory CakeML_Codegen.Sterm ...
Processing theory CakeML_Codegen.Term_as_Value ...
Processing theory CakeML.Ffi ...
Processing theory CakeML_Codegen.Rewriting_Nterm ...
Processing theory CakeML_Codegen.Pterm ...
Processing theory CakeML_Codegen.Value ...
Processing theory CakeML_Codegen.Rewriting_Pterm_Elim ...
Processing theory CakeML_Codegen.Rewriting_Pterm ...
Processing theory CakeML_Codegen.Rewriting_Sterm ...
Processing theory CakeML_Codegen.Big_Step_Sterm ...
Processing theory CakeML.Ast ...
Processing theory CakeML.CakeML_Compiler ...
Processing theory CakeML.AstAuxiliary ...
Processing theory CakeML_Codegen.Big_Step_Value ...
Processing theory CakeML.SemanticPrimitives ...
Processing theory CakeML.Evaluate ...
Processing theory CakeML.SmallStep ...
Processing theory CakeML_Codegen.Big_Step_Value_ML ...
Processing theory CakeML.SemanticPrimitivesAuxiliary ...
Processing theory CakeML.PrimTypes ...
Processing theory CakeML.BigStep ...
Processing theory CakeML.Semantic_Extras ...
Processing theory CakeML.Big_Step_Total ...
Processing theory CakeML_Codegen.CakeML_Utils ...
Processing theory CakeML.Evaluate_Termination ...
Processing theory CakeML.Matching ...
Processing theory CakeML_Codegen.CupCake_Env ...
Processing theory CakeML.Evaluate_Clock ...
Processing theory CakeML.Evaluate_Single ...
Processing theory CakeML_Codegen.CakeML_Byte ...
Processing theory CakeML.Big_Step_Determ ...
Processing theory CakeML.Big_Step_Fun_Equiv ...
Processing theory CakeML.Big_Step_Unclocked ...
Processing theory CakeML.CakeML_Code ...
Processing theory CakeML.Big_Step_Clocked ...
Processing theory CakeML.Big_Step_Unclocked_Single ...
Processing theory CakeML_Codegen.CupCake_Semantics ...
Processing theory CakeML_Codegen.CakeML_Setup ...
Processing theory CakeML_Codegen.CakeML_Backend ...
Processing theory CakeML_Codegen.CakeML_Correctness ...
Processing theory CakeML_Codegen.Composition ...
Processing theory CakeML_Codegen.Compiler ...
Processing theory CakeML_Codegen.Test_Print ...
Removing 3 theories ...
Processing theory CakeML_Codegen.Test_Composition ...
Loading 62 theories ...
Processing theory Planarity_Certificates.List_Aux ...
Processing theory Planarity_Certificates.WP ...
Processing theory Graph_Theory.Rtrancl_On ...
Processing theory Planarity_Certificates.Lib ...
Processing theory Graph_Theory.Stuff ...
Processing theory Planarity_Certificates.OptionMonad ...
Processing theory Graph_Theory.Auxiliary ...
Processing theory Planarity_Certificates.NonDetMonad ...
Processing theory Planarity_Certificates.NonDetMonadLemmas ...
Processing theory Planarity_Certificates.OptionMonadND ...
Processing theory Planarity_Certificates.OptionMonadWP ...
Processing theory Planarity_Certificates.AutoCorres_Misc ...
Processing theory Graph_Theory.Digraph ...
Processing theory Graph_Theory.Bidirected_Digraph ...
Processing theory Simpl.Generalise ...
Removing 30 theories ...
Processing theory Planarity_Certificates.Setup_AutoCorres ...
Processing theory Planarity_Certificates.Executable_Permutations ...
Processing theory Graph_Theory.Arc_Walk ...
Processing theory Graph_Theory.Vertex_Walk ...
Processing theory Graph_Theory.Weighted_Graph ...
Processing theory Graph_Theory.Shortest_Path ...
Processing theory Simpl.Language ...
Processing theory Graph_Theory.Pair_Digraph ...
Processing theory Planarity_Certificates.Permutations_2 ...
Processing theory Graph_Theory.Digraph_Component ...
Processing theory Graph_Theory.Digraph_Component_Vwalk ...
Processing theory Graph_Theory.Digraph_Isomorphism ...
Processing theory Graph_Theory.Euler ...
Processing theory Graph_Theory.Subdivision ...
Processing theory Simpl.Semantic ...
Processing theory Simpl.HoarePartialDef ...
Processing theory Simpl.Termination ...
Processing theory Simpl.HoareTotalDef ...
Processing theory Simpl.HoarePartialProps ...
Processing theory Simpl.HoarePartial ...
Processing theory Graph_Theory.Kuratowski ...
Processing theory Graph_Theory.Graph_Theory ...
Processing theory Planarity_Certificates.Graph_Genus ...
Processing theory Planarity_Certificates.Reachablen ...
Processing theory Simpl.SmallStep ...
Processing theory Planarity_Certificates.Digraph_Map_Impl ...
Processing theory Planarity_Certificates.Planar_Complete ...
Processing theory Planarity_Certificates.Check_Planarity_Verification ...
Processing theory Simpl.HoareTotalProps ...
Processing theory Simpl.HoareTotal ...
Processing theory Simpl.Hoare ...
Processing theory Simpl.StateSpace ...
Processing theory Simpl.Vcg ...
Processing theory Planarity_Certificates.Simpl_Anno ...
Processing theory Planarity_Certificates.Planar_Subdivision ...
Processing theory Planarity_Certificates.Planar_Subgraph ...
Processing theory Planarity_Certificates.Kuratowski_Combinatorial ...
Processing theory Planarity_Certificates.Check_Non_Planarity_Impl ...
Processing theory Planarity_Certificates.Check_Non_Planarity_Verification ...
Loading 36 theories ...
Processing theory Planarity_Certificates.Planarity_Certificates ...
Removing 25 theories ...
Processing theory First_Order_Terms.Fun_More ...
Processing theory First_Order_Terms.Transitive_Closure_More ...
Processing theory Ordered_Resolution_Prover.Map2 ...
Processing theory First_Order_Terms.Seq_More ...
Processing theory First_Order_Terms.Abstract_Matching ...
Processing theory First_Order_Terms.Subsumption ...
Processing theory Ordered_Resolution_Prover.Lazy_List_Liminf ...
Processing theory First_Order_Terms.Matching ...
Processing theory Knuth_Bendix_Order.Subterm_and_Context ...
Processing theory Knuth_Bendix_Order.Term_Aux ...
Processing theory Ordered_Resolution_Prover.Clausal_Logic ...
Processing theory Ordered_Resolution_Prover.Herbrand_Interpretation ...
Processing theory Ordered_Resolution_Prover.Ground_Resolution_Model ...
Processing theory Ordered_Resolution_Prover.Inference_System ...
Processing theory Ordered_Resolution_Prover.Unordered_Ground_Resolution ...
Processing theory Abstract-Rewriting.Relative_Rewriting ...
Processing theory Knuth_Bendix_Order.Order_Pair ...
Processing theory Ordered_Resolution_Prover.Ordered_Ground_Resolution ...
Processing theory Knuth_Bendix_Order.Lexicographic_Extension ...
Processing theory Ordered_Resolution_Prover.Abstract_Substitution ...
Processing theory Ordered_Resolution_Prover.Lazy_List_Chain ...
Processing theory Ordered_Resolution_Prover.Proving_Process ...
Processing theory Ordered_Resolution_Prover.Standard_Redundancy ...
Processing theory Knuth_Bendix_Order.KBO ...
Processing theory Functional_Ordered_Resolution_Prover.IsaFoR_Term ...
Processing theory Functional_Ordered_Resolution_Prover.Executable_Subsumption ...
Processing theory Ordered_Resolution_Prover.FO_Ordered_Resolution ...
Processing theory Ordered_Resolution_Prover.FO_Ordered_Resolution_Prover ...
Processing theory Functional_Ordered_Resolution_Prover.Weighted_FO_Ordered_Resolution_Prover ...
Processing theory Functional_Ordered_Resolution_Prover.Deterministic_FO_Ordered_Resolution_Prover ...
Processing theory Functional_Ordered_Resolution_Prover.Executable_FO_Ordered_Resolution_Prover ...
Loading 2 theories ...
Processing theory Power_Sum_Polynomials.Power_Sum_Polynomials ...
Processing theory Power_Sum_Polynomials.Power_Sum_Puzzle ...
Loading 92 theories ...
Removing 22 theories ...
Processing theory Refine_Imperative_HOL.User_Smashing ...
Processing theory PAC_Checker.PAC_Misc ...
Processing theory PAC_Checker.PAC_Version ...
Processing theory Refine_Imperative_HOL.Structured_Apply ...
Processing theory Refine_Imperative_HOL.Concl_Pres_Clarification ...
Processing theory Refine_Imperative_HOL.Named_Theorems_Rev ...
Processing theory Separation_Logic_Imperative_HOL.Default_Insts ...
Processing theory Refine_Imperative_HOL.PO_Normalizer ...
Processing theory Refine_Imperative_HOL.Pf_Add ...
Processing theory Refine_Imperative_HOL.Sepref_Id_Op ...
Processing theory Nested_Multisets_Ordinals.Duplicate_Free_Multiset ...
Processing theory PAC_Checker.Finite_Map_Multiset ...
Processing theory PAC_Checker.More_Loops ...
Processing theory Refine_Imperative_HOL.Pf_Mono_Prover ...
Processing theory Refine_Imperative_HOL.Sepref_Misc ...
Processing theory Refine_Imperative_HOL.Term_Synth ...
Processing theory Refine_Imperative_HOL.Sepref_Basic ...
Processing theory Refine_Imperative_HOL.Sepref_Constraints ...
Processing theory Refine_Imperative_HOL.Sepref_Frame ...
Processing theory Refine_Imperative_HOL.Sepref_Monadify ...
Processing theory Refine_Imperative_HOL.Sepref_Rules ...
Processing theory Refine_Imperative_HOL.Sepref_Combinator_Setup ...
Processing theory Refine_Imperative_HOL.Sepref_Definition ...
Processing theory Refine_Imperative_HOL.Sepref_Translate ...
Processing theory Refine_Imperative_HOL.Sepref_Intf_Util ...
Processing theory Refine_Imperative_HOL.Sepref_Tool ...
Processing theory Refine_Imperative_HOL.Sepref_HOL_Bindings ...
Processing theory Refine_Imperative_HOL.Sepref_Foreach ...
Processing theory Refine_Imperative_HOL.Sepref_Improper ...
Processing theory Refine_Imperative_HOL.Sepref ...
Processing theory Refine_Imperative_HOL.IICF_Map ...
Processing theory Refine_Imperative_HOL.IICF_Multiset ...
Processing theory Refine_Imperative_HOL.IICF_List_MsetO ...
Processing theory Refine_Imperative_HOL.IICF_Prio_Bag ...
Processing theory Refine_Imperative_HOL.IICF_Set ...
Processing theory Refine_Imperative_HOL.IICF_List_SetO ...
Processing theory Refine_Imperative_HOL.IICF_List ...
Processing theory Refine_Imperative_HOL.IICF_Array ...
Processing theory Refine_Imperative_HOL.IICF_MS_Array_List ...
Processing theory Refine_Imperative_HOL.IICF_Array_List ...
Processing theory Refine_Imperative_HOL.IICF_List_Mset ...
Processing theory Refine_Imperative_HOL.IICF_Prio_Map ...
Processing theory Refine_Imperative_HOL.IICF_Matrix ...
Processing theory Refine_Imperative_HOL.IICF_HOL_List ...
Processing theory Refine_Imperative_HOL.IICF_Indexed_Array_List ...
Processing theory Refine_Imperative_HOL.IICF_Array_Matrix ...
Processing theory Refine_Imperative_HOL.IICF_Sepl_Binding ...
Processing theory PAC_Checker.PAC_More_Poly ...
Processing theory Refine_Imperative_HOL.IICF_Abs_Heap ...
Processing theory PAC_Checker.PAC_Specification ...
Processing theory Refine_Imperative_HOL.IICF_Impl_Heap ...
Processing theory PAC_Checker.PAC_Polynomials ...
Processing theory Refine_Imperative_HOL.IICF_Abs_Heapmap ...
Processing theory Refine_Imperative_HOL.IICF_Impl_Heapmap ...
Processing theory Refine_Imperative_HOL.IICF ...
Processing theory PAC_Checker.PAC_Map_Rel ...
Processing theory PAC_Checker.PAC_Polynomials_Term ...
Processing theory PAC_Checker.PAC_Checker_Specification ...
Processing theory PAC_Checker.WB_Sort ...
Processing theory PAC_Checker.PAC_Polynomials_Operations ...
Processing theory PAC_Checker.PAC_Checker ...
Processing theory PAC_Checker.PAC_Checker_Relation ...
Processing theory PAC_Checker.PAC_Checker_Init ...
Processing theory PAC_Checker.PAC_Checker_Synthesis ...
Loading 5 theories ...
Processing theory Architectural_Design_Patterns.Auxiliary ...
Processing theory DynamicArchitectures.Configuration_Traces ...
Processing theory DynamicArchitectures.Dynamic_Architecture_Calculus ...
Removing 18 theories ...
Processing theory Architectural_Design_Patterns.RF_LTL ...
Processing theory Architectural_Design_Patterns.Blockchain ...
Loading 20 theories ...
Processing theory List-Infinite.Util_MinMax ...
Processing theory List-Infinite.Util_Nat ...
Processing theory List-Infinite.Util_Set ...
Processing theory List-Infinite.Util_NatInf ...
Processing theory List-Infinite.Util_Div ...
Removing 3 theories ...
Processing theory List-Infinite.SetInterval2 ...
Processing theory List-Infinite.InfiniteSet2 ...
Processing theory List-Infinite.SetIntervalCut ...
Processing theory List-Infinite.SetIntervalStep ...
Processing theory List-Infinite.List2 ...
Processing theory List-Infinite.ListInf ...
Processing theory AutoFocus-Stream.ListSlice ...
Processing theory List-Infinite.ListInf_Prefix ...
Processing theory Nat-Interval-Logic.IL_Interval ...
Processing theory AutoFocus-Stream.AF_Stream ...
Processing theory AutoFocus-Stream.AF_Stream_Exec ...
Processing theory Nat-Interval-Logic.IL_IntervalOperators ...
Processing theory Nat-Interval-Logic.IL_TemporalOperators ...
Processing theory AutoFocus-Stream.IL_AF_Stream ...
Processing theory AutoFocus-Stream.IL_AF_Stream_Exec ...
Loading 3 theories ...
Processing theory Architectural_Design_Patterns.Singleton ...
Processing theory Architectural_Design_Patterns.Publisher_Subscriber ...
Removing 8 theories ...
Processing theory Architectural_Design_Patterns.Blackboard ...
Loading 12 theories ...
Removing 5 theories ...
Processing theory Isabelle_Marries_Dirac.Measurement ...
Processing theory Isabelle_Marries_Dirac.Deutsch ...
Processing theory Isabelle_Marries_Dirac.Deutsch_Jozsa ...
Loading 170 theories ...
Processing theory CAVA_Base.Statistics ...
Processing theory CAVA_Base.Lexord_List ...
Processing theory CAVA_Automata.Step_Conv ...
Processing theory Collections.Record_Intf ...
Processing theory Transition_Systems_and_Automata.Basic ...
Processing theory SM.SOS_Misc_Add ...
Processing theory Partial_Order_Reduction.Basic_Extensions ...
Processing theory Partial_Order_Reduction.Set_Extensions ...
Processing theory Partial_Order_Reduction.Functions ...
Processing theory Partial_Order_Reduction.Relation_Extensions ...
Removing 2 theories ...
Processing theory Collections.Dlist_add ...
Processing theory Collections.Trie_Impl ...
Processing theory Collections.Trie2 ...
Processing theory DFS_Framework.DFS_Framework_Misc ...
Processing theory Collections.Sorted_List_Operations ...
Processing theory SM.SM_Syntax ...
Processing theory SM.SM_State ...
Processing theory Collections.Gen_Comp ...
Processing theory Partial_Order_Reduction.List_Extensions ...
Processing theory Partial_Order_Reduction.List_Prefixes ...
Processing theory Collections.ICF_Spec_Base ...
Processing theory Transition_Systems_and_Automata.Sequence ...
Processing theory Collections.DatRef ...
Processing theory Collections.ListSpec ...
Processing theory Collections.AnnotatedListSpec ...
Processing theory Partial_Order_Reduction.Word_Prefixes ...
Processing theory Transition_Systems_and_Automata.Transition_System ...
Processing theory Collections.ListGA ...
Processing theory Collections.Fifo ...
Processing theory Collections.PrioSpec ...
Processing theory Collections.MapSpec ...
Processing theory Collections.BinoPrioImpl ...
Processing theory CAVA_Automata.Digraph_Basic ...
Processing theory Partial_Order_Reduction.Traces ...
Processing theory Finger-Trees.FingerTree ...
Processing theory DFS_Framework.DFS_Framework_Refine_Aux ...
Processing theory Partial_Order_Reduction.ENat_Extensions ...
Processing theory Collections.SkewPrioImpl ...
Processing theory Collections.FTAnnotatedListImpl ...
Processing theory Collections.PrioUniqueSpec ...
Processing theory Collections.PrioByAnnotatedList ...
Processing theory Collections.GenCF ...
Processing theory Collections.FTPrioImpl ...
Processing theory Transition_Systems_and_Automata.Sequence_LTL ...
Processing theory Partial_Order_Reduction.CCPO_Extensions ...
Processing theory Collections.SetSpec ...
Processing theory Collections.SetIteratorCollectionsGA ...
Processing theory Collections.Refine_Dflt ...
Processing theory CAVA_Base.Code_String ...
Processing theory CAVA_Base.CAVA_Code_Target ...
Processing theory Collections.Algos ...
Processing theory Transition_Systems_and_Automata.Transition_System_Construction ...
Processing theory Transition_Systems_and_Automata.Transition_System_Extra ...
Processing theory Collections.SetIndex ...
Processing theory Partial_Order_Reduction.ESet_Extensions ...
Processing theory Partial_Order_Reduction.Transition_System_Extensions ...
Processing theory Partial_Order_Reduction.Transition_System_Traces ...
Processing theory Collections.PrioUniqueByAnnotatedList ...
Processing theory Collections.FTPrioUniqueImpl ...
Processing theory Collections.MapGA ...
Processing theory Collections.SetGA ...
Processing theory LTL.LTL ...
Processing theory Promela.PromelaAST ...
Processing theory Stuttering_Equivalence.PLTL ...
Processing theory Collections.ListMapImpl ...
Processing theory Collections.TrieMapImpl ...
Processing theory Collections.ListSetImpl ...
Processing theory Collections.ListSetImpl_Invar ...
Processing theory Collections.ArrayMapImpl ...
Processing theory Collections.ListMapImpl_Invar ...
Processing theory Collections.SetByMap ...
Processing theory Collections.ListSetImpl_NotDist ...
Processing theory Partial_Order_Reduction.Coinductive_List_Extensions ...
Processing theory Partial_Order_Reduction.LList_Prefixes ...
Processing theory Collections.TrieSetImpl ...
Processing theory Collections.ArraySetImpl ...
Processing theory Collections.ArrayHashMap_Impl ...
Processing theory Collections.RBTMapImpl ...
Processing theory Collections.ListSetImpl_Sorted ...
Processing theory Partial_Order_Reduction.Stuttering ...
Processing theory Collections.HashMap_Impl ...
Processing theory Partial_Order_Reduction.Transition_System_Interpreted_Traces ...
Processing theory Collections.ArrayHashMap ...
Processing theory Collections.HashMap ...
Processing theory Collections.MapStdImpl ...
Processing theory Collections.ArrayHashSet ...
Processing theory Collections.RBTSetImpl ...
Processing theory Collections.HashSet ...
Processing theory Collections.SetStdImpl ...
Processing theory Partial_Order_Reduction.Ample_Abstract ...
Processing theory Partial_Order_Reduction.Ample_Analysis ...
Processing theory Collections.ICF_Impl ...
Processing theory Collections.ICF_Refine_Monadic ...
Processing theory Collections.ICF_Autoref ...
Processing theory Collections.Collections ...
Processing theory Collections.CollectionsV1 ...
Processing theory CAVA_Base.CAVA_Base ...
Processing theory CAVA_LTL_Modelchecker.NDFS_SI_Statistics ...
Processing theory Promela.PromelaStatistics ...
Processing theory DFS_Framework.Impl_Rev_Array_Stack ...
Processing theory CAVA_Automata.Digraph ...
Processing theory SM.LTS ...
Processing theory Gabow_SCC.Find_Path ...
Processing theory LTL.Rewriting ...
Processing theory SM.SM_Cfg ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_Extras ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_LeaderFilters ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_Philosophers ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_Simple ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_ReaderWriter ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_Programs ...
Processing theory CAVA_LTL_Modelchecker.BoolProgs_LTL_Conv ...
Processing theory CAVA_Automata.Automata ...
Processing theory CAVA_Automata.Lasso ...
Processing theory CAVA_Automata.Simulation ...
Processing theory CAVA_LTL_Modelchecker.CAVA_Abstract ...
Processing theory CAVA_Automata.Digraph_Impl ...
Processing theory CAVA_Automata.Stuttering_Extension ...
Processing theory Gabow_SCC.Find_Path_Impl ...
Processing theory DFS_Framework.Param_DFS ...
Processing theory SM.Gen_Scheduler ...
Processing theory Gabow_SCC.Gabow_Skeleton ...
Processing theory SM.SM_Semantics ...
Processing theory DFS_Framework.General_DFS_Structure ...
Processing theory SM.Gen_Scheduler_Refine ...
Processing theory SM.Gen_Cfg_Bisim ...
Processing theory SM.SM_LTL ...
Processing theory SM.Decide_Locality ...
Processing theory DFS_Framework.Tailrec_Impl ...
Processing theory SM.Type_System ...
Processing theory SM.SM_Finite_Reachable ...
Processing theory CAVA_Automata.Automata_Impl ...
Processing theory Gabow_SCC.Gabow_Skeleton_Code ...
Processing theory SM.Rename_Cfg ...
Processing theory SM.SM_Visible ...
Processing theory SM.Pid_Scheduler ...
Processing theory SM.SM_Pid ...
Processing theory DFS_Framework.DFS_Invars_Basic ...
Processing theory Promela.PromelaDatastructures ...
Processing theory Promela.PromelaInvariants ...
Processing theory SM.SM_Variables ...
Processing theory DFS_Framework.Rec_Impl ...
Processing theory SM.SM_Indep ...
Processing theory Gabow_SCC.Gabow_GBG ...
Processing theory DFS_Framework.Simple_Impl ...
Processing theory DFS_Framework.Restr_Impl ...
Processing theory DFS_Framework.DFS_Framework ...
Processing theory DFS_Framework.Reachable_Nodes ...
Processing theory Gabow_SCC.Gabow_GBG_Code ...
Processing theory CAVA_LTL_Modelchecker.NDFS_SI ...
Processing theory Promela.Promela ...
Processing theory Promela.PromelaLTL ...
Processing theory Promela.PromelaLTLConv ...
Processing theory DFS_Framework.Feedback_Arcs ...
Processing theory SM.SM_Datastructures ...
Processing theory SM.SM_Sticky ...
Processing theory SM.SM_POR ...
Processing theory SM.SM_Ample_Impl ...
Processing theory SM.SM_Wrapup ...
Processing theory LTL_to_GBA.LTL_to_GBA ...
Processing theory LTL_to_GBA.LTL_to_GBA_impl ...
Processing theory CAVA_LTL_Modelchecker.CAVA_Impl ...
Processing theory CAVA_LTL_Modelchecker.Mulog ...
Loading 2 theories ...
Processing theory CAVA_LTL_Modelchecker.All_Of_Nested_DFS ...
Processing theory CAVA_LTL_Modelchecker.All_Of_CAVA_LTL_Modelchecker ...
Loading 3 theories ...
Removing 40 theories ...
Processing theory Polynomials.Poly_Mapping_Finite_Map ...
Processing theory Polynomials.MPoly_Type_Class_FMap ...
Processing theory Symmetric_Polynomials.Symmetric_Polynomials_Code ...
Processing theory Berlekamp_Zassenhaus.Hensel_Lifting_Type_Based ...
Removing 31 theories ...
Processing theory Isabelle_Marries_Dirac.Quantum_Teleportation ...
Removing 1 theories ...
Processing theory Isabelle_Marries_Dirac.Quantum_Prisoners_Dilemma ...
Removing 2 theories ...
Processing theory Isabelle_Marries_Dirac.Entanglement ...
Loading 12 theories ...
Processing theory Transition_Systems_and_Automata.Sequence_Zip ...
Processing theory Adaptive_State_Counting.FSM ...
Removing 2 theories ...
Processing theory Adaptive_State_Counting.ATC ...
Processing theory Adaptive_State_Counting.FSM_Product ...
Processing theory Adaptive_State_Counting.ASC_LB ...
Processing theory Adaptive_State_Counting.ASC_Suite ...
Processing theory Adaptive_State_Counting.ASC_Sufficiency ...
Processing theory Adaptive_State_Counting.ASC_Hoare ...
Processing theory Adaptive_State_Counting.ASC_Example ...
Removing 8 theories ...
Processing theory Dirichlet_Series.Dirichlet_Efficient_Code ...
Loading 18 theories ...
Processing theory Collections.Refine_Dflt_ICF ...
Processing theory Prpu_Maxflow.Graph_Topological_Ordering ...
Processing theory Flow_Networks.Fofu_Abs_Base ...
Processing theory Refine_Imperative_HOL.Sepref_ICF_Bindings ...
Processing theory Flow_Networks.Fofu_Impl_Base ...
Processing theory Flow_Networks.Refine_Add_Fofu ...
Processing theory Flow_Networks.Graph_Impl ...
Processing theory Flow_Networks.Network_Impl ...
Removing 40 theories ...
Processing theory Prpu_Maxflow.Generic_Push_Relabel ...
Processing theory Prpu_Maxflow.Prpu_Common_Inst ...
Processing theory Prpu_Maxflow.Fifo_Push_Relabel ...
Processing theory Prpu_Maxflow.Relabel_To_Front ...
Processing theory Flow_Networks.NetCheck ...
Processing theory Prpu_Maxflow.Prpu_Common_Impl ...
Processing theory Prpu_Maxflow.Relabel_To_Front_Impl ...
Processing theory Prpu_Maxflow.Fifo_Push_Relabel_Impl ...
Processing theory Prpu_Maxflow.Generated_Code_Test ...
Removing 10 theories ...
Processing theory Isabelle_Marries_Dirac.No_Cloning ...
Loading 7 theories ...
Processing theory Saturation_Framework.Calculus ...
Processing theory Saturation_Framework.Calculus_Variations ...
Processing theory Saturation_Framework.Intersection_Calculus ...
Processing theory Saturation_Framework.Lifting_to_Non_Ground_Calculi ...
Processing theory Saturation_Framework.Labeled_Lifting_to_Non_Ground_Calculi ...
Removing 25 theories ...
Processing theory Saturation_Framework.Given_Clause_Architectures ...
Loading 4 theories ...
Processing theory Saturation_Framework_Extensions.Given_Clause_Architectures_Revisited ...
Processing theory Saturation_Framework_Extensions.Soundness ...
Processing theory Saturation_Framework_Extensions.Standard_Redundancy_Criterion ...
Processing theory Saturation_Framework_Extensions.Clausal_Calculus ...
Removing 1 theories ...
Processing theory Saturation_Framework_Extensions.FO_Ordered_Resolution_Prover_Revisited ...
Loading 3 theories ...
Removing 22 theories ...
Processing theory Stateful_Protocol_Composition_and_Typing.Example_TLS ...
Processing theory Stateful_Protocol_Composition_and_Typing.Example_Keyserver ...
Loading 6 theories ...
Processing theory Stateful_Protocol_Composition_and_Typing.Examples ...
Processing theory EdmondsKarp_Maxflow.FordFulkerson_Algo ...
Processing theory EdmondsKarp_Maxflow.EdmondsKarp_Algo ...
Processing theory EdmondsKarp_Maxflow.Augmenting_Path_BFS ...
Removing 23 theories ...
Processing theory EdmondsKarp_Maxflow.EdmondsKarp_Impl ...
Processing theory EdmondsKarp_Maxflow.Edka_Checked_Impl ...
Processing theory EdmondsKarp_Maxflow.Edka_Benchmark_Export ...
Loading 2 theories ...
Processing theory ShortestPath.ShortestPath ...
Removing 19 theories ...
Processing theory ShortestPath.ShortestPathNeg ...
Loading 4 theories ...
Processing theory VerifyThis2019.Exc_Nres_Monad ...
Processing theory VerifyThis2019.VTcomp ...
Processing theory VerifyThis2019.Challenge2A ...
Processing theory VerifyThis2019.Challenge2B ...
Loading 2 theories ...
Processing theory Partial_Order_Reduction.Formula ...
Processing theory Partial_Order_Reduction.Ample_Correctness ...
Loading 2 theories ...
Removing 39 theories ...
Processing theory CakeML.TypeSystem ...
Loading 7 theories ...
Processing theory CakeML.TypeSystemAuxiliary ...
Processing theory VerifyThis2018.Synth_Definition ...
Processing theory VerifyThis2018.Dynamic_Array ...
Processing theory VerifyThis2018.DRAT_Misc ...
Processing theory VerifyThis2018.Array_Map_Default ...
Processing theory VerifyThis2018.Exc_Nres_Monad ...
Processing theory VerifyThis2018.VTcomp ...
Removing 2 theories ...
Processing theory VerifyThis2018.Snippets ...
Loading 2 theories ...
Processing theory VerifyThis2018.DF_System ...
Removing 1 theories ...
Processing theory VerifyThis2018.Challenge3 ...
Removing 2 theories ...
Processing theory VerifyThis2018.Challenge2 ...
Processing theory VerifyThis2018.Challenge1_short ...
Processing theory VerifyThis2018.Challenge1 ...
Removing 9 theories ...
Processing theory CakeML.Code_Test_Haskell ...
Loading 23 theories ...
Processing theory Dijkstra_Shortest_Path.Dijkstra_Misc ...
Processing theory Refine_Imperative_HOL.Sepref_Snip_Combinator ...
Processing theory Refine_Imperative_HOL.Sepref_Graph ...
Processing theory Collections_Examples.Succ_Graph ...
Processing theory Refine_Imperative_HOL.Worklist_Subsumption ...
Processing theory Refine_Imperative_HOL.Worklist_Subsumption_Impl ...
Processing theory Refine_Imperative_HOL.Sepref_DFS ...
Processing theory Refine_Imperative_HOL.Sepref_WGraph ...
Processing theory Dijkstra_Shortest_Path.Weight ...
Processing theory Refine_Imperative_HOL.Sepref_Snip_Datatype ...
Processing theory Dijkstra_Shortest_Path.GraphSpec ...
Processing theory Dijkstra_Shortest_Path.GraphGA ...
Removing 11 theories ...
Processing theory Dijkstra_Shortest_Path.Dijkstra ...
Processing theory Dijkstra_Shortest_Path.GraphByMap ...
Processing theory Dijkstra_Shortest_Path.HashGraphImpl ...
Processing theory Refine_Imperative_HOL.Sepref_Minitests ...
Processing theory Collections_Examples.Nested_DFS ...
Processing theory Dijkstra_Shortest_Path.Dijkstra_Impl_Adet ...
Processing theory Dijkstra_Shortest_Path.Test ...
Processing theory Refine_Imperative_HOL.Sepref_NDFS ...
Processing theory Refine_Imperative_HOL.Sepref_Dijkstra ...
Processing theory Refine_Imperative_HOL.Sepref_All_Examples ...
Loading 45 theories ...
Removing 7 theories ...
Processing theory Formal_SSA.While_Combinator_Exts ...
Processing theory Slicing.AuxLemmas ...
Processing theory Formal_SSA.Serial_Rel ...
Processing theory Slicing.BasicDefs ...
Processing theory Slicing.CFG ...
Processing theory Slicing.CFG_wf ...
Processing theory Slicing.SemanticsCFG ...
Processing theory Slicing.CFGExit ...
Processing theory Slicing.DynDataDependence ...
Processing theory Slicing.DataDependence ...
Processing theory Slicing.Distance ...
Processing theory Slicing.CFGExit_wf ...
Processing theory Slicing.Observable ...
Processing theory Slicing.WeakOrderDependence ...
Processing theory Formal_SSA.FormalSSA_Misc ...
Processing theory Formal_SSA.Mapping_Exts ...
Processing theory Slicing.Postdomination ...
Processing theory Slicing.DynStandardControlDependence ...
Processing theory Slicing.DynWeakControlDependence ...
Processing theory Slicing.StandardControlDependence ...
Processing theory Slicing.WeakControlDependence ...
Processing theory Slicing.PDG ...
Processing theory Formal_SSA.RBT_Mapping_Exts ...
Processing theory Slicing.Com ...
Processing theory Slicing.Labels ...
Processing theory Slicing.WCFG ...
Processing theory Slicing.Interpretation ...
Processing theory Slicing.Slice ...
Processing theory Slicing.CDepInstantiations ...
Processing theory Slicing.WellFormed ...
Processing theory Slicing.AdditionalLemmas ...
Processing theory Formal_SSA.Disjoin_Transform ...
Processing theory Formal_SSA.Graph_path ...
Processing theory Formal_SSA.SSA_CFG ...
Processing theory Formal_SSA.Minimality ...
Processing theory Formal_SSA.SSA_CFG_code ...
Processing theory Formal_SSA.Construct_SSA ...
Processing theory Formal_SSA.Construct_SSA_notriv ...
Processing theory Formal_SSA.Construct_SSA_code ...
Processing theory Formal_SSA.SSA_Transfer_Rules ...
Processing theory Formal_SSA.Construct_SSA_notriv_code ...
Processing theory Formal_SSA.Generic_Interpretation ...
Processing theory Formal_SSA.WhileGraphSSA ...
Processing theory Formal_SSA.Generic_Extract ...
Processing theory Refine_Imperative_HOL.Dijkstra_Benchmark ...
Loading 11 theories ...
Removing 18 theories ...
Processing theory Parity_Game.MoreCoinductiveList ...
Processing theory Parity_Game.ParityGame ...
Processing theory Parity_Game.Strategy ...
Processing theory Parity_Game.AttractingStrategy ...
Processing theory Parity_Game.Attractor ...
Processing theory Parity_Game.WellOrderedStrategy ...
Processing theory Parity_Game.WinningStrategy ...
Processing theory Parity_Game.WinningRegion ...
Processing theory Parity_Game.UniformStrategy ...
Loading 2 theories ...
Processing theory Parity_Game.AttractorStrategy ...
Processing theory Parity_Game.PositionalDeterminacy ...
Removing 6 theories ...
Processing theory Refine_Imperative_HOL.NDFS_Benchmark ...
Loading 13 theories ...
Processing theory Matroids.Indep_System ...
Processing theory Kruskal.Kruskal_Misc ...
Processing theory Kruskal.SeprefUF ...
Processing theory Matroids.Matroid ...
Processing theory Kruskal.UGraph ...
Processing theory Kruskal.MinWeightBasis ...
Processing theory Kruskal.Kruskal ...
Processing theory Kruskal.Kruskal_Refine ...
Removing 3 theories ...
Processing theory Kruskal.Kruskal_Impl ...
Processing theory Kruskal.UGraph_Impl ...
Loading 3 theories ...
Processing theory Kruskal.Graph_Definition ...
Processing theory Kruskal.Graph_Definition_Aux ...
Removing 2 theories ...
Processing theory Kruskal.Graph_Definition_Impl ...
Processing theory PAC_Checker.PAC_Assoc_Map_Rel ...
Processing theory Parity_Game.AttractorInductive ...
Removing 19 theories ...
Processing theory CakeML.BigSmallInvariants ...
Processing theory Refine_Imperative_HOL.Heapmap_Bench ...
Loading 4 theories ...
Processing theory Special_Function_Bounds.Bounds_Lemmas ...
Removing 5 theories ...
Processing theory Special_Function_Bounds.Exp_Bounds ...
Processing theory Sturm_Sequences.Sturm_Ex ...
Processing theory Parity_Game.Graph_TheoryCompatibility ...
Loading 3 theories ...
Removing 22 theories ...
Processing theory Floyd_Warshall.Recursion_Combinators ...
Processing theory Floyd_Warshall.Floyd_Warshall ...
Processing theory Floyd_Warshall.FW_Code ...
Loading 2 theories ...
Processing theory VerifyThis2019.Parallel_Multiset_Fold ...
Processing theory VerifyThis2019.Challenge3 ...
Processing theory Refine_Imperative_HOL.Sepref_Guide_Reference ...
Removing 6 theories ...
Processing theory Refine_Imperative_HOL.Sepref_Guide_Quickstart ...
Removing 1 theories ...
Processing theory Refine_Imperative_HOL.Sepref_Guide_General_Util ...
Removing 1 theories ...
Processing theory Knuth_Morris_Pratt.KMP ...
Loading 2 theories ...
Processing theory Complex_Geometry.Riemann_Sphere ...
Processing theory Complex_Geometry.Chordal_Metric ...
Loading 54 theories ...
Removing 44 theories ...
Processing theory UTP-Toolkit.List_Lexord_Alt ...
Processing theory UTP-Toolkit.Total_Recall ...
Processing theory UTP.utp_parser_utils ...
Processing theory UTP-Toolkit.Infinity ...
Processing theory UTP-Toolkit.Positive ...
Processing theory UTP-Toolkit.FSet_Extra ...
Processing theory UTP-Toolkit.Map_Extra ...
Processing theory UTP-Toolkit.Partial_Fun ...
Processing theory UTP-Toolkit.Finite_Fun ...
Processing theory UTP-Toolkit.List_Extra ...
Processing theory UTP-Toolkit.Sequence ...
Processing theory UTP-Toolkit.Countable_Set_Extra ...
Processing theory UTP-Toolkit.utp_toolkit ...
Processing theory UTP.utp_var ...
Processing theory UTP.utp_expr ...
Processing theory UTP.utp_expr_insts ...
Processing theory UTP.utp_expr_funcs ...
Processing theory UTP.utp_unrest ...
Processing theory UTP.utp_usedby ...
Processing theory UTP.utp_tactics ...
Processing theory UTP.utp_subst ...
Processing theory UTP.utp_meta_subst ...
Processing theory UTP.utp_pred ...
Processing theory UTP.utp_alphabet ...
Processing theory UTP.utp_lift ...
Processing theory UTP.utp_pred_laws ...
Processing theory UTP.utp_healthy ...
Processing theory UTP.utp_sequent ...
Processing theory UTP.utp_rel ...
Processing theory UTP.utp_state_parser ...
Processing theory UTP.utp_recursion ...
Processing theory UTP.utp_rel_laws ...
Processing theory UTP.utp_theory ...
Processing theory UTP.utp_hoare ...
Processing theory UTP.utp_rel_opsem ...
Processing theory UTP.utp_sym_eval ...
Processing theory UTP.utp_wp ...
Processing theory UTP.utp_dynlog ...
Processing theory UTP.utp_sp ...
Processing theory UTP.utp_concurrency ...
Processing theory UTP.utp ...
Processing theory UTP.utp_expr_ovld ...
Processing theory UTP.utp_full ...
Processing theory UTP.utp_easy_parser ...
Processing theory UTP.sum_list ...
Removing 4 theories ...
Processing theory CakeML.CakeML_Quickcheck ...
Processing theory UTP.utp_simple_time ...
Loading 10 theories ...
Removing 56 theories ...
Processing theory BTree.Basic_Assn ...
Processing theory BTree.Imperative_Loops ...
Processing theory BTree.BTree ...
Processing theory BTree.Array_SBlit ...
Processing theory BTree.Partially_Filled_Array ...
Processing theory BTree.BTree_Imp ...
Processing theory BTree.BTree_Set ...
Processing theory BTree.BTree_Split ...
Processing theory BTree.BTree_ImpSet ...
Processing theory BTree.BTree_ImpSplit ...
Loading 9 theories ...
Processing theory Coinductive.Quotient_Coinductive_List ...
Processing theory Coinductive.Quotient_TLList ...
Processing theory Coinductive.Coinductive ...
Processing theory LTL_to_GBA.All_Of_LTL_to_GBA ...
Loading 10 theories ...
Processing theory GaleStewart_Games.MoreCoinductiveList2 ...
Processing theory GaleStewart_Games.MoreENat ...
Processing theory GaleStewart_Games.AlternatingLists ...
Processing theory GaleStewart_Games.MorePrefix ...
Processing theory GaleStewart_Games.GaleStewartGames ...
Processing theory Lazy-Lists-II.LList2 ...
Removing 46 theories ...
Processing theory GaleStewart_Games.GaleStewartDefensiveStrategies ...
Processing theory GaleStewart_Games.GaleStewartDeterminedGames ...
Processing theory Topology.Topology ...
Loading 28 theories ...
Processing theory Topology.LList_Topology ...
Processing theory Buchi_Complementation.Alternate ...
Processing theory Transition_Systems_and_Automata.Acceptance ...
Processing theory Transition_Systems_and_Automata.Maps ...
Processing theory Transition_Systems_and_Automata.Refine ...
Processing theory Buchi_Complementation.Formula ...
Processing theory Transition_Systems_and_Automata.Degeneralization ...
Processing theory Transition_Systems_and_Automata.Degeneralization_Refine ...
Processing theory Transition_Systems_and_Automata.Implement ...
Removing 11 theories ...
Processing theory Transition_Systems_and_Automata.Transition_System_Refine ...
Processing theory Transition_Systems_and_Automata.Nondeterministic ...
Processing theory Transition_Systems_and_Automata.NBA ...
Processing theory Transition_Systems_and_Automata.NGBA ...
Processing theory Transition_Systems_and_Automata.NBA_Graphs ...
Processing theory Transition_Systems_and_Automata.NBA_Refine ...
Processing theory Transition_Systems_and_Automata.NGBA_Refine ...
Processing theory Transition_Systems_and_Automata.NGBA_Graphs ...
Processing theory Transition_Systems_and_Automata.NBA_Combine ...
Processing theory Buchi_Complementation.Graph ...
Processing theory Buchi_Complementation.Ranking ...
Processing theory Transition_Systems_and_Automata.NBA_Implement ...
Processing theory Transition_Systems_and_Automata.NGBA_Implement ...
Processing theory Buchi_Complementation.Complementation ...
Processing theory Transition_Systems_and_Automata.NBA_Algorithms ...
Processing theory Transition_Systems_and_Automata.NBA_Explicit ...
Processing theory Transition_Systems_and_Automata.NBA_Translate ...
Processing theory Transition_Systems_and_Automata.NGBA_Algorithms ...
Processing theory Buchi_Complementation.Complementation_Implement ...
Processing theory Buchi_Complementation.Complementation_Final ...
Loading 6 theories ...
Removing 21 theories ...
Processing theory Chandy_Lamport.Util ...
Processing theory Chandy_Lamport.Distributed_System ...
Processing theory Chandy_Lamport.Trace ...
Processing theory Chandy_Lamport.Swap ...
Processing theory Chandy_Lamport.Snapshot ...
Processing theory Chandy_Lamport.Co_Snapshot ...
Loading 6 theories ...
Processing theory Stream_Fusion_Code.Stream_Fusion ...
Processing theory Coinductive.Lazy_LList ...
Processing theory Coinductive.Lazy_TLList ...
Processing theory Stream_Fusion_Code.Stream_Fusion_List ...
Removing 6 theories ...
Processing theory Stream_Fusion_Code.Stream_Fusion_LList ...
Loading 7 theories ...
Processing theory Stream_Fusion_Code.Stream_Fusion_Examples ...
Processing theory DFS_Framework.DFS_Invars_SCC ...
Processing theory DFS_Framework.Tarjan_LowLink ...
Removing 4 theories ...
Processing theory DFS_Framework.Tarjan ...
Processing theory DFS_Framework.DFS_Find_Path ...
Processing theory DFS_Framework.Cyc_Check ...
Processing theory DFS_Framework.Nested_DFS ...
Loading 12 theories ...
Processing theory DFS_Framework.DFS_All_Examples ...
Processing theory Knot_Theory.Tangle_Relation ...
Processing theory Knot_Theory.Preliminaries ...
Processing theory Knot_Theory.Tangles ...
Processing theory Knot_Theory.Tangle_Algebra ...
Processing theory Knot_Theory.Tangle_Moves ...
Processing theory Knot_Theory.Link_Algebra ...
Removing 8 theories ...
Processing theory Knot_Theory.Example ...
Processing theory Knot_Theory.Kauffman_Matrix ...
Processing theory Knot_Theory.Computations ...
Processing theory Knot_Theory.Linkrel_Kauffman ...
Processing theory Knot_Theory.Kauffman_Invariance ...
Processing theory Knot_Theory.Knot_Theory ...
Removing 15 theories ...
Processing theory CakeML.SimpleIO ...
Processing theory Promela.All_Of_Promela ...
Loading 33 theories ...
Processing theory LTL_Master_Theorem.Quotient_Type ...
Processing theory LTL_Master_Theorem.Omega_Words_Fun_Stream ...
Processing theory Transition_Systems_and_Automata.Acceptance_Refine ...
Removing 11 theories ...
Processing theory LTL.Equivalence_Relations ...
Processing theory Boolean_Expression_Checkers.Boolean_Expression_Checkers ...
Processing theory Boolean_Expression_Checkers.Boolean_Expression_Checkers_AList_Mapping ...
Processing theory LTL.Code_Equations ...
Processing theory LTL_Master_Theorem.Syntactic_Fragments_and_Stability ...
Processing theory Transition_Systems_and_Automata.Deterministic ...
Processing theory Transition_Systems_and_Automata.DBA ...
Processing theory Transition_Systems_and_Automata.DGBA ...
Processing theory Transition_Systems_and_Automata.DBA_Combine ...
Processing theory Transition_Systems_and_Automata.DCA ...
Processing theory Transition_Systems_and_Automata.DGCA ...
Processing theory Transition_Systems_and_Automata.DCA_Combine ...
Processing theory Transition_Systems_and_Automata.DRA ...
Processing theory Transition_Systems_and_Automata.DRA_Combine ...
Processing theory Transition_Systems_and_Automata.DRA_Refine ...
Processing theory LTL_Master_Theorem.After ...
Processing theory LTL.Disjunctive_Normal_Form ...
Processing theory Transition_Systems_and_Automata.DRA_Implement ...
Processing theory Transition_Systems_and_Automata.DRA_Nodes ...
Processing theory Transition_Systems_and_Automata.DRA_Explicit ...
Processing theory Transition_Systems_and_Automata.DRA_Translate ...
Processing theory LTL_Master_Theorem.Advice ...
Processing theory LTL_Master_Theorem.Transition_Functions ...
Processing theory LTL_Master_Theorem.Master_Theorem ...
Processing theory LTL_Master_Theorem.Extra_Equivalence_Relations ...
Processing theory LTL_Master_Theorem.Restricted_Master_Theorem ...
Processing theory LTL_Master_Theorem.DRA_Construction ...
Processing theory LTL_Master_Theorem.DRA_Implementation ...
Processing theory LTL_Master_Theorem.DRA_Instantiation ...
Processing theory LTL_Master_Theorem.Code_Export ...
Loading 3 theories ...
Removing 39 theories ...
Processing theory Gabow_SCC.Gabow_SCC ...
Processing theory Gabow_SCC.Gabow_SCC_Code ...
Processing theory Gabow_SCC.All_Of_Gabow_SCC ...
Removing 9 theories ...
Processing theory CakeML.LibAuxiliary ...
Loading 19 theories ...
Processing theory HRB-Slicing.AuxLemmas ...
Processing theory HRB-Slicing.BasicDefs ...
Processing theory HRB-Slicing.CFG ...
Processing theory HRB-Slicing.CFGExit ...
Processing theory HRB-Slicing.CFG_wf ...
Processing theory HRB-Slicing.Distance ...
Processing theory HRB-Slicing.ReturnAndCallNodes ...
Processing theory HRB-Slicing.SemanticsCFG ...
Removing 5 theories ...
Processing theory HRB-Slicing.CFGExit_wf ...
Processing theory HRB-Slicing.Observable ...
Processing theory HRB-Slicing.Postdomination ...
Processing theory HRB-Slicing.SDG ...
Processing theory HRB-Slicing.HRBSlice ...
Processing theory HRB-Slicing.SCDObservable ...
Processing theory HRB-Slicing.Slice ...
Processing theory HRB-Slicing.WeakSimulation ...
Processing theory HRB-Slicing.FundamentalProperty ...
Processing theory InformationFlowSlicing_Inter.NonInterferenceInter ...
Processing theory InformationFlowSlicing_Inter.LiftingInter ...
Loading 6 theories ...
Removing 2 theories ...
Processing theory Tree-Automata.Tree ...
Processing theory Collections_Examples.Exploration ...
Processing theory Tree-Automata.Ta ...
Processing theory Tree-Automata.AbsAlgo ...
Processing theory Tree-Automata.Ta_impl ...
Processing theory Tree-Automata.Ta_impl_codegen ...
Processing theory List-Infinite.ListInfinite ...
Removing 18 theories ...
Processing theory Minimal_SSA.Irreducible ...
Loading 18 theories ...
Processing theory Nested_Multisets_Ordinals.Nested_Multiset ...
Processing theory Nested_Multisets_Ordinals.Hereditary_Multiset ...
Processing theory Nested_Multisets_Ordinals.Syntactic_Ordinal ...
Processing theory Nested_Multisets_Ordinals.Signed_Multiset ...
Processing theory Nested_Multisets_Ordinals.Signed_Hereditary_Multiset ...
Processing theory Nested_Multisets_Ordinals.Signed_Syntactic_Ordinal ...
Removing 3 theories ...
Processing theory Polynomials.Polynomials ...
Processing theory Lambda_Free_KBOs.Lambda_Free_KBO_Util ...
Processing theory Lambda_Free_KBOs.Lambda_Free_KBO_App ...
Processing theory Lambda_Free_KBOs.Lambda_Free_KBO_Std ...
Processing theory Lambda_Free_KBOs.Lambda_Free_KBO_Basic ...
Processing theory Lambda_Free_KBOs.Lambda_Encoding_KBO ...
Processing theory Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs ...
Processing theory Lambda_Free_KBOs.Lambda_Free_KBOs ...
Processing theory Formal_SSA.SSA_Semantics ...
Loading 6 theories ...
Removing 19 theories ...
Processing theory Progress_Tracking.Auxiliary ...
Processing theory Progress_Tracking.Antichain ...
Processing theory Progress_Tracking.Graph ...
Processing theory Progress_Tracking.Propagate ...
Processing theory Progress_Tracking.Exchange ...
Processing theory Progress_Tracking.Combined ...
Loading 55 theories ...
Removing 5 theories ...
Processing theory Jinja.Auxiliary ...
Processing theory Jinja.Type ...
Processing theory Jinja.Decl ...
Processing theory Jinja.TypeRel ...
Processing theory Jinja.Value ...
Processing theory HRB-Slicing.Com ...
Processing theory HRB-Slicing.Labels ...
Processing theory HRB-Slicing.ProcState ...
Processing theory Jinja.Objects ...
Processing theory Jinja.Exceptions ...
Processing theory Jinja.SystemClasses ...
Processing theory Jinja.JVMState ...
Processing theory Jinja.Conform ...
Processing theory Jinja.WellForm ...
Processing theory Jinja.JVMInstructions ...
Processing theory Jinja.JVMExceptions ...
Processing theory Jinja.JVMExecInstr ...
Processing theory Jinja.JVMExec ...
Processing theory Jinja.JVMListExample ...
Processing theory Jinja.SemiType ...
Processing theory Jinja.JVM_SemiType ...
Processing theory HRB-Slicing.PCFG ...
Processing theory HRB-Slicing.WellFormProgs ...
Processing theory Jinja.Effect ...
Processing theory Jinja.BVSpec ...
Processing theory Jinja.BVConform ...
Processing theory Jinja.EffectMono ...
Processing theory HRB-Slicing.Interpretation ...
Processing theory Jinja.TF_JVM ...
Processing theory Jinja.BVExec ...
Processing theory HRB-Slicing.WellFormed ...
Processing theory Jinja.BVSpecTypeSafe ...
Processing theory HRB-Slicing.ValidPaths ...
Processing theory HRB-Slicing.ProcSDG ...
Processing theory Jinja.BVExample ...
Processing theory HRB-Slicing.JVMCFG ...
Processing theory HRB-Slicing.JVMInterpretation ...
Processing theory HRB-Slicing.JVMPostdomination ...
Processing theory HRB-Slicing.JVMCFG_wf ...
Loading 7 theories ...
Processing theory HRB-Slicing.JVMSDG ...
Processing theory HRB-Slicing.HRBSlicing ...
Processing theory Core_DOM.Testing_Utils ...
Processing theory Core_DOM.Core_DOM_BaseTest ...
Processing theory Core_DOM.Document_adoptNode ...
Removing 32 theories ...
Processing theory Core_DOM.Node_insertBefore ...
Processing theory Core_DOM.Document_getElementById ...
Processing theory Core_DOM.Node_removeChild ...
Processing theory Core_DOM.Core_DOM_Tests ...
Processing theory CAVA_Automata.All_Of_CAVA_Automata ...
Loading 2 theories ...
Removing 41 theories ...
Processing theory IEEE_Floating_Point.Conversion_IEEE_Float ...
Processing theory IEEE_Floating_Point.Double ...
Loading 16 theories ...
Processing theory Word_Lib.Hex_Words ...
Processing theory Word_Lib.Legacy_Aliases ...
Processing theory Word_Lib.Word_16 ...
Processing theory Word_Lib.Strict_part_mono ...
Processing theory Word_Lib.Norm_Words ...
Processing theory Word_Lib.Next_and_Prev ...
Processing theory Word_Lib.More_Sublist ...
Processing theory Word_Lib.Many_More ...
Processing theory Word_Lib.Word_8 ...
Processing theory Word_Lib.Bitwise ...
Processing theory Word_Lib.Bitwise_Signed ...
Processing theory Word_Lib.Word_32 ...
Processing theory Word_Lib.Word_Lib_Sumo ...
Removing 7 theories ...
Processing theory Interval_Arithmetic_Word32.Finite_String ...
Processing theory Interval_Arithmetic_Word32.Interval_Word32 ...
Processing theory Interval_Arithmetic_Word32.Interpreter ...
Loading 6 theories ...
Removing 11 theories ...
Processing theory Jordan_Normal_Form.Derivation_Bound ...
Processing theory Jordan_Normal_Form.Show_Arctic ...
Processing theory Jordan_Normal_Form.Ring_Hom_Matrix ...
Processing theory Jordan_Normal_Form.Complexity_Carrier ...
Processing theory Jordan_Normal_Form.Matrix_Comparison ...
Processing theory Jordan_Normal_Form.Matrix_Complexity ...
Loading 4 theories ...
Processing theory MFOTL_Monitor.MFOTL ...
Removing 7 theories ...
Processing theory MFOTL_Monitor.Monitor ...
Processing theory MFOTL_Monitor.Monitor_Code ...
Processing theory MFOTL_Monitor.Examples ...
Loading 2 theories ...
Removing 3 theories ...
Processing theory Jordan_Normal_Form.Strassen_Algorithm ...
Loading 4 theories ...
Processing theory Jordan_Normal_Form.Strassen_Algorithm_Code ...
Processing theory Transition_Systems_and_Automata.NFA ...
Processing theory Transition_Systems_and_Automata.NBTA ...
Loading 3 theories ...
Processing theory Transition_Systems_and_Automata.NGBTA ...
Processing theory Transition_Systems_and_Automata.NBTA_Combine ...
Processing theory Containers.TwoSat_Ex ...
Removing 20 theories ...
Processing theory Containers.Containers_DFS_Ex ...
Processing theory Containers.Containers_TwoSat_Ex ...
Loading 7 theories ...
Removing 2 theories ...
Processing theory Core_SC_DOM.Testing_Utils ...
Processing theory Core_SC_DOM.Core_DOM_BaseTest ...
Processing theory Core_SC_DOM.Document_adoptNode ...
Processing theory Core_SC_DOM.Node_insertBefore ...
Processing theory Core_SC_DOM.Node_removeChild ...
Processing theory Core_SC_DOM.Document_getElementById ...
Loading 3 theories ...
Processing theory Core_SC_DOM.Core_DOM_Tests ...
Removing 32 theories ...
Processing theory Transition_Systems_and_Automata.DBTA ...
Processing theory Transition_Systems_and_Automata.DGBTA ...
Processing theory Transition_Systems_and_Automata.DBTA_Combine ...
Processing theory CakeML.NamespaceAuxiliary ...
Processing theory Transition_Systems_and_Automata.DFA ...
Loading 83 theories ...
Removing 16 theories ...
Processing theory IP_Addresses.Hs_Compat ...
Processing theory IP_Addresses.Lib_Numbers_toString ...
Processing theory Iptables_Semantics.List_Misc ...
Processing theory Iptables_Semantics.Remdups_Rev ...
Processing theory Iptables_Semantics.Repeat_Stabilize ...
Processing theory Iptables_Semantics.Datatype_Selectors ...
Processing theory Routing.Linorder_Helper ...
Processing theory Simple_Firewall.List_Product_More ...
Processing theory Simple_Firewall.Firewall_Common_Decision_State ...
Processing theory IP_Addresses.NumberWang_IPv4 ...
Processing theory Iptables_Semantics.Negation_Type ...
Processing theory IP_Addresses.NumberWang_IPv6 ...
Processing theory IP_Addresses.Lib_List_toString ...
Processing theory Simple_Firewall.GroupF ...
Processing theory Simple_Firewall.Lib_Enum_toString ...
Processing theory Iptables_Semantics.Word_Upto ...
Processing theory Iptables_Semantics.Ternary ...
Processing theory Iptables_Semantics.Conntrack_State ...
Processing theory Simple_Firewall.IP_Partition_Preliminaries ...
Processing theory Simple_Firewall.Iface ...
Processing theory Simple_Firewall.L4_Protocol ...
Processing theory Iptables_Semantics.L4_Protocol_Flags ...
Processing theory Simple_Firewall.Simple_Packet ...
Processing theory Iptables_Semantics.Tagged_Packet ...
Processing theory Simple_Firewall.SimpleFw_Syntax ...
Processing theory IP_Addresses.Lib_Word_toString ...
Processing theory IP_Addresses.WordInterval ...
Processing theory IP_Addresses.WordInterval_Sorted ...
Processing theory Iptables_Semantics.WordInterval_Lists ...
Processing theory Iptables_Semantics.Ports ...
Processing theory Iptables_Semantics.Firewall_Common ...
Processing theory IP_Addresses.IP_Address ...
Processing theory Iptables_Semantics.Matching_Ternary ...
Processing theory Iptables_Semantics.Unknown_Match_Tacs ...
Processing theory IP_Addresses.IPv4 ...
Processing theory IP_Addresses.Prefix_Match ...
Processing theory IP_Addresses.CIDR_Split ...
Processing theory Iptables_Semantics.Semantics_Ternary ...
Processing theory Iptables_Semantics.Fixed_Action ...
Processing theory Iptables_Semantics.Optimizing ...
Processing theory Iptables_Semantics.Semantics ...
Processing theory Iptables_Semantics.Matching ...
Processing theory Iptables_Semantics.Normalized_Matches ...
Processing theory Iptables_Semantics.Negation_Type_Matching ...
Processing theory Simple_Firewall.SimpleFw_Semantics ...
Processing theory Iptables_Semantics.Semantics_Goto ...
Processing theory Iptables_Semantics.Ruleset_Update ...
Processing theory Iptables_Semantics.Primitive_Normalization ...
Processing theory Iptables_Semantics.MatchExpr_Fold ...
Processing theory Iptables_Semantics.Call_Return_Unfolding ...
Processing theory IP_Addresses.IPv6 ...
Processing theory IP_Addresses.IP_Address_Parser ...
Processing theory IP_Addresses.IP_Address_toString ...
Processing theory IP_Addresses.Prefix_Match_toString ...
Processing theory Simple_Firewall.Primitives_toString ...
Processing theory Simple_Firewall.IP_Addr_WordInterval_toString ...
Processing theory Simple_Firewall.SimpleFw_toString ...
Processing theory Routing.Routing_Table ...
Processing theory Iptables_Semantics.IpAddresses ...
Processing theory Simple_Firewall.Service_Matrix ...
Processing theory Iptables_Semantics.Common_Primitive_Syntax ...
Processing theory Iptables_Semantics.Ipassmt ...
Processing theory Iptables_Semantics.Common_Primitive_Matcher_Generic ...
Processing theory Iptables_Semantics.Routing_IpAssmt ...
Processing theory Iptables_Semantics.Common_Primitive_Matcher ...
Processing theory Iptables_Semantics.Common_Primitive_Lemmas ...
Processing theory Iptables_Semantics.Conntrack_State_Transform ...
Processing theory Iptables_Semantics.Interfaces_Normalize ...
Processing theory Iptables_Semantics.IpAddresses_Normalize ...
Processing theory Iptables_Semantics.Common_Primitive_toString ...
Processing theory Iptables_Semantics.Output_Interface_Replace ...
Processing theory Iptables_Semantics.Protocols_Normalize ...
Processing theory Iptables_Semantics.Ports_Normalize ...
Processing theory Iptables_Semantics.No_Spoof ...
Processing theory Iptables_Semantics.Interface_Replace ...
Processing theory Iptables_Semantics.Transform ...
Processing theory Iptables_Semantics.Primitive_Abstract ...
Processing theory Iptables_Semantics.SimpleFw_Compliance ...
Processing theory Iptables_Semantics.Code_Interface ...
Processing theory Iptables_Semantics_Examples.iptables_Ln_tuned_parsed ...
Processing theory Iptables_Semantics.Parser ...
Processing theory Iptables_Semantics.Parser6 ...
Processing theory Iptables_Semantics_Examples.Analyze_Synology_Diskstation ...
Processing theory Iptables_Semantics_Examples.Parser6_Test ...
Loading 13 theories ...
Removing 4 theories ...
Processing theory LOFT.OpenFlow_Helpers ...
Processing theory Simple_Firewall.Option_Helpers ...
Processing theory LOFT.Sort_Descending ...
Processing theory LOFT.List_Group ...
Processing theory Simple_Firewall.Generic_SimpleFw ...
Processing theory Routing.Linux_Router ...
Processing theory Routing.IpRoute_Parser ...
Processing theory LOFT.Semantics_OpenFlow ...
Processing theory LOFT.OpenFlow_Matches ...
Processing theory LOFT.OpenFlow_Action ...
Processing theory LOFT.OpenFlow_Serialize ...
Processing theory LOFT.LinuxRouter_OpenFlow_Translation ...
Processing theory LOFT.RFC2544 ...
Removing 1 theories ...
Processing theory LOFT.OF_conv_test ...
Removing 2 theories ...
Processing theory Iptables_Semantics_Examples.SNS_IAS_Eduroam_Spoofing ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.Analyze_medium_sized_company ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.SQRL_2015_nospoof ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.Analyze_SQRL_Shorewall ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.Analyze_Ringofsaturn_com ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.Parser_Test ...
Removing 1 theories ...
Processing theory Iptables_Semantics_Examples.Contrived_Example ...
Removing 1 theories ...
Processing theory Iptables_Semantics.Code_haskell ...
Removing 3 theories ...
Processing theory CakeML.Tokens ...
Loading 21 theories ...
Processing theory Priority_Search_Trees.Prio_Map_Specs ...
Processing theory Priority_Search_Trees.PST_General ...
Processing theory Prim_Dijkstra_Simple.Common ...
Processing theory Prim_Dijkstra_Simple.Undirected_Graph ...
Processing theory Prim_Dijkstra_Simple.Undirected_Graph_Specs ...
Processing theory Priority_Search_Trees.PST_RBT ...
Removing 34 theories ...
Processing theory Prim_Dijkstra_Simple.Prim_Abstract ...
Processing theory Prim_Dijkstra_Simple.Undirected_Graph_Impl ...
Processing theory Prim_Dijkstra_Simple.Prim_Impl ...
Loading 17 theories ...
Removing 14 theories ...
Processing theory Collections_Examples.Exploration_DFS ...
Processing theory Collections.Refine_Dflt_Only_ICF ...
Processing theory Collections_Examples.ICF_Only_Test ...
Processing theory Collections_Examples.Foreach_Refine ...
Processing theory Collections_Examples.Refine_Fold ...
Processing theory Refine_Monadic.Breadth_First_Search ...
Processing theory Collections_Examples.PerformanceTest ...
Processing theory Collections_Examples.itp_2010 ...
Processing theory Collections_Examples.ICF_Examples ...
Processing theory Collections_Examples.Simple_DFS ...
Processing theory Collections_Examples.Bfs_Impl ...
Processing theory Collections_Examples.Refine_Monadic_Examples ...
Processing theory Collections_Examples.Coll_Test ...
Processing theory Collections_Examples.Combined_TwoSat ...
Processing theory Collections_Examples.ICF_Test ...
Loading 5 theories ...
Processing theory Collections_Examples.Collection_Autoref_Examples ...
Processing theory Collections_Examples.Collection_Examples ...
Processing theory Iptables_Semantics.Matching_Embeddings ...
Processing theory Iptables_Semantics.Semantics_Embeddings ...
Processing theory Iptables_Semantics.Access_Matrix_Embeddings ...
Processing theory Iptables_Semantics.No_Spoof_Embeddings ...
Removing 21 theories ...
Processing theory Iptables_Semantics.Documentation ...
Loading 6 theories ...
Processing theory Containers.Card_Datatype ...
Processing theory Containers.List_Proper_Interval ...
Processing theory Containers.Map_To_Mapping_Ex ...
Processing theory Containers.Compatibility_Containers_Regular_Sets ...
Processing theory Containers-Benchmarks.Clauses ...
Removing 6 theories ...
Processing theory Containers.Containers_Userguide ...
Removing 7 theories ...
Processing theory Dijkstra_Shortest_Path.Dijkstra_Impl ...
Processing theory Iptables_Semantics.Iptables_Semantics ...
Loading 5 theories ...
Processing theory Containers-Benchmarks.Benchmark_Bool ...
Processing theory Containers-Benchmarks.Benchmark_Comparison ...
Processing theory Containers-Benchmarks.Benchmark_Set ...
Processing theory Containers-Benchmarks.Benchmark_LC ...
Processing theory Containers-Benchmarks.Benchmark_Set_LC ...
Removing 33 theories ...
Processing theory Iptables_Semantics_Examples.Small_Examples ...
Processing theory Iptables_Semantics_Examples.Ports_Fail ...
Removing 35 theories ...
Processing theory CAVA_Base.All_Of_CAVA_Base ...
Processing theory Containers-Benchmarks.Benchmark_ICF ...
Loading 21 theories ...
Processing theory LTL_to_DRA.Map2 ...
Processing theory LTL_to_DRA.Preliminaries2 ...
Processing theory LTL_to_DRA.Mapping2 ...
Processing theory LTL_to_DRA.List2 ...
Processing theory LTL_to_DRA.DTS ...
Removing 7 theories ...
Processing theory LTL_to_DRA.LTL_FGXU ...
Processing theory LTL_to_DRA.LTL_Compat ...
Processing theory LTL_to_DRA.Rabin ...
Processing theory LTL_to_DRA.af ...
Processing theory LTL_to_DRA.LTL_Impl ...
Processing theory LTL_to_DRA.Logical_Characterization ...
Processing theory LTL_to_DRA.Semi_Mojmir ...
Processing theory LTL_to_DRA.af_Impl ...
Processing theory LTL_to_DRA.Mojmir ...
Processing theory LTL_to_DRA.Mojmir_Rabin ...
Processing theory LTL_to_DRA.LTL_Rabin ...
Processing theory LTL_to_DRA.Mojmir_Rabin_Impl ...
Processing theory LTL_to_DRA.LTL_Rabin_Unfold_Opt ...
Processing theory LTL_to_DRA.LTL_Rabin_Impl ...
Processing theory LTL_to_DRA.Export_Code ...
Loading 7 theories ...
Processing theory LTL.Example ...
Processing theory LTL_Normal_Form.Normal_Form ...
Processing theory Abstract_Soundness.Finite_Proof_Soundness ...
Processing theory LTL_Normal_Form.Normal_Form_Code_Export ...
Processing theory Abstract_Completeness.Propositional_Logic ...
Processing theory Abstract_Soundness.Infinite_Proof_Soundness ...
Loading 14 theories ...
Removing 33 theories ...
Processing theory Extended_Finite_State_Machines.VName ...
Processing theory Extended_Finite_State_Machines.FSet_Utils ...
Processing theory Extended_Finite_State_Machines.Trilean ...
Processing theory Extended_Finite_State_Machines.Value ...
Processing theory FinFun.FinFun ...
Processing theory Extended_Finite_State_Machines.Value_Lexorder ...
Processing theory Progress_Tracking.Exchange_Abadi ...
Processing theory Extended_Finite_State_Machines.AExp ...
Removing 3 theories ...
Processing theory Extended_Finite_State_Machines.GExp ...
Processing theory Extended_Finite_State_Machines.Transition ...
Processing theory Extended_Finite_State_Machines.EFSM ...
Loading 21 theories ...
Processing theory Extended_Finite_State_Machines.Drinks_Machine ...
Processing theory Extended_Finite_State_Machines.EFSM_LTL ...
Processing theory Extended_Finite_State_Machines.Drinks_Machine_LTL ...
Processing theory Ordinal.OrdinalDef ...
Processing theory Nested_Multisets_Ordinals.Hydra_Battle ...
Removing 4 theories ...
Processing theory Ordinal.OrdinalInduct ...
Processing theory Ordinal.OrdinalCont ...
Processing theory Ordinal.OrdinalRec ...
Processing theory Ordinal.OrdinalArith ...
Processing theory Ordinal.OrdinalInverse ...
Processing theory Ordinal.OrdinalFix ...
Processing theory Ordinal.OrdinalOmega ...
Processing theory Nested_Multisets_Ordinals.Syntactic_Ordinal_Bridge ...
Processing theory Huffman.Huffman ...
Removing 1 theories ...
Processing theory CakeML_Codegen.Test_Utils ...
Removing 7 theories ...
Processing theory Nested_Multisets_Ordinals.Goodstein_Sequence ...
Processing theory Collections.Refine_Monadic_Userguide ...
Processing theory Collections.ICF_Userguide ...
Loading 6 theories ...
Removing 56 theories ...
Processing theory Prim_Dijkstra_Simple.Directed_Graph ...
Processing theory Prim_Dijkstra_Simple.Dijkstra_Abstract ...
Processing theory Prim_Dijkstra_Simple.Directed_Graph_Specs ...
Processing theory Prim_Dijkstra_Simple.Directed_Graph_Impl ...
Processing theory MFOTL_Monitor.Slicing ...
Processing theory Prim_Dijkstra_Simple.Dijkstra_Impl ...
Loading 2 theories ...
Processing theory Transitive-Closure.RBT_Map_Set_Extension ...
Loading 2 theories ...
Processing theory Transitive-Closure.Transitive_Closure_RBT_Impl ...
Removing 34 theories ...
Processing theory Dynamic_Tables.Tables_real ...
Processing theory Dynamic_Tables.Tables_nat ...
Processing theory DFS_Framework.On_Stack ...
Loading 28 theories ...
Processing theory Amortized_Complexity.Lemmas_log ...
Processing theory Cauchy.CauchySchwarz ...
Removing 29 theories ...
Processing theory Amortized_Complexity.Priority_Queue_ops ...
Processing theory Amortized_Complexity.Priority_Queue_ops_merge ...
Processing theory Amortized_Complexity.Amortized_Framework ...
Processing theory IMO2019.IMO2019_Q5 ...
Processing theory Special_Function_Bounds.Sin_Cos_Bounds ...
Processing theory Amortized_Complexity.Pairing_Heap_Tree_Analysis2 ...
Processing theory Amortized_Complexity.Skew_Heap_Analysis ...
Processing theory Amortized_Complexity.Pairing_Heap_List2_Analysis ...
Processing theory Amortized_Complexity.Pairing_Heap_Tree_Analysis ...
Processing theory Amortized_Complexity.Pairing_Heap_List1_Analysis ...
Processing theory Special_Function_Bounds.Log_CF_Bounds ...
Removing 9 theories ...
Processing theory Amortized_Complexity.Pairing_Heap_List1_Analysis2 ...
Processing theory Amortized_Complexity.Splay_Heap_Analysis ...
Processing theory Special_Function_Bounds.Sqrt_Bounds ...
Processing theory Special_Function_Bounds.Atan_CF_Bounds ...
Processing theory Splay_Tree.Splay_Tree ...
Processing theory Amortized_Complexity.Amortized_Examples ...
Processing theory Amortized_Complexity.Splay_Tree_Analysis_Base ...
Processing theory Amortized_Complexity.Splay_Tree_Analysis ...
Processing theory Amortized_Complexity.Splay_Tree_Analysis_Optimal ...
Removing 21 theories ...
Processing theory CakeML_Codegen.Test_Embed_Data ...
Loading 10 theories ...
Processing theory Simpl.Simpl_Heap ...
Processing theory Simpl.HeapList ...
Processing theory BDD.BinDag ...
Processing theory BDD.General ...
Processing theory BDD.ProcedureSpecs ...
Processing theory BDD.RepointProof ...
Processing theory BDD.ShareRepProof ...
Removing 18 theories ...
Processing theory BDD.LevellistProof ...
Processing theory BDD.ShareReduceRepListProof ...
Processing theory BDD.NormalizeTotalProof ...
Removing 5 theories ...
Processing theory Collections.Robdd ...
Loading 33 theories ...
Processing theory Syntax_Independent_Logic.Prelim ...
Processing theory HereditarilyFinite.Ordinal ...
Processing theory Nominal2.Nominal2_Base ...
Removing 11 theories ...
Processing theory HereditarilyFinite.Rank ...
Processing theory HereditarilyFinite.OrdArith ...
Processing theory Nominal2.Nominal2_Abs ...
Processing theory Nominal2.Nominal2_FCB ...
Processing theory Nominal2.Nominal2 ...
Processing theory Goedel_HFSet_Semanticless.SyntaxN ...
Processing theory Goedel_HFSet_Semanticless.Coding ...
Processing theory Goedel_HFSet_Semanticless.Predicates ...
Processing theory Goedel_HFSet_Semanticless.Sigma ...
Processing theory Syntax_Independent_Logic.Syntax ...
Processing theory Goedel_HFSet_Semanticless.Coding_Predicates ...
Processing theory Goedel_HFSet_Semanticless.Pf_Predicates ...
Processing theory Syntax_Independent_Logic.Deduction ...
Processing theory Syntax_Independent_Logic.Standard_Model ...
Processing theory Goedel_Incompleteness.Deduction2 ...
Processing theory Goedel_Incompleteness.Abstract_Encoding ...
Processing theory Goedel_HFSet_Semanticless.Functions ...
Processing theory Goedel_Incompleteness.Abstract_Representability ...
Processing theory Goedel_Incompleteness.Diagonalization ...
Processing theory Goedel_Incompleteness.Derivability_Conditions ...
Processing theory Goedel_Incompleteness.Goedel_Formula ...
Processing theory Goedel_Incompleteness.Standard_Model_More ...
Processing theory Goedel_Incompleteness.Abstract_First_Goedel ...
Processing theory Goedel_Incompleteness.Abstract_Second_Goedel ...
Processing theory Goedel_HFSet_Semanticless.II_Prelims ...
Processing theory Goedel_HFSet_Semanticless.Pseudo_Coding ...
Processing theory Goedel_HFSet_Semanticless.Goedel_I ...
Processing theory Goedel_HFSet_Semanticless.Quote ...
Processing theory Goedel_HFSet_Semanticless.Instance ...
Loading 13 theories ...
Removing 12 theories ...
Processing theory Incompleteness.SyntaxN ...
Processing theory Incompleteness.Coding ...
Processing theory Incompleteness.Predicates ...
Processing theory Incompleteness.Sigma ...
Processing theory Incompleteness.Coding_Predicates ...
Processing theory Incompleteness.Pf_Predicates ...
Processing theory Incompleteness.Functions ...
Processing theory Incompleteness.Goedel_I ...
Processing theory Incompleteness.II_Prelims ...
Processing theory Incompleteness.Pseudo_Coding ...
Processing theory Incompleteness.Quote ...
Processing theory Incompleteness.Goedel_II ...
Removing 1 theories ...
Processing theory Goedel_HFSet_Semantic.Instance ...
Loading 3 theories ...
Processing theory Refine_Monadic.Example_Chapter ...
Processing theory Refine_Monadic.WordRefine ...
Loading 17 theories ...
Processing theory Refine_Monadic.Examples ...
Processing theory Simpl.XVcg ...
Processing theory Simpl.Closure ...
Processing theory Simpl.ProcParEx ...
Processing theory Simpl.ClosureEx ...
Processing theory Simpl.SyntaxTest ...
Processing theory Simpl.XVcgEx ...
Processing theory Simpl.ProcParExSP ...
Removing 41 theories ...
Processing theory Simpl.Compose ...
Processing theory Simpl.Quicksort ...
Processing theory Simpl.ComposeEx ...
Processing theory Simpl.VcgExTotal ...
Processing theory Simpl.VcgEx ...
Processing theory Simpl.UserGuide ...
Processing theory Simpl.VcgExSP ...
Processing theory Simpl.AlternativeSmallStep ...
Loading 2 theories ...
Removing 18 theories ...
Processing theory Simpl.Simpl ...
Processing theory LOFT.Featherweight_OpenFlow_Comparison ...
Processing theory LOFT.OpenFlow_Documentation ...
Processing theory Surprise_Paradox.Surprise_Paradox ...
Processing theory BDD.EvalProof ...
Loading 2 theories ...
Processing theory Simple_Firewall.Shadowed ...
Removing 55 theories ...
Processing theory Iptables_Semantics.Example_Semantics ...
Loading 14 theories ...
Processing theory ROBDD.Option_Helpers ...
Processing theory ROBDD.Bool_Func ...
Processing theory ROBDD.Array_List ...
Processing theory Word_Lib.Ancient_Numeral ...
Processing theory ROBDD.Pointer_Map ...
Processing theory Word_Lib.Guide ...
Processing theory ROBDD.Pointer_Map_Impl ...
Processing theory ROBDD.BDT ...
Removing 48 theories ...
Processing theory ROBDD.Abstract_Impl ...
Processing theory ROBDD.Middle_Impl ...
Processing theory ROBDD.Conc_Impl ...
Loading 26 theories ...
Processing theory ROBDD.Level_Collapse ...
Processing theory ROBDD.BDD_Code ...
Processing theory ROBDD.BDD_Examples ...
Processing theory Complx.Cache_Tactics ...
Processing theory Word_Lib.Examples ...
Processing theory Native_Word.Uint16 ...
Processing theory Native_Word.Native_Cast ...
Processing theory Native_Word.Native_Cast_Uint ...
Processing theory Complx.Language ...
Removing 49 theories ...
Processing theory Complx.SmallStep ...
Processing theory Complx.OG_Annotations ...
Processing theory Complx.SeqCatch_decomp ...
Processing theory Complx.OG_Hoare ...
Processing theory Complx.OG_Soundness ...
Processing theory Complx.OG_Tactics ...
Processing theory Complx.OG_Syntax ...
Processing theory Complx.SumArr ...
Removing 17 theories ...
Processing theory Native_Word.Native_Word_Test ...
Processing theory Native_Word.Native_Word_Test_PolyML ...
Processing theory Native_Word.Native_Word_Test_PolyML64 ...
Processing theory Native_Word.Native_Word_Test_OCaml ...
Processing theory Native_Word.Native_Word_Test_Scala ...
Processing theory Native_Word.Native_Word_Test_Emu ...
Processing theory Native_Word.Native_Word_Test_OCaml2 ...
Processing theory Native_Word.Native_Word_Test_PolyML2 ...
Loading 40 theories ...
Processing theory Deriving.Compare_Order_Instances ...
Processing theory Datatype_Order_Generator.Hash_Generator ...
Processing theory Datatype_Order_Generator.Derive ...
Processing theory Old_Datatype_Show.Old_Show ...
Processing theory Old_Datatype_Show.Old_Show_Generator ...
Processing theory Old_Datatype_Show.Old_Show_Instances ...
Removing 7 theories ...
Processing theory Modal_Logics_for_NTS.Nominal_Wellfounded ...
Processing theory Modal_Logics_for_NTS.Residual ...
Processing theory Modal_Logics_for_NTS.Transition_System ...
Processing theory Native_Word.Uint_Userguide ...
Processing theory Modal_Logics_for_NTS.Weak_Transition_System ...
Processing theory Deriving.Derive_Examples ...
Processing theory Modal_Logics_for_NTS.Nominal_Bounded_Set ...
Removing 8 theories ...
Processing theory Native_Word.Native_Word_Test_GHC ...
Processing theory Modal_Logics_for_NTS.Formula ...
Processing theory Modal_Logics_for_NTS.Validity ...
Processing theory Modal_Logics_for_NTS.Disjunction ...
Processing theory Modal_Logics_for_NTS.Logical_Equivalence ...
Processing theory Modal_Logics_for_NTS.Bisimilarity_Implies_Equivalence ...
Processing theory Modal_Logics_for_NTS.Equivalence_Implies_Bisimilarity ...
Processing theory Modal_Logics_for_NTS.Weak_Formula ...
Processing theory Modal_Logics_for_NTS.Weak_Validity ...
Processing theory Modal_Logics_for_NTS.Weak_Logical_Equivalence ...
Processing theory Modal_Logics_for_NTS.Weak_Bisimilarity_Implies_Equivalence ...
Removing 9 theories ...
Processing theory Modal_Logics_for_NTS.Weak_Equivalence_Implies_Bisimilarity ...
Processing theory Modal_Logics_for_NTS.Weak_Expressive_Completeness ...
Processing theory Modal_Logics_for_NTS.S_Transform ...
Removing 8 theories ...
Processing theory Datatype_Order_Generator.Derive_Examples ...
Loading 9 theories ...
Processing theory Old_Datatype_Show.Old_Show_Examples ...
Processing theory Modal_Logics_for_NTS.FS_Set ...
Processing theory Native_Word.Native_Word_Imperative_HOL ...
Removing 14 theories ...
Processing theory Modal_Logics_for_NTS.FL_Transition_System ...
Processing theory Modal_Logics_for_NTS.FL_Formula ...
Processing theory Modal_Logics_for_NTS.FL_Validity ...
Processing theory Modal_Logics_for_NTS.FL_Logical_Equivalence ...
Processing theory Modal_Logics_for_NTS.FL_Equivalence_Implies_Bisimilarity ...
Processing theory Modal_Logics_for_NTS.FL_Bisimilarity_Implies_Equivalence ...
Processing theory Modal_Logics_for_NTS.L_Transform ...
Loading 14 theories ...
Processing theory Aggregation_Algebras.Semigroups_Big ...
Removing 8 theories ...
Processing theory Stone_Algebras.Lattice_Basics ...
Processing theory Stone_Relation_Algebras.Fixpoints ...
Processing theory Stone_Relation_Algebras.Semirings ...
Processing theory Stone_Algebras.P_Algebras ...
Processing theory Stone_Kleene_Relation_Algebras.Iterings ...
Processing theory Stone_Kleene_Relation_Algebras.Kleene_Algebras ...
Processing theory Stone_Relation_Algebras.Relation_Algebras ...
Processing theory Stone_Relation_Algebras.Matrix_Relation_Algebras ...
Processing theory Stone_Kleene_Relation_Algebras.Kleene_Relation_Algebras ...
Processing theory Aggregation_Algebras.Aggregation_Algebras ...
Processing theory Stone_Kleene_Relation_Algebras.Matrix_Kleene_Algebras ...
Processing theory Aggregation_Algebras.Matrix_Aggregation_Algebras ...
Processing theory Aggregation_Algebras.Linear_Aggregation_Algebras ...
Loading 101 theories ...
Removing 4 theories ...
Processing theory Call_Arity.ConstOn ...
Processing theory Call_Arity.List-Interleavings ...
Processing theory Launchbury.Pointwise ...
Processing theory Launchbury.AList-Utils ...
Processing theory Launchbury.Vars ...
Processing theory Launchbury.Nominal-Utils ...
Processing theory Launchbury.AList-Utils-Nominal ...
Processing theory Collections.Locale_Code_Ex ...
Processing theory Call_Arity.Set-Cpo ...
Processing theory Launchbury.HOLCF-Join ...
Processing theory Launchbury.HOLCF-Join-Classes ...
Processing theory Call_Arity.Arity ...
Processing theory Launchbury.Env ...
Processing theory Call_Arity.Env-Set-Cpo ...
Processing theory Launchbury.HOLCF-Utils ...
Processing theory Call_Arity.AList-Utils-HOLCF ...
Processing theory Call_Arity.Cardinality-Domain ...
Processing theory Launchbury.Env-HOLCF ...
Processing theory Launchbury.Nominal-HOLCF ...
Processing theory Call_Arity.Arity-Nominal ...
Processing theory Call_Arity.AEnv ...
Processing theory Launchbury.Terms ...
Processing theory Call_Arity.AnalBinds ...
Processing theory Call_Arity.Cardinality-Domain-Lists ...
Processing theory Call_Arity.CoCallGraph ...
Processing theory Call_Arity.CoCallGraph-Nominal ...
Processing theory Call_Arity.CoCallAnalysisSig ...
Processing theory Call_Arity.CoCallAnalysisBinds ...
Processing theory Call_Arity.TTree ...
Processing theory Call_Arity.TTree-HOLCF ...
Processing theory Call_Arity.TTreeAnalysisSig ...
Processing theory Launchbury.Substitution ...
Processing theory Call_Arity.ArityAnalysisSig ...
Processing theory Call_Arity.ArityAnalysisAbinds ...
Processing theory Call_Arity.ArityAnalysisSpec ...
Processing theory Call_Arity.TTreeAnalysisSpec ...
Processing theory Call_Arity.ArityAnalysisFix ...
Processing theory Call_Arity.ArityAnalysisFixProps ...
Processing theory Call_Arity.CoCallAritySig ...
Processing theory Call_Arity.CoCallAnalysisSpec ...
Processing theory Call_Arity.EtaExpansion ...
Processing theory Call_Arity.TransformTools ...
Processing theory Call_Arity.ArityEtaExpansion ...
Processing theory Call_Arity.SestoftConf ...
Processing theory Call_Arity.ArityAnalysisStack ...
Processing theory Call_Arity.ArityStack ...
Processing theory Call_Arity.CardinalityAnalysisSig ...
Processing theory Call_Arity.CardinalityAnalysisSpec ...
Processing theory Call_Arity.Sestoft ...
Processing theory Call_Arity.EtaExpansionSafe ...
Processing theory Call_Arity.AbstractTransform ...
Removing 20 theories ...
Processing theory Launchbury.Env-Nominal ...
Processing theory Call_Arity.ArityEtaExpansionSafe ...
Processing theory Call_Arity.ArityTransform ...
Processing theory Call_Arity.CoCallGraph-TTree ...
Processing theory Call_Arity.CoCallImplTTree ...
Processing theory Call_Arity.ArityConsistent ...
Processing theory Call_Arity.SestoftGC ...
Processing theory Call_Arity.CoCallFix ...
Processing theory Call_Arity.TTreeImplCardinality ...
Processing theory Call_Arity.TTreeImplCardinalitySafe ...
Processing theory Call_Arity.CoCallImplTTreeSafe ...
Processing theory Call_Arity.CardArityTransformSafe ...
Processing theory Call_Arity.CoCallAnalysisImpl ...
Processing theory Call_Arity.CoCallImplSafe ...
Loading 26 theories ...
Processing theory Call_Arity.CallArityEnd2End ...
Processing theory Call_Arity.CallArityEnd2EndSafe ...
Processing theory Launchbury.Mono-Nat-Fun ...
Processing theory Launchbury.HasESem ...
Processing theory Launchbury.C ...
Processing theory Launchbury.CValue ...
Processing theory Launchbury.Iterative ...
Processing theory Launchbury.Value ...
Processing theory Launchbury.EvalHeap ...
Processing theory Launchbury.CValue-Nominal ...
Processing theory Launchbury.Value-Nominal ...
Processing theory Launchbury.Launchbury ...
Processing theory Launchbury.HOLCF-Meet ...
Processing theory Launchbury.C-Meet ...
Processing theory Launchbury.C-restr ...
Processing theory Launchbury.ValueSimilarity ...
Processing theory Launchbury.HeapSemantics ...
Processing theory Modal_Logics_for_NTS.Expressive_Completeness ...
Processing theory Launchbury.AbstractDenotational ...
Processing theory Launchbury.Abstract-Denotational-Props ...
Processing theory Launchbury.Denotational ...
Processing theory Launchbury.CorrectnessOriginal ...
Processing theory Launchbury.ResourcedDenotational ...
Loading 9 theories ...
Processing theory Launchbury.Denotational-Related ...
Processing theory Launchbury.CorrectnessResourced ...
Processing theory Launchbury.ResourcedAdequacy ...
Processing theory Launchbury.Adequacy ...
Processing theory Launchbury.EverythingAdequacy ...
Removing 67 theories ...
Processing theory LambdaAuth.Nominal2_Lemmas ...
Processing theory LambdaAuth.FMap_Lemmas ...
Processing theory Relational_Minimum_Spanning_Trees.Kruskal ...
Processing theory LambdaAuth.Syntax ...
Processing theory LambdaAuth.Semantics ...
Processing theory LambdaAuth.Agreement ...
Processing theory LambdaAuth.Results ...
Processing theory Relational_Disjoint_Set_Forests.Disjoint_Set_Forests ...
Removing 6 theories ...
Processing theory Relational_Minimum_Spanning_Trees.Boruvka ...
Loading 58 theories ...
Processing theory UPF_Firewall.Ports ...
Processing theory Call_Arity.BalancedTraces ...
Processing theory UPF.Monads ...
Processing theory Call_Arity.TrivialArityAnal ...
Processing theory Call_Arity.SestoftCorrect ...
Processing theory UPF_Firewall.LTL_alike ...
Processing theory UPF.UPFCore ...
Processing theory UPF.ElementaryPolicies ...
Processing theory UPF.SeqComposition ...
Processing theory UPF_Firewall.NetworkCore ...
Processing theory UPF_Firewall.DatatypeAddress ...
Processing theory UPF_Firewall.DatatypePort ...
Processing theory UPF_Firewall.IPv4 ...
Processing theory UPF_Firewall.IPv4_TCPUDP ...
Processing theory UPF_Firewall.IntegerAddress ...
Processing theory UPF_Firewall.IntegerPort ...
Processing theory UPF_Firewall.IntegerPort_TCPUDP ...
Processing theory UPF_Firewall.NetworkModels ...
Processing theory Call_Arity.NoCardinalityAnalysis ...
Processing theory Call_Arity.ArityTransformSafe ...
Processing theory UPF.ParallelComposition ...
Processing theory UPF.Analysis ...
Processing theory Call_Arity.ArityAnalysisCorrDenotational ...
Removing 55 theories ...
Processing theory UPF.Normalisation ...
Processing theory UPF.NormalisationTestSpecification ...
Processing theory UPF.UPF ...
Processing theory UPF_Firewall.PolicyCore ...
Processing theory UPF_Firewall.PolicyCombinators ...
Processing theory UPF_Firewall.PortCombinators ...
Processing theory UPF_Firewall.ProtocolPortCombinators ...
Processing theory UPF_Firewall.PacketFilter ...
Processing theory UPF_Firewall.NAT ...
Processing theory UPF_Firewall.StatefulCore ...
Processing theory UPF_Firewall.FTP ...
Processing theory UPF_Firewall.FTP_WithPolicy ...
Processing theory UPF_Firewall.VOIP ...
Processing theory UPF_Firewall.FWNormalisationCore ...
Processing theory UPF_Firewall.ElementaryRules ...
Processing theory UPF_Firewall.FTPVOIP ...
Processing theory UPF_Firewall.StatefulFW ...
Processing theory UPF_Firewall.NormalisationGenericProofs ...
Processing theory UPF_Firewall.NormalisationIntegerPortProof ...
Processing theory UPF_Firewall.NormalisationIPPProofs ...
Loading 13 theories ...
Processing theory UPF_Firewall.FWNormalisation ...
Processing theory UPF_Firewall.UPF-Firewall ...
Processing theory UPF_Firewall.DMZDatatype ...
Processing theory UPF_Firewall.DMZInteger ...
Processing theory UPF_Firewall.DMZ ...
Processing theory UPF_Firewall.PersonalFirewallDatatype ...
Processing theory UPF_Firewall.PersonalFirewallInt ...
Processing theory UPF_Firewall.PersonalFirewallIpv4 ...
Processing theory UPF_Firewall.PersonalFirewall ...
Processing theory UPF_Firewall.Transformation01 ...
Processing theory UPF_Firewall.Transformation02 ...
Processing theory UPF_Firewall.Transformation ...
Processing theory UPF_Firewall.Voice_over_IP ...
Processing theory UPF_Firewall.NAT-FW ...
Processing theory UPF_Firewall.Examples ...
Removing 43 theories ...
Processing theory Chandy_Lamport.Example ...
Processing theory Noninterference_Sequential_Composition.Propaedeutics ...
Removing 6 theories ...
Processing theory Noninterference_Sequential_Composition.SequentialComposition ...
Processing theory Noninterference_Sequential_Composition.Counterexamples ...
Processing theory Robinson_Arithmetic.Robinson_Arithmetic ...
Processing theory Syntax_Independent_Logic.Natural_Deduction ...
Removing 2 theories ...
Processing theory Syntax_Independent_Logic.Syntax_Arith ...
Processing theory Syntax_Independent_Logic.Deduction_Q ...
Processing theory Robinson_Arithmetic.Instance ...
Loading 27 theories ...
Removing 4 theories ...
Processing theory HOLCF-Prelude.HOLCF_Main ...
Processing theory HOLCF-Prelude.Data_Function ...
Processing theory HOLCF-Prelude.Numeral_Cpo ...
Processing theory Collections.SetAbstractionIterator ...
Processing theory HOLCF-Prelude.Type_Classes ...
Processing theory HOLCF-Prelude.Data_Bool ...
Processing theory HOLCF-Prelude.Data_Integer ...
Processing theory Dependent_SIFUM_Type_Systems.Preliminaries ...
Processing theory HOLCF-Prelude.Data_Tuple ...
Processing theory Dependent_SIFUM_Type_Systems.Security ...
Processing theory HOLCF-Prelude.Data_List ...
Processing theory Dependent_SIFUM_Type_Systems.Language ...
Processing theory Dependent_SIFUM_Refinement.Eg2 ...
Processing theory HOLCF-Prelude.Data_Maybe ...
Processing theory HOLCF-Prelude.HOLCF_Prelude ...
Processing theory BirdKMP.HOLCF_ROOT ...
Processing theory Dependent_SIFUM_Type_Systems.Compositionality ...
Processing theory BirdKMP.Theory_Of_Lists ...
Removing 5 theories ...
Processing theory Dependent_SIFUM_Refinement.CompositionalRefinement ...
Processing theory Dependent_SIFUM_Type_Systems.TypeSystem ...
Processing theory Dependent_SIFUM_Type_Systems.TypeSystemTactics ...
Processing theory Dependent_SIFUM_Refinement.Eg1 ...
Processing theory Dependent_SIFUM_Refinement.Eg1RefinementTrivial ...
Processing theory Dependent_SIFUM_Refinement.Eg1Eg2 ...
Processing theory Dependent_SIFUM_Refinement.Eg1Eg2RefinementSimple ...
Removing 5 theories ...
Processing theory BirdKMP.KMP ...
Loading 9 theories ...
Processing theory Rewriting_Z.Z ...
Processing theory Rewriting_Z.Lambda_Z ...
Processing theory Dependent_SIFUM_Type_Systems.Example_TypeSystem ...
Processing theory Stone_Algebras.Filters ...
Removing 13 theories ...
Processing theory Relational_Minimum_Spanning_Trees.Prim ...
Processing theory Dependent_SIFUM_Type_Systems.Example_Swap_Add ...
Processing theory Stone_Algebras.Stone_Construction ...
Processing theory Stone_Relation_Algebras.Relation_Subalgebras ...
Loading 19 theories ...
Processing theory Stone_Kleene_Relation_Algebras.Kleene_Relation_Subalgebras ...
Processing theory Slicing.ControlDependenceRelations ...
Processing theory Slicing.DynPDG ...
Processing theory Slicing.DependentLiveVariables ...
Processing theory Slicing.BitVector ...
Processing theory Slicing.Semantics ...
Processing theory Slicing.DynamicControlDependences ...
Processing theory Slicing.WEquivalence ...
Processing theory Slicing.SemanticsWellFormed ...
Processing theory Slicing.StaticControlDependences ...
Removing 12 theories ...
Processing theory Slicing.DynSlice ...
Processing theory Slicing.JVMCFG ...
Processing theory Slicing.JVMInterpretation ...
Processing theory CakeML_Codegen.Test_Embed_Data2 ...
Processing theory CakeML_Codegen.Test_Embed_Tree ...
Removing 38 theories ...
Processing theory Slicing.JVMPostdomination ...
Processing theory Slicing.JVMCFG_wf ...
Processing theory Slicing.JVMControlDependences ...
Processing theory Slicing.SemanticsWF ...
Loading 32 theories ...
Processing theory Slicing.Slicing ...
Processing theory Extended_Finite_State_Machine_Inference.Code_Target_Set ...
Processing theory Extended_Finite_State_Machine_Inference.Code_Target_List ...
Processing theory Extended_Finite_State_Machine_Inference.Group_By ...
Processing theory HOLCF-Prelude.Definedness ...
Processing theory HOLCF-Prelude.List_Comprehension ...
Processing theory HOLCF-Prelude.Fibs ...
Processing theory Extended_Finite_State_Machine_Inference.Code_Target_FSet ...
Processing theory Extended_Finite_State_Machine_Inference.Subsumption ...
Processing theory HOLCF-Prelude.GHC_Rewrite_Rules ...
Processing theory HOLCF-Prelude.HLint ...
Processing theory HOLCF-Prelude.Num_Class ...
Processing theory HOLCF-Prelude.Sieve_Primes ...
Processing theory Extended_Finite_State_Machines.AExp_Lexorder ...
Removing 68 theories ...
Processing theory Extended_Finite_State_Machines.GExp_Lexorder ...
Processing theory Extended_Finite_State_Machines.Transition_Lexorder ...
Processing theory Extended_Finite_State_Machine_Inference.Inference ...
Processing theory Extended_Finite_State_Machine_Inference.SelectionStrategies ...
Processing theory Extended_Finite_State_Machine_Inference.Same_Register ...
Processing theory Extended_Finite_State_Machine_Inference.Weak_Subsumption ...
Processing theory Extended_Finite_State_Machine_Inference.Distinguishing_Guards ...
Processing theory Extended_Finite_State_Machine_Inference.Increment_Reset ...
Processing theory Extended_Finite_State_Machine_Inference.Store_Reuse ...
Processing theory Extended_Finite_State_Machine_Inference.EFSM_Dot ...
Processing theory Extended_Finite_State_Machine_Inference.efsm2sal ...
Processing theory FOL-Fitting.FOL_Fitting ...
Processing theory FOL_Seq_Calc1.Common ...
Processing theory Extended_Finite_State_Machine_Inference.Store_Reuse_Subsumption ...
Processing theory FOL_Seq_Calc1.Tableau ...
Processing theory FOL_Seq_Calc1.Sequent ...
Processing theory Extended_Finite_State_Machine_Inference.PTA_Generalisation ...
Processing theory Extended_Finite_State_Machine_Inference.Least_Upper_Bound ...
Processing theory Extended_Finite_State_Machine_Inference.Code_Generation ...
Loading 33 theories ...
Removing 25 theories ...
Processing theory Combinatorics_Words.Arithmetical_Hints ...
Processing theory Combinatorics_Words.Reverse_Symmetry ...
Processing theory Goedel_Incompleteness.Loeb_Formula ...
Processing theory Goedel_Incompleteness.Loeb ...
Processing theory Goedel_Incompleteness.Abstract_Jeroslow_Encoding ...
Processing theory Goedel_Incompleteness.Tarski ...
Processing theory Goedel_Incompleteness.Rosser_Formula ...
Processing theory Relation_Algebra.More_Boolean_Algebra ...
Processing theory Goedel_Incompleteness.Jeroslow_Simplified ...
Processing theory Combinatorics_Words.CoWBasic ...
Processing theory Combinatorics_Words.Lyndon_Schutzenberger ...
Processing theory Combinatorics_Words.Periodicity_Lemma ...
Processing theory Combinatorics_Words.Submonoids ...
Processing theory Combinatorics_Words.CoWAll ...
Processing theory Combinatorics_Words_Graph_Lemma.Graph_Lemma ...
Processing theory Goedel_Incompleteness.Abstract_First_Goedel_Rosser ...
Removing 5 theories ...
Processing theory Syntax_Independent_Logic.Pseudo_Term ...
Processing theory Relation_Algebra.Relation_Algebra ...
Processing theory Relation_Algebra.Relation_Algebra_Vectors ...
Processing theory Relation_Algebra.Relation_Algebra_Tests ...
Processing theory Goedel_Incompleteness.Jeroslow_Original ...
Processing theory Goedel_Incompleteness.All_Abstract ...
Processing theory Relation_Algebra.Relation_Algebra_RTC ...
Removing 24 theories ...
Processing theory Relation_Algebra.Relation_Algebra_Functions ...
Processing theory Relational_Paths.More_Relation_Algebra ...
Processing theory Relational_Paths.Paths ...
Processing theory Dependent_SIFUM_Refinement.EgHighBranchRevC ...
Removing 2 theories ...
Processing theory Relational_Paths.Rooted_Paths ...
Processing theory Relational_Paths.Path_Algorithms ...
Loading 34 theories ...
Processing theory Monad_Memo_DP.Ground_Function ...
Processing theory Monad_Memo_DP.Solve_Cong ...
Processing theory Nominal2.Eqvt ...
Processing theory Monad_Memo_DP.Bottom_Up_Computation ...
Processing theory Monad_Memo_DP.Bottom_Up_Computation_Heap ...
Processing theory Nominal2.Atoms ...
Removing 11 theories ...
Processing theory Optimal_BST.Optimal_BST_Examples ...
Processing theory Szpilrajn.Szpilrajn ...
Processing theory Monad_Memo_DP.Example_Misc ...
Processing theory Monad_Memo_DP.Index ...
Processing theory Optimal_BST.Quadrilateral_Inequality ...
Processing theory Polynomials.Show_Polynomials ...
Processing theory Combinatorics_Words_Lyndon.Lyndon ...
Processing theory Combinatorics_Words_Lyndon.Lyndon_Addition ...
Processing theory Polynomials.NZM ...
Processing theory Monad_Memo_DP.Longest_Common_Subsequence ...
Processing theory Optimal_BST.Weighted_Path_Length ...
Processing theory Monad_Memo_DP.Counting_Tiles ...
Processing theory LTL_Normal_Form.Normal_Form_Complexity ...
Removing 15 theories ...
Processing theory Monad_Memo_DP.Pair_Memory ...
Processing theory Monad_Memo_DP.Memory_Heap ...
Processing theory Monad_Memo_DP.Heap_Main ...
Processing theory Monad_Memo_DP.Heap_Default ...
Processing theory Monad_Memo_DP.Knapsack ...
Processing theory Monad_Memo_DP.Tracing ...
Processing theory Monad_Memo_DP.OptBST ...
Processing theory Optimal_BST.Optimal_BST ...
Processing theory Monad_Memo_DP.CYK ...
Processing theory Optimal_BST.Optimal_BST2 ...
Processing theory Optimal_BST.Optimal_BST_Code ...
Processing theory Monad_Memo_DP.Bellman_Ford ...
Processing theory Monad_Memo_DP.Min_Ed_Dist0 ...
Loading 15 theories ...
Processing theory Monad_Memo_DP.All_Examples ...
Processing theory Containers-Benchmarks.Benchmark_Set_Default ...
Processing theory InformationFlowSlicing.NonInterferenceIntra ...
Removing 15 theories ...
Processing theory Kleene_Algebra.Matrix ...
Processing theory Minsky_Machines.Recursive_Inseparability ...
Processing theory Noninterference_Concurrent_Composition.ConcurrentComposition ...
Processing theory InformationFlowSlicing.LiftingIntra ...
Processing theory InformationFlowSlicing.NonInterferenceWhile ...
Processing theory Minsky_Machines.Minsky ...
Loading 52 theories ...
Removing 50 theories ...
Processing theory Formula_Derivatives.FSet_More ...
Processing theory Auto2_HOL.HOL_Base ...
Processing theory Auto2_HOL.Auto2_HOL ...
Processing theory Auto2_HOL.Logic_Thms ...
Processing theory Auto2_HOL.Order_Thms ...
Processing theory Formula_Derivatives.While_Default ...
Processing theory Auto2_HOL.Set_Thms ...
Processing theory LTL_Master_Theorem.Asymmetric_Master_Theorem ...
Processing theory Auto2_HOL.Arith_Thms ...
Processing theory Auto2_HOL.Lists_Thms ...
Processing theory Auto2_HOL.Auto2_Main ...
Processing theory Auto2_Imperative_HOL.SepLogic_Base ...
Processing theory Extended_Finite_State_Machines.Drinks_Machine_2 ...
Processing theory Extended_Finite_State_Machine_Inference.Drinks_Subsumption ...
Processing theory Optimal_BST.Optimal_BST_Memo ...
Processing theory Formula_Derivatives.Automaton ...
Processing theory Auto2_Imperative_HOL.Partial_Equiv_Rel ...
Processing theory Auto2_Imperative_HOL.Interval ...
Processing theory Nested_Multisets_Ordinals.Unary_PCF ...
Removing 61 theories ...
Processing theory Auto2_Imperative_HOL.Mapping_Str ...
Processing theory Formula_Derivatives.WS1S_Prelim ...
Processing theory Auto2_Imperative_HOL.Arrays_Ex ...
Processing theory Auto2_Imperative_HOL.Lists_Ex ...
Processing theory Auto2_Imperative_HOL.SepAuto ...
Processing theory Auto2_Imperative_HOL.GCD_Impl ...
Processing theory Auto2_Imperative_HOL.Arrays_Impl ...
Processing theory Auto2_Imperative_HOL.BST ...
Processing theory Auto2_Imperative_HOL.Union_Find ...
Processing theory Auto2_Imperative_HOL.BST_Impl ...
Processing theory Auto2_Imperative_HOL.Union_Find_Impl ...
Processing theory Auto2_Imperative_HOL.Connectivity ...
Processing theory Auto2_Imperative_HOL.Connectivity_Impl ...
Processing theory Auto2_Imperative_HOL.DynamicArray ...
Processing theory Auto2_Imperative_HOL.LinkedList ...
Processing theory Auto2_Imperative_HOL.Interval_Tree ...
Processing theory Auto2_Imperative_HOL.IntervalTree_Impl ...
Processing theory Formula_Derivatives.Abstract_Formula ...
Processing theory Auto2_Imperative_HOL.Quicksort ...
Processing theory Auto2_Imperative_HOL.Quicksort_Impl ...
Processing theory Auto2_Imperative_HOL.RBTree ...
Processing theory Auto2_Imperative_HOL.Rect_Intersect ...
Processing theory Auto2_Imperative_HOL.Rect_Intersect_Impl ...
Processing theory Auto2_Imperative_HOL.Dijkstra ...
Processing theory Auto2_Imperative_HOL.Indexed_PQueue ...
Processing theory Auto2_Imperative_HOL.RBTree_Impl ...
Processing theory Auto2_Imperative_HOL.Indexed_PQueue_Impl ...
Processing theory Auto2_Imperative_HOL.Dijkstra_Impl ...
Processing theory Auto2_Imperative_HOL.Sep_Examples ...
Removing 35 theories ...
Processing theory Formula_Derivatives.WS1S_Formula ...
Loading 85 theories ...
Processing theory Formula_Derivatives.WS1S_Nameful ...
Processing theory Formula_Derivatives-Examples.WS1S_Nameful_Examples ...
Removing 2 theories ...
Processing theory Algebraic_VCs.P2S2R ...
Processing theory Jinja.Hidden ...
Processing theory Jinja.State ...
Processing theory Jinja.PCompiler ...
Processing theory Jinja.JVMDefensive ...
Processing theory Quantales.Dioid_Models_New ...
Processing theory Jinja.Expr ...
Processing theory Jinja.Examples ...
Processing theory Jinja.WellType ...
Processing theory Jinja.Annotate ...
Processing theory Jinja.BigStep ...
Processing theory Jinja.DefAss ...
Processing theory Jinja.WWellForm ...
Processing theory Jinja.JWellForm ...
Processing theory Jinja.WellTypeRT ...
Processing theory Jinja.J1 ...
Processing theory Jinja.Compiler1 ...
Processing theory Jinja.Compiler2 ...
Processing theory Jinja.SmallStep ...
Processing theory Jinja.J1WellForm ...
Processing theory Jinja.execute_WellType ...
Processing theory Formula_Derivatives-Examples.WS1S_Examples ...
Processing theory Jinja.Equivalence ...
Processing theory KAT_and_DRA.KAT_Models ...
Processing theory Formula_Derivatives.Presburger_Formula ...
Removing 1 theories ...
Processing theory Formula_Derivatives.WS1S_Presburger_Equivalence ...
Processing theory Formula_Derivatives-Examples.WS1S_Presburger_Examples ...
Processing theory Jinja.LBVJVM ...
Processing theory Jinja.Correctness1 ...
Processing theory Jinja.Progress ...
Processing theory Jinja.BVNoTypeError ...
Processing theory Algebraic_VCs.VC_KAT ...
Processing theory Algebraic_VCs.VC_KAT_Examples ...
Processing theory Algebraic_VCs.VC_KAT_Examples2 ...
Processing theory Algebraic_VCs.RKAT ...
Processing theory Algebraic_VCs.RKAT_Models ...
Processing theory Algebraic_VCs.VC_RKAT ...
Processing theory Algebraic_VCs.VC_RKAT_Examples ...
Processing theory Jinja.TypeSafe ...
Removing 9 theories ...
Processing theory Jinja.execute_Bigstep ...
Processing theory Algebraic_VCs.VC_KAD ...
Processing theory Algebraic_VCs.VC_KAD_Examples ...
Processing theory Algebraic_VCs.VC_KAD_Examples2 ...
Processing theory Algebraic_VCs.Pointer_Examples ...
Processing theory Algebraic_VCs.VC_KAD_dual ...
Processing theory Algebraic_VCs.VC_KAD_dual_Examples ...
Processing theory Algebraic_VCs.VC_KAD_wf ...
Processing theory Algebraic_VCs.VC_KAD_wf_Examples ...
Processing theory Algebraic_VCs.Path_Model_Example ...
Processing theory Algebraic_VCs.KAD_is_KAT ...
Removing 16 theories ...
Processing theory Quantales.Quantale_Models ...
Processing theory Jinja.Correctness2 ...
Processing theory Quantales.Quantic_Nuclei_Conuclei ...
Processing theory Jinja.Compiler ...
Processing theory Quantales.Quantale_Left_Sided ...
Removing 11 theories ...
Processing theory Jinja.TypeComp ...
Loading 18 theories ...
Processing theory Jinja.Jinja ...
Processing theory Auto2_HOL.Auto2_Test ...
Processing theory Kleene_Algebra.Finite_Suprema ...
Processing theory Decreasing-Diagrams-II.Decreasing_Diagrams_II_Aux ...
Processing theory Kleene_Algebra.Omega_Algebra ...
Processing theory Kleene_Algebra.Omega_Algebra_Models ...
Removing 75 theories ...
Processing theory Auto2_HOL.Primes_Ex ...
Processing theory Regular_Algebras.Dioid_Power_Sum ...
Processing theory Complx.Examples ...
Processing theory Decreasing-Diagrams-II.Decreasing_Diagrams_II ...
Processing theory Stone_Relation_Algebras.Linear_Order_Matrices ...
Processing theory Residuated_Lattices.Residuated_Lattices ...
Processing theory Residuated_Lattices.Action_Algebra ...
Processing theory Residuated_Lattices.Action_Algebra_Models ...
Processing theory Formula_Derivatives.WS1S_Alt_Formula ...
Removing 37 theories ...
Processing theory Formula_Derivatives-Examples.WS1S_Alt_Examples ...
Removing 7 theories ...
Processing theory Regular_Algebras.Regular_Algebras ...
Loading 32 theories ...
Processing theory Regular_Algebras.Regular_Algebra_Models ...
Processing theory IMP2.IMP2_Utils ...
Processing theory IMP2.Subgoal_Focus_Some ...
Processing theory Show.Show_Real_Impl ...
Removing 8 theories ...
Processing theory IMP2.Named_Simpsets ...
Processing theory Formula_Derivatives-Examples.Presburger_Examples ...
Processing theory Deriving.RBT_Compare_Order_Impl ...
Processing theory Nested_Multisets_Ordinals.McCarthy_91 ...
Processing theory Containers-Benchmarks.Benchmark_RBT ...
Processing theory Quantales.Quantale_Modules ...
Processing theory VerifyThis2019.Challenge1A ...
Processing theory IMP2.IMP2_Aux_Lemmas ...
Processing theory Regular_Algebras.Pratts_Counterexamples ...
Processing theory Rewriting_Z.CL_Z ...
Processing theory IMP2.Syntax ...
Processing theory IMP2.Parser ...
Processing theory VerifyThis2019.Challenge1B ...
Processing theory Noninterference_Generic_Unwinding.GenericUnwinding ...
Processing theory IMP2.Semantics ...
Processing theory IMP2.Annotated_Syntax ...
Processing theory IMP2.IMP2_Basic_Simpset ...
Processing theory IMP2.IMP2_Basic_Decls ...
Processing theory IMP2.IMP2_Var_Abs ...
Processing theory IMP2.IMP2_Program_Analysis ...
Processing theory IMP2.IMP2_Var_Postprocessor ...
Removing 34 theories ...
Processing theory IMP2.IMP2_VCG ...
Processing theory IMP2.IMP2_Specification ...
Processing theory Decreasing-Diagrams.Decreasing_Diagrams ...
Processing theory Regular_Algebras.Regular_Algebra_Variants ...
Processing theory IMP2.IMP2 ...
Removing 10 theories ...
Processing theory IMP2_Binary_Heap.IMP2_Binary_Heap ...
Processing theory Algebraic_VCs.Domain_Quantale ...
Removing 6 theories ...
Processing theory IMP2.Examples ...
Loading 71 theories ...
Processing theory Interpreter_Optimizations.Dynamic ...
Processing theory Interpreter_Optimizations.Op ...
Processing theory Interpreter_Optimizations.OpInl ...
Processing theory Interpreter_Optimizations.Option_applicative ...
Processing theory Interpreter_Optimizations.Env ...
Processing theory Interpreter_Optimizations.List_util ...
Processing theory KAT_and_DRA.KAT2 ...
Processing theory IMP2.IMP2_from_IMP ...
Processing theory Ordinal.OrdinalVeblen ...
Processing theory Ordinal.Ordinal ...
Processing theory Kleene_Algebra.Formal_Power_Series ...
Processing theory IMP2.Quickstart_Guide ...
Processing theory Kleene_Algebra.Inf_Matrix ...
Processing theory Relation_Algebra.Relation_Algebra_Models ...
Processing theory VeriComp.Transfer_Extras ...
Processing theory VeriComp.Well_founded ...
Processing theory VeriComp.Inf ...
Processing theory VeriComp.Behaviour ...
Removing 38 theories ...
Processing theory CRDT.Util ...
Processing theory Relation_Algebra.Relation_Algebra_Direct_Products ...
Processing theory VeriComp.Semantics ...
Processing theory VeriComp.Language ...
Processing theory VeriComp.Simulation ...
Processing theory VeriComp.Compiler ...
Processing theory Noninterference_CSP.ClassicalNoninterference ...
Processing theory Noninterference_CSP.GeneralizedNoninterference ...
Processing theory CRDT.Convergence ...
Processing theory Kleene_Algebra.DRA ...
Processing theory KAT_and_DRA.DRAT2 ...
Processing theory Kleene_Algebra.PHL_DRA ...
Processing theory Residuated_Lattices.Residuated_Boolean_Algebras ...
Processing theory Interpreter_Optimizations.Result ...
Processing theory Interpreter_Optimizations.Global ...
Processing theory Stern_Brocot.Cotree ...
Removing 8 theories ...
Processing theory UPF.Service ...
Processing theory UPF.ServiceExample ...
Processing theory Interpreter_Optimizations.Unboxed ...
Processing theory Interpreter_Optimizations.OpUbx ...
Processing theory Interpreter_Optimizations.Unboxed_lemmas ...
Processing theory Stern_Brocot.Cotree_Algebra ...
Processing theory CRDT.Network ...
Processing theory IMAP-CRDT.IMAP-def ...
Processing theory IMAP-CRDT.IMAP-proof-commute ...
Processing theory Residuated_Lattices.Residuated_Relation_Algebra ...
Removing 15 theories ...
Processing theory IMAP-CRDT.IMAP-proof-helpers ...
Processing theory KAT_and_DRA.DRAT ...
Processing theory Dependent_SIFUM_Type_Systems.Example ...
Processing theory KAT_and_DRA.DRA_Models ...
Processing theory Interpreter_Optimizations.Inca ...
Processing theory KAT_and_DRA.PHL_DRAT ...
Processing theory HereditarilyFinite.Finitary ...
Processing theory Iptables_Semantics.Alternative_Semantics ...
Processing theory KAT_and_DRA.FolkTheorem ...
Processing theory HereditarilyFinite.Finite_Automata ...
Removing 20 theories ...
Processing theory Iptables_Semantics.Semantics_Stateful ...
Processing theory IMAP-CRDT.IMAP-proof-independent ...
Processing theory Card_Equiv_Relations.Card_Equiv_Relations ...
Processing theory Card_Equiv_Relations.Card_Partial_Equiv_Relations ...
Processing theory IMAP-CRDT.IMAP-proof ...
Processing theory Multirelations.C_Algebras ...
Processing theory Interpreter_Optimizations.Ubx ...
Processing theory Interpreter_Optimizations.Ubx_type_inference ...
Removing 22 theories ...
Processing theory Stern_Brocot.Stern_Brocot_Tree ...
Processing theory Stern_Brocot.Bird_Tree ...
Processing theory Interpreter_Optimizations.Inca_to_Ubx_simulation ...
Removing 7 theories ...
Processing theory Interpreter_Optimizations.Inca_to_Ubx_compiler ...
Removing 3 theories ...
Sending interrupt signal to process
+ true