diff -r 2690b6de5021 -r 6ce95c8c0ba8 src/HOL/Complex.thy
--- 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)