author | blanchet |
Mon, 03 Feb 2014 23:49:01 +0100 | |
changeset 55310 | ae419c611a3b |
parent 55309 | 455a7f9924df |
child 55311 | 2bb02ba5d4b7 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 23:44:39 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Feb 03 23:49:01 2014 +0100 @@ -122,7 +122,7 @@ Metis_Method (SOME no_typesN, NONE)] val rewrite_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method (NONE, NONE), - Meson_Method] + Meson_Method, Blast_Method, Arith_Method, Algebra_Method] val skolem_methods = [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]