src/HOL/Divides.thy
changeset 54227 63b441f49645
parent 54226 e3df2a4e02fc
child 54230 b1d955791529
     1.1 --- a/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -2620,11 +2620,6 @@
     1.4    "Suc 0 mod numeral v' = nat (1 mod numeral v')"
     1.5    by (subst nat_mod_distrib) simp_all
     1.6  
     1.7 -lemma mod_2_not_eq_zero_eq_one_int:
     1.8 -  fixes k :: int
     1.9 -  shows "k mod 2 \<noteq> 0 \<longleftrightarrow> k mod 2 = 1"
    1.10 -  by auto
    1.11 -
    1.12  instance int :: semiring_numeral_div
    1.13    by intro_classes (auto intro: zmod_le_nonneg_dividend
    1.14      simp add: zmult_div_cancel