src/HOL/Hyperreal/HTranscendental.thy
changeset 23177 3004310c95b1
parent 23114 1bd84606b403
child 27148 5b78e50adc49
     1.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Thu May 31 22:23:50 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu May 31 23:02:16 2007 +0200
     1.3 @@ -421,7 +421,7 @@
     1.4  
     1.5  lemma HFinite_sin [simp]:
     1.6       "sumhr (0, whn, %n. (if even(n) then 0 else  
     1.7 -              ((- 1) ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
     1.8 +              (-1 ^ ((n - 1) div 2))/(real (fact n))) * x ^ n)  
     1.9                \<in> HFinite"
    1.10  unfolding sumhr_app
    1.11  apply (simp only: star_zero_def starfun2_star_of)
    1.12 @@ -447,7 +447,7 @@
    1.13  
    1.14  lemma HFinite_cos [simp]:
    1.15       "sumhr (0, whn, %n. (if even(n) then  
    1.16 -            ((- 1) ^ (n div 2))/(real (fact n)) else  
    1.17 +            (-1 ^ (n div 2))/(real (fact n)) else  
    1.18              0) * x ^ n) \<in> HFinite"
    1.19  unfolding sumhr_app
    1.20  apply (simp only: star_zero_def starfun2_star_of)