- update in basic_2

- web site major upddate

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index b0891996f5b4d39903a43e15d6654452a0ad9efc..fa518c4894c9fbb071ca35144bda4b3ba37e67e5 100644 (file)
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -386,8 +386,8 @@
               <br />
             </td>
             <td class="snns top italic cyan">strongly normalizing qrst-computation</td>
-            <td class="snns top cyan">fsb ( â¦\83?,?â¦\84 â\8a¢ ⦥[?,?] ? )</td>
-            <td class="snnn top cyan">fsb_alt ( â¦\83?,?â¦\84 â\8a¢ ⦥⦥[?,?] ? )</td>
+            <td class="snns top cyan">fsb ( ⦥[?,?] â¦\83?,?,?â¦\84 )</td>
+            <td class="snnn top cyan">fsb_alt ( ⦥⦥[?,?] â¦\83?,?,?â¦\84 )</td>
             <td class="snnn top cyan">fsb_aaa fsb_csx</td>
             <td class="ssnn top cyan">
               <br />

diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index d07a8b9778739c58e71b814f630e5238b0d888f2..dd3e6c27249189492acb95f6dc8e98091da81400 100644 (file)
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -40,41 +40,52 @@
               <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="ssns capitalize italic green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn capitalize italic green">(<a href="http://lambdadelta.info/implementation.html#specifications">specifications</a> - <a href="http://lambdadelta.info/implementation.html#lddl">library</a> - <a href="http://lambdadelta.info/implementation.html#helena">Helena</a>)</td>
           </tr>
           <tr>
-            <td class="snns sky">
-              <a href="http://lambdadelta.info/index.html#foreword">Foreword</a>
+            <td class="snns capitalize sky">
+              <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
             </td>
-            <td class="snns magenta">
-              <a href="http://lambdadelta.info/news.html#milestones">Milestones</a>
+            <td class="snns capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
             </td>
-            <td class="snns orange">
-              <a href="http://lambdadelta.info/documentation.html#v2">Version 2</a>
+            <td class="snns capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
             </td>
-            <td class="snns green">
-              <a href="http://lambdadelta.info/version_2.html">Version 2</a>
+            <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="ssns capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
             </td>
-            <td class="ssnn 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>
           </tr>
           <tr>
-            <td class="snss sky">
-              <a href="http://lambdadelta.info/index.html#notice">Notice</a>
+            <td class="snss capitalize sky">
+              <a href="http://lambdadelta.info/index.html#notice">notice</a>
             </td>
-            <td class="snss magenta">
-              <a href="http://lambdadelta.info/news.html#visibility">Visibility</a>
+            <td class="snss capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
             </td>
-            <td class="snss orange">
-              <a href="http://lambdadelta.info/documentation.html#v1">Version 1</a>
+            <td class="snss capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
             </td>
-            <td class="snss green">
-              <a href="http://lambdadelta.info/version_1.html">Version 1</a>
+            <td class="snss capitalize green">
+              <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="sssn green">
+            <td class="snsn capitalize green">
               <br />
             </td>
+            <td class="ssss capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
+            </td>
           </tr>
         </tbody>
       </table>
@@ -86,11 +97,11 @@
       BibTeX database of λδ documentation:
       <a href="http://lambdadelta.info/download/lambdadelta.bib">lambdadelta.bib</a>,
       <a href="http://lambdadelta.info/download/lambdadelta.txt">lambdadelta.txt</a>
-      (revised <span class="date">2014-07</span>).
+      (revised <span class="date">2014-10</span>).
    </div>
    
-   <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="v2">
-      <img class="icon32" alt="[basic lambdadelta logo]" title="basic lambdadelta" src="http://lambdadelta.info/images/basic_32.png" /> λδ version 2 (in progress)</div>
+   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
+      <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (in progress)</div>
    <div xmlns:ld="http://lambdadelta.info/" class="text">
       The main source of information is <span class="date">P8</span>.
    </div>
@@ -173,8 +184,8 @@
       </table>
     </div>
 
-   <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="v1">
-      <img class="icon32" alt="[basic lambdadelta logo]" title="basic lambdadelta" src="http://lambdadelta.info/images/basic_32.png" /> λδ version 1 (dismissed)</div>
+   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v1">
+      <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" /> λδ version 1 (dismissed)</div>
    <div xmlns:ld="http://lambdadelta.info/" class="text">
       The main source of information is <span class="date">J1</span>.
       A summary is available in <span class="date">P5</span>.
