1.1 --- a/src/HOL/Transcendental.thy	Fri Aug 19 18:06:27 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Aug 19 18:08:05 2011 -0700
     1.3 @@ -2401,9 +2401,6 @@
     1.4  lemma tan_60: "tan (pi / 3) = sqrt 3"
     1.5  unfolding tan_def by (simp add: sin_60 cos_60)
     1.6  
     1.7 -lemma DERIV_sin_add: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
     1.8 -  by (auto intro!: DERIV_intros) (* TODO: delete *)
     1.9 -
    1.10  lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
    1.11  proof -
    1.12    have "sin ((real n + 1/2) * pi) = cos (real n * pi)"