commit by user enrico

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 29979affdfdb0a685fe066f3ce4575eb295aafdf..7a60a7b523412e27c92cf035739a1bb5a7ed4d5f 100644 (file)
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -94,8 +94,8 @@ definition nat_of_bool ≝ λb. match b with
 
 definition twice ≝ λn.\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 n n. 
 
-(* 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 n there exists a natural number m that 
+is the integer half of n. This will give us the opportunity to introduce new connectives and 
 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).