Theory HOL_Syntax_Bundles_Base

✐‹creator "Kevin Kappelmann"›
section ‹HOL Syntax Bundles›
subsection ‹Basic Syntax›
theory HOL_Syntax_Bundles_Base
  imports HOL_Basics_Base
begin

bundle HOL_ascii_syntax
begin
notation (ASCII) Not (‹(‹open_block notation=‹prefix ~››~ _)› [40] 40)
  and conj (infixr ‹&› 35)
  and disj (infixr ‹|› 30)
  and implies (infixr ‹-->› 25)
  and not_equal (infixl ‹~=› 50)
end

end