commit by user andrea

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index c46004f24d106a7f03eea1812ebc5620ee7d65a9..7a961d4d2e548357719c8969cba310478f1f5750 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -63,7 +63,9 @@ name for further reference, and we call it "east_to_west". *)
  
 lemma east_to_west : \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"\ 6east\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"\ 6west\ 5/a\ 6.
 
-(* If you stop the execution here you will see a new window on the  right side
+(* 
+\ 5h2 class="section"\ 6The goal window\ 5/h2\ 6
+If you stop the execution here you will see a new window on the  right side
 of the screen: it is the goal window, providing a sequent like representation of
 the form
 
@@ -104,7 +106,7 @@ lemma west_to_east : \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opp
 // qed.
 
 (*
-\ 5h2 class="section"\ 6Case analysis\ 5/h2\ 6
+\ 5h2 class="section"\ 6Introduction\ 5/h2\ 6
 A slightly more complex problem consists in proving that opposite is idempotent *)
 
 lemma idempotent_opposite : ∀x. \ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter1/opposite.def(1)"\ 6opposite\ 5/a\ 6 x) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x.
@@ -120,7 +122,10 @@ wish to rename x into b (since it is a bank), we just type #b. *)
 (* See the effect of the execution in the goal window on the right: b has been 
 added to the context (replacing x in the conclusion); moreover its implicit type 
 "bank" has been made explicit. 
+*)
 
+(*
+\ 5h2 class="section"\ 6Case analysis\ 5/h2\ 6
 But how are we supposed to proceed, now? Simplification cannot help us, since b
 is a variable: just try to call normalize and you will see that it has no effect.
 The point is that we must proceed by cases according to the possible values of b,
@@ -265,8 +270,9 @@ expect to need several moves to transfer all items from a bank to the other, so
 we should start our proof by applying "more". Matita syntax for invoking the 
 application of a property named foo is to write "@foo". In general, the philosophy 
 of Matita is to describe each proof of a property P as a structured collection of 
-results required for proving P, prefixed by simple modalities (<,@,...) explaining 
-the way the result is used (e.g. for rewriting, in an applicative step, and so on).
+objects involved in the proof, prefixed by simple modalities (#,<,@,...) explaining 
+the way it is actually used (e.g. for introduction, rewriting, in an applicative 
+step, and so on).
 *)
 
 lemma problem1: \ 5a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"\ 6reachable\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/start.def(1)"\ 6start\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter1/end.def(1)"\ 6end\ 5/a\ 6.