--- a/src/HOL/Lattices.thy Wed May 05 08:57:23 2010 +0200 +++ b/src/HOL/Lattices.thy Wed May 05 09:24:41 2010 +0200 @@ -581,7 +581,6 @@ min_max.sup.left_commute - subsection {* Bool as lattice *} instantiation bool :: boolean_algebra