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)
unbundle uminus_syntax
notation Groups.times (infixl ‹*› 70)
unbundle abs_syntax
end

end