X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=87ad0d3c25a609e3b2037ae5f528e5c4907a96ea;hb=9b75ad80a3ee31314c02f113b255ad533a87d3d2;hp=e7891fa0ec8f05c470e2657fc36e84bd50015c97;hpb=22ff568044ad894d0e2a48bae84c13f95ee2d637;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index e7891fa0e..87ad0d3c2 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -6,8 +6,8 @@ - - lambdadelta version 2 + + background for \lambda\delta version 2 @@ -23,7 +23,7 @@
[Spacer]
-
Summary of the Specification
+
Summary of the Specification
Here is a numerical acount of the specification's contents and its timeline. Nodes are counted according to the "intrinsinc complexity measure" @@ -35,50 +35,50 @@ - - - + + - - - - - - - - - - - + + + + + + + - - - - - - - + + + + + + + - - - - - - - + + + + + + +
categoryobjects + categoryobjects
+
+
+
+
sizesfiles26 characters65234nodes44240sizesfiles30characters46649nodes62380
propositionstheorems2lemmas115total117propositionstheorems2lemmas187total189
conceptsdeclared40defined24total64conceptsdeclared40defined25total65
@@ -96,7 +96,7 @@ -
Logical Structure of the Specification
+
Logical Structure of the Specification
The source files are grouped in planes according to the following table. Notation files covering the whole specification are provided. @@ -107,76 +107,96 @@ - - - + + - - - - - + + - - - - - - - - + + + + + + + + + + - - - + + + - - - - - + - - - - + + + + + - - - - @@ -184,7 +204,7 @@
planefiles + planefiles
+
+
+
+
+ +
+
+
+

natural numbers with infinityynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ?≤? )ynat_lt ( ?<? )ynat_minus ( ? - ? )ynat_plus ( ? + ? )natural numbers with infinityynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ?≤? )ynat_lt ( ?<? )ynat_minus ( ? - ? )ynat_plus ( ? + ? )ynat_maxynat_min
extensions to the libraryarith.ma ( ?^? ) + extensions to the libraryarith.ma ( ?^? ) +
+

+
+
+
+
+ +
+

generated logical decomposablesxoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) + generated logical decomposablesxoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) +
+
+
+

+
+
+
+
-
Physical Structure of the Specification
+
Physical Structure of the Specification
The source files are grouped in directories, one for each plane.
@@ -214,6 +234,6 @@

-
Last update: Wed, 04 Dec 2013 15:14:15 +0100
+
Last update: Sun, 05 Oct 2014 16:38:32 +0200