X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fweb%2Fground_2_src.tbl;h=ae1acddff5b7308142cd46a762425a75098612b1;hb=a02ba10c669642bd4b75a5b0ac9351c24ddb724a;hp=b99da4bd698ca2cfa93d08ba13d4958443834696;hpb=4b7a1d1c4258c10822823cb5ee1949bcdf81abcb;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index b99da4bd6..ae1acddff 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -1,28 +1,67 @@ name "ground_2_src" table { - class "grey" - [ { "plane" * } { - [ "files" * ] + class "gray" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] } ] - class "yellow" + class "green" + [ { "multiple relocation" * } { + [ { "" * } { + [ "nstream" "nstream_at ( ?@❴?❵ ) ( @⦃?,?⦄ ≡ ? )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" * ] + [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" + "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ] + [ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ] + } + ] + } + ] + class "grass" [ { "natural numbers with infinity" * } { - [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?<? )" "ynat_minus ( ? - ? )" "ynat_plus ( ? + ? )" "ynat_max" "ynat_min" * ] + [ { "" * } { + [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" + "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )" + "ynat_plus ( ? + ? )" * + ] + } + ] } ] - class "orange" + class "yellow" [ { "extensions to the library" * } { - [ "arith.ma ( ?^? )" * ] + [ { "" * } { + [ "stream ( ? @ ? ) ( ? ≐ ? )" "stream_hdtl" * ] + [ "list ( ◊ ) ( ? @ ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ] + [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ⫯? ) ( ⫰? )" * ] + [ "star" "lstar" * ] + } + ] } ] - class "red" + class "orange" [ { "generated logical decomposables" * } { - [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" "xoa_props ( ⊥ ) ( ⊤ )" * ] + [ { "" * } { + [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" "xoa_props ( ⊥ ) ( ⊤ )" * ] + } + ] + } + ] + class "red" + [ { "" * } { + [ { "" * } { + [ * ] + } + ] } ] } -class "plane" { 0 } +class "top" { * } + +class "capitalize italic" { 0 } -class "file" { 1 * } +class "italic" { 1 }