From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 20 Jul 2014 14:16:42 +0000 (+0000)
Subject: web site update
X-Git-Tag: make_still_working~868
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bda6d964ce9729a694e3fd3ead386ca9f2ca14e3;p=helm.git

web site update
---

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index a477e6d4f..41f766285 100644
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -223,6 +223,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index fb588eea5..32d81ab2b 100644
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -191,6 +191,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 3bcd218b0..c8959b5cd 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -1300,6 +1300,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index e1e583101..aa35f4139 100644
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -42,9 +42,7 @@
             <td class="snns component green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn component 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>
+            <td class="ssnn component 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">
@@ -59,11 +57,7 @@
             <td class="snns green">
               <a href="http://lambdadelta.info/version_2.html">Version 2</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>
+            <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">
@@ -92,7 +86,7 @@
       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">2012-10</span>).
+      (revised <span class="date">2014-07</span>).
    </div>
    
    <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="v2">
@@ -104,7 +98,7 @@
       <table cellpadding="4" cellspacing="0">
         <tbody>
           <tr>
-            <td class="snns top" id="ldp7">
+            <td class="snns top" id="ldR5">
               <span class="date">R5.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/cie_2010.pdf">An Efficient Validation Procedure for the Formal System λδ</a> (<span class="date">2010-07</span>). In CiE 2010 Local Proceedings. University of Azores, CMATI Booklet, pp. 204-213. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
@@ -116,7 +110,7 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldp6">
+            <td class="snns top" id="ldR4">
               <span class="date">R4.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://www.informatica.unibo.it/it/ricerca/technical-report/2009/UBLCS-2009-16">Landau's "Grundlagen der Analysis" from Automath to lambda-delta</a> (<span class="date">2009-09</span>). University of Bologna, technical report UBLCS-2009-16. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
@@ -128,7 +122,7 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldt8">
+            <td class="snns top" id="ldP8">
               <span class="date">P8.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_8s.pdf">The Formal System λδ and the "Three Problems"</a> (<span class="date">2014-06</span>). Presentation at University of Bologna (slides).</td>
@@ -140,7 +134,7 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldt7">
+            <td class="snns top" id="ldP7">
               <span class="date">P7.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_7s.pdf">An Efficient Validation Procedure for the Formal System λδ</a> (<span class="date">2010-07</span>). Presentation at CiE 2010 (slides).</td>
@@ -152,7 +146,7 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldt6">
+            <td class="snns top" id="ldP6">
               <span class="date">P6.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_6s.pdf">A Validator for the Formal System λδ</a> (revised <span class="date">2010-02</span>). Presentation at University of Bologna (slides).</td>
@@ -189,7 +183,7 @@
       <table cellpadding="4" cellspacing="0">
         <tbody>
           <tr>
-            <td class="snns top" id="ldp5">
+            <td class="snns top" id="ldJ1">
               <span class="date">J1.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://doi.acm.org/10.1145/1614431.1614436">The Formal System λδ</a> (<span class="date">2009-11</span>). In In ACM ToCL 11(1), pp. 5:1-5:37 ( <a href="http://tocl.acm.org/accepted/335guidi.pdf">accepted</a>
@@ -202,7 +196,7 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldp4">
+            <td class="snns top" id="ldR3">
               <span class="date">R3.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/cie_2007.pdf">Lambda Types on the Lambda Calculus with Abbreviations</a> (<span class="date">2007-06</span>). In CiE 2007 Local Proceedings. University of Siena, technical report 487, p. 387 (abstract of a presentation). <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
@@ -214,7 +208,7 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldp3">
+            <td class="snns top" id="ldR2">
               <span class="date">R2.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-25">Lambda Types on the Lambda Calculus with Abbreviations</a> (<span class="date">2006-11</span>). University of Bologna, technical report UBLCS-2006-25. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
@@ -226,7 +220,7 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldp2">
+            <td class="snns top" id="ldR1">
               <span class="date">R1.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-01">Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification</a> (<span class="date">2006-01</span>). University of Bologna, technical report UBLCS-2006-01. <a href="http://lambdadelta.info/documentation.html#bibtex">BibTeX entry</a>.</td>
@@ -238,7 +232,7 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldt5">
+            <td class="snns top" id="ldP5">
               <span class="date">P5.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_5s.pdf">The Formal System λδ</a> (<span class="date">2008-10</span>). Presentation at Advances in Constructive Topology and Logical Foundations (slides).</td>
@@ -250,7 +244,7 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldt4">
+            <td class="snns top" id="ldP4">
               <span class="date">P4.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_4s.pdf">Towards the Unification of Terms, Types and Contexts</a> (<span class="date">2008-03</span>). Presentation at Types 2008 (slides).</td>
@@ -262,7 +256,7 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldt3">
+            <td class="snns top" id="ldP3">
               <span class="date">P3.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_3s.pdf">Lambda Types on the Lambda Calculus with Abbreviations</a> (<span class="date">2007-06</span>). Presentation at CiE 2007 (slides).</td>
