| changeset 61971 | 720fa884656e |
| parent 61970 | 6226261144d7 |
| child 61975 | b4b11391c676 |
--- a/src/HOL/NSA/HTranscendental.thy Tue Dec 29 23:20:11 2015 +0100 +++ b/src/HOL/NSA/HTranscendental.thy Tue Dec 29 23:40:04 2015 +0100 @@ -406,7 +406,7 @@ (* -Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x" +Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S ln x" *) lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \<in> HFinite"