X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambdadelta%2Fimplementation.html;h=f0e1d32ffe2616bfbb3397061e2a04bae253f26f;hb=e36a0eced135e6f1b79d06c78a408918f65376b6;hp=82dcacfd5db933f2ca7bbc10168ec928ea5d6ca2;hpb=e90313fa853ba63f29416c2d0de40b13c913e567;p=helm.git
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 82dcacfd5..f0e1d32ff 100644
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -149,24 +149,38 @@
-
- Version 0.8.2 (2014-12).
+ 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 Coq),
+ and to Grafite
(the specification language of Matita).
The overall validation speed of the "Grundlagen der Analysis"
increases of 34% with respect to version 0.8.1.
- [Svn revision: 13005] (archived source code)
+ Documentation (J4).
+ [Svn revision: 13035] (archived source code).
-
The specification of Landau's "Grundlagen der Analysis"
+ for Coq 8:
+ grundlagen_2.v
+ (revised 2015-02).
+
+ -
+ The specification of Landau's "Grundlagen der Analysis"
for Matita 0.99.2:
grundlagen_2.tar.bz2
- (revised 2014-12).
+ (revised 2015-02).
-
The corrected specification of Landau's "Grundlagen der Analysis":
grundlagen_2.aut
(revised 2014-12).
+
+ -
+ 2015-02.
+ The translated specification of Landau's "Grundlagen der Analysis"
+ is successfully validated in λC by Coq 8.4.3.
-
2014-12.
@@ -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] (archived source code)
+ [Svn revision: 11032] (archived source code).
-
A Jed mode
@@ -255,6 +269,6 @@
- Last update: Wed, 21 Jan 2015 17:13:08 +0100
+ Last update: Sat, 21 Feb 2015 23:38:38 +0100