--- a/src/HOL/Complex/NSComplex.thy Mon Mar 01 11:52:59 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy Mon Mar 01 13:51:21 2004 +0100
@@ -394,13 +394,6 @@
by (rule hcomplex_zero_not_eq_one)
show "(u + v) * w = u * w + v * w"
by (simp add: hcomplex_add_mult_distrib)
- show "z+u = z+v ==> u=v"
- proof -
- assume eq: "z+u = z+v"
- hence "(-z + z) + u = (-z + z) + v" by (simp only: eq hcomplex_add_assoc)
- thus "u = v"
- by (simp only: hcomplex_add_minus_left hcomplex_add_zero_left)
- qed
assume neq: "w \<noteq> 0"
thus "z / w = z * inverse w"
by (simp add: hcomplex_divide_def)