diff -r 5bce8ff0d9ae -r eb64ffccfc75 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon Aug 08 09:52:09 2011 -0700
+++ b/src/HOL/Complex.thy	Mon Aug 08 10:26:26 2011 -0700
@@ -25,14 +25,12 @@
 lemma complex_surj [simp]: "Complex (Re z) (Im z) = z"
   by (induct z) simp
 
-lemma complex_equality [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y"
+lemma complex_eqI [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y"
   by (induct x, induct y) simp
 
-lemma expand_complex_eq: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
+lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
   by (induct x, induct y) simp
 
-lemmas complex_Re_Im_cancel_iff = expand_complex_eq
-
 
 subsection {* Addition and Subtraction *}
 
@@ -152,7 +150,7 @@
   right_distrib left_distrib right_diff_distrib left_diff_distrib
   complex_inverse_def complex_divide_def
   power2_eq_square add_divide_distrib [symmetric]
-  expand_complex_eq)
+  complex_eq_iff)
 
 end
 
@@ -190,7 +188,7 @@
 
 lemma Complex_eq_number_of [simp]:
   "(Complex a b = number_of w) = (a = number_of w \<and> b = 0)"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 
 subsection {* Scalar Multiplication *}
@@ -215,17 +213,17 @@
 proof
   fix a b :: real and x y :: complex
   show "scaleR a (x + y) = scaleR a x + scaleR a y"
-    by (simp add: expand_complex_eq right_distrib)
+    by (simp add: complex_eq_iff right_distrib)
   show "scaleR (a + b) x = scaleR a x + scaleR b x"
-    by (simp add: expand_complex_eq left_distrib)
+    by (simp add: complex_eq_iff left_distrib)
   show "scaleR a (scaleR b x) = scaleR (a * b) x"
-    by (simp add: expand_complex_eq mult_assoc)
+    by (simp add: complex_eq_iff mult_assoc)
   show "scaleR 1 x = x"
-    by (simp add: expand_complex_eq)
+    by (simp add: complex_eq_iff)
   show "scaleR a x * y = scaleR a (x * y)"
-    by (simp add: expand_complex_eq algebra_simps)
+    by (simp add: complex_eq_iff algebra_simps)
   show "x * scaleR a y = scaleR a (x * y)"
-    by (simp add: expand_complex_eq algebra_simps)
+    by (simp add: complex_eq_iff algebra_simps)
 qed
 
 end
@@ -405,19 +403,19 @@
 by (simp add: i_def)
 
 lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_i_not_one [simp]: "ii \<noteq> 1"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_i_not_number_of [simp]: "ii \<noteq> number_of w"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma Complex_mult_i [simp]: "Complex a b * ii = Complex (- b) a"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r"
 by (simp add: i_def complex_of_real_def)
@@ -451,31 +449,31 @@
 by (simp add: cnj_def)
 
 lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
 by (simp add: cnj_def)
 
 lemma complex_cnj_zero [simp]: "cnj 0 = 0"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_cnj_minus: "cnj (- x) = - cnj x"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_cnj_one [simp]: "cnj 1 = 1"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)"
 by (simp add: complex_inverse_def)
@@ -487,34 +485,34 @@
 by (induct n, simp_all add: complex_cnj_mult)
 
 lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_cnj_of_int [simp]: "cnj (of_int z) = of_int z"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_cnj_number_of [simp]: "cnj (number_of w) = number_of w"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z"
 by (simp add: complex_norm_def)
 
 lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_cnj_i [simp]: "cnj ii = - ii"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re z)"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im z) * ii"
-by (simp add: expand_complex_eq)
+by (simp add: complex_eq_iff)
 
 lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
-by (simp add: expand_complex_eq power2_eq_square)
+by (simp add: complex_eq_iff power2_eq_square)
 
 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
 by (simp add: norm_mult power2_eq_square)
@@ -721,4 +719,10 @@
 lemma expi_two_pi_i [simp]: "expi((2::complex) * complex_of_real pi * ii) = 1"
 by (simp add: expi_def cis_def)
 
+text {* Legacy theorem names *}
+
+lemmas expand_complex_eq = complex_eq_iff
+lemmas complex_Re_Im_cancel_iff = complex_eq_iff
+lemmas complex_equality = complex_eqI
+
 end