# HG changeset patch
# User huffman
# Date 1315346031 25200
# Node ID 264436dd949106a22d935fef05a06321d94ab255
# Parent  0694fc3248fdec2aabaa18589d3b8f0aff1716aa
remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared

diff -r 0694fc3248fd -r 264436dd9491 src/HOL/Complex.thy
--- 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)
diff -r 0694fc3248fd -r 264436dd9491 src/HOL/NSA/NSComplex.thy
--- 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)