X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fgroup.ma;h=4ecd016fb3dd31df85ead1ec01c5508cccc86b1c;hb=e1efca300fbaeb8c69a691a428a084d89a2c058f;hp=104dcf274e3943727d090dc8ff8fddd5f7bca59e;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/group.ma b/helm/software/matita/contribs/dama/dama_duality/group.ma
index 104dcf274..4ecd016fb 100644
--- a/helm/software/matita/contribs/dama/dama_duality/group.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/group.ma
@@ -44,20 +44,16 @@ record abelian_group : Type ≝
 
 notation "0" with precedence 89 for @{ 'zero }.
 
-interpretation "Abelian group zero" 'zero =
- (cic:/matita/group/zero.con _).
+interpretation "Abelian group zero" 'zero = (zero ?).
 
-interpretation "Abelian group plus" 'plus a b =
- (cic:/matita/group/plus.con _ a b).
+interpretation "Abelian group plus" 'plus a b = (plus ? a b).
 
-interpretation "Abelian group opp" 'uminus a =
- (cic:/matita/group/opp.con _ 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 =
- (cic:/matita/group/minus.con _ 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_.