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 (‹~ _› [40] 40)
  and conj (infixr ‹&› 35)
  and disj (infixr ‹|› 30)
  and implies (infixr ‹-->› 25)
  and not_equal (infixl ‹~=› 50)
syntax "_Let" :: "[letbinds, 'a] ⇒ 'a" (‹(let (_)/ in (_))› 10)
end

end