From: Claudio Sacerdoti Coen Date: Wed, 31 Aug 2005 09:35:52 +0000 (+0000) Subject: ... X-Git-Tag: working_equations_only~7 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=51bed67354ea5b083d398c147e37b462bad3fcd2;p=helm.git ... --- diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 2ddd36784..e8f03eb78 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -11,6 +11,7 @@ TODO TATTICHE + - simplify (e altre tattiche) non debbono zeta-espandere i let-in - tattica unfold su rel a let-in bound variables - theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con True.