]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
refinement for extended substitution completed
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl
index a5148f07e3e4aada49df2b2afd376879e86036a1..5c4006b1c644897e75f37f2fbe20126042d09e68 100644 (file)
@@ -240,11 +240,11 @@ table {
           }
         ]
         [ { "contxt-sensitive extended substitution" * } {
-             [ "cpy ( ⦃?,?⦄ ⊢ ? ×▶[?,?] ? )" "cpy_lift" + "cpy_cpy" * ]
+             [ "cpy ( ⦃?,?⦄ ⊢ ? ▶×[?,?] ? )" "cpy_lift" + "cpy_cpy" * ]
           }
         ]        
         [ { "local env. ref. for extended substitution" * } {
-             [ "lsuby ( ? ×⊑ ? )" "lsuby_lsuby" * ]
+             [ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ]
           }
         ]
         [ { "restricted local env. ref." * } {
@@ -269,7 +269,7 @@ table {
    class "red"
    [ { "grammar" * } {
         [ { "equivalence for local environments" * } {
-             [ "leq ( ? ≃[?,?] ? ) " * ]
+             [ "leq ( ? ≃[?,?] ? )" * ]
           }
         ]
         [ { "pointwise extension of a relation" * } {