From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Thu, 1 Mar 2012 13:00:50 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1924
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5a2800676f0a9e2bdfff0645baa131699b26af21

commit by user andrea
---

diff --git a/weblib/tutorial/chapter6.ma b/weblib/tutorial/chapter6.ma
index 430fc3f21..cadc0065c 100644
--- a/weblib/tutorial/chapter6.ma
+++ b/weblib/tutorial/chapter6.ma
@@ -1,6 +1,4 @@
-include "basics/list.ma".
-include "basics/sets.ma".
-include "basics/deqsets.ma".
+include "tutorial/chapter5.ma".
 
 definition word ≝ λS:DeqSet.list S.
 
@@ -129,4 +127,3 @@ lemma distr_cat_r_eps: ∀S.∀A,C:word S →Prop.
   (A ∪ {ϵ}) · C =1  A · C ∪ C. 
 #S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
 qed.
-