@@ -333,6 +344,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 05 Oct 2014 16:38:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 09 Oct 2014 16:26:23 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib
index 147f0a51a7c84b0b145f1aebc338e1d77bec14b8..ee6c4e6ee8e0364d0a3cb4beae6b8da10bcd2387 100644 (file)
--- a/helm/www/lambdadelta/download/lambdadelta.bib
+++ b/helm/www/lambdadelta/download/lambdadelta.bib
@@ -5,7 +5,7 @@
    title="{lambdadelta\_2}",
    howpublished="Formal specification for the proof assistant Matita 0.99.2",
    year="2014",
-   month="July",
+   month="October",
    note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$"
 }
 

diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt
index 147f0a51a7c84b0b145f1aebc338e1d77bec14b8..ee6c4e6ee8e0364d0a3cb4beae6b8da10bcd2387 100644 (file)
--- a/helm/www/lambdadelta/download/lambdadelta.txt
+++ b/helm/www/lambdadelta/download/lambdadelta.txt
@@ -5,7 +5,7 @@
    title="{lambdadelta\_2}",
    howpublished="Formal specification for the proof assistant Matita 0.99.2",
    year="2014",
-   month="July",
+   month="October",
    note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$"
 }
 

diff --git a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz
index 74759de60bbaf558513fa107526aca6383ece21e..fd2ae902b4be72435cb0b8b0fc96ddafb9e24cc0 100644 (file)
Binary files a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz and b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz differ

diff --git a/helm/www/lambdadelta/images/basic_32.png b/helm/www/lambdadelta/images/basic_32.png
deleted file mode 100644 (file)
index bfbc863..0000000
Binary files a/helm/www/lambdadelta/images/basic_32.png and /dev/null differ

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index e0f5b7aab8f90318cb400d2dcb4d3c846b43b430..3d253ae1d2c715185179b5d3852f786bae1bbd62 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -40,92 +40,52 @@
               <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="ssns capitalize italic green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn capitalize italic green">(<a href="http://lambdadelta.info/implementation.html#specifications">specifications</a> - <a href="http://lambdadelta.info/implementation.html#lddl">library</a> - <a href="http://lambdadelta.info/implementation.html#helena">Helena</a>)</td>
           </tr>
           <tr>
-            <td class="snns sky">
-              <a href="http://lambdadelta.info/index.html#foreword">Foreword</a>
+            <td class="snns capitalize sky">
+              <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
             </td>
-            <td class="snns magenta">
-              <a href="http://lambdadelta.info/news.html#milestones">Milestones</a>
+            <td class="snns capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
             </td>
-            <td class="snns orange">
-              <a href="http://lambdadelta.info/documentation.html#v2">Version 2</a>
+            <td class="snns capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
             </td>
-            <td class="snns green">
-              <a href="http://lambdadelta.info/version_2.html">Version 2</a>
+            <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="ssns capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
             </td>
-            <td class="ssnn 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>
           </tr>
           <tr>
-            <td class="snss sky">
-              <a href="http://lambdadelta.info/index.html#notice">Notice</a>
+            <td class="snss capitalize sky">
+              <a href="http://lambdadelta.info/index.html#notice">notice</a>
             </td>
-            <td class="snss magenta">
-              <a href="http://lambdadelta.info/news.html#visibility">Visibility</a>
+            <td class="snss capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
             </td>
-            <td class="snss orange">
-              <a href="http://lambdadelta.info/documentation.html#v1">Version 1</a>
+            <td class="snss capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
             </td>
-            <td class="snss green">
-              <a href="http://lambdadelta.info/version_1.html">Version 1</a>
+            <td class="snss capitalize green">
+              <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="sssn green">
+            <td class="snsn capitalize green">
               <br />
             </td>
