src/HOL/MacLaurin.thy
changeset 44319 806e0390de53
parent 44308 d2a6f9af02f4
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/MacLaurin.thy	Fri Aug 19 18:08:05 2011 -0700
     1.2 +++ b/src/HOL/MacLaurin.thy	Fri Aug 19 18:42:41 2011 -0700
     1.3 @@ -417,9 +417,6 @@
     1.4        cos (x + real (m) * pi / 2)"
     1.5  by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
     1.6  
     1.7 -lemma sin_coeff_0 [simp]: "sin_coeff 0 = 0"
     1.8 -  unfolding sin_coeff_def by simp (* TODO: move *)
     1.9 -
    1.10  lemma Maclaurin_sin_expansion2:
    1.11       "\<exists>t. abs t \<le> abs x &
    1.12         sin x =
    1.13 @@ -486,9 +483,6 @@
    1.14  
    1.15  subsection{*Maclaurin Expansion for Cosine Function*}
    1.16  
    1.17 -lemma cos_coeff_0 [simp]: "cos_coeff 0 = 1"
    1.18 -  unfolding cos_coeff_def by simp (* TODO: move *)
    1.19 -
    1.20  lemma sumr_cos_zero_one [simp]:
    1.21    "(\<Sum>m=0..<(Suc n). cos_coeff m * 0 ^ m) = 1"
    1.22  by (induct "n", auto)