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. 
 
 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).
 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. 
 
 
 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 
 
 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