
diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Thu May 26 17:51:22 2016 +0200
@@ -507,7 +507,7 @@
   unfolding sup_def
   by (rule someI2) (auto intro: sup_of_singletonI)
 
-text \<open>Condition on @{text A}: supremum exists.\<close>
+text \<open>Condition on \<open>A\<close>: supremum exists.\<close>
 
 lemma (in weak_upper_semilattice) sup_insertI:
   "[| !!s. least L s (Upper L (insert x A)) ==> P s;
@@ -638,7 +638,7 @@
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
 proof (rule finite_sup_insertI)
-  -- \<open>The textbook argument in Jacobson I, p 457\<close>
+  \<comment> \<open>The textbook argument in Jacobson I, p 457\<close>
   fix s
   assume sup: "least L s (Upper L {x, y, z})"
   show "x \<squnion> (y \<squnion> z) .= s"
@@ -652,7 +652,7 @@
   qed (simp_all add: L least_closed [OF sup])
 qed (simp_all add: L)
 
-text \<open>Commutativity holds for @{text "="}.\<close>
+text \<open>Commutativity holds for \<open>=\<close>.\<close>
 
 lemma join_comm:
   fixes L (structure)
@@ -747,7 +747,7 @@
   unfolding inf_def
   by (rule someI2) (auto intro: inf_of_singletonI)
 
-text \<open>Condition on @{text A}: infimum exists.\<close>
+text \<open>Condition on \<open>A\<close>: infimum exists.\<close>
 
 lemma (in weak_lower_semilattice) inf_insertI:
   "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
@@ -1090,7 +1090,7 @@
 (* TODO: prove dual version *)
 
 
-subsection \<open>Orders and Lattices where @{text eq} is the Equality\<close>
+subsection \<open>Orders and Lattices where \<open>eq\<close> is the Equality\<close>
 
 locale partial_order = weak_partial_order +
   assumes eq_is_equal: "op .= = op ="
@@ -1172,7 +1172,7 @@
   "x \<in> carrier L ==> \<Sqinter>{x} = x"
   using weak_inf_of_singleton unfolding eq_is_equal .
 
-text \<open>Condition on @{text A}: infimum exists.\<close>
+text \<open>Condition on \<open>A\<close>: infimum exists.\<close>
 
 lemma (in lower_semilattice) meet_assoc_lemma:
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"




