--- 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}.