src/HOL/Presburger.thy
changeset 30686 47a32dd1b86e
parent 30656 ddb1fafa2dcb
child 31790 05c92381363c
--- a/src/HOL/Presburger.thy	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Presburger.thy	Mon Mar 23 19:01:16 2009 +0100
@@ -439,12 +439,7 @@
 
 use "Tools/Qelim/presburger.ML"
 
-declaration {* fn _ =>
-  arith_tactic_add
-    (mk_arith_tactic "presburger" (fn ctxt => fn i => fn st =>
-       (warning "Trying Presburger arithmetic ...";   
-    Presburger.cooper_tac true [] [] ctxt i st)))
-*}
+setup {* Arith_Data.add_tactic "Presburger arithmetic" (K (Presburger.cooper_tac true [] [])) *}
 
 method_setup presburger = {*
 let