commit by user andrea

[helm.git] / weblib / tutorial / chapter8.ma

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).