-          </tr>
-        </tbody>
-      </table>
-    </div>
-
-   <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="specifications">Computer-checked formal specifications <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b5.png" />
-    </div>
-   <div xmlns:ld="http://lambdadelta.info/" class="text">
-      λδ comes in several versions listed in the following table,
-      which includes the major milestones:
-   </div>
-   <div xmlns:ld="http://lambdadelta.info/" class="text">
-      <table cellpadding="4" cellspacing="0">
-        <tbody>
-          <tr>
-            <td class="snns top capitalize italic gray">version</td>
-            <td class="snnn top capitalize italic gray">name</td>
-            <td class="snnn top capitalize italic gray">developed with</td>
-            <td class="snnn top capitalize italic gray">stage</td>
-            <td class="snnn top capitalize italic gray">started</td>
-            <td class="snnn top capitalize italic gray">announced</td>
-            <td class="snnn top capitalize italic gray">released</td>
-            <td class="ssnn top capitalize italic gray">dismissed</td>
-          </tr>
-          <tr>
-            <td class="snns top orange">
-              <a href="http://lambdadelta.info/version_2">Version 2</a>
-            </td>
-            <td class="snnn top orange">"basic_2"</td>
-            <td class="snnn top orange">
-              <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
-            </td>
-            <td class="snnn top orange">"A"</td>
-            <td class="snnn top orange">April 2011</td>
-            <td class="snnn top orange">July 2014</td>
-            <td class="snnn top orange">Planned in 2014</td>
-            <td class="ssnn top orange">Not planned yet</td>
-          </tr>
-          <tr>
-            <td class="snss top red">
-              <a href="http://lambdadelta.info/version_1">Version 1</a>
-            </td>
-            <td class="snsn top red">"basic_1"</td>
-            <td class="snsn top red">
-              <a href="http://coq.inria.fr/">Coq 7.3.1</a>
+            <td class="ssss capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
             </td>
-            <td class="snsn top red" />
-            <td class="snsn top red">May 2004</td>
-            <td class="snsn top red">January 2006</td>
-            <td class="snsn top red">November 2006</td>
-            <td class="sssn top red">May 2008</td>
           </tr>
         </tbody>
       </table>
@@ -134,7 +94,7 @@
    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="tools">Tools <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b5.png" />
     </div>
 
-   <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="lddl">
+   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="lddl">
       <img class="icon32" alt="[Crux logo]" title="the Crux" src="http://lambdadelta.info/images/crux_32.png" /> λδ Digital Library (LDDL)</div>
    <div xmlns:ld="http://lambdadelta.info/" class="text">
       The λδ Digital Library is part of <a href="http://helm.cs.unibo.it/">HELM</a>
@@ -167,7 +127,7 @@
    </li>
     </ul>
 
-   <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="helena">
+   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="helena">
       <img class="icon32" alt="[Helena logo]" title="Helena" src="http://lambdadelta.info/images/helena_32.png" /> Helena</div>
    <div xmlns:ld="http://lambdadelta.info/" class="text">
       Helena is a λδ processor,

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 190bf2ebbe0b21f2268d7a61a497ae83e4e4e7fe..c8664cd96e4ef83d9d876ca47534faed018bf143 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -40,41 +40,52 @@
               <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="ssns capitalize italic green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn capitalize italic green">(<a href="http://lambdadelta.info/implementation.html#specifications">specifications</a> - <a href="http://lambdadelta.info/implementation.html#lddl">library</a> - <a href="http://lambdadelta.info/implementation.html#helena">Helena</a>)</td>
           </tr>
           <tr>
-            <td class="snns sky">
-              <a href="http://lambdadelta.info/index.html#foreword">Foreword</a>
+            <td class="snns capitalize sky">
+              <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
             </td>
-            <td class="snns magenta">
-              <a href="http://lambdadelta.info/news.html#milestones">Milestones</a>
+            <td class="snns capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
             </td>
-            <td class="snns orange">
-              <a href="http://lambdadelta.info/documentation.html#v2">Version 2</a>
+            <td class="snns capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
             </td>
-            <td class="snns green">
-              <a href="http://lambdadelta.info/version_2.html">Version 2</a>
+            <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="ssns capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
             </td>
-            <td class="ssnn 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>
           </tr>
           <tr>
-            <td class="snss sky">
-              <a href="http://lambdadelta.info/index.html#notice">Notice</a>
+            <td class="snss capitalize sky">
+              <a href="http://lambdadelta.info/index.html#notice">notice</a>
             </td>
-            <td class="snss magenta">
-              <a href="http://lambdadelta.info/news.html#visibility">Visibility</a>
+            <td class="snss capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
             </td>
-            <td class="snss orange">
-              <a href="http://lambdadelta.info/documentation.html#v1">Version 1</a>
+            <td class="snss capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
             </td>
