From: Ferruccio Guidi Date: Tue, 8 Dec 2020 18:00:50 +0000 (+0100) Subject: λδ-2B and λδ-ground repackaged for publication X-Git-Tag: make_still_working~171 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3bc50da0628f7ff190c7d5ba7c3b96a7706eb823 λδ-2B and λδ-ground repackaged for publication + web site update --- diff --git a/helm/www/lambdadelta/Makefile b/helm/www/lambdadelta/Makefile index c654d6abf..063bdbe17 100644 --- a/helm/www/lambdadelta/Makefile +++ b/helm/www/lambdadelta/Makefile @@ -46,7 +46,6 @@ TABLES = $(XSLTDIR)/xhtbl.xsl SLS = helena.sl automath.sl BIB = lambdadelta.bib -CONTRIB = lambdadelta_2.tar.gz XMLS = Environment/grundlagen_2/l/not.ld.xml \ Environment/grundlagen_2/l/et.ld.xml \ diff --git a/helm/www/lambdadelta/download/lambdadelta_2B.tar.bz2 b/helm/www/lambdadelta/download/lambdadelta_2B.tar.bz2 index 25d8b9150..62023c1b5 100644 Binary files a/helm/www/lambdadelta/download/lambdadelta_2B.tar.bz2 and b/helm/www/lambdadelta/download/lambdadelta_2B.tar.bz2 differ diff --git a/helm/www/lambdadelta/download/lambdadelta_ground.tar.bz2 b/helm/www/lambdadelta/download/lambdadelta_ground.tar.bz2 index 9aecee1bd..bdc1ebb35 100644 Binary files a/helm/www/lambdadelta/download/lambdadelta_ground.tar.bz2 and b/helm/www/lambdadelta/download/lambdadelta_ground.tar.bz2 differ diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml index c52aa3931..35b3a1ca7 100644 --- a/helm/www/lambdadelta/web/home/documentation.ldw.xml +++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml @@ -11,9 +11,9 @@ Documentation BibTeX database of λδ documentation: - + lambdadelta.bib, - + lambdadelta.txt (revised ). diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml index 11b564b99..df3661e22 100644 --- a/helm/www/lambdadelta/web/home/home.ldw.xml +++ b/helm/www/lambdadelta/web/home/home.ldw.xml @@ -22,10 +22,17 @@ as a set of machine-checked digital specifications. - - λδ-2B for for Matita 0.99.4 - (released: ). - Documentation (J2a). + + + λδ-2B for for Matita 0.99.4 + (revised: ). + Documentation (J2a). + + + + lambdadelta_ground for Matita 0.99.2 + (revised ). + This is the family logo: crux_177.png @@ -55,13 +62,13 @@ M. Weber: An extended type system with lambda-typed lambda-expressions - (2018). Technical report. Faculty of Computer Science, Technical University of Berlin. + (2020). To appear in Logical Methods in Computer Science. M. Weber: An extended type system with lambda-typed lambda-expressions (extended version) - (2018). Technical report. Faculty of Computer Science, Technical University of Berlin. + (2020). Technical report. Faculty of Computer Science, Technical University of Berlin. diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml index 050a17328..98dd5f11f 100644 --- a/helm/www/lambdadelta/web/home/specification.ldw.xml +++ b/helm/www/lambdadelta/web/home/specification.ldw.xml @@ -76,10 +76,13 @@ lambdadelta_2B for Matita 0.99.4 - (revised ). + (revised ). Source scripts. Documentation (J2a). + + repackaged for publication. + repackaged without λδ-ground_2. @@ -129,9 +132,12 @@ lambdadelta_ground for Matita 0.99.2 - (revised ). + (revised ). Source scripts. + + repackaged for publication. + released [Git revision: 2020-02-27 22:45:50]. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index e4b19cdd8..c45570244 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -26,6 +26,9 @@ + + λδ-2B is repackaged for publication. + Improved theory of rst-transition. diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground.ldw.xml b/matita/matita/contribs/lambdadelta/ground/web/ground.ldw.xml index 30139a607..79e15a541 100644 --- a/matita/matita/contribs/lambdadelta/ground/web/ground.ldw.xml +++ b/matita/matita/contribs/lambdadelta/ground/web/ground.ldw.xml @@ -14,31 +14,34 @@
- + + Specification is repackaged for publication. + + Specification is released as an independent package (was ground_2). - + Centralized xoa infrastructure removed. - + Decentralized xoa infrastructure. - + Generic rt-transition counter (rtc). - + Platform-independent multiple relocation (rtmap). - + Multiple relocation with streams of naturals. - + Multiple relocation with lists of booleans. - + Natural numbers with infinity (ynat). - + Specification starts.