From e90313fa853ba63f29416c2d0de40b13c913e567 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 22 Jan 2015 12:10:43 +0000 Subject: [PATCH] informational page on ground_1 --- helm/www/lambdadelta/BTM.html | 2 +- helm/www/lambdadelta/apps_2.html | 22 +- helm/www/lambdadelta/basic_1.html | 4 +- helm/www/lambdadelta/basic_2.html | 14 +- helm/www/lambdadelta/documentation.html | 4 +- helm/www/lambdadelta/ground_1.html | 280 ++++++++++++++++++ helm/www/lambdadelta/ground_2.html | 77 +++-- helm/www/lambdadelta/implementation.html | 4 +- helm/www/lambdadelta/index.html | 4 +- helm/www/lambdadelta/news.html | 4 +- helm/www/lambdadelta/specification.html | 9 +- helm/www/lambdadelta/web/home/sitemap.tbl | 3 +- .../web/home/specification.ldw.xml | 3 +- .../lambdadelta/ground_2/web/ground_2_src.tbl | 14 +- 14 files changed, 382 insertions(+), 62 deletions(-) create mode 100644 helm/www/lambdadelta/ground_1.html diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 8cda8f76a..1e6bf7d9c 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Tue, 20 Jan 2015 18:39:00 +0100
+
Last update: Wed, 21 Jan 2015 17:13:08 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 7938d47da..a4ec380fb 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -90,7 +90,7 @@ version 1 - (core) + (background - core) (static HELM directory) helena @@ -124,7 +124,7 @@
Summary of the Specification [spacer]
-
Here is a numerical acount of the specification's contents +
Here is a numerical account of the specification's contents and its timeline.
@@ -152,29 +152,29 @@ sizes files - 4 + 14 characters - 68581 + 6787 nodes - 3637 + 10070 propositions theorems 2 lemmas - 1 + 4 total - 3 + 6 concepts declared - 3 + 6 defined - 9 + 11 total - 12 + 17 @@ -258,6 +258,6 @@

-
Last update: Tue, 20 Jan 2015 18:39:00 +0100
+
Last update: Wed, 21 Jan 2015 17:13:08 +0100
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 4871fb70f..0965840d7 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -90,7 +90,7 @@ version 1 - (core) + (background - core) (static HELM directory) helena @@ -823,6 +823,6 @@

