From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Mar 2012 12:04:58 +0000 (+0000)
Subject: Small changes
X-Git-Tag: make_still_working~1907
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e8c081077f1cb7b04685b039c9c764d63da8be3;p=helm.git

Small changes
---

diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma
index 8e62c1344..7462d74b7 100644
--- a/weblib/tutorial/chapter8.ma
+++ b/weblib/tutorial/chapter8.ma
@@ -350,7 +350,7 @@ cases (e1 a title="item-pre concat" href="cic:/fakeuri.def(1)"▹/a 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: a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S. a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1 a title="lifted cat" href="cic:/fakeuri.def(1)"⊙/a e2} a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e1}a title="cat lang" href="cic:/fakeuri.def(1)"·/a a title="in_l" href="cic:/fakeuri.def(1)"\sem/a{a title="forget" href="cic:/fakeuri.def(1)"|/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a e2|} a title="union" href="cic:/fakeuri.def(1)"∪/a a title="in_prl" href="cic:/fakeuri.def(1)"\sem/a{e2}.
diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index c7585df80..05f5e0152 100644
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -1,5 +1,7 @@
-include "re.ma".
-include "basics/listb.ma".
+(* 
+h1Moves/h1*)
+
+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