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