From: Ferruccio Guidi Date: Sun, 5 Oct 2014 14:45:02 +0000 (+0000) Subject: contrib update ... X-Git-Tag: make_still_working~824 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9b75ad80a3ee31314c02f113b255ad533a87d3d2;p=helm.git contrib update ... --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index e2a0831ee..6da2d08fc 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Sat, 04 Oct 2014 22:58:58 +0200
+
Last update: Sun, 05 Oct 2014 16:38:32 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index b4acc1f91..0e502b7f9 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Sat, 04 Oct 2014 22:58:58 +0200
+
Last update: Sun, 05 Oct 2014 16:38:32 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index b2fec9511..b0891996f 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -60,9 +60,9 @@ files 358 characters - 430798 + 430633 nodes - 1858367 + 1858385 propositions @@ -317,7 +317,7 @@ equivalence - decomposed extended equivalence + decomposed rt-equivalence scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? ) scpes_aaa scpes_cpcs scpes_scpes @@ -355,7 +355,7 @@ computation - evaluation for context-sensitive extended reduction + evaluation for context-sensitive rt-reduction cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )
@@ -397,7 +397,7 @@
- strongly normalizing extended computation + strongly normalizing rt-computation lcosx ( ? ⊢ ~⬊*[?,?,?] ? ) lcosx_cpx @@ -483,7 +483,7 @@
- decomposed extended computation + decomposed rt-computation scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? ) scpds_lift scpds_aaa scpds_scpds @@ -497,7 +497,7 @@
- context-sensitive extended computation + context-sensitive rt-computation lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? ) lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs @@ -609,7 +609,7 @@
- normal forms for context-sensitive extended reduction + normal forms for context-sensitive rt-reduction cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ ) cnx_lift cnx_crx cnx_cix @@ -623,7 +623,7 @@
- context-sensitive extended reduction + context-sensitive rt-reduction lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? ) lpx_drop lpx_frees lpx_lleq lpx_aaa @@ -653,7 +653,7 @@
- irreducible forms for context-sensitive extended reduction + irreducible forms for context-sensitive rt-reduction cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ ) cix_lift @@ -667,7 +667,7 @@
- reducible forms for context-sensitive extended reduction + reducible forms for context-sensitive rt-reduction crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ ) crx_lift @@ -933,7 +933,7 @@
- contxt-sensitive extended multiple substitution + contxt-sensitive multiple rt-substitution cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? ) cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? ) cpys_lift cpys_cpys @@ -1073,7 +1073,7 @@
- contxt-sensitive extended ordinary substitution + contxt-sensitive ordinary rt-substitution cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? ) cpy_lift cpy_nlift cpy_cpy @@ -1087,7 +1087,7 @@
- local env. ref. for extended substitution + local env. ref. for rt-substitution lsuby ( ? ⊆[?,?] ? ) lsuby_lsuby @@ -1303,6 +1303,6 @@

-
Last update: Sat, 04 Oct 2014 22:58:58 +0200
+
Last update: Sun, 05 Oct 2014 16:38:32 +0200
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 060534f39..d07a8b977 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -161,7 +161,7 @@ V2. - F. Guidi: lambdadelta_2 (revised 2014-09). Formal specification for the proof assistant Matita 0.99.2 (scripts). BibTeX entry. + F. Guidi: lambdadelta_2 (revised 2014-10). Formal specification for the proof assistant Matita 0.99.2 (scripts). BibTeX entry. @@ -333,6 +333,6 @@

-
Last update: Sat, 04 Oct 2014 22:58:58 +0200
+
Last update: Sun, 05 Oct 2014 16:38:32 +0200
diff --git a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz index e558c8d52..74759de60 100644 Binary files a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz and b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz differ diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 62ea59dd5..87ad0d3c2 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -234,6 +234,6 @@

-
Last update: Sat, 04 Oct 2014 22:58:58 +0200
+
Last update: Sun, 05 Oct 2014 16:38:32 +0200
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 590ea923f..e0f5b7aab 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -266,6 +266,6 @@

-
Last update: Sat, 04 Oct 2014 22:58:58 +0200
+
Last update: Sun, 05 Oct 2014 16:38:32 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 5010596da..190bf2ebb 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -135,6 +135,6 @@

-
Last update: Sat, 04 Oct 2014 22:58:58 +0200
+
Last update: Sun, 05 Oct 2014 16:38:32 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index d6c2de260..1110d7569 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -303,6 +303,6 @@

-
Last update: Sat, 04 Oct 2014 22:58:58 +0200
+
Last update: Sun, 05 Oct 2014 16:38:31 +0200
diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html index c50f44b4f..b28827183 100644 --- a/helm/www/lambdadelta/version_1.html +++ b/helm/www/lambdadelta/version_1.html @@ -167,6 +167,6 @@

-
Last update: Sat, 04 Oct 2014 22:58:58 +0200
+
Last update: Sun, 05 Oct 2014 16:38:32 +0200
diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html index eeacec00c..925508051 100644 --- a/helm/www/lambdadelta/version_2.html +++ b/helm/www/lambdadelta/version_2.html @@ -91,7 +91,7 @@ @@ -131,6 +131,6 @@

-
Last update: Sat, 04 Oct 2014 22:58:58 +0200
+
Last update: Sun, 05 Oct 2014 16:38:32 +0200
diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl index 3469f65f1..434ebbd64 100644 --- a/helm/www/lambdadelta/web/home/documentation_2.tbl +++ b/helm/www/lambdadelta/web/home/documentation_2.tbl @@ -47,7 +47,7 @@ table { [ { name "ldV2" "V2." "" } { "F. Guidi:" + @@("version_2.html" "lambdadelta_2") + - "(revised 2014-09)." + + "(revised 2014-10)." + "Formal specification for the proof assistant Matita 0.99.2 (scripts)." + @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } diff --git a/helm/www/lambdadelta/web/home/version_2.ldw.xml b/helm/www/lambdadelta/web/home/version_2.ldw.xml index 88abedf81..816bface5 100644 --- a/helm/www/lambdadelta/web/home/version_2.ldw.xml +++ b/helm/www/lambdadelta/web/home/version_2.ldw.xml @@ -16,7 +16,7 @@ lambdadelta_2 for Matita 0.99.2 - (revised ). + (revised ). Source scripts.