some advances on pointwise union for local environments ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl

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 f65ec6eee8d79675e0337967c4585c4551baf2a0..e274719b76267a5c8b023a365b16a27c295b389f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -247,12 +247,17 @@ table {
              [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ]
           }
         ]
-        [ { "lazy pointwise extension of a relation" * } {
+        [ { "pointwise union for local environments" * } {
+             [ "llor ( ? ⩖[?] ? ≡ ? )" * ]
+          }
+        ]
+        [ { "pointwise extension of a relation" * } {
              [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" * ]
+             [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_ldrop" + "lpx_sn_lpx_sn" * ]
           }
         ]
         [ { "basic local env. slicing" * } {
-             [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_lpx_sn" + "ldrop_leq" + "ldrop_ldrop" * ]
+             [ "ldrop ( ⇩[?,?,?] ? ≡ ? )"  "ldrop_leq" + "ldrop_ldrop" * ]
           }
         ]
         [ { "basic term relocation" * } {
@@ -268,10 +273,6 @@ table {
              [ "leq ( ? ≃[?,?] ? )" "leq_leq" * ]
           }
         ]
-        [ { "pointwise extension of a relation" * } {
-             [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_lpx_sn" * ]
-          }
-        ]
         [ { "same top term constructor" * } {
              [ "tstc ( ? ≃ ? )" "tstc_tstc" + "tstc_vector" * ]
           }