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

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index a4675f94e..b81ecb07c 100644
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -96,7 +96,7 @@ definition twice ≝ λn.a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
 
 (* 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.a title="exists" href="cic:/fakeuri.def(1)"∃/am. n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a m a title="logical or" href="cic:/fakeuri.def(1)"∨/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a 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