From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 20 Mar 2008 13:07:09 +0000 (+0000)
Subject: new semantics for 'by t'
X-Git-Tag: make_still_working~5513
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=b2a190e3c2d5b594d409db937e88f9f4f7d22b8c;p=helm.git

new semantics for 'by t'
---

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.