X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fweb%2Fhome%2Fbasic_2_blk.tbl;h=ed50adf79e14310e06514b8bfa869f724d4bb13d;hb=0fa1d4541bec571d84c726c488ba500a269bfb07;hp=8c4ee482733d1d38ac99250a069898dde70cf848;hpb=1d7c90aaa2a5d5dadb3bca87d56bf717efab4361;p=helm.git

diff --git a/helm/www/lambda_delta/web/home/basic_2_blk.tbl b/helm/www/lambda_delta/web/home/basic_2_blk.tbl
index 8c4ee4827..ed50adf79 100644
--- a/helm/www/lambda_delta/web/home/basic_2_blk.tbl
+++ b/helm/www/lambda_delta/web/home/basic_2_blk.tbl
@@ -9,30 +9,38 @@ table {
    } ]
    [ { "{X | Γ ⊢ X : W}" * } {
       class "wine" [
-         [ "typed abstraction **" ] [ "Γ ⊢ λW" ]
+         [ "local typed abstraction *" ] [ "Γ ⊢ +λW" ]
          [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
       ]
       class "magenta" [
-         [ "typed declaration ***" ] [ "Γ ⊢ pλW" ] 
-	 [ "no" ] [ "no" ] [ "no" ] [ "$p" ]
+         [ "local typed declaration **" ] [ "Γ ⊢ -λW" ]
+         [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ]
       ]
       class "prune" [
+         [ "global typed declaration ***" ] [ "Γ ⊢ pλW" ] 
+	 [ "no" ] [ "no" ] [ "no" ] [ "$p" ]
+      ]
+      class "blue" [
          [ "native type annotation *" ] [ "Γ ⊢ ⓝW" ]
 	 [ "no" ] [ "no" ] [ "yes" ] [ "no" ]
       ]
    } ]
    [ { "{X | Γ ⊢ X = V}" * } {
-      class "blue" [
-         [ "local abbreviation **" ] [ "Γ ⊢ δV" ] 
+      class "sky" [
+         [ "local abbreviation *" ] [ "Γ ⊢ +δV" ] 
          [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ]
       ]
-      class "sky" [
-         [ "global abbreviation ***" ] [ "Γ ⊢ pδV" ]
+      class "cyan" [
+         [ "local definition **" ] [ "Γ ⊢ -δV" ] 
+         [ "no" ] [ "local →δ" ] [ "no" ] [ "#i" ]
+      ]      
+      class "water" [
+         [ "global definition ***" ] [ "Γ ⊢ pδV" ]
          [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ]
       ]
    } ]
    [ { "no" * } {
-      class "cyan" [
+      class "green" [
          [ "sort ****" ] [ "Γ ⊢ ⋆k" ]
 	 [ "no" ] [ "no" ] [ "no" ] [ "no" ]
       ]
@@ -42,4 +50,3 @@ table {
 class "text" { 0 } { 2 * }
 
 class "plane" { 1 }
-