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

end