X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fapps_2.html;h=b9f19d92f2654e35a47c78b69ed4521829d7d0dd;hb=aeb003ab531d9b9faffd46c47204b564009063cf;hp=47d3e3188542c30dc144c9724e05aa47118ca12e;hpb=f694e3336cbdabdeefd86f85d827edfd26bf3464;p=helm.git diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 47d3e3188..b9f19d92f 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -31,7 +31,7 @@ - home + home news @@ -57,7 +57,7 @@ - foreword + foreword milestones @@ -76,12 +76,12 @@ helena -
+ Open Symbolic Notation (OSN) - citations + citations visibility @@ -102,7 +102,7 @@ -
Contents of the Specification [spacer] +
Contents of the Specification [butterfly]
This specification comprises a collection of checked applications of λδ version 2. @@ -122,7 +122,13 @@ Helena 0.8. -
Summary of the Specification [spacer] +
    +
  • + Examples. + Terms of λδ with special features. +
  • +
+
Summary of the Specification [butterfly]
Here is a numerical account of the specification's contents and its timeline. @@ -152,33 +158,39 @@ sizes files - 1 + 2 characters - 217 + 594 nodes - 0 + 779 propositions theorems - 0 + 2 lemmas - 0 + 1 total - 0 + 3 concepts declared 0 defined - 0 + 3 total - 0 + 3
+
    +
  • + 2017 March 6. + The Examples component is moved from the Core directory. +
  • +
  • 2012 February 24. @@ -198,7 +210,7 @@ The MLTT1 component is started.
-
Logical Structure of the Specification [spacer] +
Logical Structure of the Specification [butterfly]
This table reports the specification's components and their planes.
@@ -208,26 +220,12 @@ component plane - files - -
- - - - functional - reduction and type machine - rtm - rtm_step ( ? ⇨ ? ) + files - -
- - relocation - lift ( ↑[?,?] ? ) - -
- + examples + terms with special features + ex_cpr_omega @@ -258,6 +256,6 @@

-
Last update: Sun, 22 May 2016 11:12:18 +0200
+
Last update: Wed, 25 Oct 2017 21:44:35 +0200