src/HOL/Presburger.thy
changeset 36799 628fe06cbeff
parent 36798 3981db162131
child 36800 59b50c691b75
--- a/src/HOL/Presburger.thy	Mon May 10 13:58:18 2010 +0200
+++ b/src/HOL/Presburger.thy	Mon May 10 14:11:50 2010 +0200
@@ -398,14 +398,15 @@
 
 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')" 
   by (simp cong: conj_cong)
+
 lemma int_eq_number_of_eq:
   "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   by (rule eq_number_of_eq)
 
 use "Tools/Qelim/cooper.ML"
 
-setup CooperData.setup
-oracle linzqe_oracle = Coopereif.cooper_oracle
+setup Cooper.setup
+oracle linzqe_oracle = Cooper.cooper_oracle
 
 use "Tools/Qelim/presburger.ML"