--- a/src/HOL/Lattices.thy Thu Mar 11 14:38:19 2010 +0100 +++ b/src/HOL/Lattices.thy Thu Mar 11 14:38:20 2010 +0100 @@ -43,7 +43,7 @@ end -subsection {* Conrete lattices *} +subsection {* Concrete lattices *} notation less_eq (infix "\<sqsubseteq>" 50) and