added 'algebra' and 'meson' to 'try0'
authorblanchet
Thu Jan 30 13:38:28 2014 +0100 (2014-01-30)
changeset 55178318cd8ac1817
parent 55177 b7ca9f98faca
child 55179 71cc2db86eec
added 'algebra' and 'meson' to 'try0'
src/HOL/Groebner_Basis.thy
src/HOL/Metis.thy
src/HOL/Tools/try0.ML
     1.1 --- a/src/HOL/Groebner_Basis.thy	Thu Jan 30 13:38:28 2014 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Jan 30 13:38:28 2014 +0100
     1.3 @@ -85,4 +85,9 @@
     1.4  declare zmod_eq_dvd_iff[algebra]
     1.5  declare nat_mod_eq_iff[algebra]
     1.6  
     1.7 +
     1.8 +subsection {* Try0 *}
     1.9 +
    1.10 +ML_file "Tools/try0.ML"
    1.11 +
    1.12  end
     2.1 --- a/src/HOL/Metis.thy	Thu Jan 30 13:38:28 2014 +0100
     2.2 +++ b/src/HOL/Metis.thy	Thu Jan 30 13:38:28 2014 +0100
     2.3 @@ -52,9 +52,4 @@
     2.4      fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws
     2.5      fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
     2.6  
     2.7 -
     2.8 -subsection {* Try0 *}
     2.9 -
    2.10 -ML_file "Tools/try0.ML"
    2.11 -
    2.12  end
     3.1 --- a/src/HOL/Tools/try0.ML	Thu Jan 30 13:38:28 2014 +0100
     3.2 +++ b/src/HOL/Tools/try0.ML	Thu Jan 30 13:38:28 2014 +0100
     3.3 @@ -96,13 +96,15 @@
     3.4  val named_methods =
     3.5    [("simp", ((false, true), simp_attrs)),
     3.6     ("auto", ((true, true), full_attrs)),
     3.7 +   ("blast", ((false, true), clas_attrs)),
     3.8 +   ("metis", ((false, true), metis_attrs)),
     3.9 +   ("linarith", ((false, true), no_attrs)),
    3.10 +   ("presburger", ((false, true), no_attrs)),
    3.11 +   ("algebra", ((false, true), no_attrs)),
    3.12     ("fast", ((false, false), clas_attrs)),
    3.13     ("fastforce", ((false, false), full_attrs)),
    3.14     ("force", ((false, false), full_attrs)),
    3.15 -   ("blast", ((false, true), clas_attrs)),
    3.16 -   ("metis", ((false, true), metis_attrs)),
    3.17 -   ("linarith", ((false, true), no_attrs)),
    3.18 -   ("presburger", ((false, true), no_attrs))]
    3.19 +   ("meson", ((false, false), metis_attrs))]
    3.20  val do_methods = map do_named_method named_methods
    3.21  
    3.22  fun time_string ms = string_of_int ms ^ " ms"