From: Ferruccio Guidi Date: Tue, 5 Aug 2014 21:15:00 +0000 (+0000) Subject: - update in basic_2 and ground_2 X-Git-Tag: make_still_working~862 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ddd6cb6f4514d9ca97f857cafa218c170222f5aa;p=helm.git - update in basic_2 and ground_2 - uodated web site --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 41f766285..19f42b340 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Sun, 20 Jul 2014 16:13:31 +0200
+
Last update: Tue, 05 Aug 2014 23:07:40 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 32d81ab2b..530529624 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Sun, 20 Jul 2014 16:13:31 +0200
+
Last update: Tue, 05 Aug 2014 23:07:40 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index c8959b5cd..7b6bf13cf 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -58,29 +58,29 @@ sizes files - 362 + 367 characters - 431129 + 431873 nodes - 1829245 + 1830977 propositions theorems - 123 + 128 lemmas - 1300 + 1302 total - 1423 + 1430 concepts declared - 54 + 55 defined - 84 + 82 total - 138 + 137 @@ -277,8 +277,24 @@
stratified native validity + hsnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] ) + hsnv_aaa + +
+ + +
+ + + + +
+ + +
+ snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] ) - snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_cpcs snv_preserve + snv_lift snv_aaa snv_da_lpr snv_lstas snv_lstas_lpr snv_lpr snv_cpes snv_preserve
@@ -289,8 +305,8 @@ equivalence decomposed extended equivalence - cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? ) - cpes_cpds + cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? ) + cpes_aaa cpes_cpcs cpes_cpes
@@ -485,7 +501,7 @@
decomposed extended computation - cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? ) + cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? ) cpds_lift cpds_aaa cpds_cpds
@@ -1300,6 +1316,6 @@

-
Last update: Sun, 20 Jul 2014 16:13:31 +0200
+
Last update: Tue, 05 Aug 2014 23:07:40 +0200
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 7a90b1ba5..bc53a2b27 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -161,7 +161,7 @@ V2. - F. Guidi: lambdadelta_2 (revised 2014-07). Formal specification for the proof assistant Matita 0.99.2 (scripts). BibTeX entry. + F. Guidi: lambdadelta_2 (revised 2014-08). Formal specification for the proof assistant Matita 0.99.2 (scripts). BibTeX entry. @@ -285,6 +285,18 @@ F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata (2005-12). Presentation at University of Bologna (slides in Italian). + + + +
+ + + + + V1. + + F. Guidi: lambdadelta_1 (revised 2012-10). Formal specification for the proof assistant Coq 7.3.1 (scripts). BibTeX entry. + @@ -321,6 +333,6 @@

-
Last update: Sun, 20 Jul 2014 16:55:23 +0200
+
Last update: Tue, 05 Aug 2014 23:07:40 +0200
diff --git a/helm/www/lambdadelta/download/lambdadelta_2.tar.gz b/helm/www/lambdadelta/download/lambdadelta_2.tar.gz index 6dc4aa81c..9c43092a4 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 9b08ac7df..b1d1dc18b 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -56,20 +56,20 @@ sizes files - 29 + 31 characters - 46886 + 46619 nodes - 61467 + 61911 propositions theorems 2 lemmas - 183 + 185 total - 185 + 187 concepts @@ -234,6 +234,6 @@

-
Last update: Sun, 20 Jul 2014 16:13:31 +0200
+
Last update: Tue, 05 Aug 2014 23:07:40 +0200
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index 71b5724c5..8eacf7930 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -263,6 +263,6 @@

-
Last update: Sun, 20 Jul 2014 16:55:23 +0200
+
Last update: Tue, 05 Aug 2014 23:07:40 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 289ed627e..9bd1b957e 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -135,6 +135,6 @@

-
Last update: Sun, 20 Jul 2014 16:55:23 +0200
+
Last update: Tue, 05 Aug 2014 23:07:40 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 0f5011f06..bd9bdabf7 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -303,6 +303,6 @@

-
Last update: Sun, 20 Jul 2014 16:55:23 +0200
+
Last update: Tue, 05 Aug 2014 23:07:40 +0200
diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html index e62b68ee9..4a107c7c4 100644 --- a/helm/www/lambdadelta/version_1.html +++ b/helm/www/lambdadelta/version_1.html @@ -167,6 +167,6 @@

-
Last update: Sun, 20 Jul 2014 16:13:31 +0200
+
Last update: Tue, 05 Aug 2014 23:07:40 +0200
diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html index 719331a08..63e5d7506 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: Sun, 20 Jul 2014 16:13:31 +0200
+
Last update: Tue, 05 Aug 2014 23:07:40 +0200
diff --git a/helm/www/lambdadelta/web/home/documentation_1.tbl b/helm/www/lambdadelta/web/home/documentation_1.tbl index 07114eec2..11b9ddb31 100644 --- a/helm/www/lambdadelta/web/home/documentation_1.tbl +++ b/helm/www/lambdadelta/web/home/documentation_1.tbl @@ -86,6 +86,14 @@ table { "in Italian)." * } ] + [ { name "ldV1" "V1." "" } { + "F. Guidi:" + + @@("version_1.html" "lambdadelta_1") + + "(revised 2012-10)." + + "Formal specification for the proof assistant Coq 7.3.1 (scripts)." + + @@("documentation.html#bibtex" "BibTeX entry") ^ "." + * } + ] } class "top" [ * ] diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl index 9a50d94d2..3a4131812 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-07)." + + "(revised 2014-08)." + "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 9c002c7c9..b760295a3 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.