X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fspecification.html;h=412740783ddf216b59eaf98cf9a9b21ef0da8e77;hb=15455aa487e001c643b4f46daf82612b8409f1ae;hp=5ae4a84853d70deab334609430c59ea1238d7836;hpb=7dc9dcddc88440527569d2a7216461bcd7398ab2;p=helm.git diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index 5ae4a8485..412740783 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -45,6 +45,9 @@
+ +
+ implementation @@ -66,6 +69,9 @@ version 2 (background - core - applications) + +
+ library @@ -84,6 +90,7 @@ version 1 + (background - core) (static HELM directory) helena @@ -171,6 +178,26 @@ +
+ Informational pages on the specifications are provided. +
+ +
[spacer] λδ version 2 (active)
@@ -201,19 +228,6 @@ Background, Core, Applications. - -
- Notice on numerical acounts: - nodes are counted according to the "intrinsic complexity measure" - [F. Guidi: "Procedural Representation of CIC Proof Terms" - Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78]. -
-
- Notice on displayed logical structures: - from the logical standpoint, the source scripts are grouped in "planes" - and these are grouped in "components"; - the notation for the relations or functions - introduced in each script, is shown in parentheses (? are placeholders).
@@ -228,7 +242,13 @@ lambdadelta_1 for Coq 7.3.1 (revised 2015-01). Source scripts. -
+ +
The scripts are grouped in directories, one for each part.
@@ -277,6 +297,11 @@ Notice: the HELM rendering engine is offline. +
+ Informational pages on the parts of the specification: + Background, + Core. +
[Spacer]
@@ -303,6 +328,6 @@

-
Last update: Sun, 11 Jan 2015 18:32:40 +0100
+
Last update: Fri, 06 Mar 2015 17:53:24 +0100