-            <td class="snss green">
-              <a href="http://lambdadelta.info/version_1.html">Version 1</a>
+            <td class="snss capitalize green">
+              <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="sssn green">
+            <td class="snsn capitalize green">
               <br />
             </td>
+            <td class="ssss capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
+            </td>
           </tr>
         </tbody>
       </table>
@@ -135,6 +146,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 05 Oct 2014 16:38:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 09 Oct 2014 16:26:23 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 1110d756931c2e06b8bbb9fffa6160171ad54c87..c246291dff9f9191e8c1296cc9f0e15007a08bf0 100644 (file)
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -40,41 +40,52 @@
               <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="ssns capitalize italic green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn capitalize italic green">(<a href="http://lambdadelta.info/implementation.html#specifications">specifications</a> - <a href="http://lambdadelta.info/implementation.html#lddl">library</a> - <a href="http://lambdadelta.info/implementation.html#helena">Helena</a>)</td>
           </tr>
           <tr>
-            <td class="snns sky">
-              <a href="http://lambdadelta.info/index.html#foreword">Foreword</a>
+            <td class="snns capitalize sky">
+              <a href="http://lambdadelta.info/index.html#foreword">foreword</a>
             </td>
-            <td class="snns magenta">
-              <a href="http://lambdadelta.info/news.html#milestones">Milestones</a>
+            <td class="snns capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#milestones">milestones</a>
             </td>
-            <td class="snns orange">
-              <a href="http://lambdadelta.info/documentation.html#v2">Version 2</a>
+            <td class="snns capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v2">version 2</a>
             </td>
-            <td class="snns green">
-              <a href="http://lambdadelta.info/version_2.html">Version 2</a>
+            <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="ssns capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
             </td>
-            <td class="ssnn 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>
           </tr>
           <tr>
-            <td class="snss sky">
-              <a href="http://lambdadelta.info/index.html#notice">Notice</a>
+            <td class="snss capitalize sky">
+              <a href="http://lambdadelta.info/index.html#notice">notice</a>
             </td>
-            <td class="snss magenta">
-              <a href="http://lambdadelta.info/news.html#visibility">Visibility</a>
+            <td class="snss capitalize magenta">
+              <a href="http://lambdadelta.info/news.html#visibility">visibility</a>
             </td>
-            <td class="snss orange">
-              <a href="http://lambdadelta.info/documentation.html#v1">Version 1</a>
+            <td class="snss capitalize orange">
+              <a href="http://lambdadelta.info/documentation.html#v1">version 1</a>
             </td>
-            <td class="snss green">
-              <a href="http://lambdadelta.info/version_1.html">Version 1</a>
+            <td class="snss capitalize green">
+              <a href="http://lambdadelta.info/specification.html#v1">version 1</a>
             </td>
-            <td class="sssn green">
+            <td class="snsn capitalize green">
               <br />
             </td>
+            <td class="ssss capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
+            </td>
           </tr>
         </tbody>
       </table>

diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
new file mode 100644 (file)
index 0000000..568d80f
--- /dev/null
+++ b/helm/www/lambdadelta/specification.html
@@ -0,0 +1,260 @@
+<?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">The Formal System λδ (\lambda\delta)</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="ssns capitalize italic green">
+              <a href="http://lambdadelta.info/implementation.html">implementation</a>
+            </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="ssns capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#lddl">library</a>
+            </td>
+          </tr>
+          <tr>
+            <td class="snss capitalize sky">
+              <a href="http://lambdadelta.info/index.html#notice">notice</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">
+              <br />
+            </td>
+            <td class="ssss capitalize green">
+              <a href="http://lambdadelta.info/implementation.html#helena">helena</a>
+            </td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+
+   <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="specifications">Computer-checked formal specifications <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b5.png" />
+    </div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      λδ is developed as a machine-checked digital specification.
+      It comes in several versions listed in the next table,
+      which includes the major milestones:
+   </div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
+          <tr>
+            <td class="snns top capitalize italic gray">version</td>
+            <td class="snnn top capitalize italic gray">name</td>
+            <td class="snnn top capitalize italic gray">developed with</td>
+            <td class="snnn top capitalize italic gray">stage</td>
+            <td class="snnn top capitalize italic gray">started</td>
+            <td class="snnn top capitalize italic gray">announced</td>
+            <td class="snnn top capitalize italic gray">released</td>
+            <td class="ssnn top capitalize italic gray">dismissed</td>
+          </tr>
+          <tr>
+            <td class="snns top orange">
+              <a href="http://lambdadelta.info/specification.html#v2">Version 2</a>
+            </td>
+            <td class="snnn top orange">"basic_2"</td>
+            <td class="snnn top orange">
+              <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
+            </td>
+            <td class="snnn top orange">"A"</td>
+            <td class="snnn top orange">April 2011</td>
+            <td class="snnn top orange">June 2014</td>
+            <td class="snnn top orange">Planned in October 2014</td>
+            <td class="ssnn top orange">Not planned yet</td>
+          </tr>
+          <tr>
+            <td class="snss top red">
+              <a href="http://lambdadelta.info/specification.html#v1">Version 1</a>
+            </td>
+            <td class="snsn top red">"basic_1"</td>
+            <td class="snsn top red">
+              <a href="http://coq.inria.fr/">Coq 7.3.1</a>
+            </td>
+            <td class="snsn top red" />
+            <td class="snsn top red">May 2004</td>
+            <td class="snsn top red">December 2005</td>
+            <td class="snsn top red">November 2006</td>
+            <td class="sssn top red">May 2008</td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
+
+
+
+   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
+      <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (in progress)</div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      The formal specification of λδ version 2
+      is available in the following formats:
+   </div>
+
+   <ul xmlns:ld="http://lambdadelta.info/" id="source2">
+      <li>
+      <a href="http://lambdadelta.info/download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</a>
+      (revised <span class="date">2014-10</span>).
+      Source scripts.
+   </li>
+    </ul>
+
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      Informational pages on the parts of the specification:
+      <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>.
+   </div>
+
+
+
+   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v1">
+      <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" /> λδ version 1 (dismissed)</div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      The formal specification of λδ version 1
+      is available in the following formats:
+   </div>
+
+   <ul xmlns:ld="http://lambdadelta.info/" id="source1">
+      <li>
+      <a href="http://lambdadelta.info/download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</a>
+      (revised <span class="date">2012-10</span>).
+      Source scripts.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/" id="static1">
+      <li>
+      <a href="http://lambdadelta.info/static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5"</a>
+      (revised <span class="date">2011-09</span>).
+      Static HTML pages generated by the <a href="http://helm.cs.unibo.it/">HELM</a> rendering engine.  
+      <ul>
+          <li>
+         <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
+            Confluence of reduction</a>
+         (Church-Rosser property).
+      </li>
+          <li>
+         <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
+            Correctness of types</a>.
+      </li>
+          <li>
+         <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
+            Uniqueness of types up to conversion</a>.
+      </li>
+          <li>
+         <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
+            Subject reduction of the type assignment</a>.
+      </li>
+          <li>
+         <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
+            Strong normalization of the typed terms</a>.
+      </li>
+          <li>
+         <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
+            Decidability of the type inference problem</a>.
+      </li>
+        </ul>
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/" id="dynamic1">
+      <li>
+      <a href="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
+         lambdadelta_1 for Matita 0.5"</a>
+      (revised <span class="date">2011-09</span>).
+      <a href="http://helm.cs.unibo.it/">HELM</a> directory.
+      <span class="date">Notice: the HELM rendering engine is offline.</span>
+   </li>
+    </ul>
+
+   <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: Thu, 09 Oct 2014 16:26:23 +0200</div>
+</body>
+</html>

diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html
index b28827183afa7572eeabcbe030589d61450e36bf..40bf6063a58cb3b03521e41b1403a62ef36e596b 100644 (file)
--- a/helm/www/lambdadelta/version_1.html
+++ b/helm/www/lambdadelta/version_1.html
@@ -167,6 +167,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 05 Oct 2014 16:38:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 09 Oct 2014 15:00:23 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html
index 925508051760f3861d1c4e0fceac0699384e1f80..b1202c10953e92c1b80d20bd6db1a6c879b4399b 100644 (file)
--- a/helm/www/lambdadelta/version_2.html
+++ b/helm/www/lambdadelta/version_2.html
@@ -131,6 +131,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 05 Oct 2014 16:38:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 09 Oct 2014 15:00:23 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml
index 6dc865edc129e52f94910a27dc4287abb3df284a..338477452bf7b4fe8472d76dc5ea7031031ad427 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml
@@ -12,16 +12,16 @@
       BibTeX database of λδ documentation:
       <rlink to="download/lambdadelta.bib">lambdadelta.bib</rlink>,
       <rlink to="download/lambdadelta.txt">lambdadelta.txt</rlink>
