X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fweb%2Fground_src.tbl;h=9fed47266cd5eb7ba39dc1bd477eb20c89280916;hb=f5b6fd3125c0aefa1db23fbdd23b887fa964f385;hp=9ee7ad91a158eacbe6edf238c9ffeb3c7af1ef40;hpb=aa994e4c3126b43753f9ab8780bcb55a1df3f22a;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 9ee7ad91a..9fed47266 100644 --- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl @@ -22,7 +22,7 @@ table { class "green" [ { "relocation maps" * } { [ { "finite relocation with pairs" * } { - [ "fr2_nat ( @❨?,?❩ ≘ ? )" "fr2_nat_nat" * ] + [ "fr2_nat ( @⧣❨?,?❩ ≘ ? )" "fr2_nat_nat" * ] [ "fr2_minus ( ? ▭ ? ≘ ? )" * ] [ "fr2_append ( ?●? )" * ] [ "fr2_plus ( ?+? )" * ] @@ -33,7 +33,7 @@ table { [ "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_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" * ] @@ -53,7 +53,7 @@ table { [ "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_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" * ] @@ -71,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 ( ∁ ? )" * ] }