# HG changeset patch
# User chaieb
# Date 1181636140 -7200
# Node ID ec5b4ab52026149a058412dc9a811d76dc9a4aea
# Parent  b91295432e6d9ac53b11d79d6586319cecc3aa4d
Method now takes theorems to be added or deleted from a simpset for simplificatio before the core method starts

diff -r b91295432e6d -r ec5b4ab52026 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Tue Jun 12 10:15:32 2007 +0200
+++ b/src/HOL/Presburger.thy	Tue Jun 12 10:15:40 2007 +0200
@@ -433,16 +433,28 @@
   arith_tactic_add 
     (mk_arith_tactic "presburger" (fn i => fn st =>
        (warning "Trying Presburger arithmetic ...";   
-    Presburger.cooper_tac true ((ProofContext.init o theory_of_thm) st) i st)))
+    Presburger.cooper_tac true [] [] ((ProofContext.init o theory_of_thm) st) i st)))
   (* FIXME!!!!!!! get the right context!!*)	
 *}
-method_setup presburger = {* Method.simple_args (Scan.optional (Args.$$$ "elim" >> K false) true)  
-  (fn q => fn ctxt =>  Method.SIMPLE_METHOD' (Presburger.cooper_tac q ctxt))*} ""
-(*
+
 method_setup presburger = {*
-  Method.ctxt_args (Method.SIMPLE_METHOD' o (Presburger.cooper_tac true))
+let
+ fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
+ fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
+ val addN = "add"
+ val delN = "del"
+ val elimN = "elim"
+ val any_keyword = keyword addN || keyword delN || simple_keyword elimN
+ val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+in
+  fn src => Method.syntax 
+   ((Scan.optional (simple_keyword elimN >> K false) true) -- 
+    (Scan.optional (keyword addN |-- thms) []) -- 
+    (Scan.optional (keyword delN |-- thms) [])) src 
+  #> (fn (((elim, add_ths), del_ths),ctxt) => 
+         Method.SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
+end
 *} ""
-*)
 
 subsection {* Code generator setup *}
 text {*