src/HOL/Presburger.thy
changeset 28967 3bdb1eae352c
parent 28402 09e4aa3ddc25
child 29667 53103fc8ffa3
     1.1 --- a/src/HOL/Presburger.thy	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/HOL/Presburger.thy	Wed Dec 03 21:50:36 2008 -0800
     1.3 @@ -411,7 +411,7 @@
     1.4    by (simp cong: conj_cong)
     1.5  lemma int_eq_number_of_eq:
     1.6    "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
     1.7 -  by simp
     1.8 +  by (rule eq_number_of_eq)
     1.9  
    1.10  lemma mod_eq0_dvd_iff[presburger]: "(m::nat) mod n = 0 \<longleftrightarrow> n dvd m"
    1.11  unfolding dvd_eq_mod_eq_0[symmetric] ..