ported to new syntactic requirement about terms being surrounded by parens

[helm.git] / helm / matita / library / nat / nat.ma

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index e36c1beaa95303f52e693f11e4ac7f3d913b6928..fb7d1686efa6631d75e131aae4700384ff017843 100644 (file)
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -33,7 +33,7 @@ theorem injective_S : injective nat nat S.
 simplify.
 intros.
 rewrite > pred_Sn.
-rewrite > pred_Sn y.
+rewrite > (pred_Sn y).
 apply eq_f. assumption.
 qed.
 
@@ -86,18 +86,18 @@ theorem nat_elim2 :
 (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
 intros 5.elim n.
 apply H.
-apply nat_case m.apply H1.
+apply (nat_case m).apply H1.
 intros.apply H2. apply H3.
 qed.
 
 theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
 intros.simplify.
-apply nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False))).
+apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False)))).
 intro.elim n1.
 left.reflexivity.
 right.apply not_eq_O_S.
 intro.right.intro.
-apply not_eq_O_S n1.
+apply (not_eq_O_S n1).
 apply sym_eq.assumption.
 intros.elim H.
 left.apply eq_f. assumption.