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.
+
+
+ -
+ Notice on displayed 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).
+
+
![lambdadelta butterfly [spacer]](http://lambdadelta.info/images/b4.png) λδ 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).
+
+ -
+ 2015 January 15.
+ 17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
+
+
+
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.
+
@@ -303,6 +328,6 @@
- Last update: Sun, 11 Jan 2015 18:32:40 +0100
+ Last update: Fri, 06 Mar 2015 17:53:24 +0100
|