...

[helm.git] / matita / tests / decl.ma

diff --git a/matita/tests/decl.ma b/matita/tests/decl.ma
index a0d3a0bd610f62962e0ffb73ea4d718985f49a21..4b67f551ab6821646c7bda52a445f646504916b4 100644 (file)
--- a/matita/tests/decl.ma
+++ b/matita/tests/decl.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/test/decl".
+set "baseuri" "cic:/matita/tests/decl".
 
 include "nat/times.ma".
 include "nat/orders.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.
@@ -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
+qed.