]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
update in ground_2, static_2, basic_2, apps_2, alpha_1
[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / web / ground_2_src.tbl
index 0fcbd11553d9b27f5068157d050086c4a2326cd0..15bd8bfc222b61d43af725f7ee26b2503dd7f269 100644 (file)
@@ -12,8 +12,8 @@ table {
    class "water"
    [ { "generic rt-transition counter" * } {
         [ { "" * } {
-             [ "rtc_ist ( ð\9d\90\93â¦\83?,?â¦\84 )" "rtc_ist_shift" "rtc_ist_plus" "rtc_ist_max" * ]
-             [ "rtc ( â\8c©?,?,?,?â\8cª ) ( ð\9d\9f\98ð\9d\9f\98 ) ( ð\9d\9f\99ð\9d\9f\98 ) ( ð\9d\9f\98ð\9d\9f\99 )" "rtc_isrc ( ð\9d\90\91ð\9d\90\93â¦\83?,?â¦\84 )" "rtc_shift ( ↕*? )" "rtc_max ( ? ∨ ? )" "rtc_plus ( ? + ? )" * ]
+             [ "rtc_ist ( ð\9d\90\93â\9dª?,?â\9d« )" "rtc_ist_shift" "rtc_ist_plus" "rtc_ist_max" * ]
+             [ "rtc ( â\8c©?,?,?,?â\8cª ) ( ð\9d\9f\98ð\9d\9f\98 ) ( ð\9d\9f\99ð\9d\9f\98 ) ( ð\9d\9f\98ð\9d\9f\99 )" "rtc_isrc ( ð\9d\90\91ð\9d\90\93â\9dª?,?â\9d« )" "rtc_shift ( ↕*? )" "rtc_max ( ? ∨ ? )" "rtc_plus ( ? + ? )" * ]
           }
         ]
      }
@@ -22,24 +22,24 @@ table {
    [ { "multiple relocation" * } {
         [ { "" * } {
              [ "rtmap" "rtmap_eq ( ? ≡ ? )" "rtmap_pushs ( ⫯*[?]? )" "rtmap_nexts ( ↑*[?]? )"
-               "rtmap_tl ( â«±? )" "rtmap_tls ( â«±*[?]? )" "rtmap_isid ( ð\9d\90\88â¦\83?â¦\84 )" "rtmap_id" "rtmap_isdiv ( ð\9d\9b\80â¦\83?â¦\84 )"
-               "rtmap_fcla ( ð\9d\90\82â¦\83?â¦\84 â\89\98 ? )" "rtmap_isfin ( ð\9d\90\85â¦\83?â¦\84 )" "rtmap_isuni ( ð\9d\90\94â¦\83?â¦\84 )" "rtmap_uni ( ð\9d\90\94â\9d´?â\9dµ )"
+               "rtmap_tl ( â«±? )" "rtmap_tls ( â«±*[?]? )" "rtmap_isid ( ð\9d\90\88â\9dª?â\9d« )" "rtmap_id" "rtmap_isdiv ( ð\9d\9b\80â\9dª?â\9d« )"
+               "rtmap_fcla ( ð\9d\90\82â\9dª?â\9d« â\89\98 ? )" "rtmap_isfin ( ð\9d\90\85â\9dª?â\9d« )" "rtmap_isuni ( ð\9d\90\94â\9dª?â\9d« )" "rtmap_uni ( ð\9d\90\94â\9d¨?â\9d© )"
                "rtmap_sle ( ? ⊆ ? )" "rtmap_sdj ( ? ∥ ? )" "rtmap_sand ( ? ⋒ ? ≘ ? )" "rtmap_sor ( ? ⋓ ? ≘ ? )"
-               "rtmap_at ( @â¦\83?,?â¦\84 â\89\98 ? )" "rtmap_istot ( ð\9d\90\93â¦\83?â¦\84 )" "rtmap_after ( ? ⊚ ? ≘ ? )" "rtmap_coafter ( ? ~⊚ ? ≘ ? )"
-               "rtmap_basic ( ð\9d\90\81â\9d´?,?â\9dµ )" "rtmap_basic_after"
+               "rtmap_at ( @â\9dª?,?â\9d« â\89\98 ? )" "rtmap_istot ( ð\9d\90\93â\9dª?â\9d« )" "rtmap_after ( ? ⊚ ? ≘ ? )" "rtmap_coafter ( ? ~⊚ ? ≘ ? )"
+               "rtmap_basic ( ð\9d\90\81â\9d¨?,?â\9d© )" "rtmap_basic_after"
              * ]
              [ "nstream ( ⫯? ) ( ↑? )" "nstream_eq" "" ""
                "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" ""
                "" "" "" ""
                "" "" "" "nstream_sor"
-               "" "nstream_istot ( ?@â\9d´?â\9dµ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
+               "" "nstream_istot ( ?@â\9d¨?â\9d© )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
                "nstream_basic" ""
              * ]
 (*
-             [ "trace ( â\88¥?â\88¥ )" "trace_at ( @â¦\83?,?â¦\84 â\89\98 ? )" "trace_after ( ? â\8a\9a ? â\89\98 ? )" "trace_isid ( ð\9d\90\88â¦\83?â¦\84 )" "trace_isun ( ð\9d\90\94â¦\83?â¦\84 )"
+             [ "trace ( â\88¥?â\88¥ )" "trace_at ( @â\9dª?,?â\9d« â\89\98 ? )" "trace_after ( ? â\8a\9a ? â\89\98 ? )" "trace_isid ( ð\9d\90\88â\9dª?â\9d« )" "trace_isun ( ð\9d\90\94â\9dª?â\9d« )"
                "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≘ ? )" "trace_snot ( ∁ ? )" * ]
 *)
-             [ "mr2 ( ◊ ) ( {?,?};? )" "mr2_at ( @⦃?,?⦄ ≘ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≘ ? )" * ]
+             [ "mr2 ( ◊ ) ( ❨?,?❩;? )" "mr2_at ( @❪?,?❫ ≘ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≘ ? )" * ]
           }
         ]
      }