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.
 
  
 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
 
 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.
 
 (*
 // 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.
 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. 
 (* 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,
 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 
 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.
 *)
 
 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.