X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fnat.ma;h=a75032d7123b7018f40af65285712d5c3c4da9c1;hb=400b07e007cfbb0b4ce5ed77cfc50f227c491310;hp=fb7d1686efa6631d75e131aae4700384ff017843;hpb=5538a4548601ba1c1647ec9dc0fbbd875e5a93fd;p=helm.git

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index fb7d1686e..a75032d71 100644
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -30,7 +30,7 @@ intros. reflexivity.
 qed.
 
 theorem injective_S : injective nat nat S.
-simplify.
+unfold injective.
 intros.
 rewrite > pred_Sn.
 rewrite > (pred_Sn y).
@@ -42,7 +42,7 @@ theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m
 
 theorem not_eq_S  : \forall n,m:nat. 
 \lnot n=m \to S n \neq S m.
-intros. simplify. intros.
+intros. unfold Not. intros.
 apply H. apply injective_S. assumption.
 qed.
 
@@ -53,7 +53,7 @@ definition not_zero : nat \to Prop \def
   | (S p) \Rightarrow True ].
 
 theorem not_eq_O_S : \forall n:nat. O \neq S n.
-intros. simplify. intros.
+intros. unfold Not. intros.
 cut (not_zero O).
 exact Hcut.
 rewrite > H.exact I.
@@ -91,7 +91,7 @@ intros.apply H2. apply H3.
 qed.
 
 theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
-intros.simplify.
+intros.unfold decidable.
 apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False)))).
 intro.elim n1.
 left.reflexivity.