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
```