--- a/src/HOL/Topological_Spaces.thy Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Topological_Spaces.thy Fri Jan 04 23:22:53 2019 +0100
@@ -725,7 +725,7 @@
setup \<open>
Global_Theory.add_thms_dynamic (\<^binding>\<open>tendsto_eq_intros\<close>,
fn context =>
- Named_Theorems.get (Context.proof_of context) @{named_theorems tendsto_intros}
+ Named_Theorems.get (Context.proof_of context) \<^named_theorems>\<open>tendsto_intros\<close>
|> map_filter (try (fn thm => @{thm tendsto_eq_rhs} OF [thm])))
\<close>
@@ -1027,7 +1027,7 @@
using UV by auto
qed
-subsubsection \<open>Rules about @{const Lim}\<close>
+subsubsection \<open>Rules about \<^const>\<open>Lim\<close>\<close>
lemma tendsto_Lim: "\<not> trivial_limit net \<Longrightarrow> (f \<longlongrightarrow> l) net \<Longrightarrow> Lim net f = l"
unfolding Lim_def using tendsto_unique [of net f] by auto