--- a/src/HOL/Complex.thy Wed Sep 07 09:45:39 2011 -0700
+++ b/src/HOL/Complex.thy Wed Sep 07 10:04:07 2011 -0700
@@ -621,13 +621,6 @@
lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
by (simp add: rcis_def cis_def)
-lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>"
-proof -
- have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)"
- by (simp only: power_mult_distrib right_distrib)
- thus ?thesis by simp
-qed
-
lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
by (simp add: rcis_def cis_def norm_mult)