From: matitaweb Date: Fri, 23 Mar 2012 08:51:09 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1842 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b660835a8e13fdbae35e0377b6f607e7db1c07a8;hp=3800a841aa7115b10432f588d31b77129b3a0dc9;p=helm.git commit by user andrea --- diff --git a/weblib/tutorial/chapter1.ma b/weblib/tutorial/chapter1.ma index 7a961d4d2..9bb135c9a 100644 --- a/weblib/tutorial/chapter1.ma +++ b/weblib/tutorial/chapter1.ma @@ -206,7 +206,7 @@ cases b // qed. (* h2 class="section"Records/h2 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 a84d10a2a..905e6604a 100644 --- 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:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λa,b:a href="cic:/matita/tutorial/chapter7/pre.def(1)"pre/a S.a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a a a title="pitem or" href="cic:/fakeuri.def(1)"+/a a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a b,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a a a title="boolean or" href="cic:/fakeuri.def(1)"∨/a a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a b〉. notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}. interpretation "oplus" 'oplus a b = (lo ? a b).