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