X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fweb%2Fground_src.tbl;h=528c13cf426e8fc9554ee31d7a18d48c4a705da5;hb=8db3579bec4d9a97af526f95a179587a2fbfe3e3;hp=6253faa4c28d132eb3ab0e124000d46d28011322;hpb=2e4a7c54ef77c10cb1cef4b59518c473245ea935;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 6253faa4c..528c13cf4 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -24,14 +24,17 @@ table {
       [ { "finite relocation with pairs" * } {
           [ "fr2_nat ( @❨?,?❩ ≘ ? )" "fr2_nat_nat" * ]
           [ "fr2_minus ( ? ▭ ? ≘ ? )" * ]
-          [ "fr2_append ( ?;;? )" * ]
+          [ "fr2_append ( ?●? )" * ]
           [ "fr2_plus ( ?+? )" * ]
-          [ "fr2_map ( 𝐞 ) ( ❨?,?❩;? )" * ]
+          [ "fr2_map ( 𝐞 ) ( ❨?,?❩◗? )" * ]
         }
       ]
       [ { "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 ( ⫯? ) ( ↑? )" "tr_pn_hdtl" "tr_pn_tls" * ]
           [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
         }
       ]
@@ -57,7 +60,7 @@ table {
           [ "pr_nexts ( ↑*[?]? )" "pr_nexts_eq" * ]
           [ "pr_pushs ( ⫯*[?]? )" "pr_pushs_eq" * ]
           [ "pr_tl ( â«°? )" "pr_tl_eq" "pr_tl_eq_eq" * ]
-          [ "pr_eq ( ? ≡ ? )" * ]
+          [ "pr_eq ( ? ≐ ? )" * ]
           [ "pr_map ( ⫯? ) ( ↑? )" * ]
         }
       ]
@@ -140,7 +143,7 @@ table {
       [ { "" * } {
           [ "bool ( Ⓕ ) ( Ⓣ )" "bool_or" "bool_and" * ]
           [ "ltc" "ltc_ctc" * ]
-          [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ]
+          [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ⊜{?,?} ? )" "star" "lstar_2a" * ]
         }
       ]
     }