# HG changeset patch
# User blanchet
# Date 1391190196 -3600
# Node ID 6fe9fd75f9d79e990a0708ae8299f017362ab5a6
# Parent  ed495a5088c6b72a1c805089384b52a0c9c44ffe
added 'algebra' to the mix

diff -r ed495a5088c6 -r 6fe9fd75f9d7 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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]]
diff -r ed495a5088c6 -r 6fe9fd75f9d7 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- 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 *)
diff -r ed495a5088c6 -r 6fe9fd75f9d7 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- 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