X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fweb%2Fbasic_2_src.tbl;h=799c4c95031c64976e878d28655ec50d26e3a9dc;hb=90ee1e85245752414b93826aabe388409571187a;hp=21fd5fcca9d0bb7197c950cd40432712ffeaa2fc;hpb=e02bd4f3df78b5cc374d49d0ddf48b311188f514;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 21fd5fcca..799c4c950 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
@@ -10,6 +10,14 @@ table {
      }
    ]
 (*
+   class "wine"
+   [ { "examples" * } {
+        [ { "" * } {
+             [ "" * ]
+          }
+        ]
+     }
+   ]
    class "magenta"
    [ { "higher order dynamic typing" * } {
         [ { "higher order native type assignment" * } {
@@ -44,35 +52,25 @@ table {
           }
         ]
         [ { "stratified native validity" * } {
-             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?] )" "snv_lift" + "snv_ltpss_dx" + "snv_ltpss_sn" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_ltpr" + "snv_ltpr" + "snv_cpcs" * ]
+             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?] )" "snv_lift" + "snv_lpss" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_lpr" + "snv_lpr" + "snv_cpcs" * ]
           }
         ]
      }
    ]
    class "blue"
    [ { "equivalence" * } {
-        [ { "focalized equivalence" * } {
-             [ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" + "lfpcs_fpcs" + "lfpcs_lfprs" + "lfpcs_lfpcs" * ]
-             [ "fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )" "fpcs_aaa" + "fpcs_cpcs" + "fpcs_fprs" + "fpcs_fpcs" * ]
-          }
-        ]
         [ { "local env. ref. for stratified static type assignment" * } {
              [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_cpcs" * ]
           }
         ]
         [ { "context-sensitive equivalence" * } {
-             [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_ltpss_dx" + "cpcs_ltpss_sn" + "cpcs_delift" + "cpcs_aaa" + "cpcs_ltpr" + "cpcs_cprs" + "cpcs_cpcs" * ]
+             [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_lpss" + "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ]
           }
         ]
      }
    ]
    class "sky"
    [ { "conversion" * } {
-        [ { "focalized conversion" * } {
-             [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ]
-             [ "fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )" "fpc_fpc" * ]
-          }
-        ]
         [ { "context-sensitive conversion" * } {
              [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ]
           }