--- a/src/HOL/Complex.thy Tue Sep 06 13:16:46 2011 -0700
+++ b/src/HOL/Complex.thy Tue Sep 06 14:53:51 2011 -0700
@@ -528,12 +528,6 @@
lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
by (simp add: sgn_div_norm divide_inverse scaleR_conv_of_real mult_commute)
-lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
- by (simp add: i_def complex_of_real_def)
-
-lemma i_mult_eq2 [simp]: "ii * ii = -(1::complex)"
- by (simp add: i_def complex_one_def)
-
lemma complex_eq_cancel_iff2 [simp]:
shows "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
by (simp add: complex_of_real_def)
--- a/src/HOL/NSA/NSComplex.thy Tue Sep 06 13:16:46 2011 -0700
+++ b/src/HOL/NSA/NSComplex.thy Tue Sep 06 14:53:51 2011 -0700
@@ -163,8 +163,8 @@
apply (simp add: minus_equation_iff [of x y])
done
-lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
-by transfer (rule i_mult_eq2)
+lemma hcomplex_i_mult_eq [simp]: "iii * iii = -1"
+by transfer (rule i_squared)
lemma hcomplex_i_mult_left [simp]: "!!z. iii * (iii * z) = -z"
by transfer (rule complex_i_mult_minus)