-      (revised <date date="2014-07"/>).
+      (revised <date date="2014-10"/>).
    </body>
    
-   <section name="v2"><basic-icon/>λδ version 2 (in progress)</section>
+   <subsection name="v2"><version2-icon/>λδ version 2 (in progress)</subsection>
    <body>
       The main source of information is <date date="P8"/>.
    </body>
    <table name="documentation_2"/>
 
-   <section name="v1"><basic-icon/>λδ version 1 (dismissed)</section>
+   <subsection name="v1"><version1-icon/>λδ version 1 (dismissed)</subsection>
    <body>
       The main source of information is <date date="J1"/>.
       A summary is available in <date date="P5"/>.

diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml
index 0613d899fb64e99f11c4950f1d2c5e052eb248e0..1c357b3c1d51cf2ec9bab7947f1e724ecb3bbf78 100644 (file)
--- a/helm/www/lambdadelta/web/home/implementation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml
@@ -7,16 +7,9 @@
 >
    <sitemap name="sitemap"/>
 
-   <section5 name="specifications">Computer-checked formal specifications</section5>
-   <body>
-      λδ comes in several versions listed in the following table,
-      which includes the major milestones:
-   </body>
-   <table name="versions"/>
-
    <section5 name="tools">Tools</section5>
 
-   <section name="lddl"><crux-icon/>λδ Digital Library (LDDL)</section>
+   <subsection name="lddl"><crux-icon/>λδ Digital Library (LDDL)</subsection>
    <body>
       The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
       and contains resources expressed in λδ.      
@@ -39,7 +32,7 @@
       (in "complete_rg" λδ).
    </news>
 
-   <section name="helena"><helena-icon/>Helena</section>
+   <subsection name="helena"><helena-icon/>Helena</subsection>
    <body>
       Helena is a λδ processor,
       implemented in <link to="http://caml.inria.fr/">Caml</link>

diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl
index 6f9092683f78616c0d14068b0c4ea9e856502a98..9144fbaf705559db993465e1acc7f923d615d8a5 100644 (file)
--- a/helm/www/lambdadelta/web/home/sitemap.tbl
+++ b/helm/www/lambdadelta/web/home/sitemap.tbl
@@ -3,34 +3,37 @@ name "sitemap"
 table [
    class "sky" {
       [ @@("index" "home") * ]
-      [ @@("index#foreword" "Foreword") * ]
-      [ @@("index#notice" "Notice") * ]
+      [ @@("index#foreword" "foreword") * ]
+      [ @@("index#notice" "notice") * ]
    }
    class "magenta" {
       [ @@"news" * ]
-      [ @@("news#milestones" "Milestones") * ]
-      [ @@("news#visibility" "Visibility") * ]
+      [ @@("news#milestones" "milestones") * ]
+      [ @@("news#visibility" "visibility") * ]
    }
    class "orange" {
       [ @@"documentation" * ] 
-      [ @@("documentation#v2" "Version 2") * ]
-      [ @@("documentation#v1" "Version 1") * ]
+      [ @@("documentation#v2" "version 2") * ]
+      [ @@("documentation#v1" "version 1") * ]
    }
    class "green" {
-      [ @@"implementation" 
-        "(" ^ @@("implementation#specifications" "specifications") + "-" +
-        @@("implementation#lddl" "library") + "-" +
-        @@("implementation#helena" "Helena") ^ ")"
+      [ @@"specification" * ] 
+      [ @@("specification#v2" "version 2")
+        "(" ^ @@("ground_2" "background") + "-" + 
+        @@("basic_2" "core") + "-" +
+        @@("apps_2" "applications") ^ ")"
       * ]
-      [ @@("version_2" "Version 2") 
-        "(" ^ @@("ground_2" "Background") + "-" + 
-        @@("basic_2" "Core") + "-" +
-        @@("apps_2" "Applications") ^ ")"
-      * ]
-      [ @@("version_1" "Version 1") * ] *
+      [ @@("specification#v1" "version 1") * ]
+   }
+   class "green" {
+      [ @@"implementation" * ] 
+      [ @@("implementation#lddl" "library") * ]
+      [ @@("implementation#helena" "helena") * ]
    }
 ]
 
-class "capitalize italic" [ 0 ]
+class "capitalize" [ * ]
+
+class "italic" [ 0 ]
 
 ext ".html" [ * ]

diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml
new file mode 100644 (file)
index 0000000..d32c6ca
--- /dev/null
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -0,0 +1,88 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<page xmlns="http://lambdadelta.info/"
+      description = "\lambda\delta home page"
+      title = "\lambda\delta home page"
+      head = "The Formal System λδ (\lambda\delta)"
+>
+   <sitemap name="sitemap"/>
+
+   <section5 name="specifications">Computer-checked formal specifications</section5>
+   <body>
+      λδ is developed as a machine-checked digital specification.
+      It comes in several versions listed in the next table,
+      which includes the major milestones:
+   </body>
+   <table name="versions"/>
+
+<!-- VERSION 2 =========================================================== -->
+
+   <subsection name="v2"><version2-icon/>λδ version 2 (in progress)</subsection>
+   <body>
+      The formal specification of λδ version 2
+      is available in the following formats:
+   </body>
+
+   <topitem name="source2">
+      <rlink to="download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</rlink>
+      (revised <date date="2014-10"/>).
+      Source scripts.
+   </topitem>
+
+   <body>
+      Informational pages on the parts of the specification:
+      <rlink to="ground_2.html">Background</rlink>,
+      <rlink to="basic_2.html">Core</rlink>,
+      <rlink to="apps_2.html">Applications</rlink>.
+   </body>
+
+<!-- VERSION 1 =========================================================== -->
+
+   <subsection name="v1"><version1-icon/>λδ version 1 (dismissed)</subsection>
+   <body>
+      The formal specification of λδ version 1
+      is available in the following formats:
+   </body>
+
+   <topitem name="source1">
+      <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
+      (revised <date date="2012-10"/>).
+      Source scripts.
+   </topitem>
+
+   <topitem name="static1">
+      <rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5"</rlink>
+      (revised <date date="2011-09"/>).
+      Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.  
+      <list><item>
+         <rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
+            Confluence of reduction</rlink>
+         (Church-Rosser property).
+      </item><item>
+         <rlink to="static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
+            Correctness of types</rlink>.
+      </item><item>
+         <rlink to="static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
+            Uniqueness of types up to conversion</rlink>.
+      </item><item>
+         <rlink to="static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
+            Subject reduction of the type assignment</rlink>.
+      </item><item>
+         <rlink to="static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
+            Strong normalization of the typed terms</rlink>.
+      </item><item>
+         <rlink to="static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
+            Decidability of the type inference problem</rlink>.
+      </item></list>
+   </topitem>
+
+   <topitem name="dynamic1">
+      <link to="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
+         lambdadelta_1 for Matita 0.5"</link>
+      (revised <date date="2011-09"/>).
+      <link to="http://helm.cs.unibo.it/">HELM</link> directory.
+      <date date="Notice: the HELM rendering engine is offline."/>
+   </topitem>
+
+   <footer/>
+</page>

diff --git a/helm/www/lambdadelta/web/home/version_1.ldw.xml b/helm/www/lambdadelta/web/home/version_1.ldw.xml
deleted file mode 100644 (file)
index e80bfe1..0000000
--- a/helm/www/lambdadelta/web/home/version_1.ldw.xml
+++ /dev/null
@@ -1,58 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-
-<page xmlns="http://lambdadelta.info/"
-      description = "\lambda\delta home page"
-      title = "\lambda\delta home page"
-      head = "The Formal System λδ version 1"
->
-   <sitemap name="sitemap"/>
-
-   <section6 name="foreword">Formats</section6>
-
-   <body>
-      The formal specification of λδ version 1
-      is available in the following formats:
-   </body>
-
-   <topitem name="source">
-      <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
-      (revised <date date="2012-10"/>).
-      Source scripts.
-   </topitem>
-
-   <topitem name="static">
-      <rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5"</rlink>
-      (revised <date date="2011-09"/>).
-      Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.  
-      <list><item>
-         <rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
-            Confluence of reduction</rlink>
-         (Church-Rosser property).
-      </item><item>
-         <rlink to="static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
-            Correctness of types</rlink>.
-      </item><item>
-         <rlink to="static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
-            Uniqueness of types up to conversion</rlink>.
-      </item><item>
-         <rlink to="static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
-            Subject reduction of the type assignment</rlink>.
-      </item><item>
-         <rlink to="static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
-            Strong normalization of the typed terms</rlink>.
-      </item><item>
-         <rlink to="static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
-            Decidability of the type inference problem</rlink>.
-      </item></list>
-   </topitem>
-
-   <topitem name="dynamic">
-      <link to="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
-         lambdadelta_1 for Matita 0.5"</link>
-      (revised <date date="2011-09"/>).
-      <link to="http://helm.cs.unibo.it/">HELM</link> directory.
-      <date date="Notice: the HELM rendering engine is offline."/>
-   </topitem>
-
-   <footer/>
-</page>

diff --git a/helm/www/lambdadelta/web/home/version_2.ldw.xml b/helm/www/lambdadelta/web/home/version_2.ldw.xml
deleted file mode 100644 (file)
index 816bfac..0000000
--- a/helm/www/lambdadelta/web/home/version_2.ldw.xml
+++ /dev/null
@@ -1,31 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-
-<page xmlns="http://lambdadelta.info/"
-      description = "\lambda\delta home page"
-      title = "\lambda\delta home page"
-      head = "The Formal System λδ version 2"
->
-   <sitemap name="sitemap"/>
-
-   <section4 name="foreword">Formats</section4>
-   
-   <body>
-      The formal specification of λδ version 2
-      is available in the following formats:
-   </body>
-
-   <topitem name="source">
-      <rlink to="download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</rlink>
-      (revised <date date="2014-10"/>).
-      Source scripts.
-   </topitem>
-
-   <topitem name="parts">
-      <rlink to="ground_2.html">Background</rlink>,
-      <rlink to="basic_2.html">Core</rlink>,
-      <rlink to="apps_2.html">Applications</rlink>.
-      Informational pages on the parts of the specification.
-   </topitem>
-
-   <footer/>
-</page>

diff --git a/helm/www/lambdadelta/web/home/versions.tbl b/helm/www/lambdadelta/web/home/versions.tbl
index 5c4112e16aa921a6649d23060f93fc9172c0bbe7..49d240c11b6945939e8746afe3986196755145ad 100644 (file)
--- a/helm/www/lambdadelta/web/home/versions.tbl
+++ b/helm/www/lambdadelta/web/home/versions.tbl
@@ -4,18 +4,19 @@ table {
    class "gray"   
       [ "version" "name" "developed with"
         "stage" "started" "announced" "released" "dismissed"
-      ] 
+      ]
    class "orange" 
-      [ @@("version_2" "Version 2") "\"basic_2\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2")
-        "\"A\"" "April 2011" "July 2014" "Planned in 2014" "Not planned yet"
-      ] 
+      [ @@("specification#v2" "Version 2") "\"basic_2\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2")
+        "\"A\"" "April 2011" "June 2014" "Planned in October 2014" "Not planned yet"
+      ]
    class "red"
