X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fwww%2Flambdadelta%2Fspecification.html;h=839278835d95546b623e097006e7fc435f170c57;hb=f10cfe417b6b8ec1c7ac85c6ecf5fb1b3fdf37db;hp=4ecf9994cc69fcc390c16feb17b850388058ef31;hpb=836e4f30514bceb27394604bbfbae31a62723dae;p=helm.git
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index 4ecf9994c..839278835 100644
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -122,8 +122,8 @@
@@ -146,7 +146,7 @@
- ![lambdadelta butterfly [spacer]](http://lambdadelta.info/images/b4.png) λδ version 2 (in progress)
+ λδ version 2 (ongoing)
The formal specification of λδ version 2
is available in the following formats:
@@ -160,7 +160,11 @@
Source scripts.
- Notice: compile with the latest version of Matita from
+ The scripts are grouped in directories, first by part, then by component.
+
+
+ Notice:
+ the scripts are checked by the latest version of Matita from
HELM Subversion repository
at path <trunk/matita/>.
@@ -173,6 +177,12 @@
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].
+
@@ -185,15 +195,20 @@
|