X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fimplementation.html;h=79f013900e7b10c901c0a498e7589377a219d986;hb=77c6a180035cd63f3edd4db54bd7e9b411f9e85e;hp=12458806e6ed391ace7df458b53bad75a2e5f372;hpb=75e8188b0ce9aa9bd54ef004e2709f29078820f3;p=helm.git
diff --git a/helm/www/lambda_delta/implementation.html b/helm/www/lambda_delta/implementation.html
index 12458806e..79f013900 100644
--- a/helm/www/lambda_delta/implementation.html
+++ b/helm/www/lambda_delta/implementation.html
@@ -59,8 +59,8 @@ paper (as it happens for most currently digitalized Mathematics).
F. Guidi: lambda_delta
(revised 2011-09). Formal
-specification with the proof assistant Matita 0.5 (HTML pages generated
+specification for Matita 0.5
+(HTML pages generated
by the HELM
rendering engine)
Here are the most relevant theorems proved in the formal specification:
@@ -110,17 +110,15 @@ problem.
style="font-style: italic;"
href="http://mowgli.cs.unibo.it:58080/apply?keys=RT&xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&prop.media-type=text/html¶m.thmedia-type=text/html¶m.thkeys=T1%2CT2%2CL%2CE¶m.embedkeys=d_c%2CTC1%2CHC2%2CL¶m.thencoding=UTF-8&prop.encoding=UTF-8&prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN¶m.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN¶m.encoding=UTF-8¶m.media-type=text/html¶m.keys=d_c%2CC1%2CHC2%2CL&profile=default¶m.profile=default¶m.CICURI=theory:/matita/lambda_delta/">lambda_delta
(revised 2011-09). Formal
-specification with the proof assistant Matita 0.5 (Matita 0.5 (HELM directory).
F. Guidi: lambda_delta_1 (revised 2011-09).
-Formal specification with the proof assistant Coq 7.3.1 (source
+ href="download/lambda_delta_1.tar.gz">lambda_delta_1
+(revised 2011-09).
+Formal specification for Coq 7.3.1
+(source
proof scripts). BibTeX entry.
@@ -176,6 +174,13 @@ The processor source code is available in the directory HELM Svn
repository. The Svn revisions containing the stable versions
of Helena are indicated below.
+
+
+ - Version 0.8.2. In
+progress.
+
+
- Version 0.8.1 (2010-11).
Exploits a subset of "complete_rg" λδ as the intermediate language.
@@ -188,7 +193,8 @@ source code)
@@ -227,6 +233,7 @@ BibTeX database of λδ documentation: lambda_delta.bib,
+
lambda_delta.txt (revised 2011-09).
@@ -265,10 +272,9 @@ editing ".aut" files (containing ![PNG Used Here [PNG Used Here]](download/PNGnow2.png)
+ title="PNG Used Here" src="download/PNGnow2.png">
-Last update 2011-09-09 by Ferruccio
+Last update 2012-02-21 by Ferruccio
Guidi