From: Ferruccio Guidi Date: Fri, 6 Mar 2015 15:25:02 +0000 (+0000) Subject: - new naming sheme for documentation yields more stable names X-Git-Tag: make_still_working~729 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c211eb61218aa9b43dfd2baae45407f0aa87ca79;p=helm.git - new naming sheme for documentation yields more stable names - update for document J2a --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 40ff9c8b5..b84be907c 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -222,6 +222,6 @@

-
Last update: Sat, 21 Feb 2015 23:38:39 +0100
+
Last update: Fri, 06 Mar 2015 16:17:54 +0100
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index e6ecc8d7c..f169633b0 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -258,6 +258,6 @@

-
Last update: Sat, 21 Feb 2015 23:38:38 +0100
+
Last update: Fri, 06 Mar 2015 16:17:54 +0100
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html index 739454623..87daf7e41 100644 --- a/helm/www/lambdadelta/basic_1.html +++ b/helm/www/lambdadelta/basic_1.html @@ -102,7 +102,7 @@ -
Abstract Syntax and Behavior [spacer] +
Abstract Syntax and Behavior [spacer]
This is a summary of available syntactic items and reductions (block structure).
@@ -823,6 +823,6 @@

-
Last update: Thu, 05 Mar 2015 16:42:28 +0100
+
Last update: Fri, 06 Mar 2015 16:17:54 +0100
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 76d0594a8..d41e116cf 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1384,6 +1384,6 @@

-
Last update: Sat, 21 Feb 2015 23:38:38 +0100
+
Last update: Fri, 06 Mar 2015 16:17:54 +0100
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html index 5f7506bd5..2b367888d 100644 --- a/helm/www/lambdadelta/documentation.html +++ b/helm/www/lambdadelta/documentation.html @@ -110,21 +110,21 @@ lambdadelta.bib, view lambdadelta.txt - (revised 2014-10). + (revised 2015-03).
[spacer] λδ version 3 (proposed)
- The main source of information is J4. + The main source of information is J3a.
- - +
- J4. + + J3a. F. Guidi: A Verified Translation of Landau's "Grundlagen" from Automath into a Pure Type System, via λδ (2015-02). Submitted to JFR, Univerity of Bologna.F. Guidi: A Verified Translation of Landau's "Grundlagen" from Automath into a Pure Type System, via λδ (2015-02). Submitted to JFR, Univerity of Bologna. BibTeX entry.
@@ -138,16 +138,16 @@
[spacer] λδ version 2 (active)
- The main source of information is J2. + The main source of information is J2a.
- - + - @@ -168,8 +168,8 @@ - @@ -180,8 +180,8 @@ - @@ -192,8 +192,8 @@ - @@ -204,8 +204,8 @@ - @@ -234,7 +234,7 @@ [spacer] λδ version 1 (superseded)
The main source of information is J1. - A summary is available in P5. + A summary is available in P1e.
- J2. + + J2a. F. Guidi: The Formal System λδ Revised - Stage A: Extending the Applicability Condition (2014-11). Submitted to ACM ToCL. CoRR identifier 1411.0154 [v1].F. Guidi: The Formal System λδ Revised, Stage A: Extending the Applicability Condition (2014-11). Submitted to ACM ToCL. CoRR identifier 1411.0154 [v2] (revised 2015-03). BibTeX entry.
@@ -156,8 +156,8 @@
- R5. + + R2b. F. Guidi: An Efficient Validation Procedure for the Formal System λδ (2010-07). In CiE 2010 Local Proceedings. University of Azores, CMATI Booklet, pp. 204-213. BibTeX entry.
- R4. + + R2a. F. Guidi: Landau's "Grundlagen der Analysis" from Automath to lambda-delta (2009-09). University of Bologna, technical report UBLCS-2009-16. BibTeX entry.
- P8. + + P2c. F. Guidi: The Formal System λδ and the "Three Problems" (2014-06). Presentation at University of Bologna (slides).
- P7. + + P2b. F. Guidi: An Efficient Validation Procedure for the Formal System λδ (2010-07). Presentation at CiE 2010 (slides).
- P6. + + P2a. F. Guidi: A Validator for the Formal System λδ (revised 2010-02). Presentation at University of Bologna (slides).
@@ -253,8 +253,8 @@ - @@ -265,8 +265,8 @@ - @@ -277,8 +277,8 @@ - @@ -289,8 +289,8 @@ - @@ -301,8 +301,8 @@ - @@ -313,8 +313,8 @@ - @@ -325,8 +325,8 @@ - @@ -337,8 +337,8 @@ - @@ -352,7 +352,7 @@ - +
- R3. + + R1c. F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). In CiE 2007 Local Proceedings. University of Siena, technical report 487, p. 387 (abstract of a presentation). BibTeX entry.
- R2. + + R1b. F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2006-11). University of Bologna, technical report UBLCS-2006-25. BibTeX entry.
- R1. + + R1a. F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification (2006-01). University of Bologna, technical report UBLCS-2006-01. BibTeX entry.
- P5. + + P1e. F. Guidi: The Formal System λδ (2008-10). Presentation at Advances in Constructive Topology and Logical Foundations (slides).
- P4. + + P1d. F. Guidi: Towards the Unification of Terms, Types and Contexts (2008-03). Presentation at Types 2008 (slides).
- P3. + + P1c. F. Guidi: Lambda Types on the Lambda Calculus with Abbreviations (2007-06). Presentation at CiE 2007 (slides).
- P2. + + P1b. F. Guidi: Lambda Tipi sul Lambda Calcolo con Abbreviazioni (2007-01). Presentation at University of Padova (slides in Italian).
- P1. + + P1a. 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.F. Guidi: lambdadelta_1 (revised 2015-01). Formal specification for the proof assistant Coq 7.3.1 (scripts). BibTeX entry.
@@ -389,6 +389,6 @@

