X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fimplementation.html;h=f0e1d32ffe2616bfbb3397061e2a04bae253f26f;hb=d1ab998b8c8dacdfceee97d6275955675cf8be83;hp=d9285e579bf23ff7d715dc657195eb0e362b001b;hpb=c6aece41fb3865f411bfe2a886b3b3cfb519031f;p=helm.git

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index d9285e579..f0e1d32ff 100644
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -149,24 +149,38 @@
    </div>
     <ul xmlns:ld="http://lambdadelta.info/" id="v2">
       <li>
-        <span class="emph gamma">Version 0.8.2 (2014-12).</span>
+        <span class="emph gamma">Version 0.8.2 (2015-02).</span>
       Uses λδ "Version 3" with layer variables as core language.
-      Supports exportation to Grafite
+      Supports exportation to Gallina
+      (the specification language of <a href="http://coq.inria.fr/">Coq</a>),
+      and to Grafite
       (the specification language of <a href="http://matita.cs.unibo.it/">Matita</a>).
       The overall validation speed of the "Grundlagen der Analysis"
       increases of 34% with respect to version 0.8.1.
-      [Svn revision: 13005] (<a href="http://lambdadelta.info/download/helena_0.8.2.tar.gz">archived source code</a>)
+      <a href="http://lambdadelta.info/documentation.html#ldJ4">Documentation (J4)</a>.
+      [Svn revision: 13035] (<a href="http://lambdadelta.info/download/helena_0.8.2.tar.gz">archived source code</a>).
       <ul>
           <li>
          The specification of Landau's "Grundlagen der Analysis"
+         for <a href="http://coq.inria.fr/">Coq 8</a>:
+         <a href="http://lambdadelta.info/download/grundlagen_2.v">grundlagen_2.v</a>
+         (revised <span class="emph gamma">2015-02</span>).
+      </li>
+          <li>
+         The specification of Landau's "Grundlagen der Analysis"
          for <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>:
          <a href="http://lambdadelta.info/download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</a>
-         (revised <span class="emph gamma">2014-12</span>).
+         (revised <span class="emph gamma">2015-02</span>).
       </li>
           <li>
          The corrected specification of Landau's "Grundlagen der Analysis":  
          <a href="http://lambdadelta.info/download/grundlagen_2.aut">grundlagen_2.aut</a>
          (revised <span class="emph gamma">2014-12</span>).
+      </li>
+          <li>
+            <span class="emph gamma">2015-02.</span>
+         The translated specification of Landau's "Grundlagen der Analysis"
+         is successfully validated in λC by <a href="http://coq.inria.fr/">Coq 8.4.3</a>.
       </li>
           <li>
             <span class="emph gamma">2014-12.</span>
@@ -183,7 +197,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] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>)
+      [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>
@@ -255,6 +269,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Feb 2015 19:13:36 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 21 Feb 2015 23:38:38 +0100</div>
   </body>
 </html>