-      [ @@("version_1" "Version 1") "\"basic_1\"" @("http://coq.inria.fr/" "Coq 7.3.1")
-        "" "May 2004" "January 2006" "November 2006" "May 2008" ] 
+      [ @@("specification#v1" "Version 1") "\"basic_1\"" @("http://coq.inria.fr/" "Coq 7.3.1")
+        "" "May 2004" "December 2005" "November 2006" "May 2008"
+      ]
 }
 
 class "top"               { * }
 
 class "capitalize italic" [ 0 ]
 
-ext ".html" { 1 }
+ext   ".html"             { 0 }

diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl
index 014d2e65ed3f39a47a7269115c6581e979c16bff..a6b25cb6fc2d9d3cf1d9dab7e41ab7b5cf89c18e 100644 (file)
--- a/helm/www/lambdadelta/xslt/ld_web_root.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl
@@ -124,12 +124,17 @@
    <span class="date"><xsl:value-of select="@date"/></span>
 </xsl:template>
 
-<xsl:template match="ld:basic-icon">
-   <img class="icon32"
-       alt="[basic lambdadelta logo]"
-       title="basic lambdadelta"
-       src="{$baseurl}images/basic_32.png"
-   />
+<xsl:template match="ld:version2-icon">
+   <xsl:call-template name="butterfly">
+      <xsl:with-param name="name" select="4"/>
+   </xsl:call-template>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+<xsl:template match="ld:version1-icon">
+   <xsl:call-template name="butterfly">
+      <xsl:with-param name="name" select="6"/>
+   </xsl:call-template>
    <xsl:call-template name="sp"/>
 </xsl:template>