--- a/src/HOL/Presburger.thy Wed Sep 14 10:24:39 2005 +0200
+++ b/src/HOL/Presburger.thy Wed Sep 14 17:25:52 2005 +0200
@@ -10,7 +10,8 @@
theory Presburger
imports NatSimprocs SetInterval
-uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML") ("presburger.ML")
+uses ("cooper_dec.ML") ("cooper_proof.ML") ("qelim.ML")
+ ("reflected_presburger.ML") ("reflected_cooper.ML") ("presburger.ML")
begin
text {* Theorem for unitifying the coeffitients of @{text x} in an existential formula*}
@@ -982,8 +983,10 @@
by (simp cong: conj_cong)
use "cooper_dec.ML"
+use "reflected_presburger.ML"
+use "reflected_cooper.ML"
oracle
- presburger_oracle ("term") = CooperDec.presburger_oracle
+ presburger_oracle ("term") = ReflectedCooper.presburger_oracle
use "cooper_proof.ML"
use "qelim.ML"