informational page on ground_1

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 8cda8f76abfe9f1e610dce6e362d32d7cc5ad42b..1e6bf7d9c604b03ba6029aaae82485df2807b864 100644 (file)
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -222,6 +222,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:39:00 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 7938d47dacd09e87a1e22eeb2c689df6fe877faf..a4ec380fb559768f450d6009d943c71f5a77c4d1 100644 (file)
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -90,7 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -124,7 +124,7 @@
     </ul>
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
+    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
          and its timeline.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
@@ -152,29 +152,29 @@
           <tr>
             <td class="snns capitalize italic cyan">sizes</td>
             <td class="snns italic cyan">files</td>
-            <td class="snnn right italic cyan">4</td>
+            <td class="snnn right italic cyan">14</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">68581</td>
+            <td class="snnn right italic cyan">6787</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">3637</td>
+            <td class="ssnn right italic cyan">10070</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
             <td class="snnn right italic green">2</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">1</td>
+            <td class="snnn right italic green">4</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">3</td>
+            <td class="ssnn right italic green">6</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
             <td class="snss italic yellow">declared</td>
-            <td class="snsn right italic yellow">3</td>
+            <td class="snsn right italic yellow">6</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">9</td>
+            <td class="snsn right italic yellow">11</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">12</td>
+            <td class="sssn right italic yellow">17</td>
           </tr>
         </tbody>
       </table>
@@ -258,6 +258,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:39:00 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html
index 4871fb70f9c39dcc2074601fc5491ed4a0897a2c..0965840d7350a893b427334cea26c57b53ad1bf6 100644 (file)
--- a/helm/www/lambdadelta/basic_1.html
+++ b/helm/www/lambdadelta/basic_1.html
@@ -90,7 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -823,6 +823,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:39:00 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index b05d3b07d3f1bddd58c17ac40e071f3b13304621..ca505d6478418a441ca2a055c673334f85ee63e0 100644 (file)
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -90,7 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -116,7 +116,7 @@
 -->
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
+    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
          and its timeline.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
@@ -148,7 +148,7 @@
             <td class="snns italic cyan">characters</td>
             <td class="snnn right italic cyan">433402</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">1874774</td>
+            <td class="ssnn right italic cyan">1874778</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
@@ -211,7 +211,7 @@
       <li>
         <span class="emph alpha">2014 April 16.</span>
          Lazy equivalence on local environments
-        addded as q-step to rst-computation on closures
+        added as q-step to rst-computation on closures
          (anniversary milestone).
    </li>
     </ul>
@@ -1019,7 +1019,7 @@
             <td class="nnns top capitalize italic yellow">
               <br />
             </td>
-            <td class="snns top italic yellow">contxt-sensitive multiple rt-substitution</td>
+            <td class="snns top italic yellow">context-sensitive multiple rt-substitution</td>
             <td class="snns top yellow">cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )</td>
             <td class="snnn top yellow">cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )</td>
             <td class="snnn top yellow">cpys_lift cpys_cpys</td>
@@ -1159,7 +1159,7 @@
             <td class="nnns top capitalize italic orange">
               <br />
             </td>
-            <td class="snns top italic orange">contxt-sensitive ordinary rt-substitution</td>
+            <td class="snns top italic orange">context-sensitive ordinary rt-substitution</td>
             <td class="snns top orange">cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )</td>
             <td class="snnn top orange">cpy_lift cpy_nlift cpy_cpy</td>
             <td class="snnn top orange">
