src/HOL/NSA/HTranscendental.thy

     Copyright   : 2001 University of Edinburgh
 
 Converted to Isar and polished by lcp
 *)
 
-section{*Nonstandard Extensions of Transcendental Functions*}
+section\<open>Nonstandard Extensions of Transcendental Functions\<close>
 
 theory HTranscendental
 imports Transcendental HSeries HDeriv
 begin
 
 definition
   exphr :: "real => hypreal" where
-    --{*define exponential function using standard part *}
+    \<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))"

 definition
   coshr :: "real => hypreal" where
   "coshr x = st(sumhr (0, whn, %n. cos_coeff n * x ^ n))"
 
 
-subsection{*Nonstandard Extension of Square Root Function*}
+subsection\<open>Nonstandard Extension of Square Root Function\<close>
 
 lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
 by (simp add: starfun star_n_zero_num)
 
 lemma STAR_sqrt_one [simp]: "( *f* sqrt) 1 = 1"

 lemma NSLIMSEQ_sin_cos_pi:
      "(%n. real n * sin (pi / real n) * cos (pi / real n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S pi"
 by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
 
 
-text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
+text\<open>A familiar approximation to @{term "cos x"} when @{term x} is small\<close>
 
 lemma STAR_cos_Infinitesimal_approx:
   fixes x :: "'a::{real_normed_field,banach} star"
   shows "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x\<^sup>2"
 apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
 apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
             add.assoc [symmetric] numeral_2_eq_2)
 done
 
 lemma STAR_cos_Infinitesimal_approx2:
-  fixes x :: hypreal  --{*perhaps could be generalised, like many other hypreal results*}
+  fixes x :: hypreal  \<comment>\<open>perhaps could be generalised, like many other hypreal results\<close>
   shows "x \<in> Infinitesimal ==> ( *f* cos) x @= 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