src/HOL/Presburger.thy
changeset 24075 366d4d234814
parent 23856 ebec38420a85
child 24094 6db35c14146d
     1.1 --- a/src/HOL/Presburger.thy	Mon Jul 30 19:46:15 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Tue Jul 31 00:56:26 2007 +0200
     1.3 @@ -439,8 +439,8 @@
     1.4  
     1.5  use "Tools/Qelim/presburger.ML"
     1.6  
     1.7 -setup {* 
     1.8 -  arith_tactic_add 
     1.9 +declaration {* fn _ =>
    1.10 +  arith_tactic_add
    1.11      (mk_arith_tactic "presburger" (fn i => fn st =>
    1.12         (warning "Trying Presburger arithmetic ...";   
    1.13      Presburger.cooper_tac true [] [] ((ProofContext.init o theory_of_thm) st) i st)))