diff -r d2e5df3d1201 -r 65f8680c3f16 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Fri Apr 23 20:52:04 2004 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Fri Apr 23 21:46:04 2004 +0200
@@ -186,6 +186,7 @@
   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   by (unfold greatest_def) blast
 
+
 subsubsection {* Supremum *}
 
 lemma (in lattice) joinI:
@@ -212,7 +213,8 @@
   shows "x \<in> carrier L ==> \<Squnion> {x} = x"
   by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
 
-text {* Condition on A: supremum exists. *}
+
+text {* Condition on @{text A}: supremum exists. *}
 
 lemma (in lattice) sup_insertI:
   "[| !!s. least L s (Upper L (insert x A)) ==> P s;