the generation of the web site is completed!

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 9b46aa52c321ad21fa5852a207708351578694f3..a477e6d4f9b8da1c94fcf9f95440a8d328a76a8c 100644 (file)
--- 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 11:29:55 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index ece3b07ca811216589804886307c210ebe7c0d86..fb588eea561a5b3772fbaf5798d1af2175748a01 100644 (file)
--- 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 11:29:55 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 9595ea5b3002eaab40d1cc911196f9d04e9fc3a9..3bcd218b0b3c5ecfdb8ec5d53c4c210efe9100da 100644 (file)
--- 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 11:29:55 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index e41618049b3d5aaea062d1b4235b517df1995b82..e1e583101cf327e51a2960c195f8084d2e61e2fb 100644 (file)
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -42,9 +42,9 @@
             <td class="snns component green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn component green">
-              <br />
-            </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">
@@ -96,7 +96,7 @@
    </div>
    
    <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="v2">
-      <img class="icon32" alt="[basic lambdadelta]" title="basic lambdadelta" src="http://lambdadelta.info/images/basic_32.png" /> λδ version 2 (in progress)</div>
+      <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="text">
       The main source of information is <span class="date">P8</span>.
    </div>
@@ -180,7 +180,7 @@
     </div>
 
    <div xmlns:ld="http://lambdadelta.info/" class="head2sn" id="v1">
-      <img class="icon32" alt="[basic lambdadelta]" title="basic lambdadelta" src="http://lambdadelta.info/images/basic_32.png" /> λδ version 1 (dismissed)</div>
+      <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="text">
       The main source of information is <span class="date">J1</span>.
       A summary is available in <span class="date">P5</span>.
@@ -327,6 +327,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 11:35:27 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 32705c284b36b661d67a99a526fe366af330c3ff..8100642108138aec675bfd7613814157a6306fec 100644 (file)
--- 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 11:29:55 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index cb9b23247edeb484cfdd1f099750506ba2d81ebb..77a7b0f2905e15cf045860416b88a81802f2bb08 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -1,255 +1,274 @@
-<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
-<html dir="ltr" lang="en-us"><head>
-
+<?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 component sky">
+              <a href="http://lambdadelta.info/index.html">home</a>
+            </td>
+            <td class="snns component magenta">
+              <a href="http://lambdadelta.info/news.html">news</a>
+            </td>
+            <td class="snns component orange">
+              <a href="http://lambdadelta.info/documentation.html">documentation</a>
+            </td>
+            <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>
+          </tr>
+          <tr>
+            <td class="snns 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>
+            <td class="snns 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>
+            <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>
+            <td class="snss 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>
+            <td class="snss green">
+              <a href="http://lambdadelta.info/version_1.html">Version 1</a>
+            </td>
+            <td class="sssn green">
+              <br />
+            </td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
 
