--- a/src/HOL/Transcendental.thy Fri Aug 19 08:39:43 2011 -0700
+++ b/src/HOL/Transcendental.thy Fri Aug 19 08:40:15 2011 -0700
@@ -1268,28 +1268,6 @@
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
done
-lemma lemma_STAR_sin:
- "(if even n then 0
- else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos:
- "0 < n -->
- -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos1:
- "0 < n -->
- (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
-by (induct "n", auto)
-
-lemma lemma_STAR_cos2:
- "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) * 0 ^ n
- else 0) = 0"
-apply (induct "n")
-apply (case_tac [2] "n", auto)
-done
-
lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
unfolding sin_def by (rule summable_sin [THEN summable_sums])