src/HOL/Complex.thy
changeset 44823 6ce95c8c0ba8
parent 44764 264436dd9491
child 44824 34b83d981380
     1.1 --- a/src/HOL/Complex.thy	Wed Sep 07 09:45:39 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Wed Sep 07 10:04:07 2011 -0700
     1.3 @@ -621,13 +621,6 @@
     1.4  lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
     1.5    by (simp add: rcis_def cis_def)
     1.6  
     1.7 -lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>"
     1.8 -proof -
     1.9 -  have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)"
    1.10 -    by (simp only: power_mult_distrib right_distrib)
    1.11 -  thus ?thesis by simp
    1.12 -qed
    1.13 -
    1.14  lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
    1.15    by (simp add: rcis_def cis_def norm_mult)
    1.16