src/HOL/Algebra/Lattice.thy

--- a/src/HOL/Algebra/Lattice.thy	Fri Mar 17 22:33:06 2006 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Sat Mar 18 09:58:49 2006 +0100
@@ -29,7 +29,7 @@
                    x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
 
 constdefs (structure L)
-  less :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
+  lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
   "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
 
   -- {* Upper and lower bounds of a set. *}