diff -r f06e5a5a4b46 -r a9599d3d7610 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -30,7 +30,7 @@
   shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
 
-subsubsection \<open>@{text Liminf} and @{text Limsup}\<close>
+subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>
 
 definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
   "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"