src/HOL/Presburger.thy

   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))
+         SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
 end
 *} "Cooper's algorithm for Presburger arithmetic"
 
 lemma [presburger, algebra]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
 lemma [presburger, algebra]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger