diff -r 54d231cbc19a -r 2f5e8d70a179 src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Thu May 10 00:39:56 2007 +0200
+++ b/src/HOL/Integ/Numeral.thy	Thu May 10 02:51:53 2007 +0200
@@ -368,9 +368,28 @@
 
 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
 
+lemma Ints_double_eq_0_iff:
+  assumes in_Ints: "a \<in> Ints"
+  shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
+proof -
+  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
+  then obtain z where a: "a = of_int z" ..
+  show ?thesis
+  proof
+    assume "a = 0"
+    thus "a + a = 0" by simp
+  next
+    assume eq: "a + a = 0"
+    hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
+    hence "z + z = 0" by (simp only: of_int_eq_iff)
+    hence "z = 0" by (simp only: double_eq_0_iff)
+    thus "a = 0" by (simp add: a)
+  qed
+qed
+
 lemma Ints_odd_nonzero:
   assumes in_Ints: "a \<in> Ints"
-  shows "1 + a + a \<noteq> (0::'a::ordered_idom)"
+  shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
 proof -
   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
   then obtain z where a: "a = of_int z" ..
@@ -389,17 +408,17 @@
 
 lemma iszero_number_of_BIT:
   "iszero (number_of (w BIT x)::'a) = 
-   (x = B0 \<and> iszero (number_of w::'a::{ordered_idom,number_ring}))"
-  by (simp add: iszero_def number_of_eq numeral_simps double_eq_0_iff 
+   (x = B0 \<and> iszero (number_of w::'a::{ring_char_0,number_ring}))"
+  by (simp add: iszero_def number_of_eq numeral_simps Ints_double_eq_0_iff 
     Ints_odd_nonzero Ints_def split: bit.split)
 
 lemma iszero_number_of_0:
-  "iszero (number_of (w BIT B0) :: 'a::{ordered_idom,number_ring}) = 
+  "iszero (number_of (w BIT B0) :: 'a::{ring_char_0,number_ring}) = 
   iszero (number_of w :: 'a)"
   by (simp only: iszero_number_of_BIT simp_thms)
 
 lemma iszero_number_of_1:
-  "~ iszero (number_of (w BIT B1)::'a::{ordered_idom,number_ring})"
+  "~ iszero (number_of (w BIT B1)::'a::{ring_char_0,number_ring})"
   by (simp add: iszero_number_of_BIT)