--- a/src/HOL/Library/Lub_Glb.thy Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Library/Lub_Glb.thy Fri Jan 04 23:22:53 2019 +0100
@@ -45,7 +45,7 @@
where "ubs R S = Collect (isUb R S)"
-subsection \<open>Rules about the Operators @{term leastP}, @{term ub} and @{term lub}\<close>
+subsection \<open>Rules about the Operators \<^term>\<open>leastP\<close>, \<^term>\<open>ub\<close> and \<^term>\<open>lub\<close>\<close>
lemma leastPD1: "leastP P x \<Longrightarrow> P x"
by (simp add: leastP_def)
@@ -118,7 +118,7 @@
where "lbs R S = Collect (isLb R S)"
-subsection \<open>Rules about the Operators @{term greatestP}, @{term isLb} and @{term isGlb}\<close>
+subsection \<open>Rules about the Operators \<^term>\<open>greatestP\<close>, \<^term>\<open>isLb\<close> and \<^term>\<open>isGlb\<close>\<close>
lemma greatestPD1: "greatestP P x \<Longrightarrow> P x"
by (simp add: greatestP_def)