src/HOL/Nonstandard_Analysis/HTranscendental.thy
changeset 69597 ff784d5a5bfb
parent 68611 4bc4b5c0ccfc
child 70208 65b3bfc565b5
     1.1 --- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Sat Jan 05 17:00:43 2019 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Sat Jan 05 17:24:33 2019 +0100
     1.3 @@ -592,7 +592,7 @@
     1.4  by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
     1.5  
     1.6  
     1.7 -text\<open>A familiar approximation to @{term "cos x"} when @{term x} is small\<close>
     1.8 +text\<open>A familiar approximation to \<^term>\<open>cos x\<close> when \<^term>\<open>x\<close> is small\<close>
     1.9  
    1.10  lemma STAR_cos_Infinitesimal_approx:
    1.11    fixes x :: "'a::{real_normed_field,banach} star"