@@ -1384,6 +1384,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:39:00 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index 2b7aee243ab97929199cf571d2b1dfc93bfb942a..ffa999aa230e6b4d30e76af2071122fe7629729a 100644 (file)
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -90,7 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -366,6 +366,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:38:59 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html
new file mode 100644 (file)
index 0000000..7c788ec
--- /dev/null
+++ b/helm/www/lambdadelta/ground_1.html
@@ -0,0 +1,280 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml" dir="ltr" lang="en-us">
+  <head>
+    <meta http-equiv="Content-Language" content="en-us" />
+    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
+    <meta http-equiv="Content-Style-Type" content="text/css" />
+    <meta name="author" content="Ferruccio Guidi" />
+    <meta name="description" content="\lambda\delta home page" />
+    <title>\lambda\delta home page</title>
+    <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
+    <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
+    <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
+    <link rel="shortcut icon" href="http://lambdadelta.info/images/crux_16.ico" />
+  </head>
+  <body lang="en-US">
+    <div class="spacer">
+      <a href="http://lambdadelta.info/">
+        <img class="icon32" alt="[lambdadelta home]" title="lambdadelta home" src="http://lambdadelta.info/images/crux_32.png" />
+      </a>
+    </div>
+    <div class="head1">cic:/BOLOGNA/lambdadelta/ground_1/ (background for λδ version 1)</div>
+    <div class="spacer">
+      <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+      <br />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
+          <tr>
+            <td class="snns capitalize italic sky">
+              <a href="http://lambdadelta.info/index.html">home</a>
+            </td>
+            <td class="snns capitalize italic magenta">
+              <a href="http://lambdadelta.info/news.html">news</a>
+            </td>
+            <td class="snns capitalize italic orange">
+              <a href="http://lambdadelta.info/documentation.html">documentation</a>
+            </td>
+            <td class="snns capitalize italic green">
+              <a href="http://lambdadelta.info/specification.html">specification</a>
+            </td>
+            <td class="snnn capitalize italic green">
+              <br />
+            </td>
+            <td class="snnn capitalize italic green">
+              <br />
+            </td>
+            <td class="snns capitalize italic green">
+              <a href="http://lambdadelta.info/implementation.html">implementation</a>
+            </td>
+            <td class="ssnn capitalize italic green">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns capitalize sky">
+              <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
+            </td>
+            <td class="snns capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
+            </td>
+            <td class="snns capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
+            </td>
+            <td class="snns capitalize green">
+              <a href="http://lambdadelta.info/specification.html#v2">version 2</a>
+            </td>
+            <td class="snnn capitalize green">(<a href="http://lambdadelta.info/ground_2.html">background</a> - <a href="http://lambdadelta.info/basic_2.html">core</a> - <a href="http://lambdadelta.info/apps_2.html">applications</a>)</td>
+            <td class="snnn capitalize green">
+              <br />
+            </td>
+            <td class="snns capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
+            </td>
+            <td class="ssnn capitalize green">(<a href="http://lambdadelta.info/static/lddl/">static LDDL directory</a>)</td>
+          </tr>
+          <tr>
+            <td class="snss capitalize sky">
+              <a href="http://lambdadelta.info/index.html#citations">citations</a>
+            </td>
+            <td class="snss capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
+            </td>
+            <td class="snss capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
+            </td>
+            <td class="snss capitalize green">
+              <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
+            </td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
+            <td class="snss capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
+            </td>
+            <td class="sssn capitalize green">
+              <br />
+            </td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
+         and its timeline.
+   </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
+          <tr>
+            <td class="snns capitalize italic gray">category</td>
+            <td class="snns italic gray">objects</td>
+            <td class="snnn right italic gray">
+              <br />
+            </td>
+            <td class="snnn italic gray">
+              <br />
+            </td>
+            <td class="snnn right italic gray">
+              <br />
+            </td>
+            <td class="snnn italic gray">
+              <br />
+            </td>
+            <td class="ssnn right italic gray">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns capitalize italic cyan">sizes</td>
+            <td class="snns italic cyan">files</td>
+            <td class="snnn right italic cyan">10</td>
+            <td class="snns italic cyan">characters</td>
+            <td class="snnn right italic cyan">15063</td>
+            <td class="snns italic cyan">nodes</td>
+            <td class="ssnn right italic cyan" />
+          </tr>
+          <tr>
+            <td class="snns capitalize italic green">propositions</td>
+            <td class="snns italic green">theorems</td>
+            <td class="snnn right italic green">0</td>
+            <td class="snns italic green">lemmas</td>
+            <td class="snnn right italic green">50</td>
+            <td class="snns italic green">total</td>
+            <td class="ssnn right italic green">50</td>
+          </tr>
+          <tr>
+            <td class="snss capitalize italic yellow">concepts</td>
+            <td class="snss italic yellow">declared</td>
+            <td class="snsn right italic yellow">24</td>
+            <td class="snss italic yellow">defined</td>
+            <td class="snsn right italic yellow">4</td>
+            <td class="snss italic yellow">total</td>
+            <td class="sssn right italic yellow">28</td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph delta">January 2015.</span>
+      Update with backports from the abandoned specification of λδ version 2.
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph delta">May 2008.</span>
+      Specification is concluded.
+   </li>
+    </ul>
+    <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="emph alpha">May 2004.</span>
+      Specification starts.
+   </li>
+    </ul>
+    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="structure">Logical Structure of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">This table reports the specification's components and their planes.
+   </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
+          <tr>
+            <td class="snns top capitalize italic gray">component</td>
+            <td class="snns top italic gray">plane</td>
+            <td class="snns top gray">files</td>
+            <td class="snnn top gray">
+              <br />
+            </td>
+            <td class="snnn top gray">
+              <br />
+            </td>
+            <td class="ssnn top gray">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic yellow">extensions to the library</td>
+            <td class="snns top italic yellow" />
+            <td class="snns top yellow">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/ground_1/bg_hints.txt">bg_hints</a>
+            </td>
+            <td class="snnn top yellow">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/ground_1/bg_blt.txt">bg_blt</a>
+            </td>
+            <td class="snnn top yellow">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/ground_1/bg_plist.txt">bg_plist</a>
+            </td>
+            <td class="ssnn top yellow">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic orange">generated logical decomposables</td>
+            <td class="snns top italic orange" />
+            <td class="snns top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/ground_1/bg_types.txt">bg_types</a>
+            </td>
+            <td class="snnn top orange">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/ground_1/bg_props.txt">bg_props</a>
+            </td>
+            <td class="snnn top orange">
+              <br />
+            </td>
+            <td class="ssnn top orange">
+              <br />
+            </td>
+          </tr>
+          <tr>
+            <td class="snss top capitalize italic red">preamble</td>
+            <td class="snss top italic red" />
+            <td class="snss top red">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/ground_1/bg_require.txt">bg_require</a>
+            </td>
+            <td class="snsn top red">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/ground_1/bg_rewrite.txt">bg_rewrite</a>
+            </td>
+            <td class="snsn top red">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/ground_1/bg_tactics.txt">bg_tactics</a>
+            </td>
+            <td class="sssn top red">
+              <a href="http://lambdadelta.info/static/coq/lambdadelta/ground_1/bg_subst.txt">bg_subst</a>
+            </td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+    <div class="spacer">
+      <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+      <br />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+      <a href="http://validator.w3.org/check?uri=referer">
+        <img class="w3c" alt="[Valid XHTML 1.1]" title="Valid XHTML 1.1" src="http://www.w3.org/Icons/valid-xhtml11-blue" />
+      </a>
+      <a href="http://jigsaw.w3.org/css-validator/check/referer">
+        <img class="w3c" alt="[Valid CSS level 2]" title="Valid CSS level 2" src="http://www.w3.org/Icons/valid-css2-blue" />
+      </a>
+      <a href="http://www.w3.org/XML/">
+        <img class="w3c" alt="[Generated from XML via XSL]" title="Generated from XML via XSL" src="http://lambdadelta.info/images/xml_xsl2.png" />
+      </a>
+      <a href="http://www.w3.org/Graphics/PNG/">
+        <img class="w3c" alt="[PNG used here]" title="PNG used here" src="http://lambdadelta.info/images/PNGnow2.png" />
+      </a>
+      <a href="http://www.anybrowser.org/campaign/">
+        <img class="w3c" alt="[Viewable with any browser]" title="Viewable with any browser" src="http://www.anybrowser.org/campaign/bvgraphics/abtfile.png" />
+      </a>
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">
+      <br />
+    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
+  </body>
+</html>

diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 92bd89f68894e1c0bb38b90012f260c5d578203a..17b7562e305eaad3830853aa26f4cd43b616eee0 100644 (file)
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -90,7 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -104,7 +104,7 @@
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="summary">Summary of the Specification <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical acount of the specification's contents
+    <div xmlns:ld="http://lambdadelta.info/" class="text">Here is a numerical account of the specification's contents
          and its timeline.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
@@ -134,7 +134,7 @@
             <td class="snns italic cyan">files</td>
             <td class="snnn right italic cyan">30</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">68581</td>
+            <td class="snnn right italic cyan">46649</td>
             <td class="snns italic cyan">nodes</td>
             <td class="ssnn right italic cyan">62380</td>
           </tr>
@@ -208,26 +208,53 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top capitalize italic yellow">natural numbers with infinity</td>
+            <td class="snns top capitalize italic grass">natural numbers with infinity</td>
+            <td class="snns top italic grass" />
+            <td class="snns top grass">ynat ( ∞ )</td>
+            <td class="snnn top grass">ynat_pred ( ⫰? )</td>
+            <td class="snnn top grass">ynat_succ ( ⫯? )</td>
+            <td class="snnn top grass">ynat_le ( ? ≤ ? )</td>
+            <td class="snnn top grass">ynat_lt ( ? &lt; ? )</td>
+            <td class="snnn top grass">ynat_minus ( ? - ? )</td>
+            <td class="snnn top grass">ynat_plus ( ? + ? )</td>
+            <td class="snnn top grass">ynat_max</td>
+            <td class="ssnn top grass">ynat_min</td>
+          </tr>
+          <tr>
+            <td class="snns top capitalize italic yellow">extensions to the library</td>
             <td class="snns top italic yellow" />
