--- a/src/HOL/Hyperreal/HTranscendental.thy Thu May 31 22:23:50 2007 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy Thu May 31 23:02:16 2007 +0200
@@ -421,7 +421,7 @@
lemma HFinite_sin [simp]:
"sumhr (0, whn, %n. (if even(n) then 0 else
- ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)
+ (-1 ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)
\<in> HFinite"
unfolding sumhr_app
apply (simp only: star_zero_def starfun2_star_of)
@@ -447,7 +447,7 @@
lemma HFinite_cos [simp]:
"sumhr (0, whn, %n. (if even(n) then
- ((- 1) ^ (n div 2))/(real (fact n)) else
+ (-1 ^ (n div 2))/(real (fact n)) else
0) * x ^ n) \<in> HFinite"
unfolding sumhr_app
apply (simp only: star_zero_def starfun2_star_of)