src/HOL/Integ/Presburger.thy
changeset 14941 1edb674e0c33
parent 14758 af3b71a46a1c
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Integ/Presburger.thy	Mon Jun 14 14:20:55 2004 +0200
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Mon Jun 14 16:46:48 2004 +0200
     1.3 @@ -985,6 +985,9 @@
     1.4    by (simp cong: conj_cong)
     1.5  
     1.6  use "cooper_dec.ML"
     1.7 +oracle
     1.8 +  presburger_oracle = CooperDec.mk_presburger_oracle
     1.9 +
    1.10  use "cooper_proof.ML"
    1.11  use "qelim.ML"
    1.12  use "presburger.ML"