commit by user andrea

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index a4675f94ebbc7a83bea5d170720692f0b1d4f4bf..b81ecb07ce6d173afdb34e42eec39df53b55d412 100644 (file)
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -96,7 +96,7 @@ definition twice ≝ λn.\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6
 
 (* We are interested to prove that for any natural number m there exists a natural number m that 
 is the integer half of m. This will give us the opportunity to introduce new connectives and 
-quantifiers, and later on to make some interesting consideration on proofs and computations. *)
+quantifiers and, later on, to make some interesting consideration on proofs and computations. *)
 
 theorem ex_half: ∀n.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6m. n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 m \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 m).
 #n elim n normalize 
@@ -183,7 +183,7 @@ n and a boolean indicating which one between the two conditions A(n) and B(n) is
 This is precisely the quotient-remainder pair returned by div2.
 In both cases we proceed by recurrence (respectively, induction or recursion) over the 
 input argument n. In case n = 0, we conclude the proof in ex_half by providing the
-witness O and a proof of A(O); this corresponds to returning the pair 〈O,tt〉 in div2.
+witness O and a proof of A(O); this corresponds to returning the pair 〈O,ff〉 in div2.
 Similarly, in the inductive case n = S a, we must exploit the inductive hypothesis 
 for a (i.e. the result of the recursive call), distinguishing two subcases according 
 to the the two possibilites A(a) or B(a) (i.e. the two possibile values of the remainder