src/HOL/Algebra/Lattice.thy

     and trans [trans]:
                   "[| x \<sqsubseteq> y; y \<sqsubseteq> z;
                    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. *}
   Upper :: "[_, 'a set] => 'a set"
   "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>