diff -r 96699d8eb49e -r 21bbd410ba04 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Fri Aug 01 17:41:37 2008 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Fri Aug 01 18:10:52 2008 +0200
@@ -4,7 +4,7 @@
   Author:    Clemens Ballarin, started 7 November 2003
   Copyright: Clemens Ballarin
 
-Most congruence rules by Stefan Hohe.
+Most congruence rules by Stephan Hohe.
 *)
 
 theory Lattice imports Congruence begin
@@ -964,7 +964,7 @@
 qed
 
 
-subsection {* Complete lattices *}
+subsection {* Complete Lattices *}
 
 locale weak_complete_lattice = weak_lattice +
   assumes sup_exists:
@@ -1115,12 +1115,7 @@
 end
 
 
-subsubsection {* Upper and lower bounds of a set *}
-
-(* all relevant lemmas are global and already proved above *)
-
-
-subsubsection {* Least and greatest, as predicate *}
+text {* Least and greatest, as predicate *}
 
 lemma (in partial_order) least_unique:
   "[| least L x A; least L y A |] ==> x = y"
@@ -1131,7 +1126,7 @@
   using weak_greatest_unique unfolding eq_is_equal .
 
 
-subsection {* Lattices *}
+text {* Lattices *}
 
 locale upper_semilattice = partial_order +
   assumes sup_of_two_exists:
@@ -1150,7 +1145,7 @@
 locale lattice = upper_semilattice + lower_semilattice
 
 
-subsubsection {* Supremum *}
+text {* Supremum *}
 
 declare (in partial_order) weak_sup_of_singleton [simp del]
 
@@ -1169,7 +1164,7 @@
   using weak_join_assoc L unfolding eq_is_equal .
 
 
-subsubsection {* Infimum *}
+text {* Infimum *}
 
 declare (in partial_order) weak_inf_of_singleton [simp del]
 
@@ -1190,7 +1185,7 @@
   using weak_meet_assoc L unfolding eq_is_equal .
 
 
-subsection {* Total Orders *}
+text {* Total Orders *}
 
 locale total_order = partial_order +
   assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
@@ -1211,7 +1206,7 @@
   by unfold_locales (auto intro: sup_of_two_exists inf_of_two_exists)
 
 
-subsection {* Complete lattices *}
+text {* Complete lattices *}
 
 locale complete_lattice = lattice +
   assumes sup_exists:
@@ -1280,7 +1275,7 @@
 
 subsection {* Examples *}
 
-subsubsection {* Powerset of a Set is a Complete Lattice *}
+subsubsection {* The Powerset of a Set is a Complete Lattice *}
 
 theorem powerset_is_complete_lattice:
   "complete_lattice (| carrier = Pow A, eq = op =, le = op \<subseteq> |)"