commit by user andrea

diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma
index 7a961d4d2e548357719c8969cba310478f1f5750..9bb135c9a9527819c51d31b045dd648a0a85a90d 100644 (file)
--- a/weblib/tutorial/chapter1.ma
+++ b/weblib/tutorial/chapter1.ma
@@ -206,7 +206,7 @@ cases b // qed.
 (*
 \ 5h2 class="section"\ 6Records\ 5/h2\ 6
 It is time to proceed with our formalization of the farmer's problem. 
-A state of the system is defined by the position of four item: the goat, the 
+A state of the system is defined by the position of four items: the goat, the 
 wolf, the cabbage, and the boat. The simplest way to declare such a data type
 is to use a record.
 *)

diff --git a/weblib/tutorial/chapter8.ma b/weblib/tutorial/chapter8.ma
index a84d10a2a53223040e5d88c560203869bfc53a20..905e6604a628d70087956466d4150030e08b816c 100644 (file)
--- a/weblib/tutorial/chapter8.ma
+++ b/weblib/tutorial/chapter8.ma
@@ -26,8 +26,6 @@ If we define
 then, we just have •(i1+i2) = •(i1)⊕ •(i2).
 *)
 
-include "tutorial/chapter7.ma".
-
 definition lo ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λa,b:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 a \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 b,\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 a \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 b〉.
 notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
 interpretation "oplus" 'oplus a b = (lo ? a b).