X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_duality%2Fattic%2Frings.ma;h=7b9eae009c353c1cc64a3b79562315b757e6a373;hb=05ebdd213d5968b9f0eeaa01e4f9aac33ef86c7c;hp=d4db003dc7a57b71fe97257d7c278f060994e73d;hpb=c077ca16ea87ba612435a47eee714b5388204d93;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_duality/attic/rings.ma b/helm/software/matita/contribs/dama/dama_duality/attic/rings.ma
index d4db003dc..7b9eae009 100644
--- a/helm/software/matita/contribs/dama/dama_duality/attic/rings.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/attic/rings.ma
@@ -65,14 +65,12 @@ theorem not_eq_zero_one: ∀R:ring.0 ≠ one R.
  apply (not_eq_zero_one_ ? ? ? (r_ring_properties R)).
 qed.
 
-interpretation "Ring mult" 'times a b =
- (cic:/matita/attic/rings/mult.con _ a b).
+interpretation "Ring mult" 'times a b = (mult _ a b).
 
 notation "1" with precedence 89
 for @{ 'one }.
 
-interpretation "Ring one" 'one =
- (cic:/matita/attic/rings/one.con _).
+interpretation "Ring one" 'one = (one _).
 
 lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0.
  intros;