A few changes to factorization and gcd.

[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 e2bf56542a96c2a9e9b18b392988b60c17e24da2..e36c1beaa95303f52e693f11e4ac7f3d913b6928 100644 (file)
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -26,7 +26,7 @@ definition pred: nat \to nat \def
 | (S p) \Rightarrow p ].
 
 theorem pred_Sn : \forall n:nat.n=(pred (S n)).
-intros; reflexivity.
+intros. reflexivity.
 qed.
 
 theorem injective_S : injective nat nat S.