- update for helena 0.8.2 and related files

[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 1d2ffdc96863561cb284aaab40930cc0b8804880..9112a8037985ab0da12e3dc852c616d779995338 100644 (file)
--- a/helm/www/lambdadelta/web/home/implementation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml
@@ -46,22 +46,34 @@
       The Svn revisions containing the stable versions of Helena are indicated next.
    </body>
    <topitem name="v2">
-      <notice class="gamma" notice="Version 0.8.2 (2014-12)."/>
+      <notice class="gamma" notice="Version 0.8.2 (2015-02)."/>
       Uses λδ "Version 3" with layer variables as core language.
-      Supports exportation to Grafite
+      Supports exportation to Gallina
+      (the specification language of <link to="http://coq.inria.fr/">Coq</link>),
+      and to Grafite
       (the specification language of <link to="http://matita.cs.unibo.it/">Matita</link>).
       The overall validation speed of the "Grundlagen der Analysis"
       increases of 34% with respect to version 0.8.1.
-      [Svn revision: 13005] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>)
+      <rlink to="documentation.html#ldJ4">Documentation (J4)</rlink>.
+      [Svn revision: 13035] (<rlink to="download/helena_0.8.2.tar.gz">archived source code</rlink>).
       <list><item>
+         The specification of Landau's "Grundlagen der Analysis"
+         for <link to="http://coq.inria.fr/">Coq 8</link>:
+         <rlink to="download/grundlagen_2.v">grundlagen_2.v</rlink>
+         (revised <notice class="gamma" notice="2015-02"/>).
+      </item><item>
          The specification of Landau's "Grundlagen der Analysis"
          for <link to="http://matita.cs.unibo.it/">Matita 0.99.2</link>:
          <rlink to="download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</rlink>
-         (revised <notice class="gamma" notice="2014-12"/>).
+         (revised <notice class="gamma" notice="2015-02"/>).
       </item><item>
          The corrected specification of Landau's "Grundlagen der Analysis":  
          <rlink to="download/grundlagen_2.aut">grundlagen_2.aut</rlink>
          (revised <notice class="gamma" notice="2014-12"/>).
+      </item><item>
+         <notice class="gamma" notice="2015-02."/>
+         The translated specification of Landau's "Grundlagen der Analysis"
+         is successfully validated in λC by <link to="http://coq.inria.fr/">Coq 8.4.3</link>.
       </item><item>
          <notice class="gamma" notice="2014-12."/>
          The corrected specification of Landau's "Grundlagen der Analysis"
@@ -74,7 +86,7 @@
       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.
-      [Svn revision: 11032] (<rlink to="download/helena_0.8.1.tar.gz">archived source code</rlink>)
+      [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):