From 1e8c081077f1cb7b04685b039c9c764d63da8be3 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 6 Mar 2012 12:04:58 +0000 Subject: [PATCH] Small changes --- weblib/tutorial/chapter8.ma | 2 +- weblib/tutorial/chapter9.ma | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) 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}. diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma index c7585df80..05f5e0152 100644 --- a/weblib/tutorial/chapter9.ma +++ b/weblib/tutorial/chapter9.ma @@ -1,5 +1,7 @@ -include "re.ma". -include "basics/listb.ma". +(* +h1Moves/h1*) + +include "chapter8.ma". let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝ match E with @@ -157,5 +159,4 @@ lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) → |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/ ] ] -qed. - +qed. \ No newline at end of file -- 2.39.2