Small changes

diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma
index 8e62c13441b1731633a170832b6a21ee54b6bb72..7462d74b7717a254898c1c0fb9cf60673c19bcc7 100644 (file)
--- a/weblib/tutorial/chapter8.ma
+++ b/weblib/tutorial/chapter8.ma
@@ -350,7 +350,7 @@ cases (e1 \ 5a title="item-pre concat" href="cic:/fakeuri.def(1)"\ 6▹\ 5/a\ 6 i) #i1 #
 qed.
 
 (* We conclude this section with the proof of the main semantic properties
-of ⊙ and ⊛.)
+of ⊙ and ⊛. *)
 
 lemma sem_odot: 
   ∀S.∀e1,e2: \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1 \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 e2} \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e1}\ 5a title="cat lang" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a title="in_l" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e2|} \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e2}.

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