From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Mar 2012 12:11:14 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1905
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cee37c7a5aa40d1b6d978a5e1aa3a2d91cdb7a63;p=helm.git

commit by user andrea
---

diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index a5dfd1c98..b3f46ae04 100644
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -1,7 +1,15 @@
 (* 
-h1Moves/h1*)
+h1Moves/h1We 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