| changeset 30510 | 4120fc59dd85 | 
| parent 30242 | aea5d7fa7ef5 | 
| child 30549 | d2d7874648bd | 
--- a/src/HOL/Presburger.thy Fri Mar 13 19:53:09 2009 +0100 +++ b/src/HOL/Presburger.thy Fri Mar 13 19:58:26 2009 +0100 @@ -460,7 +460,7 @@ (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"