| changeset 16836 | 45a3dc4688bc |
| parent 16417 | 9bc16273c2d4 |
| child 17378 | 105519771c67 |
--- a/src/HOL/Presburger.thy Thu Jul 14 19:28:17 2005 +0200 +++ b/src/HOL/Presburger.thy Thu Jul 14 19:28:18 2005 +0200 @@ -983,7 +983,7 @@ use "cooper_dec.ML" oracle - presburger_oracle = CooperDec.mk_presburger_oracle + presburger_oracle ("term") = CooperDec.presburger_oracle use "cooper_proof.ML" use "qelim.ML"