diff -r 76646fc8b1bf -r 2e38e3c94990 src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Mon Oct 09 14:10:55 2000 +0200
+++ b/src/HOL/Lattice/CompleteLattice.thy	Mon Oct 09 17:06:33 2000 +0200
@@ -256,7 +256,7 @@
 subsection {* Complete lattices are lattices *}
 
 text {*
-  Complete lattices (with general bounds) available are indeed plain
+  Complete lattices (with general bounds available) are indeed plain
   lattices as well.  This holds due to the connection of general
   versus binary bounds that has been formally established in
   \S\ref{sec:gen-bin-bounds}.