| changeset 14941 | 1edb674e0c33 |
| parent 14758 | af3b71a46a1c |
| child 14981 | e73f8140af78 |
--- a/src/HOL/Presburger.thy Mon Jun 14 14:20:55 2004 +0200 +++ b/src/HOL/Presburger.thy Mon Jun 14 16:46:48 2004 +0200 @@ -985,6 +985,9 @@ by (simp cong: conj_cong) use "cooper_dec.ML" +oracle + presburger_oracle = CooperDec.mk_presburger_oracle + use "cooper_proof.ML" use "qelim.ML" use "presburger.ML"