src/HOL/Algebra/Lattice.thy
changeset 16325 a6431098a929
parent 15328 35951e6a7855
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Algebra/Lattice.thy	Wed Jun 08 15:14:09 2005 +0200
     1.2 +++ b/src/HOL/Algebra/Lattice.thy	Wed Jun 08 16:11:09 2005 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4    join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
     1.5    "x \<squnion> y == sup L {x, y}"
     1.6  
     1.7 -  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65)
     1.8 +  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
     1.9    "x \<sqinter> y == inf L {x, y}"
    1.10  
    1.11