diff -r 5f612b6d64a8 -r b09f3ad3208f src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu May 06 17:59:20 2010 +0200
+++ b/src/HOL/Int.thy	Thu May 06 18:16:07 2010 +0200
@@ -1063,20 +1063,24 @@
 
 text {* First version by Norbert Voelker *}
 
-definition (*for simplifying equalities*)
-  iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
-where
+definition (*for simplifying equalities*) iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool" where
   "iszero z \<longleftrightarrow> z = 0"
 
 lemma iszero_0: "iszero 0"
-by (simp add: iszero_def)
-
-lemma not_iszero_1: "~ iszero 1"
-by (simp add: iszero_def eq_commute)
+  by (simp add: iszero_def)
+
+lemma iszero_Numeral0: "iszero (Numeral0 :: 'a::number_ring)"
+  by (simp add: iszero_0)
+
+lemma not_iszero_1: "\<not> iszero 1"
+  by (simp add: iszero_def)
+
+lemma not_iszero_Numeral1: "\<not> iszero (Numeral1 :: 'a::number_ring)"
+  by (simp add: not_iszero_1)
 
 lemma eq_number_of_eq [simp]:
   "((number_of x::'a::number_ring) = number_of y) =
-   iszero (number_of (x + uminus y) :: 'a)"
+     iszero (number_of (x + uminus y) :: 'a)"
 unfolding iszero_def number_of_add number_of_minus
 by (simp add: algebra_simps)