X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama_didactic%2Freals.ma;h=3328c0e962a83bc5ee929d38533d02d741744a1f;hb=b284579a0c4d45bc8483f295434a465ca685f444;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..3328c0e96 100644
--- a/helm/software/matita/contribs/dama/dama_didactic/reals.ma
+++ b/helm/software/matita/contribs/dama/dama_didactic/reals.ma
@@ -90,8 +90,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.