
diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Algebra/Complete_Lattice.thy
--- a/src/HOL/Algebra/Complete_Lattice.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Algebra/Complete_Lattice.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -1153,8 +1153,8 @@
   fix B
   assume "B \<subseteq> carrier ?L"
   then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
-    txt \<open>@{term "\<Inter> B"} is not the infimum of @{term B}:
-      @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! \<close>
+    txt \<open>\<^term>\<open>\<Inter> B\<close> is not the infimum of \<^term>\<open>B\<close>:
+      \<^term>\<open>\<Inter> {} = UNIV\<close> which is in general bigger than \<^term>\<open>A\<close>! \<close>
     by (fastforce intro!: greatest_LowerI simp: Lower_def)
   then show "\<exists>i. greatest ?L i (Lower ?L B)" ..
 qed




