X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter2.ma;fp=weblib%2Ftutorial%2Fchapter2.ma;h=7a60a7b523412e27c92cf035739a1bb5a7ed4d5f;hb=948676ae86382ebdfd13b7d485da02137cce558d;hp=29979affdfdb0a685fe066f3ce4575eb295aafdf;hpb=4cfd39d4bae224eb6f6391c7423f8ee722f7f00b;p=helm.git

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 29979affd..7a60a7b52 100644
--- 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.a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a 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.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).