# HG changeset patch
# User chaieb
# Date 1181636132 -7200
# Node ID b91295432e6d9ac53b11d79d6586319cecc3aa4d
# Parent  da040caa059654d9cc5a05b1042a3ef05c9b6a3e
algebra_tac moved to file Tools/Groebner_Basis/groebner.ML; Method now takes theorems to be added or deleted from a simpset for simplificatio *before* the core method starts

diff -r da040caa0596 -r b91295432e6d src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Mon Jun 11 18:34:12 2007 +0200
+++ b/src/HOL/Groebner_Basis.thy	Tue Jun 12 10:15:32 2007 +0200
@@ -4,7 +4,6 @@
 *)
 
 header {* Semiring normalization and Groebner Bases *}
-
 theory Groebner_Basis
 imports NatBin
 uses
@@ -14,6 +13,8 @@
   ("Tools/Groebner_Basis/groebner.ML")
 begin
 
+
+
 subsection {* Semiring normalization *}
 
 setup NormalizerData.setup
@@ -436,23 +437,22 @@
 
 use "Tools/Groebner_Basis/groebner.ML"
 
-ML {*
-  fun algebra_tac ctxt i = ObjectLogic.full_atomize_tac i 
-  THEN (fn st =>
-   case try (nth (cprems_of st)) (i - 1) of
-    NONE => no_tac st
-  | SOME p => let val th = Groebner.ring_conv ctxt (Thm.dest_arg p)
-              in rtac th i st end
-              handle TERM _ => no_tac st
-              handle THM _ => no_tac st
-              handle ERROR _ => no_tac st
-              handle CTERM _ => no_tac st);
-*}
+method_setup algebra =
+{* 
+let
+ 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
+fn src => Method.syntax 
+    ((Scan.optional (keyword addN |-- thms) []) -- 
+    (Scan.optional (keyword delN |-- thms) [])) src 
+ #> (fn ((add_ths, del_ths), ctxt) => 
+       Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
+end
 
-method_setup algebra = {*
-  Method.ctxt_args (Method.SIMPLE_METHOD' o algebra_tac)
 *} ""
 
-
-
 end