# HG changeset patch
# User huffman
# Date 1313768415 25200
# Node ID 6a383003d0a98c7222f61f499da14ecb4d85b07f
# Parent  33572a766836ba6da23a413448e0dad4f60d398d
remove unused lemmas

diff -r 33572a766836 -r 6a383003d0a9 src/HOL/Transcendental.thy
--- 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])