1.1 --- a/src/HOL/Transcendental.thy	Fri Aug 19 08:39:43 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Fri Aug 19 08:40:15 2011 -0700
     1.3 @@ -1268,28 +1268,6 @@
     1.4  apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
     1.5  done
     1.6  
     1.7 -lemma lemma_STAR_sin:
     1.8 -     "(if even n then 0
     1.9 -       else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0"
    1.10 -by (induct "n", auto)
    1.11 -
    1.12 -lemma lemma_STAR_cos:
    1.13 -     "0 < n -->
    1.14 -      -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
    1.15 -by (induct "n", auto)
    1.16 -
    1.17 -lemma lemma_STAR_cos1:
    1.18 -     "0 < n -->
    1.19 -      (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
    1.20 -by (induct "n", auto)
    1.21 -
    1.22 -lemma lemma_STAR_cos2:
    1.23 -  "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) *  0 ^ n
    1.24 -                         else 0) = 0"
    1.25 -apply (induct "n")
    1.26 -apply (case_tac [2] "n", auto)
    1.27 -done
    1.28 -
    1.29  lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)"
    1.30  unfolding sin_def by (rule summable_sin [THEN summable_sums])
    1.31