-  
-    <meta content="text/html; charset=UTF-8" http-equiv="content-type"><title>λδ home page</title>
-    
-    <meta content="Ferruccio Guidi" name="author">
-    <meta content="The formal system λδ" name="description">
-    <link rel="shortcut icon" href="images/crux_16.ico"></head><body>
-    <div style="text-align: center;">
-      <br>
-      <a href="http://lambdadelta.info/"><img alt="[Crux Logo]" title="The Crux" src="images/crux_32.png" style="border: 0px solid ; width: 32px; height: 32px;"></a>
-      <h1>The Formal System λδ (\lambda\delta)<br>
-      </h1>
-      <h2>Towards the unification of terms, types, environments and
-        contexts</h2>
-      <img style="width: 95%; height: 4px;" alt="[Separator]" title="Separator" src="images/rainbow.png"><br>
-      <table style="text-align: left; width: 95%; margin-left: auto; margin-right: auto;" border="0" cellpadding="2" cellspacing="20">
+   <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/b9.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 style="vertical-align: top;">
-              <ul>
-                <li><a href="index.html">Foreword</a></li>
-              </ul>
-              <ul>
-                <li><a href="news.html">News</a></li>
-              </ul>
-              <ul>
-                <li><a href="documentation.html">Papers</a></li>
-              </ul>
-              <ul>
-                <li>Resources<br>
-                </li>
-              </ul>
-            </td>
-            <td style="vertical-align: top; text-align: left;">
-              <h3 style="text-align: right;">Computer-checked formal
-                specifications <img style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" src="images/b9.png"></h3>
-              <span style="font-weight: bold;">Resource
-                1</span> below provides for the statically generated <span style="font-weight: bold;">natural language
-                representation</span> of
-              λδ meta-theory (faster rendering w.r.t. resource 2 below).<br>
-              <span style="font-weight: bold;">Resource 2</span> below
-              provides
-              for the dynamically generated <span style="font-weight: bold;">natural
-                language representation</span> of
-              λδ meta-theory (powered by the <a href="http://helm.cs.unibo.it/">HELM</a>
-              rendering engine).<br>
-              Remarkably, λδ was born and developed in the digital
-              format of <span style="font-weight: bold;">resource 3</span>
-              below, which is not the
-              formal counterpart of some informal material previously
-              written on
-              paper (as it happens for most currently digitalized
-              Mathematics).<br>
-              <ol>
-                <li><a name="static"></a>F. Guidi: <a style="font-style: italic;" href="http://lambdadelta.info/static/matita/lambdadelta/">lambdadelta</a>
-                  (revised <span style="font-weight: bold;">2011-09</span>).
-                  Formal
-                  specification for <a href="http://matita.cs.unibo.it/">Matita</a> 0.5
-                  (HTML pages generated
-                  by the <a href="http://helm.cs.unibo.it/">HELM</a>
-                  rendering engine)
-                  Here are the most relevant theorems proved in the
-                  formal specification:
-                  <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>.<br>
-                    </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>.<br>
-                      <br>
-                    </li>
-                  </ul>
-                </li>
-                <li><a name="dynamic"></a>F. Guidi: <a style="font-style: italic;" 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</a>
-                  (revised <span style="font-weight: bold;">2011-09</span>).
-                  Formal
-                  specification for <a href="http://matita.cs.unibo.it/">Matita</a> 0.5 (<a href="http://helm.cs.unibo.it/">HELM</a> directory).<br>
-                  <span style="font-weight: bold;">Currently, the HELM rendering engine is offline.</span><br>
-                 <br>
-                </li>
-                <li><a name="ldp1"></a>F. Guidi: <a href="http://lambdadelta.info/download/lambdadelta_1.tar.gz"><span style="font-style: italic;">lambdadelta_1</span></a>
-                  (revised <span style="font-weight: bold;">2012-10</span>).
-Formal
-                  specification for <span style="font-weight: bold;">Coq
-                    7.3.1</span>
-                  (source
-                  proof scripts). <a href="#bibtex">BibTeX entry</a>.<br>
-                </li>
-              </ol>
-              <h3 style="text-align: right;">Tools <img style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" src="images/b5.png"></h3>
-              <a name="lddl"></a><img style="width: 32px; height: 32px;" alt="[Crux Logo]" title="The Crux" src="images/crux_32.png"><span style="font-weight: bold;"> </span>The <span style="font-weight: bold;"><span style="text-decoration: underline;">λδ
-                  Digital
-                  Library
-                  (LDDL)</span></span> is part of <a href="http://helm.cs.unibo.it/">HELM</a>
-              and contains a set of
-              resources expressed in λδ.<br>
-              <ul>
-                <li><span style="font-weight: bold;">Contents:</span>
-                  Landau's "<span style="font-style: italic;">Grundlagen
-                    der Analysis</span>" (from
-                  Jutting's specification in <a href="http://www.win.tue.nl/automath/">Automath</a>).<br>
-                  <span style="font-weight: bold;"></span></li>
-              </ul>
-              <ul>
-                <li><span style="font-weight: bold;">Access:</span> <a
-href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span style="font-weight: bold;">2012-10</span>), <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span style="font-weight: bold;">2012-10</span>), <a href="http://lambdadelta.info/xml/">HELM server URL</a>
-                  (updated <span style="font-weight: bold;">2012-10</span>).</li>
-              </ul>
-              <ul>
-                <li><span style="font-weight: bold;">Examples:</span> <a href="http://lambdadelta.info/static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
-                    definition
-                    "t234"</a> (in "basic_rg" λδ), <a href="http://lambdadelta.info/static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
-                    definition
-                    "t234"</a> (in "complete_rg" λδ).<br>
-                </li>
-              </ul>
-              <br>
-              <a name="helena"></a><span style="font-weight: bold;"><img style="width: 32px; height: 32px;" alt="[Helena Logo]" title="Helena" src="images/helena_32.png"> <span style="text-decoration: underline;">Helena</span></span>
-              is a λδ
-              processor,
-              implemented in <a href="http://caml.inria.fr/">Caml</a>
-              as a part of
-              the <a href="http://helm.cs.unibo.it/">HELM</a> software,
-              meant for
-              testing the stable features of the calculus as well as the
-              unstable
-              ones.<br>
-              The processor source code is available in the directory <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2Ftrunk%2Fhelm%2Fsoftware%2Fhelena%2F&amp;rev=0&amp;sc=0">/trunk/helm/software/helena/</a>
-              of the <a href="http://helm.cs.unibo.it/software/index.html">HELM
-                Svn
-                repository</a>. The Svn revisions containing the stable
-              versions
-              of&nbsp; Helena are indicated below. <br>
-              <ul>
-                <li><span style="font-weight: bold;">Version 0.8.2.</span>
-                  In
-                  progress.<br>
-                </li>
-              </ul>
-              <ul>
-                <li><span style="font-weight: bold;">Version 0.8.1
-                    (2010-11).</span>
-                  Exploits a subset of "complete_rg" λδ as the
-                  intermediate language.
-                  Features importation from ".hln" files containing λδ
-                  textual syntax.
-                  The overall validation speed of the "<span style="font-style: italic;">Grundlagen
-                    der
-                    Analysis</span>" 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><span style="font-weight: bold;">2009-12.</span>
-                      Helena
-                      appears in&nbsp;F. Wiedijk's <a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">index
-of
-computer
-                        math systems</a>.</li>
-                  </ul>
-                </li>
-              </ul>
-              <ul>
-                <li><a style="font-weight: bold;" href="documentation.html#ldp6">Version 0.8.0</a><span style="font-weight: bold;"> (2009-09).</span>
-                  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>.
-                  [Svn
-                  revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived
-                    source code</a>)<br>
-                  <ul>
-                    <li><span style="font-weight: bold;">2009-09.</span>
-                      Jutting's specification of Landau's "<span style="font-style: italic;">Grundlagen
-                        der
-                        Analysis</span>" enters λδ Digital Library.<br>
-                      <span style="font-weight: bold;"></span></li>
-                    <li><span style="font-weight: bold;">2009-06.</span>
-                      Jutting's specification of Landau's "<span style="font-style: italic;">Grundlagen
-                        der
-                        Analysis</span>" is
-                      successfully processed, enabling sort inclusion<span style="font-weight: bold;"></span>.</li>
-                  </ul>
-                </li>
-              </ul>
-              <h3 style="text-align: right;">Other resources <img style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" src="images/b4.png"></h3>
-              <ul>
-                <li><a name="bibtex"></a>A
-                  BibTeX database of λδ documentation: <a href="http://lambdadelta.info/download/lambdadelta.bib"><span style="font-style: italic;">lambdadelta.bib</span></a>,
-                  <a style="font-style: italic;" href="http://lambdadelta.info/download/lambdadelta.txt">lambdadelta.txt</a>
-                  (revised <span style="font-weight: bold;">2012-10</span>).</li>
-              </ul>
-              <ul>
-                <li>A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
-                  for
-                  editing ".hln" files (containing λδ textual syntax): <a style="font-style: italic;" href="http://lambdadelta.info/download/helena.sl">helena.sl</a>
-                  (revised <span style="font-weight: bold;">2010-11</span>).</li>
-              </ul>
-              <ul>
-                <li>A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
-                  for
-                  editing ".aut" files (containing <a href="http://www.win.tue.nl/automath/">Automath</a>
-                  textual syntax): <a style="font-style: italic;" href="http://lambdadelta.info/download/automath.sl">automath.sl</a>
-                  (revised <span style="font-weight: bold;">2008-07</span>).</li>
-              </ul>
-              <ul>
-                <li>A logo for λδ: <a href="images/crux_177.png"><span style="font-style: italic;">crux_177.png</span></a>
-                  (revised <span style="font-weight: bold;">2012-09</span>).<br>
-                </li>
-              </ul>
+            <td class="snns component gray">version</td>
+            <td class="snnn component gray">name</td>
+            <td class="snnn component gray">developed with</td>
+            <td class="snnn component gray">started</td>
+            <td class="snnn component gray">announced</td>
+            <td class="snnn component gray">released</td>
+            <td class="ssnn component gray">dismissed</td>
+          </tr>
+          <tr>
+            <td class="snns orange">2</td>
+            <td class="snnn orange">
+              <a href="http://lambdadelta.info/version_2.html">basic_2</a>
+            </td>
+            <td class="snnn orange">
+              <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
+            </td>
+            <td class="snnn orange">April 2011</td>
+            <td class="snnn orange">July 2014</td>
+            <td class="snnn orange">Planned in 2014</td>
+            <td class="ssnn orange">Not planned yet</td>
+          </tr>
+          <tr>
+            <td class="snss red">1</td>
+            <td class="snsn red">
+              <a href="http://lambdadelta.info/version_1.html">basic_1</a>
+            </td>
+            <td class="snsn red">
+              <a href="http://coq.inria.fr/">Coq 7.3.1</a>
             </td>
