new semantics for 'by t'

diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma
index 5308f9350fa3762f8c496719266481289b274e97..84a597fda6be9e9f16e8861e7b6f837a541caebd 100644 (file)
--- 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.