X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fattic%2Frings.ma;h=d4db003dc7a57b71fe97257d7c278f060994e73d;hb=cf07c50b03a49344eb4cbe2e1bc18fcef880b9e9;hp=2ea188847b81ab9c368ef18186e76831a29af8c9;hpb=a42d4bd78f10ac8fc725c50c193503a3f29b848f;p=helm.git

diff --git a/helm/software/matita/dama/attic/rings.ma b/helm/software/matita/dama/attic/rings.ma
index 2ea188847..d4db003dc 100644
--- a/helm/software/matita/dama/attic/rings.ma
+++ b/helm/software/matita/dama/attic/rings.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/rings/".
+
 
 include "group.ma".
 
@@ -66,13 +66,13 @@ theorem not_eq_zero_one: ∀R:ring.0 ≠ one R.
 qed.
 
 interpretation "Ring mult" 'times a b =
- (cic:/matita/rings/mult.con _ a b).
+ (cic:/matita/attic/rings/mult.con _ a b).
 
 notation "1" with precedence 89
 for @{ 'one }.
 
 interpretation "Ring one" 'one =
- (cic:/matita/rings/one.con _).
+ (cic:/matita/attic/rings/one.con _).
 
 lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0.
  intros;