# HG changeset patch
# User blanchet
# Date 1391085508 -3600
# Node ID 318cd8ac18177687d8531833378035b312ff46e3
# Parent  b7ca9f98faca7f33b77e88f2abf1f6ca16d4cf19
added 'algebra' and 'meson' to 'try0'

diff -r b7ca9f98faca -r 318cd8ac1817 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu Jan 30 13:38:28 2014 +0100
+++ b/src/HOL/Groebner_Basis.thy	Thu Jan 30 13:38:28 2014 +0100
@@ -85,4 +85,9 @@
 declare zmod_eq_dvd_iff[algebra]
 declare nat_mod_eq_iff[algebra]
 
+
+subsection {* Try0 *}
+
+ML_file "Tools/try0.ML"
+
 end
diff -r b7ca9f98faca -r 318cd8ac1817 src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Thu Jan 30 13:38:28 2014 +0100
+++ b/src/HOL/Metis.thy	Thu Jan 30 13:38:28 2014 +0100
@@ -52,9 +52,4 @@
     fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws
     fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
 
-
-subsection {* Try0 *}
-
-ML_file "Tools/try0.ML"
-
 end
diff -r b7ca9f98faca -r 318cd8ac1817 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Jan 30 13:38:28 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Thu Jan 30 13:38:28 2014 +0100
@@ -96,13 +96,15 @@
 val named_methods =
   [("simp", ((false, true), simp_attrs)),
    ("auto", ((true, true), full_attrs)),
+   ("blast", ((false, true), clas_attrs)),
+   ("metis", ((false, true), metis_attrs)),
+   ("linarith", ((false, true), no_attrs)),
+   ("presburger", ((false, true), no_attrs)),
+   ("algebra", ((false, true), no_attrs)),
    ("fast", ((false, false), clas_attrs)),
    ("fastforce", ((false, false), full_attrs)),
    ("force", ((false, false), full_attrs)),
-   ("blast", ((false, true), clas_attrs)),
-   ("metis", ((false, true), metis_attrs)),
-   ("linarith", ((false, true), no_attrs)),
-   ("presburger", ((false, true), no_attrs))]
+   ("meson", ((false, false), metis_attrs))]
 val do_methods = map do_named_method named_methods
 
 fun time_string ms = string_of_int ms ^ " ms"