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=38fccc2b774e493a94eedef76342b56079c0e694;hp=7d8a068c8e4c48a3d09a7a38286802e789a73cf2;hpb=d4302f43737034a69bd475e5f46e8d126229375e;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 7d8a068c8..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
@@ -90,8 +85,8 @@ axiom Relev_le: ∀x,y:R.
 
 lemma stupido: ∀x:R.R0+x=x.
  assume x:R.
- conclude (R0+x) = (x+R0) by _.
-               = x by _
+ conclude (R0+x) = (x+R0).
+                 = x
  done.
 qed.