Theory HOL_Syntax_Bundles_Lattices

✐‹creator "Kevin Kappelmann"›
subsection ‹Lattice Syntax›
theory HOL_Syntax_Bundles_Lattices
  imports
    HOL.Lattices
begin

open_bundle lattice_syntax ― ‹minimised version from theory Main›
begin
notation
  bot  (‹⊥›) and
  top  (‹⊤›) and
  inf  (infixl ‹⊓› 70) and
  sup  (infixl ‹⊔› 65)
end

end