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 
 
 (* 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 
 
 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
 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 
 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