-
Last update: Sat, 21 Feb 2015 23:38:38 +0100
+
Last update: Fri, 06 Mar 2015 16:17:54 +0100
diff --git a/helm/www/lambdadelta/download/basic2a.pdf b/helm/www/lambdadelta/download/basic2a.pdf index 74cbdc164..e47b376d9 100644 Binary files a/helm/www/lambdadelta/download/basic2a.pdf and b/helm/www/lambdadelta/download/basic2a.pdf differ diff --git a/helm/www/lambdadelta/download/lambdadelta.bib b/helm/www/lambdadelta/download/lambdadelta.bib index dce057e23..080080f38 100644 --- a/helm/www/lambdadelta/download/lambdadelta.bib +++ b/helm/www/lambdadelta/download/lambdadelta.bib @@ -1,6 +1,6 @@ % \lambda\delta version 3 (proposed) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -@misc{lambdadeltaJ4, +@misc{lambdadeltaJ3a, author="F. {Guidi}", title="{A Verified Translation of Landau's `Grundlagen'' from Automath into a Pure Type System, via $\lambda\delta$}", year="2015", @@ -10,9 +10,9 @@ % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -@misc{lambdadeltaJ2, +@misc{lambdadeltaJ2a, author="F. {Guidi}", - title="{The Formal System $\lambda\delta$ Revised - Stage A: Extending the Applicability Condition}", + title="{The Formal System $\lambda\delta$ Revised, Stage A: Extending the Applicability Condition}", howpublished="CoRR identifier 1411.0154", year="2014", month="November", @@ -28,7 +28,7 @@ note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$" } -@incollection{lambdadeltaR5, +@incollection{lambdadeltaR2b, author="F. {Guidi}", title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}", editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}", @@ -40,7 +40,7 @@ month="July" } -@techreport{lambdadeltaR4, +@techreport{lambdadeltaR2a, author="F. {Guidi}", title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", type="Technical Report", @@ -66,7 +66,7 @@ month="November" } -@incollection{lambdadeltaR3, +@incollection{lambdadeltaR1c, author="F. {Guidi}", title="{Lambda Types on the Lambda Calculus with Abbreviations}", editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}", @@ -78,7 +78,7 @@ month="June" } -@techreport{lambdadeltaR2, +@techreport{lambdadeltaR1b, author="F. {Guidi}", title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", type="Technical Report", @@ -89,7 +89,7 @@ month="November" } -@techreport{lambdadeltaR1, +@techreport{lambdadeltaR1a, author="F. {Guidi}", title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", type="Technical Report", diff --git a/helm/www/lambdadelta/download/lambdadelta.txt b/helm/www/lambdadelta/download/lambdadelta.txt index dce057e23..080080f38 100644 --- a/helm/www/lambdadelta/download/lambdadelta.txt +++ b/helm/www/lambdadelta/download/lambdadelta.txt @@ -1,6 +1,6 @@ % \lambda\delta version 3 (proposed) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -@misc{lambdadeltaJ4, +@misc{lambdadeltaJ3a, author="F. {Guidi}", title="{A Verified Translation of Landau's `Grundlagen'' from Automath into a Pure Type System, via $\lambda\delta$}", year="2015", @@ -10,9 +10,9 @@ % \lambda\delta version 2 (active) %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -@misc{lambdadeltaJ2, +@misc{lambdadeltaJ2a, author="F. {Guidi}", - title="{The Formal System $\lambda\delta$ Revised - Stage A: Extending the Applicability Condition}", + title="{The Formal System $\lambda\delta$ Revised, Stage A: Extending the Applicability Condition}", howpublished="CoRR identifier 1411.0154", year="2014", month="November", @@ -28,7 +28,7 @@ note="Available at the $\lambda\delta$ Web site: $<$http://lambdadelta.info/$>$" } -@incollection{lambdadeltaR5, +@incollection{lambdadeltaR2b, author="F. {Guidi}", title="{An Efficient Validation Procedure for the Formal System $\lambda\delta$}", editor="F. {Ferreira} and H. {Guerra} and E. {Mayordomo} and J. {Rasga}", @@ -40,7 +40,7 @@ month="July" } -@techreport{lambdadeltaR4, +@techreport{lambdadeltaR2a, author="F. {Guidi}", title="{Landau's ``Grundlagen der Analysis'' from Automath to lambda-delta}", type="Technical Report", @@ -66,7 +66,7 @@ month="November" } -@incollection{lambdadeltaR3, +@incollection{lambdadeltaR1c, author="F. {Guidi}", title="{Lambda Types on the Lambda Calculus with Abbreviations}", editor="S. {Barry Cooper} and T. F. {Kent} and B. {L\"owe} and A. {Sorbi}", @comment="{\"}", @@ -78,7 +78,7 @@ month="June" } -@techreport{lambdadeltaR2, +@techreport{lambdadeltaR1b, author="F. {Guidi}", title="{Lambda-Types on the Lambda-Calculus with Abbreviations}", type="Technical Report", @@ -89,7 +89,7 @@ month="November" } -@techreport{lambdadeltaR1, +@techreport{lambdadeltaR1a, author="F. {Guidi}", title="{Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification}", type="Technical Report", diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html index f8e72014b..a9f2cf2bf 100644 --- a/helm/www/lambdadelta/ground_1.html +++ b/helm/www/lambdadelta/ground_1.html @@ -275,6 +275,6 @@

-
Last update: Sat, 21 Feb 2015 23:38:38 +0100
+
Last update: Fri, 06 Mar 2015 16:17:54 +0100
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index b2cc62e27..a8f176a5a 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -328,6 +328,6 @@

-
Last update: Sat, 21 Feb 2015 23:38:38 +0100
+
Last update: Fri, 06 Mar 2015 16:17:54 +0100
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html index f0e1d32ff..6e429e20d 100644 --- a/helm/www/lambdadelta/implementation.html +++ b/helm/www/lambdadelta/implementation.html @@ -157,7 +157,7 @@ (the specification language of Matita). The overall validation speed of the "Grundlagen der Analysis" increases of 34% with respect to version 0.8.1. - Documentation (J4). + Documentation (J3a). [Svn revision: 13035] (archived source code).
  • @@ -220,7 +220,7 @@ Supports λδ "Version 2" with naive implementation of impredicative sort inclusion. Features importation from Automath and exportation to XML. - Documentation (R4). + Documentation (R2a). [Svn revision: 10304] (archived source code).
    • @@ -269,6 +269,6 @@

      -
      Last update: Sat, 21 Feb 2015 23:38:38 +0100
      +
      Last update: Fri, 06 Mar 2015 16:17:54 +0100
      diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 317de931d..047fffc78 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -202,6 +202,6 @@

      -
      Last update: Sat, 21 Feb 2015 23:38:38 +0100
      +
      Last update: Fri, 06 Mar 2015 16:17:54 +0100
      diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 3b45a688c..267710b06 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -146,7 +146,7 @@ @@ -159,7 +159,7 @@
        @@ -292,14 +292,14 @@
          @@ -354,6 +354,6 @@

          -
          Last update: Thu, 05 Mar 2015 16:46:30 +0100
          +
          Last update: Fri, 06 Mar 2015 16:17:54 +0100
          diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html index e4fab5899..08d1f256e 100644 --- a/helm/www/lambdadelta/specification.html +++ b/helm/www/lambdadelta/specification.html @@ -328,6 +328,6 @@

          -
          Last update: Sat, 21 Feb 2015 23:38:38 +0100
          +
          Last update: Fri, 06 Mar 2015 16:17:54 +0100
          diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml index a51f64307..bfcf84527 100644 --- a/helm/www/lambdadelta/web/home/documentation.ldw.xml +++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml @@ -14,25 +14,25 @@ lambdadelta.bib, lambdadelta.txt - (revised ). + (revised ). λδ version 3 (proposed) - The main source of information is . + The main source of information is . λδ version 2 (active) - The main source of information is . + The main source of information is .
          λδ version 1 (superseded) The main source of information is . - A summary is available in . + A summary is available in .
          diff --git a/helm/www/lambdadelta/web/home/documentation_1.tbl b/helm/www/lambdadelta/web/home/documentation_1.tbl index a12c18683..65ba89668 100644 --- a/helm/www/lambdadelta/web/home/documentation_1.tbl +++ b/helm/www/lambdadelta/web/home/documentation_1.tbl @@ -16,7 +16,7 @@ table { @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] - [ { name "ldR3" "R3." "" } { + [ { name "ldR1c" "R1c." "" } { "F. Guidi:" + @@("download/cie_2007.pdf" "Lambda Types on the Lambda Calculus with Abbreviations") + @@ -27,7 +27,7 @@ table { @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] - [ { name "ldR2" "R2." "" } { + [ { name "ldR1b" "R1b." "" } { "F. Guidi:" + @("http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-25" "Lambda Types on the Lambda Calculus with Abbreviations") + @@ -36,7 +36,7 @@ table { @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] - [ { name "ldR1" "R1." "" } { + [ { name "ldR1a" "R1a." "" } { "F. Guidi:" + @("http://www.informatica.unibo.it/it/ricerca/technical-report/2006/UBLCS-2006-01" "Lambda Types on the Lambda Calculus with Abbreviations: a Certified Specification") + @@ -45,14 +45,14 @@ table { @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] - [ { name "ldP5" "P5." "" } { + [ { name "ldP1e" "P1e." "" } { "F. Guidi:" + @@("download/ld_talk_5s.pdf" "The Formal System λδ") + "(2008-10)." + "Presentation at Advances in Constructive Topology and Logical Foundations (slides)." * } ] - [ { name "ldP4" "P4." "" } { + [ { name "ldP1d" "P1d." "" } { "F. Guidi:" + @@("download/ld_talk_4s.pdf" "Towards the Unification of Terms, Types and Contexts") + @@ -60,7 +60,7 @@ table { "Presentation at Types 2008 (slides)." * } ] - [ { name "ldP3" "P3." "" } { + [ { name "ldP1c" "P1c." "" } { "F. Guidi:" + @@("download/ld_talk_3s.pdf" "Lambda Types on the Lambda Calculus with Abbreviations") + @@ -68,7 +68,7 @@ table { "Presentation at CiE 2007 (slides)." * } ] - [ { name "ldP2" "P2." "" } { + [ { name "ldP1b" "P1b." "" } { "F. Guidi:" + @@("download/ld_talk_2s.pdf" "Lambda Tipi sul Lambda Calcolo con Abbreviazioni") + @@ -77,7 +77,7 @@ table { "in Italian)." * } ] - [ { name "ldP1" "P1." "" } { + [ { name "ldP1a" "P1a." "" } { "F. Guidi:" + @@("download/ld_talk_1s.pdf" "Lambda Tipi sul Lambda Calcolo con Abbreviazioni: una Specifica Certificata") + @@ -89,7 +89,7 @@ table { [ { name "ldV1" "V1." "" } { "F. Guidi:" + @@("version_1.html" "lambdadelta_1") + - "(revised 2012-10)." + + "(revised 2015-01)." + "Formal specification for the proof assistant Coq 7.3.1 (scripts)." + @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } diff --git a/helm/www/lambdadelta/web/home/documentation_2.tbl b/helm/www/lambdadelta/web/home/documentation_2.tbl index 04d6cf8b9..1d00bf77e 100644 --- a/helm/www/lambdadelta/web/home/documentation_2.tbl +++ b/helm/www/lambdadelta/web/home/documentation_2.tbl @@ -1,18 +1,20 @@ name "documentation_2" table { - [ { name "ldJ2" "J2." "" } { + [ { name "ldJ2a" "J2a." "" } { "F. Guidi:" + @@("download/basic2a.pdf" - "The Formal System λδ Revised - Stage A: Extending the Applicability Condition") + + "The Formal System λδ Revised, Stage A: Extending the Applicability Condition") + "(2014-11)." + "Submitted to ACM ToCL." + "CoRR identifier" + @("http://arxiv.org/abs/1411.0154" "1411.0154") + - "[v1]." + "[v2] (revised" + + "2015-03)." + + @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] - [ { name "ldR5" "R5." "" } { + [ { name "ldR2b" "R2b." "" } { "F. Guidi:" + @@("download/cie_2010.pdf" "An Efficient Validation Procedure for the Formal System λδ") + @@ -22,7 +24,7 @@ table { @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] - [ { name "ldR4" "R4." "" } { + [ { name "ldR2a" "R2a." "" } { "F. Guidi:" + @("http://www.informatica.unibo.it/it/ricerca/technical-report/2009/UBLCS-2009-16" "Landau's \"Grundlagen der Analysis\" from Automath to lambda-delta") + @@ -31,7 +33,7 @@ table { @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] - [ { name "ldP8" "P8." "" } { + [ { name "ldP2c" "P2c." "" } { "F. Guidi:" + @@("download/ld_talk_8s.pdf" "The Formal System λδ and the \"Three Problems\"") + @@ -39,7 +41,7 @@ table { "Presentation at University of Bologna (slides)." * } ] - [ { name "ldP7" "P7." "" } { + [ { name "ldP2b" "P2b." "" } { "F. Guidi:" + @@("download/ld_talk_7s.pdf" "An Efficient Validation Procedure for the Formal System λδ") + @@ -47,7 +49,7 @@ table { "Presentation at CiE 2010 (slides)." * } ] - [ { name "ldP6" "P6." "" } { + [ { name "ldP2a" "P2a." "" } { "F. Guidi:" + @@("download/ld_talk_6s.pdf" "A Validator for the Formal System λδ") + diff --git a/helm/www/lambdadelta/web/home/documentation_3.tbl b/helm/www/lambdadelta/web/home/documentation_3.tbl index ec291e009..4df01fc55 100644 --- a/helm/www/lambdadelta/web/home/documentation_3.tbl +++ b/helm/www/lambdadelta/web/home/documentation_3.tbl @@ -1,12 +1,13 @@ name "documentation_3" table { - [ { name "ldJ4" "J4." "" } { + [ { name "ldJ3a" "J3a." "" } { "F. Guidi:" + @@("download/gda.pdf" "A Verified Translation of Landau's \"Grundlagen\" from Automath into a Pure Type System, via λδ") + "(2015-02)." + - "Submitted to JFR, Univerity of Bologna." + "Submitted to JFR, Univerity of Bologna." + + @@("documentation.html#bibtex" "BibTeX entry") ^ "." * } ] } diff --git a/helm/www/lambdadelta/web/home/implementation.ldw.xml b/helm/www/lambdadelta/web/home/implementation.ldw.xml index 9112a8037..05bb7c6c2 100644 --- a/helm/www/lambdadelta/web/home/implementation.ldw.xml +++ b/helm/www/lambdadelta/web/home/implementation.ldw.xml @@ -54,7 +54,7 @@ (the specification language of Matita). The overall validation speed of the "Grundlagen der Analysis" increases of 34% with respect to version 0.8.1. - Documentation (J4). + Documentation (J3a). [Svn revision: 13035] (archived source code). The specification of Landau's "Grundlagen der Analysis" @@ -104,7 +104,7 @@ Supports λδ "Version 2" with naive implementation of impredicative sort inclusion. Features importation from Automath and exportation to XML. - Documentation (R4). + Documentation (R2a). [Svn revision: 10304] (archived source code). A Jed mode diff --git a/helm/www/lambdadelta/web/home/news.ldw.xml b/helm/www/lambdadelta/web/home/news.ldw.xml index 3e0f1f4af..46f208da9 100644 --- a/helm/www/lambdadelta/web/home/news.ldw.xml +++ b/helm/www/lambdadelta/web/home/news.ldw.xml @@ -38,7 +38,7 @@ - λδ version 2A + λδ version 2A is released. @@ -47,7 +47,7 @@ - First communication on λδ version 2. + First communication on λδ version 2. @@ -140,12 +140,12 @@ - λδ version 1 + λδ version 1 is released. - First communication on λδ version 1. + First communication on λδ version 1.