Theory HOL_Syntax_Bundles_Lattices

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

bundle lattice_syntax ― ‹copied from theory Main›
begin
notation
  bot ("⊥")
  and top ("⊤")
  and inf (infixl "⊓" 70)
  and sup (infixl "⊔" 65)
end
bundle no_lattice_syntax
begin
no_notation
  bot ("⊥")
  and top ("⊤")
  and inf (infixl "⊓" 70)
  and sup (infixl "⊔" 65)
end

unbundle lattice_syntax


end