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