diff -r 38975527c757 -r e55503200061 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Thu Sep 08 11:31:53 2011 +0200
+++ b/src/HOL/Complex.thy	Thu Sep 08 07:06:59 2011 -0700
@@ -253,6 +253,10 @@
   shows "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
   by (simp add: complex_of_real_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)
+
 lemma complex_split_polar:
      "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
   by (simp add: complex_eq_iff polar_Ex)
@@ -539,10 +543,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 complex_eq_cancel_iff2 [simp]:
-  shows "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
-  by (simp add: complex_of_real_def)
-
 lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
   by (simp add: complex_sgn_def divide_inverse)