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/?a=commitdiff_plain;h=3bc50da0628f7ff190c7d5ba7c3b96a7706eb823;p=helm.git
λδ-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.
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.