X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fweb%2Fground_src.tbl;h=80d76fbe080bb36c23b8bf8843154458454e9945;hb=f31020f1ae14e28c246b6cd9cf91b5864f4f536a;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..80d76fbe0 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -22,16 +22,20 @@ table {
   class "green"
   [ { "relocation maps" * } {
       [ { "finite relocation with pairs" * } {
-          [ "fr2_nat ( @❨?,?❩ ≘ ? )" "fr2_nat_nat" * ]
+          [ "fr2_nat ( ＠⧣❨?,?❩ ≘ ? )" "fr2_nat_nat" * ]
           [ "fr2_minus ( ? ▭ ? ≘ ? )" * ]
-          [ "fr2_append ( ?;;? )" * ]
+          [ "fr2_append ( ?●? )" * ]
           [ "fr2_plus ( ?+? )" * ]
-          [ "fr2_map ( 𝐞 ) ( ❨?,?❩;? )" * ]
+          [ "fr2_map ( 𝐞 ) ( ❨?,?❩◗? )" * ]
         }
       ]
       [ { "total relocation" * } {
-          [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_pat" "tr_pap_pn" "tr_pap_pap" * ]
-          [ "tr_pn ( ⫯? ) ( ↑? )" * ]
+          [ "tr_uni ( 𝐮❨?❩ )" "tr_uni_eq" "tr_uni_hdtl" "tr_uni_tls" "tr_uni_pap" "tr_uni_compose" * ]
+          [ "tr_id ( 𝐢 ) " "tr_id_hdtl" "tr_id_pushs" "tr_id_tls" "tr_id_pap" "tr_id_compose" * ]
+          [ "tr_compose ( ?∘? )" "tr_compose_eq" "tr_compose_tls" "tr_compose_pn" "tr_compose_pushs" "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" * ]
         }
       ]
@@ -48,8 +52,8 @@ table {
           [ "pr_fcla ( 𝐂❨?❩ ≘ ? )" "pr_fcla_eq" "fcla_uni" "pr_fcla_fcla" * ]
           [ "pr_isu ( 𝐔❨?❩ )" "pr_isu_tl" "pr_isu_uni" * ]
           [ "pr_isi ( 𝐈❨?❩ )" "pr_isi_eq" "pr_isi_tl" "pr_isi_pushs" "pr_isi_tls" "pr_isi_id" "pr_isi_uni" "pr_isi_pat" "pr_isi_nat" * ]
-          [ "pr_nat ( @↑❨?,?❩ ≘ ? )" "pr_nat_uni" "pr_nat_basic" "pr_nat_nat" * ]
-          [ "pr_pat ( @❨?,?❩ ≘ ? )" "pr_pat_lt" "pr_pat_eq" "pr_pat_tls" "pr_pat_id" "pr_pat_uni" "pr_pat_basic" "pr_pat_pat" "pr_pat_pat_id" * ]
+          [ "pr_nat ( ＠§❨?,?❩ ≘ ? )" "pr_nat_uni" "pr_nat_basic" "pr_nat_nat" * ]
+          [ "pr_pat ( ＠⧣❨?,?❩ ≘ ? )" "pr_pat_lt" "pr_pat_eq" "pr_pat_tls" "pr_pat_id" "pr_pat_uni" "pr_pat_basic" "pr_pat_pat" "pr_pat_pat_id" * ]
           [ "pr_basic ( 𝐛❨?,?❩ )" * ]
           [ "pr_uni ( 𝐮❨?❩ )" "pr_uni_eq" * ]
           [ "pr_id ( 𝐢 ) " "pr_id_eq" * ]
@@ -57,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 ( ? ≡ ? )" * ]
+          [ "pr_eq ( ? ≐ ? )" * ]
           [ "pr_map ( ⫯? ) ( ↑? )" * ]
         }
       ]
@@ -67,10 +71,10 @@ table {
             "" "" "nstream_isid" "nstream_id ( 𝐢 )" ""
             "" "" "" ""
             "" "" "" "nstream_sor"
-            "" "nstream_istot ( ?@❨?❩ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
+            "" "nstream_istot ( ?＠⧣❨?❩ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
             "nstream_basic" ""
           * ]
-          [ "trace ( ∥?∥ )" "trace_at ( @❨?,?❩ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈❨?❩ )" "trace_isun ( 𝐔❨?❩ )"
+          [ "trace ( ∥?∥ )" "trace_at ( ＠⧣❨?,?❩ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈❨?❩ )" "trace_isun ( 𝐔❨?❩ )"
             "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≘ ? )" "trace_snot ( ∁ ? )"
           * ]
         }
@@ -106,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"  ]
@@ -125,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 ( ? ⨮{?} ? )" * ]
         }
@@ -140,7 +144,7 @@ table {
       [ { "" * } {
           [ "bool ( Ⓕ ) ( Ⓣ )" "bool_or" "bool_and" * ]
           [ "ltc" "ltc_ctc" * ]
-          [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ]
+          [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ⊜{?,?} ? )" "star" "lstar_2a" * ]
         }
       ]
     }