+            <td class="snsn red">May 2004</td>
+            <td class="snsn red">January 2006</td>
+            <td class="snsn red">November 2006</td>
+            <td class="sssn red">May 2008</td>
           </tr>
         </tbody>
       </table>
-      <br>
-      <a href="http://validator.w3.org/check?uri=referer"><img alt="[Valid HTML 4.01 Transitional]" title="Valid HTML 4.01
-          Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"></a> <a href="http://www.anybrowser.org/campaign/"><img alt="[Use Any
-          Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"></a> <img style="width: 88px; height: 31px;" alt="[PNG Used Here]" title="PNG Used Here" src="images/PNGnow2.png"><br>
-      <br>
-      Last update 2014-02-22 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
-        Guidi</a><br>
     </div>
-  
-</body></html>
+
+   <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">
+      <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>
+      and contains resources expressed in λδ.      
+   </div>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">Contents:</span>
+      Landau's "Grundlagen der Analysis"
+      (from Jutting's specification in  <a href="http://www.win.tue.nl/automath/">Automath</a>).
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">Access:</span>
+      <a href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span class="date">2012-10</span>),
+      <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span class="date">2012-10</span>),
+      <a href="http://lambdadelta.info/xml/">HELM server URL</a> (updated <span class="date">2012-10</span>).
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">Examples:</span>
+      <a href="http://lambdadelta.info/static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+         Grundlagen's definition "t234"</a>
+      (in "basic_rg" λδ),
+      <a href="http://lambdadelta.info/static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+         Grundlagen's definition "t234"</a>
+      (in "complete_rg" λδ).
+   </li>
+    </ul>
+
+   <div xmlns:ld="http://lambdadelta.info/" class="head2sn" 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,
+      implemented in <a href="http://caml.inria.fr/">Caml</a>
+      as a part of the <a href="http://helm.cs.unibo.it/">HELM</a> software,
+      meant for testing the stable features of the calculus as well as the unstable ones.
+   </div>
+   <div xmlns:ld="http://lambdadelta.info/" class="text">
+      The processor source code is available in the directory
+      <a href="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2Ftrunk%2Fhelm%2Fsoftware%2Fhelena%2F&amp;rev=0&amp;sc=0">/trunk/helm/software/helena/</a>
+      of the <a href="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</a>.
+      The Svn revisions containing the stable versions of Helena are indicated next.
+   </div>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">Version 0.8.2.</span>
+      In progress.
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">Version 0.8.1 (2010-11).</span>
+      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.
+      [Svn revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>)
+      <ul>
+          <li>
+         A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
+         for editing ".hln" files (containing λδ textual syntax):
+         <a href="http://lambdadelta.info/download/helena.sl">helena.sl</a>
+         (revised <span class="date">2010-11</span>).
+      </li>
+          <li>
+         <span class="date">2009-12.</span>
+         Helena appears in F. Wiedijk's
+         <a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
+            index of computer math systems</a>.
+      </li>
+        </ul>
+   </li>
+    </ul>
+   <ul xmlns:ld="http://lambdadelta.info/">
+      <li>
+        <span class="date">Version 0.8.0 (2009-09).</span>
+      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>.
+      [Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
+      <ul>
+          <li>
+         A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
+         for editing ".aut" files
+         (containing <a href="http://www.win.tue.nl/automath/">Automath</a> textual syntax):
+         <a href="http://lambdadelta.info/download/automath.sl">automath.sl</a>
+         (revised <span class="date">2008-07</span>).
+      </li>
+          <li>
+         <span class="date">2009-09.</span>
+         Jutting's specification of Landau's "Grundlagen der Analysis"
+         enters λδ Digital Library.
+      </li>
+          <li>
+         <span class="date">2009-06.</span>
+         Jutting's specification of Landau's "Grundlagen der Analysis"
+         is successfully processed, enabling sort inclusion.
+      </li>
+        </ul>
+   </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: Sun, 20 Jul 2014 15:02:32 +0200</div>
+</body>
+</html>

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index e6e6a2434b6ee71eaaedc5aefb83d1c3363b62d9..3f33aa0575948bd717443af1a232cb42ac608be5 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -42,9 +42,9 @@
             <td class="snns component green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn component green">
-              <br />
-            </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">
@@ -100,51 +100,6 @@
       as a machine-checked digital specification
       that is not the formal counterpart of some previously published informal material.
    </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 component gray">version</td>
-            <td class="snnn component gray">name</td>
-            <td class="snnn component gray">developed with</td>
-            <td class="snnn component gray">started</td>
-            <td class="snnn component gray">announced</td>
-            <td class="snnn component gray">released</td>
-            <td class="ssnn component gray">dismissed</td>
-          </tr>
-          <tr>
-            <td class="snns orange">2</td>
-            <td class="snnn orange">
-              <a href="http://lambdadelta.info/version_2.html">basic_2</a>
-            </td>
-            <td class="snnn orange">
-              <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
-            </td>
-            <td class="snnn orange">April 2011</td>
-            <td class="snnn orange">July 2014</td>
-            <td class="snnn orange">Planned in 2014</td>
-            <td class="ssnn orange">Not planned yet</td>
-          </tr>
-          <tr>
-            <td class="snss red">1</td>
-            <td class="snsn red">
-              <a href="http://lambdadelta.info/version_1.html">basic_1</a>
-            </td>
-            <td class="snsn red">
-              <a href="http://coq.inria.fr/">Coq 7.3.1</a>
-            </td>
-            <td class="snsn red">May 2004</td>
-            <td class="snsn red">January 2006</td>
-            <td class="snsn red">November 2006</td>
-            <td class="sssn red">May 2008</td>
-          </tr>
-        </tbody>
-      </table>
-    </div>
    <div xmlns:ld="http://lambdadelta.info/" class="text">
       This is the System logo: <a href="http://lambdadelta.info/images/crux_177.png">crux_177.png</a>
       (revised <span class="date">2012-09</span>).
@@ -186,6 +141,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 11:29:55 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index f526a75a9b98c2190a52a0000630ef62327f24b1..54a3d4af6fd282ff74b973e2ffee661984238d3d 100644 (file)
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -42,9 +42,9 @@
             <td class="snns component green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn component green">
-              <br />
-            </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">
@@ -286,6 +286,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 11:29:55 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html
index 856c396a83c4351315674702472ed99ed469a85f..1549b10d654b9e91f806c10cebc75930801fda9f 100644 (file)
--- a/helm/www/lambdadelta/version_1.html
+++ b/helm/www/lambdadelta/version_1.html
@@ -42,9 +42,9 @@
             <td class="snns component green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn component green">
-              <br />
-            </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">
@@ -169,6 +169,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 11:29:55 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html
index 530f2ad47513fbda1a1d7bfb4e4a04f056236387..bbbf58ff76fb4bca410cdeaaeeed394208131479 100644 (file)
--- a/helm/www/lambdadelta/version_2.html
+++ b/helm/www/lambdadelta/version_2.html
@@ -42,9 +42,9 @@
             <td class="snns component green">
               <a href="http://lambdadelta.info/implementation.html">implementation</a>
             </td>
-            <td class="ssnn component green">
-              <br />
-            </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">
@@ -134,6 +134,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 11:29:55 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 20 Jul 2014 15:02:32 +0200</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml
new file mode 100644 (file)
index 0000000..b8cc305
--- /dev/null
+++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml
@@ -0,0 +1,99 @@
+<?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"/>
+
+   <section9 name="specifications">Computer-checked formal specifications</section9>
+   <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>
+   <body>
+      The λδ Digital Library is part of <link to="http://helm.cs.unibo.it/">HELM</link>
+      and contains resources expressed in λδ.      
+   </body>
+   <news date="Contents:">
+      Landau's "Grundlagen der Analysis"
+      (from Jutting's specification in  <link to="http://www.win.tue.nl/automath/">Automath</link>).
+   </news>
+   <news date="Access:">
+      <rlink to="static/lddl/">static pages</rlink> (updated <date date="2012-10"/>),
+      <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <date date="2012-10"/>),
+      <rlink to="xml/">HELM server URL</rlink> (updated <date date="2012-10"/>).
+   </news>
+   <news date="Examples:">
+      <rlink to="static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+         Grundlagen's definition "t234"</rlink>
+      (in "basic_rg" λδ),
+      <rlink to="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">
+         Grundlagen's definition "t234"</rlink>
+      (in "complete_rg" λδ).
+   </news>
+
+   <section name="helena"><helena-icon/>Helena</section>
+   <body>
+      Helena is a λδ processor,
+      implemented in <link to="http://caml.inria.fr/">Caml</link>
+      as a part of the <link to="http://helm.cs.unibo.it/">HELM</link> software,
+      meant for testing the stable features of the calculus as well as the unstable ones.
+   </body>
+   <body>
+      The processor source code is available in the directory
+      <link to="http://helm.cs.unibo.it/websvn/listing.php?repname=helm&amp;path=%2Ftrunk%2Fhelm%2Fsoftware%2Fhelena%2F&amp;rev=0&amp;sc=0">/trunk/helm/software/helena/</link>
+      of the <link to="http://helm.cs.unibo.it/software/index.html">HELM Svn repository</link>.
+      The Svn revisions containing the stable versions of Helena are indicated next.
+   </body>
+   <news date="Version 0.8.2.">
+      In progress.
+   </news>
+   <news date="Version 0.8.1 (2010-11).">
+      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.
+      [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>
+         for editing ".hln" files (containing λδ textual syntax):
+         <rlink to="download/helena.sl">helena.sl</rlink>
+         (revised <date date="2010-11"/>).
+      </item><item>
+         <date date="2009-12."/>
+         Helena appears in F. Wiedijk's
+         <link to="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
+            index of computer math systems</link>.
+      </item></list>
+   </news>
+   <news date="Version 0.8.0 (2009-09).">
+      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>.
+      [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>
+         for editing ".aut" files
+         (containing <link to="http://www.win.tue.nl/automath/">Automath</link> textual syntax):
+         <rlink to="download/automath.sl">automath.sl</rlink>
+         (revised <date date="2008-07"/>).
+      </item><item>
+         <date date="2009-09."/>
+         Jutting's specification of Landau's "Grundlagen der Analysis"
+         enters λδ Digital Library.
+      </item><item>
+         <date date="2009-06."/>
+         Jutting's specification of Landau's "Grundlagen der Analysis"
+         is successfully processed, enabling sort inclusion.
+      </item></list>
+   </news>
+   <footer/>
+</page>

diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml
index 1b6c27c19c6d44c52a36c9f4a9df1f3c2c69927d..677e33bd9b833604b59a3cf38b1f8a795e821280 100644 (file)
--- a/helm/www/lambdadelta/web/home/index.ldw.xml
+++ b/helm/www/lambdadelta/web/home/index.ldw.xml
@@ -20,11 +20,6 @@
       as a machine-checked digital specification
       that is not the formal counterpart of some previously published informal material.
    </body>
-   <body>
-      λδ comes in several versions listed in the following table,
-      which includes the major milestones:
-   </body>
-   <table name="versions"/>
    <body>
       This is the System logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
       (revised <date date="2012-09"/>).

diff --git a/helm/www/lambdadelta/web/home/sitemap.tbl b/helm/www/lambdadelta/web/home/sitemap.tbl
index 71cc44367402ad993900f3037ea1104a4e9c212b..9ee265a89f9ca0ba21206ca9c1cbe6d4885d2950 100644 (file)
--- a/helm/www/lambdadelta/web/home/sitemap.tbl
+++ b/helm/www/lambdadelta/web/home/sitemap.tbl
@@ -17,9 +17,14 @@ table [
       [ @@("documentation#v1" "Version 1") * ]
    }
    class "green" {
-      [ @@"implementation" * ]
+      [ @@"implementation" 
+        "(" ^ @@("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/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl
index 2eef8f14933c64a9b3356b755f66755224133932..d0024b8dc14ef6fce865aa3cbb9eac4528177888 100644 (file)
--- a/helm/www/lambdadelta/xslt/ld_web_root.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl
@@ -120,13 +120,31 @@
 
 <xsl:template match="ld:basic-icon">
    <img class="icon32"
-       alt="[basic lambdadelta]"
+       alt="[basic lambdadelta logo]"
        title="basic lambdadelta"
        src="{$baseurl}images/basic_32.png"
    />
    <xsl:call-template name="sp"/>
 </xsl:template>
 
+<xsl:template match="ld:crux-icon">
+   <img class="icon32"
+       alt="[Crux logo]"
+       title="the Crux"
+       src="{$baseurl}images/crux_32.png"
+   />
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
+<xsl:template match="ld:helena-icon">
+   <img class="icon32"
+       alt="[Helena logo]"
+       title="Helena"
+       src="{$baseurl}images/helena_32.png"
+   />
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
 <xsl:template match="ld:footer">
    <xsl:call-template name="rule"/>
    <div class="spacer"><br/></div>