-            <td class="snns top yellow">ynat ( ∞ )</td>
-            <td class="snnn top yellow">ynat_pred ( ⫰? )</td>
-            <td class="snnn top yellow">ynat_succ ( ⫯? )</td>
-            <td class="snnn top yellow">ynat_le ( ? ≤ ? )</td>
-            <td class="snnn top yellow">ynat_lt ( ? &lt; ? )</td>
-            <td class="snnn top yellow">ynat_minus ( ? - ? )</td>
-            <td class="snnn top yellow">ynat_plus ( ? + ? )</td>
-            <td class="snnn top yellow">ynat_max</td>
-            <td class="ssnn top yellow">ynat_min</td>
+            <td class="snns top yellow">star</td>
+            <td class="snnn top yellow">lstar</td>
+            <td class="snnn top yellow">bool ( Ⓕ ) ( Ⓣ )</td>
+            <td class="snnn top yellow">arith ( ?^? )</td>
+            <td class="snnn top yellow">list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )</td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
+            <td class="snnn top yellow">
+              <br />
+            </td>
+            <td class="ssnn top yellow">
+              <br />
+            </td>
           </tr>
           <tr>
-            <td class="snns top capitalize italic orange">extensions to the library</td>
+            <td class="snns top capitalize italic orange">generated logical decomposables</td>
             <td class="snns top italic orange" />
-            <td class="snns top orange">star</td>
-            <td class="snnn top orange">lstar</td>
-            <td class="snnn top orange">bool ( Ⓕ ) ( Ⓣ )</td>
-            <td class="snnn top orange">arith ( ?^? )</td>
-            <td class="snnn top orange">list ( ◊ ) ( ? @ ? ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )</td>
+            <td class="snns top orange">xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )</td>
+            <td class="snnn top orange">xoa_props ( ⊥ ) ( ⊤ )</td>
+            <td class="snnn top orange">
+              <br />
+            </td>
+            <td class="snnn top orange">
+              <br />
+            </td>
+            <td class="snnn top orange">
+              <br />
+            </td>
             <td class="snnn top orange">
               <br />
             </td>
@@ -242,10 +269,14 @@
             </td>
           </tr>
           <tr>
-            <td class="snss top capitalize italic red">generated logical decomposables</td>
+            <td class="snss top capitalize italic red" />
             <td class="snss top italic red" />
-            <td class="snss top red">xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )</td>
-            <td class="snsn top red">xoa_props ( ⊥ ) ( ⊤ )</td>
+            <td class="snss top red">
+              <br />
+            </td>
+            <td class="snsn top red">
+              <br />
+            </td>
             <td class="snsn top red">
               <br />
             </td>
