commit by user andrea

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index d309eeed28e429c98678179880d499b143e91bcb..714dcb575db9e7f3f34a61a5d04a5000628b3d64 100644 (file)
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -35,7 +35,7 @@ called induction. The induction principle states that, given a property P(n) ove
 numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m), than we can conclude
 P(n) for any n. 
 
-The elim tactic, allow you to apply induction in a vcery simple way. If your goal is P(n), the 
+The elim tactic, allow you to apply induction in a very simple way. If your goal is P(n), the 
 invocation of
   elim n
 will break down your task to prove the two subgoals P(0) and ∀m.P(m) → P(S m).
@@ -81,11 +81,9 @@ For Matita, the task is trivial and we can simply close the goal 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 quantifiers, and later on to make some interesting consideration
-on proofs and computations. *)
+(* 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. *)
 
 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