-
Last update: Tue, 20 Jan 2015 18:39:00 +0100
+
Last update: Wed, 21 Jan 2015 17:13:08 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index b05d3b07d..ca505d647 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -90,7 +90,7 @@ version 1 - (core) + (background - core) (static HELM directory) helena @@ -116,7 +116,7 @@ -->
Summary of the Specification [spacer]
-
Here is a numerical acount of the specification's contents +
Here is a numerical account of the specification's contents and its timeline.
@@ -148,7 +148,7 @@ characters 433402 nodes - 1874774 + 1874778 propositions @@ -211,7 +211,7 @@
  • 2014 April 16. Lazy equivalence on local environments - addded as q-step to rst-computation on closures + added as q-step to rst-computation on closures (anniversary milestone).
    • @@ -1019,7 +1019,7 @@
    - contxt-sensitive multiple rt-substitution + context-sensitive multiple rt-substitution cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? ) cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? ) cpys_lift cpys_cpys @@ -1159,7 +1159,7 @@
    - contxt-sensitive ordinary rt-substitution + context-sensitive ordinary rt-substitution cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) cpy_lift cpy_nlift cpy_cpy @@ -1384,6 +1384,6 @@

    -
    Last update: Tue, 20 Jan 2015 18:39:00 +0100
    +
    Last update: Wed, 21 Jan 2015 17:13:08 +0100
    diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 2b7aee243..ffa999aa2 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -90,7 +90,7 @@ version 1 - (core) + (background - core) (static HELM directory) helena @@ -366,6 +366,6 @@

    -
    Last update: Tue, 20 Jan 2015 18:38:59 +0100
    +
    Last update: Wed, 21 Jan 2015 17:13:08 +0100
    diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html new file mode 100644 index 000000000..7c788ec66 --- /dev/null +++ b/helm/www/lambdadelta/ground_1.html @@ -0,0 +1,280 @@ + + + + + + + + + + \lambda\delta home page + + + + + + +
    + + [lambdadelta home] + +
    +
    cic:/BOLOGNA/lambdadelta/ground_1/ (background for λδ version 1)
    +
    + [Spacer] +
    +
    +
    +
    +
    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    + home + + news + + documentation + + specification + +
    +     		+
    +     		+ implementation + +
    +
    + foreword + + milestones + + version 2 + + version 2 + (background - core - applications) +
    +     		+ library + (static LDDL directory)
    + citations + + visibility + + version 1 + + version 1 + (background - core)(static HELM directory) + helena + +
    +
    +
    +
    Summary of the Specification [spacer] +
    +
    Here is a numerical account of the specification's contents + and its timeline. +
    +
    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    categoryobjects +
    +     		+
    +     		+
    +     		+
    +     		+
    +
    sizesfiles10characters15063nodes +
    propositionstheorems0lemmas50total50
    conceptsdeclared24defined4total28
    +
    +
      +
    • + January 2015. + Update with backports from the abandoned specification of λδ version 2. +
      • +
    +
      +
    • + May 2008. + Specification is concluded. +
      • +
    +
      +
    • + May 2004. + Specification starts. +
      • +
    +
    Logical Structure of the Specification [spacer] +
    +
    This table reports the specification's components and their planes. +
    +
    + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
    componentplanefiles +
    +     		+
    +     		+
    +
    extensions to the library + + bg_hints + + bg_blt + + bg_plist + +
    +
    generated logical decomposables + + bg_types + + bg_props + +
    +     		+
    +
    preamble + + bg_require + + bg_rewrite + + bg_tactics + + bg_subst +
    +
    +
    + [Spacer] +
    +
    +
    +
    +
    + + [Valid XHTML 1.1] + + + [Valid CSS level 2] + + + [Generated from XML via XSL] + + + [PNG used here] + + + [Viewable with any browser] + +
    +
    +
    +
    +
    Last update: Wed, 21 Jan 2015 17:13:08 +0100
    + + diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 92bd89f68..17b7562e3 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -90,7 +90,7 @@ version 1 - (core) + (background - core) (static HELM directory) helena @@ -104,7 +104,7 @@
    Summary of the Specification [spacer]
    -
    Here is a numerical acount of the specification's contents +
    Here is a numerical account of the specification's contents and its timeline.
    @@ -134,7 +134,7 @@ files 30 characters - 68581 + 46649 nodes 62380 @@ -208,26 +208,53 @@ - natural numbers with infinity + natural numbers with infinity + + ynat ( ∞ ) + ynat_pred ( ⫰? ) + ynat_succ ( ⫯? ) + ynat_le ( ? ≤ ? ) + ynat_lt ( ? < ? ) + ynat_minus ( ? - ? ) + ynat_plus ( ? + ? ) + ynat_max + ynat_min + + + extensions to the library - ynat ( ∞ ) - ynat_pred ( ⫰? ) - ynat_succ ( ⫯? ) - ynat_le ( ? ≤ ? ) - ynat_lt ( ? < ? ) - ynat_minus ( ? - ? ) - ynat_plus ( ? + ? ) - ynat_max - ynat_min + star + lstar + bool ( Ⓕ ) ( Ⓣ ) + arith ( ?^? ) + list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) + +
    + + +
    + + +
    + + +
    + - extensions to the library + generated logical decomposables - star - lstar - bool ( Ⓕ ) ( Ⓣ ) - arith ( ?^? ) - list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) + xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ ) + xoa_props ( ⊥ ) ( ⊤ ) + +
    + + +
    + + +
    +
    @@ -242,10 +269,14 @@ - generated logical decomposables + - xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ ) - xoa_props ( ⊥ ) ( ⊤ ) + +
    + + +
    +
    @@ -297,6 +328,6 @@

    -
    Last update: Tue, 20 Jan 2015 18:39:00 +0100
    +
    Last update: Wed, 21 Jan 2015 17:13:08 +0100
    diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 5e0673464..82dcacfd5 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -90,7 +90,7 @@ version 1 - (core) + (background - core) (static HELM directory) helena @@ -255,6 +255,6 @@

    -
    Last update: Tue, 20 Jan 2015 18:38:59 +0100
    +
    Last update: Wed, 21 Jan 2015 17:13:08 +0100
    diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 60ac77f4d..afc6f7d8a 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -90,7 +90,7 @@ version 1 - (core) + (background - core) (static HELM directory) helena @@ -202,6 +202,6 @@

    -
    Last update: Tue, 20 Jan 2015 18:38:59 +0100
    +
    Last update: Wed, 21 Jan 2015 17:13:08 +0100
    diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 2d4bbb7a9..a1dfcd590 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -90,7 +90,7 @@ version 1 - (core) + (background - core) (static HELM directory) helena @@ -335,6 +335,6 @@

    -
    Last update: Tue, 20 Jan 2015 18:38:59 +0100
    +
    Last update: Wed, 21 Jan 2015 17:13:08 +0100
    diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 47b54eed9..464ace831 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -90,7 +90,7 @@ version 1 - (core) + (background - core) (static HELM directory) helena @@ -299,8 +299,9 @@
    Informational pages on the parts of the specification: -Core. -
    + Background, + Core. +
    [Spacer]
    @@ -327,6 +328,6 @@

    -
    Last update: Tue, 20 Jan 2015 18:39:00 +0100
    +
    Last update: Wed, 21 Jan 2015 17:13:08 +0100
    diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl index 8d6b24e85..e3c2b0525 100644 --- a/helm/www/lambdadelta/web/home/sitemap.tbl +++ b/helm/www/lambdadelta/web/home/sitemap.tbl @@ -24,7 +24,8 @@ table [ @@("apps_2" "applications") ^ ")" * ] [ @@("specification#v1" "version 1") - "(" ^ @@("basic_1" "core") ^ ")" + "(" ^ @@("ground_1" "background") + "-" + + @@("basic_1" "core") ^ ")" "(" ^ @@("static/matita/lambdadelta/" "static HELM directory") ^ ")" * ] } diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml index 5c7813d83..556549c39 100644 --- a/helm/www/lambdadelta/web/home/specification.ldw.xml +++ b/helm/www/lambdadelta/web/home/specification.ldw.xml @@ -136,9 +136,8 @@ Informational pages on the parts of the specification: - + Background, Core. -