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

diff --git a/matita/dama/attic/rings.ma b/matita/dama/attic/rings.ma
index 2ea188847..d4db003dc 100644
--- a/matita/dama/attic/rings.ma
+++ b/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;