# HG changeset patch
# User haftmann
# Date 1273180318 -7200
# Node ID b91ef008b5605a1618b2eb31e0450b4fbc6fb222
# Parent  c8ea75ea4a29db002fc64acc8249c45734a2a27b
moved method syntax here

diff -r c8ea75ea4a29 -r b91ef008b560 src/HOL/Tools/Groebner_Basis/groebner.ML
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Thu May 06 23:11:58 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Thu May 06 23:11:58 2010 +0200
@@ -9,13 +9,14 @@
      vars: cterm list, semiring: cterm list * thm list, ideal : thm list} ->
     (cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
     conv ->  conv ->
- {ring_conv : conv, 
- simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list),
- multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list,
- poly_eq_ss: simpset, unwind_conv : conv}
-    val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
-    val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic
-    val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
+     {ring_conv : conv, 
+     simple_ideal: (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list),
+     multi_ideal: cterm list -> cterm list -> cterm list -> (cterm * cterm) list,
+     poly_eq_ss: simpset, unwind_conv : conv}
+  val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
+  val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic
+  val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
+  val algebra_method: (Proof.context -> Method.method) context_parser
 end
 
 structure Groebner : GROEBNER =
@@ -1024,6 +1025,21 @@
 fun algebra_tac add_ths del_ths ctxt i = 
  ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i
  
- 
+local
+
+fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
+val addN = "add"
+val delN = "del"
+val any_keyword = keyword addN || keyword delN
+val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+
+in
+
+val algebra_method = ((Scan.optional (keyword addN |-- thms) []) -- 
+   (Scan.optional (keyword delN |-- thms) [])) >>
+  (fn (add_ths, del_ths) => fn ctxt =>
+       SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt))
 
 end;
+
+end;