X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fweb%2Fhome%2Fspecification.ldw.xml;h=5c7813d8312de724f16ec869fc187f16df991a64;hb=0cb16b42f119c1cb6135f237092892e2f82929ee;hp=9712c9a83a58685fcfd3a679034c17deaed95fff;hpb=bfdaedc0ea2ee29ce9444ce1283a2642a86e8d86;p=helm.git diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml index 9712c9a83..5c7813d83 100644 --- a/helm/www/lambdadelta/web/home/specification.ldw.xml +++ b/helm/www/lambdadelta/web/home/specification.ldw.xml @@ -28,6 +28,23 @@ + + Informational pages on the specifications are provided. + + + + 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]. + + + + 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). + +

Î»Î´ version 2 (active)

@@ -59,19 +76,6 @@ Core, Applications. - - - 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]. - - - - 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). - @@ -130,5 +134,12 @@ + + Informational pages on the parts of the specification: + + Core. + + +