| changeset 16325 | a6431098a929 |
| parent 15328 | 35951e6a7855 |
| child 16417 | 9bc16273c2d4 |
--- 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 "\<squnion>\<index>" 65) "x \<squnion> y == sup L {x, y}" - meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65) + meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70) "x \<sqinter> y == inf L {x, y}"