--- a/src/HOL/Hyperreal/MacLaurin.thy Tue Jun 05 00:54:03 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy Tue Jun 05 07:58:50 2007 +0200
@@ -420,7 +420,7 @@
apply safe
apply (simp (no_asm))
apply (simp (no_asm))
-apply (case_tac "n", clarify, simp, simp)
+apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
--- a/src/HOL/Hyperreal/Transcendental.thy Tue Jun 05 00:54:03 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy Tue Jun 05 07:58:50 2007 +0200
@@ -516,22 +516,22 @@
apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
done
-lemma lemma_STAR_sin [simp]:
+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 [simp]:
+lemma lemma_STAR_cos:
"0 < n -->
-1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
by (induct "n", auto)
-lemma lemma_STAR_cos1 [simp]:
+lemma lemma_STAR_cos1:
"0 < n -->
(-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0"
by (induct "n", auto)
-lemma lemma_STAR_cos2 [simp]:
+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")
@@ -1001,7 +1001,7 @@
lemma sin_zero [simp]: "sin 0 = 0"
by (auto intro!: sums_unique [symmetric] LIMSEQ_const
- simp add: sin_def sums_def simp del: power_0_left)
+ simp add: sin_def sums_def lemma_STAR_sin)
lemma lemma_series_zero2:
"(\<forall>m. n \<le> m --> f m = 0) --> f sums setsum f {0..<n}"