X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fground_2.html;h=1622d9cffb9346b047c8a3691e7c7d86fdb53348;hb=32def68dd99ad5f20f001e3e76b51afa6f69dec5;hp=e5218996f8e362497548f1df7f8acb5b337263e0;hpb=7562d9781dc4f351ddc3b2f8edd21f4976621948;p=helm.git diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index e5218996f..1622d9cff 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -23,7 +23,7 @@
[Spacer]
-
+

@@ -36,18 +36,24 @@ news + + specification + + +
+ + +
+ documentation - specification + implementation - +
- - implementation - @@ -56,16 +62,20 @@ milestones + + version 2 + + (background - core - applications) + +
+ version 2 - version 2 - - (background - core - applications) - library + (static LDDL directory) @@ -74,29 +84,30 @@ visibility + + version 1 + + (background - core) + (static HELM directory) version 1 - version 1 + helena - +
- - 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.
-
+
@@ -121,51 +132,56 @@ - + - + - + - + - + - + - + - + - +
sizes files3039 characters6858159130 nodes62380107813
propositions theorems29 lemmas187238 total189247
concepts declared4045 defined2528 total6573
-
    +
      +
    • + 2015 October 11. + Multiple relocation with lists of booleans. +
      • +
    +
    • 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.
      -
      +
      @@ -184,40 +200,65 @@ - - + + + + + + + + - + + - + + + + + + + + + + + + + + + - + - - - - - - - - + + + + + + - + - - - - + + @@ -232,14 +273,9 @@ - + - - -

      		+
      		+
      multiple relocation + trace ( ∥?∥ )trace_at ( @⦃?,?⦄ ≡ ? )trace_after ( ? ⊚ ? ≡ ? )trace_isid ( 𝐈⦃?⦄ )trace_sor ( ? ⋓ ? ≡ ? )
      		+

      		+ +
      +       		mr2mr2_at ( @⦃?,?⦄ ≡ ? )mr2_plus ( ? + ? )mr2_minus ( ? ▭ ? ≡ ? )
      		+
      +
      natural numbers with infinity + ynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ? ≤ ? )ynat_lt ( ? < ? )ynat_plus ( ? + ? )
      natural numbers with infinityextensions to the library - ynat ( ∞ )ynat_pred ( ⫰? )ynat_succ ( ⫯? )ynat_le ( ? ≤ ? )ynat_lt ( ? < ? )ynat_minus ( ? - ? )ynat_plus ( ? + ? )ynat_maxynat_minstarlstarbool ( Ⓕ ) ( Ⓣ )arith ( ?^? ) ( ⫯? ) ( ⫰? )list ( ◊ ) ( ? @ ? ) ( |?| )list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )
      extensions to the librarygenerated logical decomposables - starlstarbool ( Ⓕ ) ( Ⓣ )arith ( ?^? )list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ )
      generated logical decomposables - xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )xoa_props ( ⊥ ) ( ⊤ ) -
      -       		+
      		@@ -261,8 +297,7 @@
      - -
      +
      [Spacer]
      @@ -288,6 +323,6 @@

      -
      Last update: Tue, 04 Nov 2014 16:28:52 +0100
      - +
      Last update: Wed, 14 Oct 2015 21:43:44 +0200
      +