]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / ground / web / ground_src.tbl
index 2b655f20c4b71fbf3ceedd5b7ff8beb09fe81465..485443977aaea0681948b81a269e7c2dfc0b3f14 100644 (file)
@@ -30,11 +30,12 @@ table {
         }
       ]
       [ { "total relocation" * } {
-          [ "tr_uni ( 𝐮❨?❩ )" * ]
-          [ "tr_id ( 𝐢 ) " * ]
-          [ "tr_compose ( ?∘? )" "tr_compose_pn" * ]
-          [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_pat" "tr_pap_pn" "tr_pap_pap" * ]
-          [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_hdtl" "tr_pn_tls" * ]
+          [ "tr_uni ( 𝐮❨?❩ )" "tr_uni_pap" "tr_uni_compose" * ]
+          [ "tr_id ( 𝐢 ) " "tr_id_pushs" "tr_id_pap" * ]
+          [ "tr_compose ( ?∘? )" "tr_compose_eq" "tr_compose_tls" "tr_compose_pn" "tr_compose_pap" "tr_compose_compose" * ]
+          [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
+          [ "tr_pushs ( ⫯*[?]? )" * ]
+          [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_eq" "tr_pn_hdtl" "tr_pn_tls" * ]
           [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
         }
       ]
@@ -60,7 +61,7 @@ table {
           [ "pr_nexts ( ↑*[?]? )" "pr_nexts_eq" * ]
           [ "pr_pushs ( ⫯*[?]? )" "pr_pushs_eq" * ]
           [ "pr_tl ( ⫰? )" "pr_tl_eq" "pr_tl_eq_eq" * ]
-          [ "pr_eq ( ? â\89¡ ? )" * ]
+          [ "pr_eq ( ? â\89\90 ? )" * ]
           [ "pr_map ( ⫯? ) ( ↑? )" * ]
         }
       ]
@@ -109,7 +110,7 @@ table {
           [ "nat_max ( ?∨? )" * ]
           [ "nat_minus ( ?-? )" "nat_minus_plus" * ]
           [ "nat_plus ( ?+? )" "nat_plus_pred" "nat_plus_rplus" * ]
-          [ "nat_rplus ( ?+? )" "nat_rplus_succ" * ]
+          [ "nat_rplus ( ?+? )" "nat_rplus_pplus" "nat_rplus_succ" * ]
           [ "nat_pred ( ↓? )" "nat_pred_succ" * ]
           [ "nat_succ ( ↑? )" "nat_succ_iter" "nat_succ_tri" * ]
           [ "nat ( 𝟎 )" "nat_iter ( ?^{?}? )" *"nat_tri"  ]
@@ -128,8 +129,8 @@ table {
   class "yellow"
   [ { "extensions to the library" * } {
       [ { "streams" * } {
-          [ "stream_tls ( ⇂*{?}[?]? )" "stream_tls_eq" * ]
-          [ "stream_hdtl ( ⇃{?}? ) ( ⇂{?}? )" * ]
+          [ "stream_tls ( ⇂*{?}[?]? )" "stream_tls_eq" "stream_tls_plus" * ]
+          [ "stream_hdtl ( ⇃{?}? ) ( ⇂{?}? )" "stream_hdtl_eq" * ]
           [ "stream_eq ( ? ≗{?} ? )" "stream_eq_eq" * ]
           [ "stream ( ? ⨮{?} ? )" * ]
         }
@@ -143,7 +144,7 @@ table {
       [ { "" * } {
           [ "bool ( Ⓕ ) ( Ⓣ )" "bool_or" "bool_and" * ]
           [ "ltc" "ltc_ctc" * ]
-          [ "logic ( â\8a¥ ) ( â\8a¤ )" "relations ( ? â\8a\86 ? )" "functions" "exteq ( ? â\89\90{?,?} ? )" "star" "lstar_2a" * ]
+          [ "logic ( â\8a¥ ) ( â\8a¤ )" "relations ( ? â\8a\86 ? )" "functions" "exteq ( ? â\8a\9c{?,?} ? )" "star" "lstar_2a" * ]
         }
       ]
     }