diff -r ebdd5508f386 -r d4312962161a src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon Jun 25 14:06:50 2018 +0100
+++ b/src/HOL/Complex.thy	Tue Jun 26 14:51:18 2018 +0100
@@ -211,7 +211,7 @@
     by simp
   also from insert.prems have "f x \<in> \<real>" by simp
   hence "Im (f x) = 0" by (auto elim!: Reals_cases)
-  also have "Re (prod f A) = (\<Prod>x\<in>A. Re (f x))" 
+  also have "Re (prod f A) = (\<Prod>x\<in>A. Re (f x))"
     by (intro insert.IH insert.prems) auto
   finally show ?case using insert.hyps by simp
 qed auto
@@ -590,6 +590,9 @@
 lemma complex_mult_cnj: "z * cnj z = complex_of_real ((Re z)\<^sup>2 + (Im z)\<^sup>2)"
   by (simp add: complex_eq_iff power2_eq_square)
 
+lemma cnj_add_mult_eq_Re: "z * cnj w + cnj z * w = 2 * Re (z * cnj w)"
+  by (rule complex_eqI) auto
+
 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<^sup>2"
   by (simp add: norm_mult power2_eq_square)
 
@@ -796,7 +799,7 @@
 lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im (cis a ^ n)"
   by (auto simp add: DeMoivre)
 
-lemma cis_pi: "cis pi = -1"
+lemma cis_pi [simp]: "cis pi = -1"
   by (simp add: complex_eq_iff)
 
 
@@ -976,7 +979,7 @@
 
 lemma bij_betw_roots_unity:
   assumes "n > 0"
-  shows   "bij_betw (\<lambda>k. cis (2 * pi * real k / real n)) {..<n} {z. z ^ n = 1}" 
+  shows   "bij_betw (\<lambda>k. cis (2 * pi * real k / real n)) {..<n} {z. z ^ n = 1}"
     (is "bij_betw ?f _ _")
   unfolding bij_betw_def
 proof (intro conjI)
@@ -1015,7 +1018,7 @@
   finally have card: "card {z::complex. z ^ n = 1} = n"
     using assms by (intro antisym card_roots_unity) auto
 
-  have "card (?f ` {..<n}) = card {z::complex. z ^ n = 1}" 
+  have "card (?f ` {..<n}) = card {z::complex. z ^ n = 1}"
     using card inj by (subst card_image) auto
   with subset and assms show "?f ` {..<n} = {z::complex. z ^ n = 1}"
     by (intro card_subset_eq finite_roots_unity) auto
@@ -1219,12 +1222,7 @@
 
 text \<open>Legacy theorem names\<close>
 
-lemmas expand_complex_eq = complex_eq_iff
-lemmas complex_Re_Im_cancel_iff = complex_eq_iff
-lemmas complex_equality = complex_eqI
 lemmas cmod_def = norm_complex_def
-lemmas complex_norm_def = norm_complex_def
-lemmas complex_divide_def = divide_complex_def
 
 lemma legacy_Complex_simps:
   shows Complex_eq_0: "Complex a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"