src/HOL/Presburger.thy
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 30656 ddb1fafa2dcb
     1.1 --- a/src/HOL/Presburger.thy	Mon Mar 16 17:51:24 2009 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Mon Mar 16 18:24:30 2009 +0100
     1.3 @@ -455,12 +455,11 @@
     1.4   val any_keyword = keyword addN || keyword delN || simple_keyword elimN
     1.5   val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
     1.6  in
     1.7 -  fn src => Method.syntax 
     1.8 -   ((Scan.optional (simple_keyword elimN >> K false) true) -- 
     1.9 -    (Scan.optional (keyword addN |-- thms) []) -- 
    1.10 -    (Scan.optional (keyword delN |-- thms) [])) src 
    1.11 -  #> (fn (((elim, add_ths), del_ths),ctxt) => 
    1.12 -         SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
    1.13 +  Scan.optional (simple_keyword elimN >> K false) true --
    1.14 +  Scan.optional (keyword addN |-- thms) [] --
    1.15 +  Scan.optional (keyword delN |-- thms) [] >>
    1.16 +  (fn ((elim, add_ths), del_ths) => fn ctxt =>
    1.17 +    SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
    1.18  end
    1.19  *} "Cooper's algorithm for Presburger arithmetic"
    1.20