src/HOL/Transcendental.thy
changeset 44307 6a383003d0a9
parent 44305 3bdc02eb1637
child 44308 d2a6f9af02f4
--- 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])