commit by user andrea

diff --git a/weblib/tutorial/chapter10.ma b/weblib/tutorial/chapter10.ma
index a5595ac5079fd539a7cebcceddda497791ec4282..95e3a55c121f51e6d4e870933c552901846fd0a8 100644 (file)
--- a/weblib/tutorial/chapter10.ma
+++ b/weblib/tutorial/chapter10.ma
@@ -258,14 +258,14 @@ lemma bisim_correct: ∀S.∀e1,e2:\ 5a href="cic:/matita/tutorial/chapter7/pre.de
         |#p1 #H (cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … H)) [#eqp >(\P eqp) // |@r_visited]
         ]
      |whd % [@\ 5a href="cic:/matita/tutorial/chapter5/unique_append_unique.def(6)"\ 6unique_append_unique\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/bool/andb_true_r.def(4)"\ 6andb_true_r\ 5/a\ 6 … u_frontier)]
-      @\ 5a href="cic:/matita/tutorial/chapter5/unique_append_elim.dec"\ 6unique_append_elim\ 5/a\ 6 #q #H
+      @\ 5a href="cic:/matita/tutorial/chapter5/unique_append_elim.def(7)"\ 6unique_append_elim\ 5/a\ 6 #q #H
        [cases (\ 5a href="cic:/matita/tutorial/chapter10/memb_sons.def(8)"\ 6memb_sons\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter5/memb_filter_memb.def(5)"\ 6memb_filter_memb\ 5/a\ 6 … H)) -H
         #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (w1\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6])))
         >\ 5a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"\ 6moves_left\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter9/moves_left.def(9)"\ 6moves_left\ 5/a\ 6 >mw1 >mw2 >m1 >m2 % // 
        |@r_frontier @\ 5a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"\ 6memb_cons\ 5/a\ 6 //
        ]
-     |@\ 5a href="cic:/matita/tutorial/chapter5/unique_append_elim.dec"\ 6unique_append_elim\ 5/a\ 6 #q #H
-       [@\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"\ 6injective_notb\ 5/a\ 6 @(\ 5a href="cic:/matita/tutorial/chapter5/filter_true.def(5)"\ 6filter_true\ 5/a\ 6 … H)
+     |@\ 5a href="cic:/matita/tutorial/chapter5/unique_append_elim.def(7)"\ 6unique_append_elim\ 5/a\ 6 #q #H
+       [@\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"\ 6injective_notb\ 5/a\ 6 @(\ 5a href="cic:/matita/tutorial/chapter5/memb_filter_true.def(5)"\ 6memb_filter_true\ 5/a\ 6 … H\ 5span class="error" title="error location"\ 6\ 5/span\ 6)
        |cut ((q\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=p) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) 
          [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @\ 5a href="cic:/matita/tutorial/chapter5/memb_cons.def(5)"\ 6memb_cons\ 5/a\ 6 //]
         cases (\ 5a href="cic:/matita/basics/bool/andb_true.def(5)"\ 6andb_true\ 5/a\ 6 … u_frontier) #notp #_ @(\bf ?)