--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 18:43:16 2014 +0100
@@ -191,11 +191,11 @@
val arith_methodss =
[[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
- Metis_Method], [Meson_Method]]
-val datatype_methodss = [[Simp_Size_Method, Simp_Method]]
+ Algebra_Method], [Metis_Method], [Meson_Method]]
+val datatype_methodss = [[Simp_Method], [Simp_Size_Method]]
val metislike_methodss =
[[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
- Force_Method], [Meson_Method]]
+ Force_Method, Algebra_Method], [Meson_Method]]
val rewrite_methodss =
[[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
val skolem_methodss = [[Metis_Method, Blast_Method], [Meson_Method]]
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 18:43:16 2014 +0100
@@ -101,6 +101,7 @@
| Force_Method => Clasimp.force_tac ctxt
| Arith_Method => Arith_Data.arith_tac ctxt
| Blast_Method => blast_tac ctxt
+ | Algebra_Method => Groebner.algebra_tac [] [] ctxt
| _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
(* main function for preplaying Isar steps; may throw exceptions *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 18:43:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 18:43:16 2014 +0100
@@ -15,7 +15,7 @@
datatype proof_method =
Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
- Arith_Method | Blast_Method | Meson_Method
+ Arith_Method | Blast_Method | Meson_Method | Algebra_Method
datatype isar_proof =
Proof of (string * typ) list * (label * term) list * isar_step list
@@ -66,7 +66,7 @@
datatype proof_method =
Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
- Arith_Method | Blast_Method | Meson_Method
+ Arith_Method | Blast_Method | Meson_Method | Algebra_Method
datatype isar_proof =
Proof of (string * typ) list * (label * term) list * isar_step list
@@ -92,7 +92,8 @@
| Force_Method => "force"
| Arith_Method => "arith"
| Blast_Method => "blast"
- | Meson_Method => "meson")
+ | Meson_Method => "meson"
+ | Algebra_Method => "algebra")
fun steps_of_proof (Proof (_, _, steps)) = steps