X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fweb%2Fbasic_2_src.tbl;h=7d4282e13b0e3879ebdd02e74fea389b298cf3c3;hb=e6282b0c066eee7329560e1929150776ca64aa4a;hp=d960b585944b286b4ae599fea8d048796b78b074;hpb=8621771bc5c35065bbd12df9cb5fcaf7dc4aa515;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index d960b5859..7d4282e13 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -170,6 +170,9 @@ table {
              [ "lfdeq ( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
           }
         ]
+        [ { "syntactic equivalence on referred entries" * } {
+             [ "lfeq ( ? ≡[?] ? )" * ]
+          }
         [ { "generic extension on referred entries" * } {
              [ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ]
           }
@@ -207,7 +210,7 @@ table {
    [ { "relocation" * } {
         [ { "generic slicing for local environments" * } {
              [ "drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" * ]
-             [ "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_ext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
+             [ "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
           }
         ]
         [ { "generic relocation" * } {
@@ -356,7 +359,7 @@ class "italic"            { 1 }
           }
         ]
         [ { "pointwise extension of a relation" * } {
-             [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ]
+             [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ]
           }
         ]
              [ "cpx_lreq" + "cpr_cir" + "fpb_lift" + "fpbq_lift" ]