diff -r 059caec54d91 -r a6431098a929 src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Wed Jun 08 15:14:09 2005 +0200 +++ b/src/HOL/Algebra/Lattice.thy Wed Jun 08 16:11:09 2005 +0200 @@ -58,7 +58,7 @@ join :: "[_, 'a, 'a] => 'a" (infixl "\\" 65) "x \ y == sup L {x, y}" - meet :: "[_, 'a, 'a] => 'a" (infixl "\\" 65) + meet :: "[_, 'a, 'a] => 'a" (infixl "\\" 70) "x \ y == inf L {x, y}"