# 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 \ carrier L; y \ carrier L; z \ carrier L |] ==> x \ z" constdefs (structure L) - less :: "[_, 'a, 'a] => bool" (infixl "\\" 50) + lless :: "[_, 'a, 'a] => bool" (infixl "\\" 50) "x \ y == x \ y & x ~= y" -- {* Upper and lower bounds of a set. *}