# HG changeset patch
# User haftmann
# Date 1142672329 -3600
# Node ID 83404ccd270a8c511753d7797fa0405ef2593294
# Parent  dac2c80142532a90b649a2e42effdecb1c583437
renamed constant less in lattice

diff -r dac2c8014253 -r 83404ccd270a 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. *}