src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -2620,11 +2620,6 @@
   "Suc 0 mod numeral v' = nat (1 mod numeral v')"
   by (subst nat_mod_distrib) simp_all
 
-lemma mod_2_not_eq_zero_eq_one_int:
-  fixes k :: int
-  shows "k mod 2 \<noteq> 0 \<longleftrightarrow> k mod 2 = 1"
-  by auto
-
 instance int :: semiring_numeral_div
   by intro_classes (auto intro: zmod_le_nonneg_dividend
     simp add: zmult_div_cancel