Small changes

[helm.git] / weblib / tutorial / chapter9.ma

diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index c7585df80f775b72be82981149eee8493761515e..05f5e0152112367275cf463493b17382a3d8c616 100644 (file)
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -1,5 +1,7 @@
-include "re.ma".
-include "basics/listb.ma".
+(* 
+\ 5h1\ 6Moves\ 5/h1\ 6*)
+
+include "chapter8.ma".
 
 let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
  match E with
@@ -157,5 +159,4 @@ lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
     |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/ 
     ]
   ]
-qed.
-
+qed.
\ No newline at end of file