- new tactic subst removes simple non recursive equalities from the context

[helm.git] / helm / software / matita / contribs / prova.ma

diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma
index 407db9b6658f907ba5b0d8718e6524773858421f..457899a8ce8d4c9d3c0a6a5950557214a41fb7e3 100644 (file)
--- 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