# HG changeset patch
# User wenzelm
# Date 971103993 -7200
# Node ID 2e38e3c94990ae6a52515e0f3da2904d02801d5c
# Parent  76646fc8b1bfe1f5353e43e4dd0e3104e69d0f4c
tuned text;

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