✐‹creator "Kevin Kappelmann"› subsection ‹Lattice Syntax› theory HOL_Syntax_Bundles_Lattices imports HOL.Lattices begin open_bundle lattice_syntax ― ‹copied from theory Main› begin notation bot (‹⊥›) and top (‹⊤›) and inf (infixl ‹⊓› 70) and sup (infixl ‹⊔› 65) end end