notation "0" with precedence 89 for @{ 'zero }.
-interpretation "Abelian group zero" 'zero = (zero _).
+interpretation "Abelian group zero" 'zero = (zero ?).
-interpretation "Abelian group plus" 'plus a b = (plus _ a b).
+interpretation "Abelian group plus" 'plus a b = (plus ? a b).
-interpretation "Abelian group opp" 'uminus a = (opp _ a).
+interpretation "Abelian group opp" 'uminus a = (opp ? a).
definition minus ≝
λG:abelian_group.λa,b:G. a + -b.
-interpretation "Abelian group minus" 'minus a b = (minus _ a b).
+interpretation "Abelian group minus" 'minus a b = (minus ? a b).
lemma plus_assoc: ∀G:abelian_group.∀x,y,z:G.x+(y+z)≈x+y+z ≝ plus_assoc_.
lemma plus_comm: ∀G:abelian_group.∀x,y:G.x+y≈y+x ≝ plus_comm_.