# HG changeset patch
# User huffman
# Date 1313802485 25200
# Node ID 425c1f8f9487718f8e5c139adcb14bcfdd9cf2be
# Parent  b7e9fa025f153ebd227e21da9f452e6db58c39b0
remove unused lemma DERIV_sin_add

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