X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2Fprova.ma;h=457899a8ce8d4c9d3c0a6a5950557214a41fb7e3;hb=adfdd6bb94218accd7ada471084170b846c52994;hp=407db9b6658f907ba5b0d8718e6524773858421f;hpb=71514bcf3ee362f9d10e2933ab17f2d4ede1ae32;p=helm.git

diff --git a/matita/contribs/prova.ma b/matita/contribs/prova.ma
index 407db9b66..457899a8c 100644
--- a/matita/contribs/prova.ma
+++ b/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