--- a/src/HOL/Analysis/FPS_Convergence.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy Sat Jan 05 17:24:33 2019 +0100
@@ -17,7 +17,7 @@
subsection%unimportant \<open>Balls with extended real radius\<close>
text \<open>
- The following is a variant of @{const ball} that also allows an infinite radius.
+ The following is a variant of \<^const>\<open>ball\<close> that also allows an infinite radius.
\<close>
definition eball :: "'a :: metric_space \<Rightarrow> ereal \<Rightarrow> 'a set" where
"eball z r = {z'. ereal (dist z z') < r}"