X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambda_delta%2Fweb%2Fhome%2Fbasic_2_src.tbl;h=254dfcc969e420989ef6a41ddf2072ffc51edb6e;hb=708aa01d44c67343f0dac0353b52c7c2457069b3;hp=a8c6d34b95feafb0afbfeb58544232c8f1321086;hpb=aae326321d5aa84b996a4da6a41a590c52c9ebbd;p=helm.git

diff --git a/helm/www/lambda_delta/web/home/basic_2_src.tbl b/helm/www/lambda_delta/web/home/basic_2_src.tbl
index a8c6d34b9..254dfcc96 100644
--- a/helm/www/lambda_delta/web/home/basic_2_src.tbl
+++ b/helm/www/lambda_delta/web/home/basic_2_src.tbl
@@ -126,8 +126,8 @@ table {
           }
 	]
 	[ { "partial unfold" * } {
-             [ "ltpss ( ? [?,?] ▶* ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_tpss" "ltpss_ltpss" * ] 
-	     [ "tpss ( ? ⊢ ? [?,?] ▶* ? )" "tpss_alt ( ? ⊢ ? [?,?] ▶▶* ? )" "tpss_lift" "tpss_tpss" * ]
+             [ "ltpss ( ? ▶*[?,?] ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_tpss" "ltpss_ltpss" * ] 
+	     [ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ]
           }
 	]
 	[ { "generic local env. slicing" * } { 
@@ -148,7 +148,7 @@ table {
    class "orange"   
    [ { "substitution" * } { 
         [ { "parallel substitution" * } {
-	     [ "tps ( ? ⊢ ? [?,?] ▶ ? )" "tps_lift" "tps_tps" * ]
+	     [ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" "tps_tps" * ]
           }
 	]
 	[ { "global env. slicing" * } {
@@ -156,7 +156,11 @@ table {
           }
 	]
 	[ { "basic local env. slicing" * } {
-             [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_ldrop" * ]
+             [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_ldrop" "ldrop_sfr" * ]
+          }
+	]
+        [ { "local env. ref. for substitution" * } {
+             [ "lsubs ( ? ≼[?,?] ? )" "lsubs_lsubs" "lsubs_sfr ( ≼[?,?] ? )" * ]
           }
 	]
         [ { "basic term relocation" * } {
@@ -168,10 +172,6 @@ table {
    ]
    class "red"   
    [ { "grammar" * } {
-        [ { "local env. ref. for substitution" * } {
-             [ "lsubs ( ? [?,?] ≼ ? )" "lsubs_lsubs" * ]
-          }
-	]
 	[ { "same head term form" * } {
              [ "tshf ( ? ≈ ? )" "tshf_tshf" * ]
           }