| changeset 20053 | 7f32ce6354d6 |
| parent 19277 | f7602e74d948 |
| child 20194 | c9dbce9a23a1 |
--- a/src/HOL/Integ/presburger.ML Sat Jul 08 12:54:40 2006 +0200 +++ b/src/HOL/Integ/presburger.ML Sat Jul 08 12:54:41 2006 +0200 @@ -30,7 +30,7 @@ (*-----------------------------------------------------------------*) -val presburger_ss = simpset_of (theory "Presburger"); +val presburger_ss = simpset (); val binarith = map thm ["Pls_0_eq", "Min_1_eq", "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",