From: Claudio Sacerdoti Coen Date: Mon, 5 Sep 2005 15:48:04 +0000 (+0000) Subject: ... X-Git-Tag: V_0_1_2_1~96 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=172e33ea0aabf7ef066e73fbe577061955327693;p=helm.git ... --- diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index fc7f23833..7f5cb644f 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -11,6 +11,8 @@ TODO TATTICHE + - tattiche e fallimenti: una tattica che non progredisce dovrebbe fallire, + giusto? - comportamento di tutte le tattiche nei confronti dei let-in - tattica unfold su rel a let-in bound variables - theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con