X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=87ad0d3c25a609e3b2037ae5f528e5c4907a96ea;hb=9b75ad80a3ee31314c02f113b255ad533a87d3d2;hp=cd6e401ad4391f22b9452284af5762600b7466c7;hpb=b3fa0689fbbfb2619549ca5fd03570724996ac49;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index cd6e401ad..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 characters71023nodes58438sizesfiles30characters46649nodes62380
propositionstheorems2lemmas165total167propositionstheorems2lemmas187total189
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,96 +107,96 @@ - - - + + - - - - - - - - - - - - - - - - - + + + + + + + + + + - - - + + - - - - - - - - - - - + + + - - - - - - @@ -204,7 +204,7 @@
planefiles + planefiles
+
+
+
+
+
+
+
natural numbers with infinityynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ?≤? )ynat_lt ( ?<? )ynat_minus ( ? - ? )ynat_plus ( ? + ? )ynat_maxynat_minnatural 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.
@@ -234,6 +234,6 @@

-
Last update: Fri, 10 Jan 2014 19:06:18 +0100
+
Last update: Sun, 05 Oct 2014 16:38:32 +0200