src/HOL/Nonstandard_Analysis/HTranscendental.thy
changeset 67443 3abf6a722518
parent 67091 1393c2340eec
child 68611 4bc4b5c0ccfc
     1.1 --- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Tue Jan 16 09:12:16 2018 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Tue Jan 16 09:30:00 2018 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  definition
     1.6    exphr :: "real => hypreal" where
     1.7 -    \<comment>\<open>define exponential function using standard part\<close>
     1.8 +    \<comment> \<open>define exponential function using standard part\<close>
     1.9    "exphr x =  st(sumhr (0, whn, %n. inverse (fact n) * (x ^ n)))"
    1.10  
    1.11  definition
    1.12 @@ -603,7 +603,7 @@
    1.13  done
    1.14  
    1.15  lemma STAR_cos_Infinitesimal_approx2:
    1.16 -  fixes x :: hypreal  \<comment>\<open>perhaps could be generalised, like many other hypreal results\<close>
    1.17 +  fixes x :: hypreal  \<comment> \<open>perhaps could be generalised, like many other hypreal results\<close>
    1.18    shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
    1.19  apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
    1.20  apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult