minor bugs fixed in the web site, and minor updates

diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html
index d64ee8ae3aa729818b1f72338c50ea3738f73e48..e5eacedbd2cb9f8c9f7f24da13422d5502f1b38f 100644 (file)
--- a/helm/www/lambdadelta/basic_1.html
+++ b/helm/www/lambdadelta/basic_1.html
@@ -823,6 +823,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>

-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 29 Dec 2015 22:50:57 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:56:06 +0100</div>

   </body>
 </html>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index a60c9bbf9f064ae455099894677fe06f6346b769..4509b93ed2c40ebb4d6d07639042f9a1a3d15bd5 100644 (file)
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -389,6 +389,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>

-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:54:53 +0100</div>

   </body>
 </html>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html
index 205e37de71fce694a0fd0594110024902e81586a..3ac157fb6cda79ed239e13a7b715923b7c02bc85 100644 (file)
--- a/helm/www/lambdadelta/ground_1.html
+++ b/helm/www/lambdadelta/ground_1.html
@@ -275,6 +275,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>

-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Tue, 29 Dec 2015 22:50:57 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:56:06 +0100</div>

   </body>
 </html>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 90f3bfd87c5555e8460273934b790413109ed953..c613e6bb8cf17620328f8c8bdb14bf1e960776dc 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -291,6 +291,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>

-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:56:06 +0100</div>

   </body>
 </html>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 8a582d04c4bc8ae17bdaff2e8c444b7a9c8c9682..b0c4d0792ae3e0247566ee0d36342216b39405a9 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -137,14 +137,14 @@
       <li>
       C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
       <span class="emph alpha">ELPI: fast, Embeddable, λProlog Interpreter</span>
       <li>
       C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
       <span class="emph alpha">ELPI: fast, Embeddable, λProlog Interpreter</span>

