Theory HOL_Syntax_Bundles_Groups

✐‹creator "Kevin Kappelmann"›
subsection ‹Group Syntax›
theory HOL_Syntax_Bundles_Groups
  imports HOL.Groups
begin

bundle HOL_groups_syntax
begin
notation Groups.zero (‹0›)
notation Groups.one (‹1›)
notation Groups.plus (infixl ‹+› 65)
notation Groups.minus (infixl ‹-› 65)
notation Groups.uminus (‹(‹open_block notation=‹prefix -››- _)› [81] 80)
notation Groups.times (infixl ‹*› 70)
notation abs (‹¦_¦›)
end

end