X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=08790c17e402ea0ac5ad0eb86123d3670eaff9b7;hb=658c000ee2ea2da04cf29efc0acdaf16364fbf5e;hp=7f5ada5fd4507a58f1d1793ed569cd74cba67166;hpb=68b5af5ca8f1e7f98485b92692b3dcb1ae240d19;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 7f5ada5fd..08790c17e 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -23,7 +23,7 @@
[Spacer]
-
+

@@ -45,9 +45,15 @@
- + +
+ + implementation + +
+ @@ -63,9 +69,13 @@ version 2 (background - core - applications) - + +
+ + library + (static LDDL directory) @@ -80,23 +90,24 @@ version 1 - -
- - + (background - core) + (static HELM directory) + helena + +
+
- -
Summary of the Specification [spacer] +
Summary of the Specification [spacer]
-
Here is a numerical acount of the specification's contents +
Here is a numerical account of the specification's contents and its timeline.
-
+
@@ -148,24 +159,23 @@
-
    +
    • 2013 November 27. Natural numbers with infinity.
    -
      +
      • 2011 August 10. Specification starts.
      - -
      Logical Structure of the Specification [spacer] +
      Logical Structure of the Specification [spacer]
      -
      This table reports the specification's components and their planes. +
      This table reports the specification's components and their planes.
      -
      +
      @@ -198,26 +208,53 @@ - + + + + + + + + + + + + + - - - - - - - - + + + + + + + + + - + - - - - + + + + + @@ -232,10 +269,14 @@ - + - + + @@ -261,8 +302,7 @@
      natural numbers with infinitynatural numbers with infinity + ynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ? ≤ ? )ynat_lt ( ? < ? )ynat_minus ( ? - ? )ynat_plus ( ? + ? )ynat_maxynat_min
      extensions to the library - ynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ? ≤ ? )ynat_lt ( ? < ? )ynat_minus ( ? - ? )ynat_plus ( ? + ? )ynat_maxynat_minstarlstarbool ( Ⓕ ) ( Ⓣ )arith ( ?^? )list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| ) +
      +
      +
      +
      +
      +
      +
      +
      extensions to the librarygenerated logical decomposables - starlstarbool ( Ⓕ ) ( Ⓣ )arith ( ?^? )list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) +
      +
      +
      +
      +
      +

      generated logical decomposables - xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) +
      +
      +
      +

      - -
      +
      [Spacer]
      @@ -288,6 +328,6 @@

      -
      Last update: Wed, 24 Dec 2014 22:58:52 +0100
      - +
      Last update: Fri, 06 Mar 2015 17:53:24 +0100
      +