X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_didactic%2Freals.ma;h=4dffb53fb45000d9ea2bc76524486d5b36e5d90d;hb=700b170aa9b0377d33f1edd44de8d89129477fb8;hp=3328c0e962a83bc5ee929d38533d02d741744a1f;hpb=fd93fa0155994b70482e0f07d8e45c238cce835d;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama_didactic/reals.ma b/helm/software/matita/contribs/dama/dama_didactic/reals.ma
index 3328c0e96..4dffb53fb 100644
--- a/helm/software/matita/contribs/dama/dama_didactic/reals.ma
+++ b/helm/software/matita/contribs/dama/dama_didactic/reals.ma
@@ -27,24 +27,19 @@ axiom Relev: R→R→R.
 axiom Rle: R→R→Prop.
 axiom Rge: R→R→Prop.
 
-interpretation "real plus" 'plus x y =
- (cic:/matita/didactic/reals/Rplus.con x y).
+interpretation "real plus" 'plus x y = (Rplus x y).
 
-interpretation "real opp" 'uminus x =
- (cic:/matita/didactic/reals/Ropp.con x). 
+interpretation "real opp" 'uminus x = (Ropp x). 
 
 notation "hvbox(a break · b)"
   right associative with precedence 55
 for @{ 'mult $a $b }.
 
-interpretation "real mult" 'mult x y =
- (cic:/matita/didactic/reals/Rmult.con x y).
+interpretation "real mult" 'mult x y = (Rmult x y).
 
-interpretation "real leq" 'leq x y =
- (cic:/matita/didactic/reals/Rle.con x y).
+interpretation "real leq" 'leq x y = (Rle x y).
 
-interpretation "real geq" 'geq x y =
- (cic:/matita/didactic/reals/Rge.con x y).
+interpretation "real geq" 'geq x y = (Rge x y).
 
 let rec elev (x:R) (n:nat) on n: R ≝
  match n with