# HG changeset patch # User haftmann # Date 1273044281 -7200 # Node ID 6d25e8dab1e393a9a2b9c7e95731ba5e59fa60cf # Parent bd7f659f7de54ce1cf656d10414e89922bfdd745 tuned whitespace diff -r bd7f659f7de5 -r 6d25e8dab1e3 src/HOL/Lattices.thy --- 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