X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter2.ma;fp=weblib%2Ftutorial%2Fchapter2.ma;h=29979affdfdb0a685fe066f3ce4575eb295aafdf;hb=4cfd39d4bae224eb6f6391c7423f8ee722f7f00b;hp=b81ecb07ce6d173afdb34e42eec39df53b55d412;hpb=7e2f8faa727b72aeebc6eb5a49ca843dcb50dfe0;p=helm.git

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index b81ecb07c..29979affd 100644
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -30,8 +30,8 @@ match n with
 
 (* It is worth to observe that the previous algorithm works by recursion over the first 
 argument. This means that, for instance, (add O x) will reduce to x, as expected, but (add x O)
-is stack. How can we prove that, for a generic x, (add x O) = x? The mathematical tool do it is 
-called induction. The induction principle states that, given a property P(n) over natural 
+is stack. How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do it 
+is called induction. The induction principle states that, given a property P(n) over natural 
 numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m), than we can conclude
 P(n) for any n.