From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 2 Oct 2006 15:30:44 +0000 (+0000)
Subject: ...
X-Git-Tag: 0.4.95@7852~953
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aff6791b3666237a8f95f2eb9d877c1b89b03161;p=helm.git

...
---

diff --git a/matita/tests/applys.ma b/matita/tests/applys.ma
index d9cbc9098..c929e5be5 100644
--- a/matita/tests/applys.ma
+++ b/matita/tests/applys.ma
@@ -30,5 +30,10 @@ qed.
 theorem prova2 :
  \forall n. S n \divides (S n)!.
 intros.
+(* o fare una List.rev quando si fa la make_passives... la tira su, 
+   ma tardi....
+letin www \def sym_times.
+clearbody www.
+*)
 applyS (witness ? ? ? (refl_eq ? ?)).
 qed.