From 88d9b90eb45721abe07bfce2c4d0768ef6420443 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 26 Sep 2006 08:48:08 +0000 Subject: [PATCH] discriminate => destruct --- helm/software/matita/tests/decl.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma index a0d3a0bd6..138e37e71 100644 --- a/helm/software/matita/tests/decl.ma +++ b/helm/software/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