src/HOL/Algebra/Lattice.thy
changeset 16325 a6431098a929
parent 15328 35951e6a7855
child 16417 9bc16273c2d4
equal deleted inserted replaced
16324:059caec54d91 16325:a6431098a929
    56   "\<Sqinter>A == THE x. greatest L x (Lower L A)"
    56   "\<Sqinter>A == THE x. greatest L x (Lower L A)"
    57 
    57 
    58   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
    58   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
    59   "x \<squnion> y == sup L {x, y}"
    59   "x \<squnion> y == sup L {x, y}"
    60 
    60 
    61   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65)
    61   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
    62   "x \<sqinter> y == inf L {x, y}"
    62   "x \<sqinter> y == inf L {x, y}"
    63 
    63 
    64 
    64 
    65 subsubsection {* Upper *}
    65 subsubsection {* Upper *}
    66 
    66