changeset 69597 | ff784d5a5bfb |
parent 68611 | 4bc4b5c0ccfc |
child 70228 | 2d5b122aa0ff |
--- a/src/HOL/Nonstandard_Analysis/HLim.thy Sat Jan 05 17:00:43 2019 +0100 +++ b/src/HOL/Nonstandard_Analysis/HLim.thy Sat Jan 05 17:24:33 2019 +0100 @@ -108,7 +108,7 @@ by (simp add: NSLIM_def) -subsubsection \<open>Equivalence of @{term filterlim} and @{term NSLIM}\<close> +subsubsection \<open>Equivalence of \<^term>\<open>filterlim\<close> and \<^term>\<open>NSLIM\<close>\<close> lemma LIM_NSLIM: assumes f: "f \<midarrow>a\<rightarrow> L"