diff -r afaa031ed4da -r 105519771c67 src/HOL/Presburger.thy
--- 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"