X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=62ea59dd506a6158dfa4b173ec58ae29cbec623c;hb=d48d412796a295256c048256c8f7a843e3406980;hp=4dd340fa4a74f76667927225e18e07bfe36b0844;hpb=08726a4392355fb8340894b1dcabccf95d46b565;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 4dd340fa4..62ea59dd5 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
+
+
+
+
sizesfiles29 characters71585nodes58746sizesfiles30characters46649nodes62380
propositionstheorems2lemmas167total169propositionstheorems2lemmas187total189
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: Mon, 20 Jan 2014 17:00:19 +0100
+
Last update: Sat, 04 Oct 2014 22:58:58 +0200