X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprova.ma;h=457899a8ce8d4c9d3c0a6a5950557214a41fb7e3;hb=78a298ace44f95591f8352b60f08575cb7d2da52;hp=407db9b6658f907ba5b0d8718e6524773858421f;hpb=8a8cb7db0c80d9945969960e69f440ca326e2b92;p=helm.git

diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma
index 407db9b66..457899a8c 100644
--- a/helm/software/matita/contribs/prova.ma
+++ b/helm/software/matita/contribs/prova.ma
@@ -19,9 +19,9 @@ include "nat/nat.ma".
 theorem pippo: \forall (P,Q,R:nat \to Prop).
                \forall x,y. x=y \to P x \to Q x \to R x.
                intros.
-               try rewrite > P in Q.  
+               rewrite > P in Q.  
 (*             
-theorem pippo2: \forall (P,Q,R:nat \to Prop).
-                \forall x,y. x=y \to P x \to Q x \to R x.
-                intros. rewrite > H in y.
-*)
+theorem pippo: \forall (P,Q,R:nat \to Prop).
+               \forall x,y. x=y \to P x \to Q x \to R x.
+               intros. rewrite > H in y.
+*)
\ No newline at end of file