lddl update with the disambiguated "grundlagen"

[helm.git] / helm / www / lambdadelta / web / home / implementation.ldw.xml

diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml
index 48ff2c594966c98553b5b4c4493630fa35bd25ca..8e27e166b780f17a4fa1ee1e755f05b190012a05 100644 (file)
--- a/helm/www/lambdadelta/web/home/implementation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml
@@ -22,8 +22,8 @@
    <topitem name="access">
       <notice class="alpha" notice="Access:"/>
       <rlink to="static/lddl/">static pages</rlink> (updated <notice class="beta" notice="2012-10"/>),
-      <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="beta" notice="2012-10"/>),
-      <rlink to="xml/">HELM server URL</rlink> (updated <notice class="beta" notice="2012-10"/>).
+      <rlink to="download/lddl.tar.bz2">data set</rlink> (updated <notice class="beta" notice="2014-12"/>),
+      <rlink to="xml/">HELM server URL</rlink> (updated <notice class="beta" notice="2014-12"/>).
    </topitem>
    <topitem name="examples">
       <notice class="alpha" notice="Examples:"/>
@@ -51,10 +51,15 @@
    <topitem name="v2">
       <notice class="beta" notice="Version 0.8.2."/>
       In progress.
+      <list><item>
+         <notice class="gamma" notice="2014-12."/>
+         The corrected specification of Landau's "Grundlagen der Analysis"
+         is successfully validated in λδ "Version 3".
+      </item></list>
    </topitem>
    <topitem name="v1">
       <notice class="beta" notice="Version 0.8.1 (2010-11)."/>
-      Exploits a subset of "complete_rg" λδ as the intermediate language.
+      Uses a subset of λδ "Version 4" 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 to version 0.8.0.
@@ -73,7 +78,7 @@
    </topitem>
    <topitem name="v0">
       <notice class="beta" notice="Version 0.8.0 (2009-09)."/>
-      Supports "basic_rg" λδ with naive implementation of impredicative sort inclusion.
+      Supports λδ "Version 2" 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#ldR4">Documentation (R4)</rlink>.