src/HOL/Nonstandard_Analysis/HTranscendental.thy

 imports Complex_Main HSeries HDeriv
 begin
 
 definition
   exphr :: "real => hypreal" where
-    \<comment>\<open>define exponential function using standard part\<close>
+    \<comment> \<open>define exponential function using standard part\<close>
   "exphr x =  st(sumhr (0, whn, %n. inverse (fact n) * (x ^ n)))"
 
 definition
   sinhr :: "real => hypreal" where
   "sinhr x = st(sumhr (0, whn, %n. sin_coeff n * x ^ n))"

 apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
             add.assoc [symmetric] numeral_2_eq_2)
 done
 
 lemma STAR_cos_Infinitesimal_approx2:
-  fixes x :: hypreal  \<comment>\<open>perhaps could be generalised, like many other hypreal results\<close>
+  fixes x :: hypreal  \<comment> \<open>perhaps could be generalised, like many other hypreal results\<close>
   shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
 apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult
             simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
 done