@@ -274,7 +268,7 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldt2">
+            <td class="snns top" id="ldP2">
               <span class="date">P2.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_2s.pdf">Lambda Tipi sul Lambda Calcolo con Abbreviazioni</a> (<span class="date">2007-01</span>). Presentation at University of Padova (slides <span class="date">in Italian</span>).</td>
@@ -286,7 +280,7 @@
             </td>
           </tr>
           <tr>
-            <td class="snns top" id="ldt1">
+            <td class="snns top" id="ldP1">
               <span class="date">P1.</span>
             </td>
             <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/ld_talk_1s.pdf">Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata</a> (<span class="date">2005-12</span>). Presentation at University of Bologna (slides <span class="date">in Italian</span>).</td>
@@ -327,6 +321,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:15:22 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib
index 580d39fcf..147f0a51a 100644
--- a/helm/www/lambdadelta/download/lambdadelta.bib
+++ b/helm/www/lambdadelta/download/lambdadelta.bib
@@ -1,6 +1,6 @@
 % \lambda\delta version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@misc{lambdadelta8,
+@misc{lambdadeltaV2,
    author="F. {Guidi}",
    title="{lambdadelta\_2}",
    howpublished="Formal specification for the proof assistant Matita 0.99.2",
@@ -9,7 +9,7 @@
    note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$"
 }
 
-@incollection{lambdadelta7,
+@incollection{lambdadeltaR5,
    author="F. {Guidi}", 
    title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}",
    editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}",
@@ -21,7 +21,7 @@
    month="July"
 }
 
