From 91973888e1e704c30dd6d31ccb7c995a312ee31c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 26 Sep 2006 08:48:08 +0000 Subject: [PATCH] discriminate => destruct --- matita/tests/decl.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2