Theory HOL_Syntax_Bundles_Functions

✐‹creator "Kevin Kappelmann"›
subsection ‹Function Syntax›
theory HOL_Syntax_Bundles_Functions
  imports HOL.Fun
begin

bundle HOL_function_syntax
begin
notation comp (infixl "∘" 55)
end
bundle no_HOL_function_syntax
begin
no_notation comp (infixl "∘" 55)
end


end