From: Claudio Sacerdoti Coen Date: Tue, 26 Sep 2006 08:48:08 +0000 (+0000) Subject: discriminate => destruct X-Git-Tag: 0.4.95@7852~998 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=91973888e1e704c30dd6d31ccb7c995a312ee31c;p=helm.git discriminate => destruct --- diff --git a/matita/tests/decl.ma b/matita/tests/decl.ma index a0d3a0bd6..138e37e71 100644 --- a/matita/tests/decl.ma +++ b/matita/tests/decl.ma @@ -200,7 +200,7 @@ theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty. suppose (Node t1 t2 = Empty) (absurd). (* Discriminate should really generate a theorem to be useful with declarative tactics *) - discriminate absurd. + destruct absurd. by final done. qed. \ No newline at end of file