commit by user andrea

diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index a5dfd1c981f218b3a91d6da067d5ffcc638145d4..b3f46ae04282a96988fde5cd17d334c7fa48234c 100644 (file)
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -1,7 +1,15 @@
 (* 
-\ 5h1\ 6Moves\ 5/h1\ 6*)
+\ 5h1\ 6Moves\ 5/h1\ 6We now define the move operation, that corresponds to the advancement of the 
+state in response to the processing of an input character a. The intuition is 
+clear: we have to look at points inside $e$ preceding the given character a,
+let the point traverse the character, and broadcast it. All other points must 
+be removed.
+
+We can give a particularly elegant definition in terms of the
+lifted operators of the previous section:
+*)
 
-include "chapter8.ma".
+include "tutorial/chapter8.ma".
 
 let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
  match E with