]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
- grafiteParser: we added the comand "defined" as a presentational
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl
index 1723a00052b6e7cca30d88c405538c221404abbc..c31b9bf066fe0f559a84b5b53f0554ed43b5bced 100644 (file)
@@ -12,7 +12,7 @@ table {
    class "wine"
    [ { "examples" * } {
         [ { "terms with special features" * } {
-             [ "ex_sta_ldec" + "ex_cpr_omega" + "ex_fpbg_refl" * ]
+             [ "ex_sta_ldec" + "ex_cpr_omega" + "ex_fpbg_refl" + "ex_snv_eta" * ]
           }
         ]
      }
@@ -52,7 +52,7 @@ table {
         ]
         [ { "stratified native validity" * } {
              [ "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
-             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_scpes" + "snv_preserve" * ]
+             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" * ]
           }
         ]
      }