1.1 --- a/src/HOL/Complex.thy	Fri Aug 19 18:08:05 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Fri Aug 19 18:42:41 2011 -0700
     1.3 @@ -606,14 +606,6 @@
     1.4  abbreviation expi :: "complex \<Rightarrow> complex"
     1.5    where "expi \<equiv> exp"
     1.6  
     1.7 -lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
     1.8 -  unfolding cos_coeff_def sin_coeff_def
     1.9 -  by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
    1.10 -
    1.11 -lemma sin_coeff_Suc: "sin_coeff (Suc n) = cos_coeff n / real (Suc n)"
    1.12 -  unfolding cos_coeff_def sin_coeff_def
    1.13 -  by (simp del: mult_Suc)
    1.14 -
    1.15  lemma expi_imaginary: "expi (Complex 0 b) = cis b"
    1.16  proof (rule complex_eqI)
    1.17    { fix n have "Complex 0 b ^ n =