--- 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;