X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fdecl.ma;fp=helm%2Fsoftware%2Fmatita%2Ftests%2Fdecl.ma;h=a9d083b64cc4eea3198120fbe7a5c7453c1b761f;hb=36014ac060f150e7d93f607c914a0b06239715c0;hp=138e37e71fbbd941ad9c48559796071d5d7d0135;hpb=5e63ff16f7193322fd1b75a1eb443a65643fdbe2;p=helm.git

diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma
index 138e37e71..a9d083b64 100644
--- a/helm/software/matita/tests/decl.ma
+++ b/helm/software/matita/tests/decl.ma
@@ -129,7 +129,7 @@ assume p:nat.
 suppose (n=m) (H).
 suppose (S m = S p) (K).
 suppose (n = S p) (L).
-obtain (S n) = (S m) by (eq_f ? ? ? ? ? H).
+conclude (S n) = (S m) by (eq_f ? ? ? ? ? H).
              = (S p) by K.
              = n by (sym_eq ? ? ? L)
 done.
@@ -142,7 +142,7 @@ assume p:nat.
 suppose (n=m) (H).
 suppose (S m = S p) (K).
 suppose (n = S p) (L).
-obtain (S n) = (S m) by _.
+conclude (S n) = (S m) by _.
              = (S p) by _.
              = n by _
 done.