commit by user andrea

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index b81ecb07ce6d173afdb34e42eec39df53b55d412..29979affdfdb0a685fe066f3ce4575eb295aafdf 100644 (file)
--- 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)
 
 (* 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. 
 
 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.