author | haftmann |
Sat, 18 Mar 2006 09:58:49 +0100 | |
changeset 19286 | 83404ccd270a |
parent 19285 | dac2c8014253 |
child 19287 | 45b8ddc2fab8 |
--- 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. *}