@@ -297,6 +328,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:39:00 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 5e06734647efc63f3673b510366e0e1c12b297d1..82dcacfd5db933f2ca7bbc10168ec928ea5d6ca2 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -90,7 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -255,6 +255,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:38:59 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 60ac77f4d88d1b5f67c8d171bff4bae61a8f8dd0..afc6f7d8a9401fed265a5822e96ff71d51d91381 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -90,7 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -202,6 +202,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:38:59 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 2d4bbb7a99ae1ae3006a36430746e901b4fdc637..a1dfcd5903c13ad7d314762f4b0c3d8ba3956282 100644 (file)
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -90,7 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -335,6 +335,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:38:59 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index 47b54eed9457a7cc8c3526bc4df2ca8954df740f..464ace8317f729f85f2ccbb357a0b4bcbc4bb887 100644 (file)
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -90,7 +90,7 @@
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
+            <td class="snsn capitalize green">(<a href="http://lambdadelta.info/ground_1.html">background</a> - <a href="http://lambdadelta.info/basic_1.html">core</a>)</td>
             <td class="snsn capitalize green">(<a href="http://lambdadelta.info/static/matita/lambdadelta/">static HELM directory</a>)</td>
             <td class="snss capitalize green">
               <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
@@ -299,8 +299,9 @@
     </ul>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
       Informational pages on the parts of the specification:
-<!--      <rlink to="ground_2.html">Background</rlink>, --><a href="http://lambdadelta.info/basic_1.html">Core</a>.
-<!--      <rlink to="apps_2.html">Applications</rlink>. --></div>
+      <a href="http://lambdadelta.info/ground_1.html">Background</a>,
+      <a href="http://lambdadelta.info/basic_1.html">Core</a>.
+   </div>
     <div class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>
@@ -327,6 +328,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 20 Jan 2015 18:39:00 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl
index 8d6b24e85cfd0a97fbaf922669ef4c33068e4ec2..e3c2b05256f74723701a1bb3e9c5f05bb3f9cb72 100644 (file)
--- a/helm/www/lambdadelta/web/home/sitemap.tbl
+++ b/helm/www/lambdadelta/web/home/sitemap.tbl
@@ -24,7 +24,8 @@ table [
         @@("apps_2" "applications") ^ ")"
       * ]
       [ @@("specification#v1" "version 1")
-        "(" ^ @@("basic_1" "core") ^ ")"
+        "(" ^ @@("ground_1" "background") + "-" + 
+        @@("basic_1" "core") ^ ")"
         "(" ^ @@("static/matita/lambdadelta/" "static HELM directory") ^ ")"
       * ]
    }

diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml
index 5c7813d8312de724f16ec869fc187f16df991a64..556549c393d00f5190ddc0d40f9f3c4440c27379 100644 (file)
--- a/helm/www/lambdadelta/web/home/specification.ldw.xml
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -136,9 +136,8 @@
 
    <body>
       Informational pages on the parts of the specification:
-<!--      <rlink to="ground_2.html">Background</rlink>, -->
+      <rlink to="ground_1.html">Background</rlink>,
       <rlink to="basic_1.html">Core</rlink>.
-<!--      <rlink to="apps_2.html">Applications</rlink>. -->
    </body>
 
    <footer/>

diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
index 9f478280fb912e3db7e7c61d0ccb81bca6fa1e81..467d427ff13f7b50e43812e231498a53226ff0bf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -9,7 +9,7 @@ table {
         ]
      }
    ]
-   class "yellow"
+   class "grass"
    [ { "natural numbers with infinity" * } {
         [ { "" * } {
            [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )"
@@ -21,7 +21,7 @@ table {
         ]
      }
    ]
-   class "orange"
+   class "yellow"
    [ { "extensions to the library" * } {
         [ { "" * } {
              [ "star" "lstar" "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? )"
@@ -31,7 +31,7 @@ table {
         ]
      }
    ]
-   class "red"
+   class "orange"
    [ { "generated logical decomposables" * } {
         [ { "" * } {
              [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" "xoa_props ( ⊥ ) ( ⊤ )" * ]
@@ -39,6 +39,14 @@ table {
         ]
      }
    ]
+   class "red"
+   [ { "" * } {
+        [ { "" * } {
+             [ * ]
+          }
+        ]
+     }
+   ]
 }
 
 class "top"               { * }