-@techreport{lambdadelta6,
+@techreport{lambdadeltaR4,
    author="F. {Guidi}", 
    title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", 
    type="Technical Report",
@@ -34,7 +34,7 @@
 
 % \lambda\delta version 1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@article{lambdadelta5,
+@article{lambdadeltaJ1,
    author="F. {Guidi}",
    title="{The Formal System $\lambda\delta$}",
    journal="Transactions on Computational Logic",
@@ -47,7 +47,7 @@
    month="November"
 }
 
-@incollection{lambdadelta4,
+@incollection{lambdadeltaR3,
    author="F. {Guidi}", 
    title="{Lambda Types on the Lambda Calculus with Abbreviations}",
    editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}",
@@ -59,7 +59,7 @@
    month="June"
 }
 
-@techreport{lambdadelta3,
+@techreport{lambdadeltaR2,
    author="F. {Guidi}", 
    title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", 
    type="Technical Report",
@@ -70,7 +70,7 @@
    month="November"
 }
 
-@techreport{lambdadelta2,
+@techreport{lambdadeltaR1,
    author="F. {Guidi}", 
    title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", 
    type="Technical Report",
@@ -81,7 +81,7 @@
    month="January"
 }
 
-@misc{lambdadelta1,
+@misc{lambdadeltaV1,
    author="F. {Guidi}",
    title="{lambdadelta\_1}",
    howpublished="Formal specification for the proof assistant Coq 7.3.1",
diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt
index 580d39fcf..147f0a51a 100644
--- a/helm/www/lambdadelta/download/lambdadelta.txt
+++ b/helm/www/lambdadelta/download/lambdadelta.txt
@@ -1,6 +1,6 @@
 % \lambda\delta version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@misc{lambdadelta8,
+@misc{lambdadeltaV2,
    author="F. {Guidi}",
    title="{lambdadelta\_2}",
    howpublished="Formal specification for the proof assistant Matita 0.99.2",
@@ -9,7 +9,7 @@
    note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$"
 }
 
-@incollection{lambdadelta7,
+@incollection{lambdadeltaR5,
    author="F. {Guidi}", 
    title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}",
    editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}",
@@ -21,7 +21,7 @@
    month="July"
 }
 
-@techreport{lambdadelta6,
+@techreport{lambdadeltaR4,
    author="F. {Guidi}", 
    title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", 
    type="Technical Report",
@@ -34,7 +34,7 @@
 
 % \lambda\delta version 1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-@article{lambdadelta5,
+@article{lambdadeltaJ1,
    author="F. {Guidi}",
    title="{The Formal System $\lambda\delta$}",
    journal="Transactions on Computational Logic",
@@ -47,7 +47,7 @@
    month="November"
 }
 
-@incollection{lambdadelta4,
+@incollection{lambdadeltaR3,
    author="F. {Guidi}", 
    title="{Lambda Types on the Lambda Calculus with Abbreviations}",
    editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}",
@@ -59,7 +59,7 @@
    month="June"
 }
 
-@techreport{lambdadelta3,
+@techreport{lambdadeltaR2,
    author="F. {Guidi}", 
    title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", 
    type="Technical Report",
@@ -70,7 +70,7 @@
    month="November"
 }
 
-@techreport{lambdadelta2,
+@techreport{lambdadeltaR1,
    author="F. {Guidi}", 
    title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", 
    type="Technical Report",
@@ -81,7 +81,7 @@
    month="January"
 }
 
-@misc{lambdadelta1,
+@misc{lambdadeltaV1,
    author="F. {Guidi}",
    title="{lambdadelta\_1}",
    howpublished="Formal specification for the proof assistant Coq 7.3.1",
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 810064210..9b08ac7df 100644
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -234,6 +234,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 77a7b0f29..f03c51a06 100644
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -42,9 +42,7 @@
             <td class="snns component green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn component 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>
+            <td class="ssnn component 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">
@@ -59,11 +57,7 @@
             <td class="snns green">
               <a href="http://lambdadelta.info/version_2.html">Version 2</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>
+            <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">
@@ -196,7 +190,7 @@
       Exploits a subset of "complete_rg" λδ as the intermediate language.
       Features importation from ".hln" files containing λδ textual syntax.
       The overall validation speed of the "Grundlagen der Analysis"
-      increases of 22% with respect toversion 0.8.0.
+      increases of 22% with respect to version 0.8.0.
       [Svn revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>)
       <ul>
           <li>
@@ -220,7 +214,7 @@
       Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
       Features importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
       and exportation to <a href="http://www.w3.org/XML/">XML</a>.
-      <a href="http://lambdadelta.info/documentation.html#ldp6">Documentation</a>.
+      <a href="http://lambdadelta.info/documentation.html#ldR4">Documentation (R4)</a>.
       [Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
       <ul>
           <li>
@@ -269,6 +263,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 3f33aa057..dca01c171 100644
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -42,9 +42,7 @@
             <td class="snns component green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn component 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>
+            <td class="ssnn component 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">
@@ -59,11 +57,7 @@
             <td class="snns green">
               <a href="http://lambdadelta.info/version_2.html">Version 2</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>
+            <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">
@@ -141,6 +135,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 54a3d4af6..7d54817f3 100644
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -42,9 +42,7 @@
             <td class="snns component green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn component 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>
+            <td class="ssnn component 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">
@@ -59,11 +57,7 @@
             <td class="snns green">
               <a href="http://lambdadelta.info/version_2.html">Version 2</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>
+            <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">
@@ -88,177 +82,200 @@
 
    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="milestones">Milestones <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b5.png" />
     </div>
-   <div xmlns:ld="http://lambdadelta.info/" class="text">
-      <ul>
-        <li>
-          <span class="date">June 2014.</span>
-         <a href="http://lambdadelta.info/documentation.html#ldt8">First communication on λδ version 2.</a>
-      </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">December 2012.</span>
-         The character "_" is removed from the denomination "lambda_delta":
-         <ul>
-            <li>
-               The denomination "\lambda\delta" is used in λδ-related texts.
-            </li>
-            <li>
-               The denomination "lambdadelta" is used in λδ-related identifiers.
-            </li>
-            <li>
-              Permanent λδ URL acquired:
-              <a href="http://lambdadelta.info/">http://lambdadelta.info/</a>
-              (pointing at this site).
-            </li>
-         </ul>
-      </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">September 2011.</span>
-         The denomination "lambda-delta" changes to "lambda_delta":
-         <ul>
-            <li>
-               The character "-" is reserved in λδ textual syntax
-               (recognized by "Helena 0.8.1").            
-            </li>
-            <li>
-               Eventually, the occurrences of the character "-"
-               will be replaced by "_" in all λδ-related identifiers.
-            </li>
-            <li>
-               In particular, this refactoring involves file names and path names.
-            </li>
-         </ul>
-      </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">April 2011.</span>
-         The specification of <a href="http://lambdadelta.info/version_2.html">λδ version 2</a>
-         and related topics is restarted in
-         <a href="http://matita.cs.unibo.it/">Matita 0.5</a>.
-      </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">December 2010.</span>
-         Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012). 
-      </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">November 2010.</span>
-         "Helena 0.8.1" is released. 
-      </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">September 2009.</span>
-         "Helena 0.8.0" is released and the
-         <a href="http://lambdadelta.info/implementation.html#lddl">λδ Digital Library</a>
-         is started.
-      </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">June 2009.</span>
-         "Helena", a <a href="http://lambdadelta.info/implementation.html#helena">validator for λδ version 2</a>,
-         is available as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> software. 
-      </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">September 2008.</span>
-         This site is online.
-      </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">July 2008.</span>
-         <a href="http://lambdadelta.info/documentation.html#ldp5">First journal paper on λδ</a>
-         accepted for publication.
-      </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">July 2008.</span>
-         First <a href="http://helm.cs.unibo.it/procedural/">procedural reconstruction</a>
-         for <a href="http://matita.cs.unibo.it/">Matita 0.5</a>
-         of the λδ version 1 for Coq 7.3.1.
-      </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">June 2008.</span>
-         The <a href="http://lambdadelta.info/version_1.html#static">
-            HTML pages of the specification of λδ version 1 for Matita 0.5</a>
-         are online.
-      </li>
-      </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">July 2014.</span>
+      A new version of this site is online.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">June 2014.</span>
+      <a href="http://lambdadelta.info/documentation.html#ldP8">First communication on λδ version 2.</a>
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">December 2012.</span>
+      The character "_" is removed from the denomination "lambda_delta":
       <ul>
-        <li>
-          <span class="date">May 2008.</span>
-         The specification of λδ version 1 is dismissed.
+          <li>
+         The denomination "\lambda\delta" is used in λδ-related texts.
       </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">March 2008.</span>
-         The specification of λδ version 2 is started with Coq 7.3.1 (false start).
+          <li>
+         The denomination "lambdadelta" is used in λδ-related identifiers.
       </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">September 2007.</span>
-         The <a href="http://lambdadelta.info/version_1.html#dynamic">
-            specification of λδ version 1 for Matita 0.4</a>
-         is online.
+          <li>
+         Permanent λδ URL acquired:
+         <a href="http://lambdadelta.info/">http://lambdadelta.info/</a>
+         (pointing at this site).
       </li>
-      </ul>
+        </ul>
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">September 2011.</span>
+      The denomination "lambda-delta" changes to "lambda_delta":
       <ul>
-        <li>
-          <span class="date">November 2006.</span>
-         <a href="http://lambdadelta.info/documentation.html#ldp3">λδ version 1</a>
-         is released.
+          <li>
+         The character "-" is reserved in λδ textual syntax
+         (recognized by "Helena 0.8.1").            
       </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">December 2005.</span>
-         <a href="http://lambdadelta.info/documentation.html#ldt1">First communication on λδ</a>.
+          <li>
+         Eventually, the occurrences of the character "-"
+         will be replaced by "_" in all λδ-related identifiers.
       </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">May 2004.</span>
-         The specification of <a href="http://lambdadelta.info/version_1.html">λδ version 1</a>
-         is started with Coq 7.3.1.
+          <li>
+         In particular, this refactoring involves file names and path names.
       </li>
-      </ul>
-   </div>
+        </ul>
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">April 2011.</span>
+      The specification of <a href="http://lambdadelta.info/version_2.html">λδ version 2</a>
+      and related topics is restarted in
+      <a href="http://matita.cs.unibo.it/">Matita 0.5</a>.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">December 2010.</span>
+      Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012). 
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">November 2010.</span>
+      "Helena 0.8.1" is released. 
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">September 2009.</span>
+      "Helena 0.8.0" is released and the
+      <a href="http://lambdadelta.info/implementation.html#lddl">λδ Digital Library</a>
+      is started.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">June 2009.</span>
+      "Helena", a <a href="http://lambdadelta.info/implementation.html#helena">validator for λδ version 2</a>,
+      is available as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> software. 
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">September 2008.</span>
+      This site is online.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">July 2008.</span>
+      <a href="http://lambdadelta.info/documentation.html#ldJ1">First journal paper on λδ</a>
+      accepted for publication.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">July 2008.</span>
+      First <a href="http://helm.cs.unibo.it/procedural/">procedural reconstruction</a>
+      for <a href="http://matita.cs.unibo.it/">Matita 0.5</a>
+      of the λδ version 1 for Coq 7.3.1.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">June 2008.</span>
+      The <a href="http://lambdadelta.info/version_1.html#static">
+         HTML pages of the specification of λδ version 1 for Matita 0.5</a>
+      are online.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">May 2008.</span>
+      The specification of λδ version 1 is dismissed.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">March 2008.</span>
+      The specification of λδ version 2 is started with Coq 7.3.1 (false start).
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">September 2007.</span>
+      The <a href="http://lambdadelta.info/version_1.html#dynamic">
+         specification of λδ version 1 for Matita 0.4</a>
+      is online.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">November 2006.</span>
+      <a href="http://lambdadelta.info/documentation.html#ldR2">λδ version 1</a>
+      is released.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">December 2005.</span>
+      <a href="http://lambdadelta.info/documentation.html#ldP1">First communication on λδ version 1</a>.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">May 2004.</span>
+      The specification of <a href="http://lambdadelta.info/version_1.html">λδ version 1</a>
+      is started with Coq 7.3.1.
+   </li>
+    </ul>
 
    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="visibility">Visibility <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
     </div>
-   <div xmlns:ld="http://lambdadelta.info/" class="text">
-      <ul>
-        <li>
-          <span class="date">June 2014.</span>
-         The <a href="http://www.google.com/">Google</a>
-         search for "formal system lambda delta" gives
-         5 resources about λδ in the first 6 results.
-      </li>
-      </ul>
-      <ul>
-        <li>
-          <span class="date">June 2014.</span>
-         The <a href="http://www.yahoo.com/">Yahoo</a>
-         search for "formal system lambda delta" gives
-         4 resources about λδ in the first 5 results.
-      </li>
-      </ul>
-   </div>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">June 2014.</span>
+      The <a href="http://www.google.com/">Google</a>
+      search for "formal system lambda delta" gives
+      5 resources about λδ in the first 6 results.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">June 2014.</span>
+      The <a href="http://www.yahoo.com/">Yahoo</a>
+      search for "formal system lambda delta" gives
+      4 resources about λδ in the first 5 results.
+   </li>
+    </ul>
 
    <div class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
@@ -286,6 +303,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html
index 1549b10d6..e62b68ee9 100644
--- a/helm/www/lambdadelta/version_1.html
+++ b/helm/www/lambdadelta/version_1.html
@@ -42,9 +42,7 @@
             <td class="snns component green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn component 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>
+            <td class="ssnn component 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">
@@ -59,11 +57,7 @@
             <td class="snns green">
               <a href="http://lambdadelta.info/version_2.html">Version 2</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>
+            <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">
@@ -88,60 +82,64 @@
 
    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Formats <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b6.png" />
     </div>
+
    <div xmlns:ld="http://lambdadelta.info/" class="text">
       The formal specification of λδ version 1
       is available in the following formats:
-      <ul id="source">
-        <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.
+   </div>
+
+   <ul xmlns:ld="http://lambdadelta.info/" id="source">
+      <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="static">
+      <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>
-      </ul>
-      <ul id="static">
-        <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>
+         <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
+            Correctness of types</a>.
       </li>
-      </ul>
-      <ul id="dynamic">
-        <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>
+         <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
+            Uniqueness of types up to conversion</a>.
       </li>
-      </ul>
-   </div>
+          <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="dynamic">
+      <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" />
@@ -169,6 +167,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html
index bbbf58ff7..719331a08 100644
--- a/helm/www/lambdadelta/version_2.html
+++ b/helm/www/lambdadelta/version_2.html
@@ -42,9 +42,7 @@
             <td class="snns component green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn component 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>
+            <td class="ssnn component 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">
@@ -59,11 +57,7 @@
             <td class="snns green">
               <a href="http://lambdadelta.info/version_2.html">Version 2</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>
+            <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">
@@ -88,26 +82,29 @@
 
    <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="foreword">Formats <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" />
     </div>
+   
    <div xmlns:ld="http://lambdadelta.info/" class="text">
       The formal specification of λδ version 2
       is available in the following formats:
-      <ul id="source">
-        <li>
-         <a href="http://lambdadelta.info/download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</a>
-         (revised <span class="date">2014-07</span>).
-         Source scripts.
-      </li>
-      </ul>
-      <ul id="parts">
-        <li>
-         <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>.
-         Informational pages on the parts of the specification.
-      </li>
-      </ul>
    </div>
 
+   <ul xmlns:ld="http://lambdadelta.info/" id="source">
+      <li>
+      <a href="http://lambdadelta.info/download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</a>
+      (revised <span class="date">2014-07</span>).
+      Source scripts.
+   </li>
+    </ul>
+
+   <ul xmlns:ld="http://lambdadelta.info/" id="parts">
+      <li>
+      <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>.
+      Informational pages on the parts of the specification.
+   </li>
+    </ul>
+
    <div class="spacer">
       <img class="rule" alt="[Spacer]" title="lambdadelta rainbow rule" src="http://lambdadelta.info/images/rainbow.png" />
     </div>
@@ -134,6 +131,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 16:13:31 +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 3e7a6526f..86d91160f 100644
--- a/helm/www/lambdadelta/web/home/documentation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml
@@ -12,7 +12,7 @@
       BibTeX database of λδ documentation:
       <rlink to="download/lambdadelta.bib">lambdadelta.bib</rlink>,
       <rlink to="download/lambdadelta.txt">lambdadelta.txt</rlink>
-      (revised <date date="2012-10"/>).
+      (revised <date date="2014-07"/>).
    </body>
    
    <section name="v2"><basic-icon/>λδ version 2 (in progress)</section>
diff --git a/helm/www/lambdadelta/web/home/documentation_1.tbl b/helm/www/lambdadelta/web/home/documentation_1.tbl
index fe91832cd..07114eec2 100644
--- a/helm/www/lambdadelta/web/home/documentation_1.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_1.tbl
@@ -1,7 +1,7 @@
 name "documentation_1"
 
 table {
-   [ { name "ldp5" "<span class=\"date\">J1.</span>" "" } {
+   [ { name "ldJ1" "<span class=\"date\">J1.</span>" "" } {
      "F. Guidi:" +
      @("http://doi.acm.org/10.1145/1614431.1614436"
      "The Formal System λδ") +
@@ -16,7 +16,7 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
-   [ { name "ldp4" "<span class=\"date\">R3.</span>" "" } {
+   [ { name "ldR3" "<span class=\"date\">R3.</span>" "" } {
      "F. Guidi:" +
      @@("download/cie_2007.pdf"
      "Lambda Types on the Lambda Calculus with Abbreviations") +
@@ -27,7 +27,7 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
-   [ { name "ldp3" "<span class=\"date\">R2.</span>" "" } {
+   [ { name "ldR2" "<span class=\"date\">R2.</span>" "" } {
      "F. Guidi:" +
      @("http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-25"
      "Lambda Types on the Lambda Calculus with Abbreviations") +
@@ -36,7 +36,7 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
-   [ { name "ldp2" "<span class=\"date\">R1.</span>" "" } {
+   [ { name "ldR1" "<span class=\"date\">R1.</span>" "" } {
      "F. Guidi:" +
      @("http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-01"
      "Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification") +
@@ -45,14 +45,14 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
-   [ { name "ldt5" "<span class=\"date\">P5.</span>" "" } {
+   [ { name "ldP5" "<span class=\"date\">P5.</span>" "" } {
      "F. Guidi:" +
      @@("download/ld_talk_5s.pdf" "The Formal System λδ") +
      "(<span class=\"date\">2008-10</span>)." +
      "Presentation at Advances in Constructive Topology and Logical Foundations (slides)."
      * }
    ]
-   [ { name "ldt4" "<span class=\"date\">P4.</span>" "" } {
+   [ { name "ldP4" "<span class=\"date\">P4.</span>" "" } {
      "F. Guidi:" +
      @@("download/ld_talk_4s.pdf"
      "Towards the Unification of Terms, Types and Contexts") +
@@ -60,7 +60,7 @@ table {
      "Presentation at Types 2008 (slides)."
      * }
    ]
-   [ { name "ldt3" "<span class=\"date\">P3.</span>" "" } {
+   [ { name "ldP3" "<span class=\"date\">P3.</span>" "" } {
      "F. Guidi:" +
      @@("download/ld_talk_3s.pdf"
      "Lambda Types on the Lambda Calculus with Abbreviations") +
@@ -68,7 +68,7 @@ table {
      "Presentation at CiE 2007 (slides)."
      * }
    ]
-   [ { name "ldt2" "<span class=\"date\">P2.</span>" "" } {
+   [ { name "ldP2" "<span class=\"date\">P2.</span>" "" } {
      "F. Guidi:" +
      @@("download/ld_talk_2s.pdf"
      "Lambda Tipi sul Lambda Calcolo con Abbreviazioni") +
@@ -77,7 +77,7 @@ table {
      "<span class=\"date\">in Italian</span>)."
      * }
    ]
-   [ { name "ldt1" "<span class=\"date\">P1.</span>" "" } {
+   [ { name "ldP1" "<span class=\"date\">P1.</span>" "" } {
      "F. Guidi:" +
      @@("download/ld_talk_1s.pdf"
      "Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata") +
diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl
index 7262f6c81..9a50d94d2 100644
--- a/helm/www/lambdadelta/web/home/documentation_2.tbl
+++ b/helm/www/lambdadelta/web/home/documentation_2.tbl
@@ -1,7 +1,7 @@
 name "documentation_2"
 
 table {
-   [ { name "ldp7" "<span class=\"date\">R5.</span>" "" } {
+   [ { name "ldR5" "<span class=\"date\">R5.</span>" "" } {
      "F. Guidi:" +
      @@("download/cie_2010.pdf"
      "An Efficient Validation Procedure for the Formal System λδ") +
@@ -11,7 +11,7 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ]
-   [ { name "ldp6" "<span class=\"date\">R4.</span>" "" } {
+   [ { name "ldR4" "<span class=\"date\">R4.</span>" "" } {
      "F. Guidi:" + 
      @("http://www.informatica.unibo.it/it/ricerca/technical-report/2009/UBLCS-2009-16"
      "Landau's \"Grundlagen der Analysis\" from Automath to lambda-delta") +
@@ -20,7 +20,7 @@ table {
      @@("documentation.html#bibtex" "BibTeX entry") ^ "."
      * }
    ] 
-   [ { name "ldt8" "<span class=\"date\">P8.</span>" "" } {
+   [ { name "ldP8" "<span class=\"date\">P8.</span>" "" } {
      "F. Guidi:" + 
      @@("download/ld_talk_8s.pdf"
      "The Formal System λδ and the \"Three Problems\"") +
@@ -28,7 +28,7 @@ table {
      "Presentation at University of Bologna (slides)."
      * }
    ] 
-   [ { name "ldt7" "<span class=\"date\">P7.</span>" "" } {
+   [ { name "ldP7" "<span class=\"date\">P7.</span>" "" } {
      "F. Guidi:" + 
      @@("download/ld_talk_7s.pdf"
      "An Efficient Validation Procedure for the Formal System λδ") +
@@ -36,7 +36,7 @@ table {
      "Presentation at CiE 2010 (slides)."
      * }
    ]
-   [ { name "ldt6" "<span class=\"date\">P6.</span>" "" } {
+   [ { name "ldP6" "<span class=\"date\">P6.</span>" "" } {
      "F. Guidi:" + 
      @@("download/ld_talk_6s.pdf"
      "A Validator for the Formal System λδ") +
diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml
index b8cc30553..1ae011367 100644
--- a/helm/www/lambdadelta/web/home/implementation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml
@@ -59,7 +59,7 @@
       Exploits a subset of "complete_rg" λδ as the intermediate language.
       Features importation from ".hln" files containing λδ textual syntax.
       The overall validation speed of the "Grundlagen der Analysis"
-      increases of 22% with respect toversion 0.8.0.
+      increases of 22% with respect to version 0.8.0.
       [Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>)
       <list><item>
          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
@@ -77,7 +77,7 @@
       Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
       Features importation from <link to="http://www.win.tue.nl/automath/">Automath</link>
       and exportation to <link to="http://www.w3.org/XML/">XML</link>.
-      <rlink to="documentation.html#ldp6">Documentation</rlink>.
+      <rlink to="documentation.html#ldR4">Documentation (R4)</rlink>.
       [Svn revision: 10304] (<rlink to="download/helena_0.8.0.tar.gz">archived source code</rlink>).
       <list><item>
          A <link to="http://www.jedsoft.org/jed/">Jed mode</link>
diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml
index cee19459d..92dda5491 100644
--- a/helm/www/lambdadelta/web/home/news.ldw.xml
+++ b/helm/www/lambdadelta/web/home/news.ldw.xml
@@ -8,116 +8,128 @@
    <sitemap name="sitemap"/>
 
    <section5 name="milestones">Milestones</section5>
-   <body>
-      <news date="June 2014.">
-         <rlink to="documentation.html#ldt8">First communication on λδ version 2.</rlink>
-      </news>
-      <news date="December 2012.">
-         The character "_" is removed from the denomination "lambda_delta":
-         <list>
-            <item>
-               The denomination "\lambda\delta" is used in λδ-related texts.
-            </item>
-            <item>
-               The denomination "lambdadelta" is used in λδ-related identifiers.
-            </item>
-            <item>
-              Permanent λδ URL acquired:
-              <rlink to="">http://lambdadelta.info/</rlink>
-              (pointing at this site).
-            </item>
-         </list>
-      </news>
-      <news date="September 2011.">
-         The denomination "lambda-delta" changes to "lambda_delta":
-         <list>
-            <item>
-               The character "-" is reserved in λδ textual syntax
-               (recognized by "Helena 0.8.1").            
-            </item>
-            <item>
-               Eventually, the occurrences of the character "-"
-               will be replaced by "_" in all λδ-related identifiers.
-            </item>
-            <item>
-               In particular, this refactoring involves file names and path names.
-            </item>
-         </list>
-      </news>
-      <news date="April 2011.">
-         The specification of <rlink to="version_2.html">λδ version 2</rlink>
-         and related topics is restarted in
-         <link to="http://matita.cs.unibo.it/">Matita 0.5</link>.
-      </news>
-      <news date="December 2010.">
-         Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012). 
-      </news>
-      <news date="November 2010.">
-         "Helena 0.8.1" is released. 
-      </news>
-      <news date="September 2009.">
-         "Helena 0.8.0" is released and the
-         <rlink to="implementation.html#lddl">λδ Digital Library</rlink>
-         is started.
-      </news>
-      <news date="June 2009.">
-         "Helena", a <rlink to="implementation.html#helena">validator for λδ version 2</rlink>,
-         is available as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software. 
-      </news>
-      <news date="September 2008.">
-         This site is online.
-      </news>
-      <news date="July 2008.">
-         <rlink to="documentation.html#ldp5">First journal paper on λδ</rlink>
-         accepted for publication.
-      </news>
-      <news date="July 2008.">
-         First <link to="http://helm.cs.unibo.it/procedural/">procedural reconstruction</link>
-         for <link to="http://matita.cs.unibo.it/">Matita 0.5</link>
-         of the λδ version 1 for Coq 7.3.1.
-      </news>
-      <news date="June 2008.">
-         The <rlink to="version_1.html#static">
-            HTML pages of the specification of λδ version 1 for Matita 0.5</rlink>
-         are online.
-      </news>
-      <news date="May 2008.">
-         The specification of λδ version 1 is dismissed.
-      </news>
-      <news date="March 2008.">
-         The specification of λδ version 2 is started with Coq 7.3.1 (false start).
-      </news>
-      <news date="September 2007.">
-         The <rlink to="version_1.html#dynamic">
-            specification of λδ version 1 for Matita 0.4</rlink>
-         is online.
-      </news>
-      <news date="November 2006.">
-         <rlink to="documentation.html#ldp3">λδ version 1</rlink>
-         is released.
-      </news>
-      <news date="December 2005.">
-         <rlink to="documentation.html#ldt1">First communication on λδ</rlink>.
-      </news>
-      <news date="May 2004.">
-         The specification of <rlink to="version_1.html">λδ version 1</rlink>
-         is started with Coq 7.3.1.
-      </news>
-   </body>
+
+   <news date="July 2014.">
+      A new version of this site is online.
+   </news>
+
+   <news date="June 2014.">
+      <rlink to="documentation.html#ldP8">First communication on λδ version 2.</rlink>
+   </news>
+
+   <news date="December 2012.">
+      The character "_" is removed from the denomination "lambda_delta":
+      <list><item>
+         The denomination "\lambda\delta" is used in λδ-related texts.
+      </item><item>
+         The denomination "lambdadelta" is used in λδ-related identifiers.
+      </item><item>
+         Permanent λδ URL acquired:
+         <rlink to="">http://lambdadelta.info/</rlink>
+         (pointing at this site).
+      </item></list>
+   </news>
+
+   <news date="September 2011.">
+      The denomination "lambda-delta" changes to "lambda_delta":
+      <list><item>
+         The character "-" is reserved in λδ textual syntax
+         (recognized by "Helena 0.8.1").            
+      </item><item>
+         Eventually, the occurrences of the character "-"
+         will be replaced by "_" in all λδ-related identifiers.
+      </item><item>
+         In particular, this refactoring involves file names and path names.
+      </item></list>
+   </news>
+
+   <news date="April 2011.">
+      The specification of <rlink to="version_2.html">λδ version 2</rlink>
+      and related topics is restarted in
+      <link to="http://matita.cs.unibo.it/">Matita 0.5</link>.
+   </news>
+
+   <news date="December 2010.">
+      Transient λδ URL acquired: http://lambda-delta.info/ (expires on December 2012). 
+   </news>
+
+   <news date="November 2010.">
+      "Helena 0.8.1" is released. 
+   </news>
+
+   <news date="September 2009.">
+      "Helena 0.8.0" is released and the
+      <rlink to="implementation.html#lddl">λδ Digital Library</rlink>
+      is started.
+   </news>
+
+   <news date="June 2009.">
+      "Helena", a <rlink to="implementation.html#helena">validator for λδ version 2</rlink>,
+      is available as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software. 
+   </news>
+
+   <news date="September 2008.">
+      This site is online.
+   </news>
+
+   <news date="July 2008.">
+      <rlink to="documentation.html#ldJ1">First journal paper on λδ</rlink>
+      accepted for publication.
+   </news>
+
+   <news date="July 2008.">
+      First <link to="http://helm.cs.unibo.it/procedural/">procedural reconstruction</link>
+      for <link to="http://matita.cs.unibo.it/">Matita 0.5</link>
+      of the λδ version 1 for Coq 7.3.1.
+   </news>
+
+   <news date="June 2008.">
+      The <rlink to="version_1.html#static">
+         HTML pages of the specification of λδ version 1 for Matita 0.5</rlink>
+      are online.
+   </news>
+
+   <news date="May 2008.">
+      The specification of λδ version 1 is dismissed.
+   </news>
+
+   <news date="March 2008.">
+      The specification of λδ version 2 is started with Coq 7.3.1 (false start).
+   </news>
+
+   <news date="September 2007.">
+      The <rlink to="version_1.html#dynamic">
+         specification of λδ version 1 for Matita 0.4</rlink>
+      is online.
+   </news>
+
+   <news date="November 2006.">
+      <rlink to="documentation.html#ldR2">λδ version 1</rlink>
+      is released.
+   </news>
+
+   <news date="December 2005.">
+      <rlink to="documentation.html#ldP1">First communication on λδ version 1</rlink>.
+   </news>
+
+   <news date="May 2004.">
+      The specification of <rlink to="version_1.html">λδ version 1</rlink>
+      is started with Coq 7.3.1.
+   </news>
 
    <section4 name="visibility">Visibility</section4>
-   <body>
-      <news date="June 2014.">
-         The <link to="http://www.google.com/">Google</link>
-         search for "formal system lambda delta" gives
-         5 resources about λδ in the first 6 results.
-      </news>
-      <news date="June 2014.">
-         The <link to="http://www.yahoo.com/">Yahoo</link>
-         search for "formal system lambda delta" gives
-         4 resources about λδ in the first 5 results.
-      </news>
-   </body>
+
+   <news date="June 2014.">
+      The <link to="http://www.google.com/">Google</link>
+      search for "formal system lambda delta" gives
+      5 resources about λδ in the first 6 results.
+   </news>
+
+   <news date="June 2014.">
+      The <link to="http://www.yahoo.com/">Yahoo</link>
+      search for "formal system lambda delta" gives
+      4 resources about λδ in the first 5 results.
+   </news>
 
    <footer/>
 </page>
diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl
index 9ee265a89..df44a964b 100644
--- a/helm/www/lambdadelta/web/home/sitemap.tbl
+++ b/helm/www/lambdadelta/web/home/sitemap.tbl
@@ -18,12 +18,14 @@ table [
    }
    class "green" {
       [ @@"implementation" 
-        "(" ^ @@("implementation#specifications" "specifications") +
-        @@("implementation#lddl" "library") +
+        "(" ^ @@("implementation#specifications" "specifications") + "-" +
+        @@("implementation#lddl" "library") + "-" +
         @@("implementation#helena" "Helena") ^ ")"
       * ]
       [ @@("version_2" "Version 2") 
-        @@("ground_2" "Background") + @@("basic_2" "Core") + @@("apps_2" "Applications")
+        "(" ^ @@("ground_2" "Background") + "-" + 
+        @@("basic_2" "Core") + "-" +
+        @@("apps_2" "Applications") ^ ")"
       * ]
       [ @@("version_1" "Version 1") * ] *
    }
diff --git a/helm/www/lambdadelta/web/home/version_1.ldw.xml b/helm/www/lambdadelta/web/home/version_1.ldw.xml
index 06a871cae..e80bfe1a7 100644
--- a/helm/www/lambdadelta/web/home/version_1.ldw.xml
+++ b/helm/www/lambdadelta/web/home/version_1.ldw.xml
@@ -8,54 +8,51 @@
    <sitemap name="sitemap"/>
 
    <section6 name="foreword">Formats</section6>
+
    <body>
       The formal specification of λδ version 1
       is available in the following formats:
-      <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>
    </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
index 2e1578514..9c002c7c9 100644
--- a/helm/www/lambdadelta/web/home/version_2.ldw.xml
+++ b/helm/www/lambdadelta/web/home/version_2.ldw.xml
@@ -8,21 +8,24 @@
    <sitemap name="sitemap"/>
 
    <section4 name="foreword">Formats</section4>
+   
    <body>
       The formal specification of λδ version 2
       is available in the following formats:
-      <topitem name="source">
-         <rlink to="download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</rlink>
-         (revised <date date="2014-07"/>).
-         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>
    </body>
 
+   <topitem name="source">
+      <rlink to="download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</rlink>
+      (revised <date date="2014-07"/>).
+      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>