X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter8.ma;h=7462d74b7717a254898c1c0fb9cf60673c19bcc7;hb=1e8c081077f1cb7b04685b039c9c764d63da8be3;hp=8e62c13441b1731633a170832b6a21ee54b6bb72;hpb=12f5034282288694272f5386db7a68d41e0d5326;p=helm.git

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