X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter1.ma;h=9043bdad712795d8f6f76104e72d4dc6601a3455;hb=44c1079dabf1d3c0b69d0155ddbaea8627ec901c;hp=b21fd3e1787add792e06acdb24dbf62c14dba2b0;hpb=1410ea677188e9e11d748c69e208d1e90b0a324e;p=helm.git

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index b21fd3e17..9043bdad7 100644
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -243,7 +243,7 @@ need a few more applications to handle reachability, and side conditions.
 The magic number to let automation work is, in this case, 9.  *)
 
 lemma problem: a href="cic:/matita/tutorial/chapter1/reachable.ind(1,0,0)"reachable/a a href="cic:/matita/tutorial/chapter1/start.def(1)"start/a a href="cic:/matita/tutorial/chapter1/end.def(1)"end/a.
-normalize /9/ qed. 
+normalize /span class="autotactic"9span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"one/a, a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a, a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"with_boat/a, a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"opposite_side/a, a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a, a href="cic:/matita/tutorial/chapter1/move.con(0,2,0)"move_wolf/a, a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"move_cabbage/a, a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"move_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/ qed. 
 
 (* Let us now try to derive the proof in a more interactive way. Of course, we
 expect to need several moves to transfer all items from a bank to the other, so 
@@ -304,7 +304,7 @@ requires /2/ since move_goat opens an additional subgoal. By applying "]" we
 refocus on the skipped goal, going back to a situation similar to the one we
 started with. *)
 
-  | /2/ ] 
+  | /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a/span/span/ ] 
 
 (* Let us perform the next step, namely moving back the boat, in a sligtly 
 different way. The more operation expects as second argument the new 
@@ -319,7 +319,7 @@ the system. *)
 trivial. Wespan style="font-family: Verdana,sans-serif;" /spancan just apply automation to all of them, and it will close the two
 trivial goals. *)
 
-/2/
+/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"opposite_side/a, a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"move_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/
 
 (* Let us come to the next step, that consists in moving the wolf. Suppose that 
 instead of specifying the next intermediate state, we prefer to specify the next 
@@ -338,12 +338,12 @@ be arbitrary). The simplest way to proceed is to focus on the bank, that is
 the fourth subgoal, and explicitly instatiate it. Instead of repeatedly using "|",
 we can perform focusing by typing "4:" as described by the following command. *)
 
-[4: @a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a] /2/
+[4: @a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a] /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"with_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a/span/span/
 
 (* Alternatively, we can directly instantiate the bank into the move. Let
 us complete the proof in this, very readable way. *)
 
-@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a … )) /2/
-@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"move_cabbage/a ?? a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a … )) /2/
-@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"move_boat/a ??? a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a … )) /2/
-@a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"one/a /2/ qed.
\ No newline at end of file
+@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a … )) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"with_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/
+@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,3,0)"move_cabbage/a ?? a href="cic:/matita/tutorial/chapter1/bank.con(0,1,0)"east/a … )) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,2,0)"opposite_side/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/
+@(a href="cic:/matita/tutorial/chapter1/reachable.con(0,2,0)"more/a … (a href="cic:/matita/tutorial/chapter1/move.con(0,4,0)"move_boat/a ??? a href="cic:/matita/tutorial/chapter1/bank.con(0,2,0)"west/a … )) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/safe_state.con(0,1,0)"with_boat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,2,0)"west_east/a/span/span/
+@a href="cic:/matita/tutorial/chapter1/reachable.con(0,1,0)"one/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/tutorial/chapter1/move.con(0,1,0)"move_goat/a, a href="cic:/matita/tutorial/chapter1/opp.con(0,1,0)"east_west/a/span/span/ qed.
\ No newline at end of file