-      (2015). In proc. of LPAR 20. LNCS 9450, pp. 460-468.
+      (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer.

    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="C6">
       <li>
       A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
       <span class="emph alpha">Formal metatheory of programming languages in the Matita interactive theorem prover</span>
    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="C6">
       <li>
       A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
       <span class="emph alpha">Formal metatheory of programming languages in the Matita interactive theorem prover</span>

-      (2012). In JAR 49(3), pp. 427-451.
+      (2012). In Journal of Automated Reasoning, 49(3), pp. 427-451. Springer.

    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="C5">
    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="C5">


@@ -172,7 +172,7 @@
       <li>
       M.E. Maietti:
       <span class="emph alpha">A minimalist two-level foundation for constructive mathematics</span>
       <li>
       M.E. Maietti:
       <span class="emph alpha">A minimalist two-level foundation for constructive mathematics</span>

-      (2009). In APAL 160(3), pp. 319-354.
+      (2009). In Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier. 

    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="C1">
    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="C1">


@@ -186,15 +186,15 @@
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="disclaimer">Disclaimer <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="disclaimer">Disclaimer <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b9.png" />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">

-      The systens of the λδ family <span xmlns="http://lambdadelta.info/" class="emph">are not</span> related intentionally to any other system
+      The systens of the λδ family <span class="emph alpha">are not</span> related intentionally to any other system

       having (variations of) the symbols λ and δ in its name or syntax.
       Examples include (but are not limited to):
    </div>
     <ul xmlns:ld="http://lambdadelta.info/" id="D1">
       <li>
       having (variations of) the symbols λ and δ in its name or syntax.
       Examples include (but are not limited to):
    </div>
     <ul xmlns:ld="http://lambdadelta.info/" id="D1">
       <li>

-        <span xmlns="http://lambdadelta.info/" class="emph">λ-δ</span> of
+        <span class="emph alpha">λ-δ</span> of

       A. Church:
       A. Church:

-      <span xmlns="http://lambdadelta.info/" class="emph">The calculi of lambda-conversion</span>
+      <span class="emph alpha">The calculi of lambda-conversion</span>

       (1941).
       Annals of Mathematics Studies 6.
       Princeton University Press.
       (1941).
       Annals of Mathematics Studies 6.
       Princeton University Press.


@@ -202,9 +202,9 @@
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="D2">
       <li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="D2">
       <li>

-        <span xmlns="http://lambdadelta.info/" class="emph">∆Λ</span> of
+        <span class="emph alpha">∆Λ</span> of

       N.G. de Bruijn:
       N.G. de Bruijn:

-      <span xmlns="http://lambdadelta.info/" class="emph">Generalizing Automath by means of a lambda-typed lambda calculus</span>
+      <span class="emph alpha">Generalizing Automath by means of a lambda-typed lambda calculus</span>

       (1987).
       In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
       Marcel Dekker.
       (1987).
       In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
       Marcel Dekker.


@@ -212,10 +212,10 @@
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="D3">
       <li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="D3">
       <li>

-        <span xmlns="http://lambdadelta.info/" class="emph">λ<sub>∆</sub>
+        <span class="emph alpha">λ<sub xmlns="http://lambdadelta.info/">∆</sub>

         </span> of
       N.J. Rehof, M.H. Sørensen:
         </span> of
       N.J. Rehof, M.H. Sørensen:

-      <span xmlns="http://lambdadelta.info/" class="emph">The λ<sub>∆</sub>-calculus</span>
+      <span class="emph alpha">The λ<sub xmlns="http://lambdadelta.info/">∆</sub>-calculus</span>

       (1994).
       In Lecture Notes in Computer Science, 789, pp. 516–542.
       Springer.
       (1994).
       In Lecture Notes in Computer Science, 789, pp. 516–542.
       Springer.


@@ -223,9 +223,9 @@
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="D4">
       <li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="D4">
       <li>

-        <span xmlns="http://lambdadelta.info/" class="emph alpha">λ∆</span> of
+        <span class="emph alpha">λ∆</span> of

       S. Ronchi Della Rocca, L. Paolini:
       S. Ronchi Della Rocca, L. Paolini:

-      <span xmlns="http://lambdadelta.info/" class="emph">The Parametric Lambda Calculus</span>
+      <span class="emph alpha">The Parametric Lambda Calculus</span>

       (2004).
       Texts in Theoretical Computer Science, An EATCS Series.
       Springer.
       (2004).
       Texts in Theoretical Computer Science, An EATCS Series.
       Springer.


@@ -233,18 +233,18 @@
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="D5">
       <li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="D5">
       <li>

-        <span xmlns="http://lambdadelta.info/" class="emph">λD</span> of
+        <span class="emph alpha">λD</span> of

       R. Nederpelt, H. Geuvers:
       R. Nederpelt, H. Geuvers:

-      <span xmlns="http://lambdadelta.info/" class="emph">Type Theory and Formal Proof</span>
+      <span class="emph alpha">Type Theory and Formal Proof</span>

       (2014).
       Cambridge University Press.
    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="D6">
       <li>
       (2014).
       Cambridge University Press.
    </li>
     </ul>
     <ul xmlns:ld="http://lambdadelta.info/" id="D6">
       <li>

-        <span xmlns="http://lambdadelta.info/" class="emph">Cλξ</span> of
+        <span class="emph alpha">Cλξ</span> of

       N.G. de Bruijn:
       N.G. de Bruijn:

-      <span xmlns="http://lambdadelta.info/" class="emph">A namefree lambda calculus with facilities for internal definition of expressions and segments</span>
+      <span class="emph alpha">A namefree lambda calculus with facilities for internal definition of expressions and segments</span>

       (1978).
       TH-report 78-WSK-03.
       Eindhoven University of Technology, Eindhoven.
       (1978).
       TH-report 78-WSK-03.
       Eindhoven University of Technology, Eindhoven.


@@ -276,6 +276,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>

-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:56:06 +0100</div>

   </body>
 </html>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 02ed66ceb6837f096bd6c6ff9d1d804d6d13416e..e387da2f420925068bf14f0b4476b4c53364aa43 100644 (file)
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -373,6 +373,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>

-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:03 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:54:53 +0100</div>

   </body>
 </html>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index ee93a0f9adb86b98f2d347a0e659aed66a3e0c09..7b2a58987c53743ab764f2f5604fc0c019812c79 100644 (file)
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -211,7 +211,7 @@
     <div xmlns:ld="http://lambdadelta.info/" class="text">
      Informational pages on the specifications are provided.
    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
      Informational pages on the specifications are provided.
    </div>

-    <ul xmlns:ld="http://lambdadelta.info/" id="">
+    <ul xmlns:ld="http://lambdadelta.info/" id="notice1">

       <li>
         <span class="emph alpha">Notice on displayed numerical acounts:</span>
       nodes are counted according to the "intrinsic complexity measure"
       <li>
         <span class="emph alpha">Notice on displayed numerical acounts:</span>
       nodes are counted according to the "intrinsic complexity measure"


@@ -219,7 +219,7 @@
       Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
    </li>
     </ul>
       Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
    </li>
     </ul>

-    <ul xmlns:ld="http://lambdadelta.info/" id="">
+    <ul xmlns:ld="http://lambdadelta.info/" id="notice2">

       <li>
         <span class="emph alpha">Notice on displayed logical structures:</span>
       from the logical standpoint, the source scripts are grouped in "planes"
       <li>
         <span class="emph alpha">Notice on displayed logical structures:</span>
       from the logical standpoint, the source scripts are grouped in "planes"


@@ -360,6 +360,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>

-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 12:08:04 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 30 Dec 2015 14:54:53 +0100</div>

   </body>
 </html>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/web/home/index.ldw.xml b/helm/www/lambdadelta/web/home/index.ldw.xml
index 9ebac8e8069440e00a9906da6ac5850e41aaa8e6..5110c14703bf1f775c64e5b52b4ccc6c9361e077 100644 (file)
--- a/helm/www/lambdadelta/web/home/index.ldw.xml
+++ b/helm/www/lambdadelta/web/home/index.ldw.xml
@@ -21,10 +21,10 @@
    </body>
    <body>
       This is the family logo: <rlink to="images/crux_177.png">crux_177.png</rlink>
    </body>
    <body>
       This is the family logo: <rlink to="images/crux_177.png">crux_177.png</rlink>

-      (revised <notice class="alpha" notice="2012-09"/>).
+      (revised <notice class="alpha" text="2012-09"/>).

    </body>
    <body>
    </body>
    <body>

-      <notice class="alpha" notice="Notice for the user of Internet Explorer."/>
+      <notice class="alpha" text="Notice for the user of Internet Explorer."/>

       To view this site correctly, please select a font
       with <link to="http://www.unicode.org/">Unicode</link> support.
       For example "Lucida Sans Unicode" (it should be already installed on your system).
       To view this site correctly, please select a font
       with <link to="http://www.unicode.org/">Unicode</link> support.
       For example "Lucida Sans Unicode" (it should be already installed on your system).


@@ -41,43 +41,43 @@
 
    <topitem name="C7">
       C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:
 
    <topitem name="C7">
       C. Dunchev, F. Guidi, C. Sacerdoti Coen, E. Tassi:

-      <notice class="alpha" notice="ELPI: fast, Embeddable, λProlog Interpreter"/>
-      (2015). In proc. of LPAR 20. LNCS 9450, pp. 460-468.
+      <notice class="alpha">ELPI: fast, Embeddable, λProlog Interpreter</notice>
+      (2015). In proc. of LPAR 20. Lecture Notes in Computer Science, 9450, pp. 460-468. Springer.

    </topitem>
 
    <topitem name="C6">
       A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:
    </topitem>
 
    <topitem name="C6">
       A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi:

-      <notice class="alpha" notice="Formal metatheory of programming languages in the Matita interactive theorem prover"/>
-      (2012). In JAR 49(3), pp. 427-451.
+      <notice class="alpha">Formal metatheory of programming languages in the Matita interactive theorem prover</notice>
+      (2012). In Journal of Automated Reasoning, 49(3), pp. 427-451. Springer.

    </topitem>
 
    <topitem name="C5">
       M.E. Maietti:
    </topitem>
 
    <topitem name="C5">
       M.E. Maietti:

-      <notice class="alpha" notice="Consistency of the minimalist foundation with Church thesis and Bar Induction"/>
+      <notice class="alpha">Consistency of the minimalist foundation with Church thesis and Bar Induction</notice>

       (2012). Submitted article.
    </topitem>
 
    <topitem name="C4">
       W. Ricciotti:
       (2012). Submitted article.
    </topitem>
 
    <topitem name="C4">
       W. Ricciotti:

-      <notice class="alpha" notice="Theoretical and implementation aspects in the mechanization of the metatheory of programming languages"/>
+      <notice class="alpha">Theoretical and implementation aspects in the mechanization of the metatheory of programming languages</notice>

       (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna.
    </topitem>
 
    <topitem name="C3">
       C.E. Brown:
       (July 2011). Ph.D. Thesis in Computer Science, Technical Report UBLCS-2011-09, University of Bologna.
    </topitem>
 
    <topitem name="C3">
       C.E. Brown:

-      <notice class="alpha" notice="Faithful Reproductions of the Automath Landau Formalization"/>
+      <notice class="alpha">Faithful Reproductions of the Automath Landau Formalization</notice>

       (2011). Technical report.
    </topitem>
 
    <topitem name="C2">
       M.E. Maietti:
       (2011). Technical report.
    </topitem>
 
    <topitem name="C2">
       M.E. Maietti:

-      <notice class="alpha" notice="A minimalist two-level foundation for constructive mathematics"/>
-      (2009). In APAL 160(3), pp. 319-354.
+      <notice class="alpha">A minimalist two-level foundation for constructive mathematics</notice>
+      (2009). In Annals of Pure and Applied Logic, 160(3), pp. 319-354. Elsevier. 

    </topitem>
 
    <topitem name="C1">
       V. Rahili: 
    </topitem>
 
    <topitem name="C1">
       V. Rahili: 

-      <notice class="alpha" notice="First Year Report: Realisability methods of proof and semantics with application to expansion"/>
+      <notice class="alpha">First Year Report: Realisability methods of proof and semantics with application to expansion</notice>

       (July 2007). Technical report.
    </topitem>
 
       (July 2007). Technical report.
    </topitem>
 


@@ -85,59 +85,59 @@
 
    <section9 name="disclaimer">Disclaimer</section9>
    <body>
 
    <section9 name="disclaimer">Disclaimer</section9>
    <body>

-      The systens of the λδ family <span class="emph">are not</span> related intentionally to any other system
+      The systens of the λδ family <notice class="alpha" text="are not"/> related intentionally to any other system

       having (variations of) the symbols λ and δ in its name or syntax.
       Examples include (but are not limited to):
    </body>
 
    <topitem name="D1">
       having (variations of) the symbols λ and δ in its name or syntax.
       Examples include (but are not limited to):
    </body>
 
    <topitem name="D1">

-      <span class="emph">λ-δ</span> of
+      <notice class="alpha">λ-δ</notice> of

       A. Church:
       A. Church:

-      <span class="emph">The calculi of lambda-conversion</span>
+      <notice class="alpha">The calculi of lambda-conversion</notice>

       (1941).
       Annals of Mathematics Studies 6.
       Princeton University Press.
    </topitem>
 
    <topitem name="D2">
       (1941).
       Annals of Mathematics Studies 6.
       Princeton University Press.
    </topitem>
 
    <topitem name="D2">

-      <span class="emph">∆Λ</span> of
+      <notice class="alpha">∆Λ</notice> of

       N.G. de Bruijn:
       N.G. de Bruijn:

-      <span class="emph">Generalizing Automath by means of a lambda-typed lambda calculus</span>
+      <notice class="alpha">Generalizing Automath by means of a lambda-typed lambda calculus</notice>

       (1987).
       In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
       Marcel Dekker.
    </topitem>
 
    <topitem name="D3">
       (1987).
       In Lecture Notes in Pure and Applied Mathematics 106, pp. 71-92.
       Marcel Dekker.
    </topitem>
 
    <topitem name="D3">

-      <span class="emph">λ<sub>∆</sub></span> of
+      <notice class="alpha">λ<sub>∆</sub></notice> of

       N.J. Rehof, M.H. Sørensen:
       N.J. Rehof, M.H. Sørensen:

-      <span class="emph">The λ<sub>∆</sub>-calculus</span>
+      <notice class="alpha">The λ<sub>∆</sub>-calculus</notice>

       (1994).
       In Lecture Notes in Computer Science, 789, pp. 516–542.
       Springer.
    </topitem>
 
    <topitem name="D4">
       (1994).
       In Lecture Notes in Computer Science, 789, pp. 516–542.
       Springer.
    </topitem>
 
    <topitem name="D4">

-      <span class="emph alpha">λ∆</span> of
+      <notice class="alpha">λ∆</notice> of

       S. Ronchi Della Rocca, L. Paolini:
       S. Ronchi Della Rocca, L. Paolini:

-      <span class="emph">The Parametric Lambda Calculus</span>
+      <notice class="alpha">The Parametric Lambda Calculus</notice>

       (2004).
       Texts in Theoretical Computer Science, An EATCS Series.
       Springer.
    </topitem>
 
    <topitem name="D5">
       (2004).
       Texts in Theoretical Computer Science, An EATCS Series.
       Springer.
    </topitem>
 
    <topitem name="D5">

-      <span class="emph">λD</span> of
+      <notice class="alpha">λD</notice> of

       R. Nederpelt, H. Geuvers:
       R. Nederpelt, H. Geuvers:

-      <span class="emph">Type Theory and Formal Proof</span>
+      <notice class="alpha">Type Theory and Formal Proof</notice>

       (2014).
       Cambridge University Press.
    </topitem>
 
    <topitem name="D6">
       (2014).
       Cambridge University Press.
    </topitem>
 
    <topitem name="D6">

-      <span class="emph">Cλξ</span> of
+      <notice class="alpha">Cλξ</notice> of

       N.G. de Bruijn:
       N.G. de Bruijn:

-      <span class="emph">A namefree lambda calculus with facilities for internal definition of expressions and segments</span>
+      <notice class="alpha">A namefree lambda calculus with facilities for internal definition of expressions and segments</notice>

       (1978).
       TH-report 78-WSK-03.
       Eindhoven University of Technology, Eindhoven.
       (1978).
       TH-report 78-WSK-03.
       Eindhoven University of Technology, Eindhoven.

diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml
index e8c3d5b13a2ed1dfcc42697849931df3f7c36c1f..a489b47a8f2ca93d61cea3d4d4a52ea84d1cbb91 100644 (file)
--- a/helm/www/lambdadelta/web/home/specification.ldw.xml
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -14,15 +14,15 @@
    </body>
    <body>
       The life cycle of a specification consists of four periods.
    </body>
    <body>
       The life cycle of a specification consists of four periods.

-      <notice class="alpha" notice="Alpha:"/>
+      <notice class="alpha" text="Alpha:"/>

       the definitions are designed and the major propositions are proved,
       then the calculus is announced with a presentation.
       the definitions are designed and the major propositions are proved,
       then the calculus is announced with a presentation.

-      <notice class="beta" notice="Beta:"/>
+      <notice class="beta" text="Beta:"/>

       major changes and additions may occur before the calculus is released on paper.
       major changes and additions may occur before the calculus is released on paper.

-      <notice class="gamma" notice="Gamma:"/>
+      <notice class="gamma" text="Gamma:"/>

       subsequent improvements occur until the specification is completed or superseded,
       while major changes and additions are announced and reported on paper.
       subsequent improvements occur until the specification is completed or superseded,
       while major changes and additions are announced and reported on paper.

-      <notice class="delta" notice="Delta:"/>
+      <notice class="delta" text="Delta:"/>

       after its conclusion, the specification is modified just for maintenance. 
    </body>
    <table name="versions"/>
       after its conclusion, the specification is modified just for maintenance. 
    </body>
    <table name="versions"/>


@@ -30,14 +30,14 @@
    <body>
      Informational pages on the specifications are provided.
    </body>
    <body>
      Informational pages on the specifications are provided.
    </body>

-   <topitem>
-      <notice class="alpha" notice="Notice on displayed numerical acounts:"/>
+   <topitem name="notice1">
+      <notice class="alpha" text="Notice on displayed numerical acounts:"/>

       nodes are counted according to the "intrinsic complexity measure"
       [F. Guidi: "Procedural Representation of CIC Proof Terms"
       Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
    </topitem>
       nodes are counted according to the "intrinsic complexity measure"
       [F. Guidi: "Procedural Representation of CIC Proof Terms"
       Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
    </topitem>

-   <topitem>
-      <notice class="alpha" notice="Notice on displayed logical structures:"/>
+   <topitem name="notice2">
+      <notice class="alpha" text="Notice on displayed logical structures:"/>

       from the logical standpoint, the source scripts are grouped in "planes"
       and these are grouped in "components";
       the notation for the relations or functions
       from the logical standpoint, the source scripts are grouped in "planes"
       and these are grouped in "components";
       the notation for the relations or functions


@@ -55,7 +55,7 @@
    <topitem name="source2">
       <body>
          <rlink to="download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</rlink>
    <topitem name="source2">
       <body>
          <rlink to="download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</rlink>

-         (revised <notice class="gamma" notice="2014-10"/>).
+         (revised <notice class="gamma" text="2014-10"/>).

          Source scripts.
          <rlink to="documentation.html#ldR2c">Documentation (R2c)</rlink>.
       </body>
          Source scripts.
          <rlink to="documentation.html#ldR2c">Documentation (R2c)</rlink>.
       </body>


@@ -63,7 +63,7 @@
          The scripts are grouped in directories, first by part, then by component.
       </body>
       <body>
          The scripts are grouped in directories, first by part, then by component.
       </body>
       <body>

-         <notice class="alpha" notice="Notice:"/>
+         <notice class="alpha" text="Notice:"/>

          the scripts are checked by the latest version of Matita from
          <link to="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</link>
          at path &lt;trunk/matita/&gt;.
          the scripts are checked by the latest version of Matita from
          <link to="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</link>
          at path &lt;trunk/matita/&gt;.


@@ -88,11 +88,11 @@
    <topitem name="source1">
       <body>
          <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
    <topitem name="source1">
       <body>
          <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>

-         (revised <notice class="delta" notice="2015-09"/>).
+         (revised <notice class="delta" text="2015-09"/>).

          Source scripts.
          <rlink to="documentation.html#ldJ1a">Documentation (J1a)</rlink>.
          <list><item>
          Source scripts.
          <rlink to="documentation.html#ldJ1a">Documentation (J1a)</rlink>.
          <list><item>

-            <notice class="delta" notice="2015 January 15."/>
+            <notice class="delta" text="2015 January 15."/>

             17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
          </item></list>
       </body>      
             17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
          </item></list>
       </body>      


@@ -103,7 +103,7 @@
 
    <topitem name="static1">
       <rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</rlink>
 
    <topitem name="static1">
       <rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</rlink>

-      (revised <notice class="delta" notice="2011-09"/>).
+      (revised <notice class="delta" text="2011-09"/>).

       Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.  
       <list><item>
          <rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
       Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.  
       <list><item>
          <rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">


@@ -130,9 +130,9 @@
    <topitem name="dynamic1">
       <link to="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
          lambdadelta_1 for Matita 0.5</link>
    <topitem name="dynamic1">
       <link to="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
          lambdadelta_1 for Matita 0.5</link>

-      (revised <notice class="delta" notice="2011-09"/>).
+      (revised <notice class="delta" text="2011-09"/>).

       <link to="http://helm.cs.unibo.it/">HELM</link> directory.
       <link to="http://helm.cs.unibo.it/">HELM</link> directory.

-      <notice class="alpha" notice="Notice: the HELM rendering engine is offline."/>
+      <notice class="alpha" text="Notice: the HELM rendering engine is offline."/>

    </topitem>
 
    <body>
    </topitem>
 
    <body>

diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl
index ee9d210537f7a20dbeac2312dc8882f716f61b10..388873a990a50ce3fc10810d2acfc88d38faf814 100644 (file)
--- a/helm/www/lambdadelta/xslt/ld_web_root.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl
@@ -141,7 +141,13 @@
 </xsl:template>
 
 <xsl:template match="ld:notice">
 </xsl:template>
 
 <xsl:template match="ld:notice">

-   <span class="emph {@class}"><xsl:value-of select="@notice"/></span>
+   <span class="emph {@class}">
+      <xsl:choose>
+         <xsl:when test="@notice"><xsl:value-of select="@notice"/></xsl:when>
+         <xsl:when test="@text"><xsl:value-of select="@text"/></xsl:when>
+         <xsl:otherwise><xsl:apply-templates/></xsl:otherwise>
+      </xsl:choose>
+   </span>

 </xsl:template>
 
 <xsl:template match="ld:version3-icon">
 </xsl:template>
 
 <xsl:template match="ld:version3-icon">