--- a/src/HOL/Complex/Complex.thy Thu May 10 03:00:15 2007 +0200
+++ b/src/HOL/Complex/Complex.thy Thu May 10 03:07:26 2007 +0200
@@ -744,16 +744,6 @@
lemma complex_number_of [simp]: "complex_of_real (number_of w) = number_of w"
by (rule of_real_number_of_eq)
-text{*This theorem is necessary because theorems such as
- @{text iszero_number_of_0} only hold for ordered rings. They cannot
- be generalized to fields in general because they fail for finite fields.
- They work for type complex because the reals can be embedded in them.*}
-(* TODO: generalize and move to Real/RealVector.thy *)
-lemma iszero_complex_number_of [simp]:
- "iszero (number_of w :: complex) = iszero (number_of w :: real)"
-by (simp only: complex_of_real_zero_iff complex_number_of [symmetric]
- iszero_def)
-
lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v"
by (simp only: complex_number_of [symmetric] complex_cnj_complex_of_real)
--- a/src/HOL/Complex/NSComplex.thy Thu May 10 03:00:15 2007 +0200
+++ b/src/HOL/Complex/NSComplex.thy Thu May 10 03:07:26 2007 +0200
@@ -659,15 +659,6 @@
"hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)"
by transfer (rule complex_number_of [symmetric])
-text{*This theorem is necessary because theorems such as
- @{text iszero_number_of_0} only hold for ordered rings. They cannot
- be generalized to fields in general because they fail for finite fields.
- They work for type complex because the reals can be embedded in them.*}
-lemma iszero_hcomplex_number_of [simp]:
- "iszero (number_of w :: hcomplex) = iszero (number_of w :: real)"
-by (transfer iszero_def, simp)
-
-
(*
Goal "z + hcnj z =
hcomplex_of_hypreal (2 * hRe(z))"