commit by user andrea

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index 1d9359bb6332523cf89cc0da1ce1a4b01356f1a5..161cd325ce5eec0a13095a7bab4fe3ed0a3617e4 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -204,8 +204,8 @@ applicative nodes). In this case, there is a solution in six moves, and we
 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: \ 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.
-normalize /9/ qed. *)
+lemma problem: \ 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.
+normalize /9/ 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 
@@ -348,7 +348,7 @@ cases b // qed.
 
 (* Let's do now an important remark.
 Comment both problem and problem1, state another time the problem of the goat, the
-wolf and the cabbage, and try again to run automation at level /9/. *)
+wolf and the cabbage, and try again to run automation at level /9/. 
 
 lemma problem_bis: \ 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.
-normalize /9/  
\ No newline at end of file
+normalize /9/ qed.  *)
\ No newline at end of file