From b2a190e3c2d5b594d409db937e88f9f4f7d22b8c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 20 Mar 2008 13:07:09 +0000 Subject: [PATCH] new semantics for 'by t' --- helm/software/matita/tests/decl.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma index 5308f9350..84a597fda 100644 --- a/helm/software/matita/tests/decl.ma +++ b/helm/software/matita/tests/decl.ma @@ -125,9 +125,9 @@ assume p:nat. suppose (n=m) (H). suppose (S m = S p) (K). suppose (n = S p) (L). -conclude (S n) = (S m) by (eq_f ? ? ? ? ? H). +conclude (S n) = (S m) by H. = (S p) by K. - = n by (sym_eq ? ? ? L) + = n by L done. qed. -- 2.39.2