From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 22 Jul 2016 17:40:26 +0000 (+0000)
Subject: corrected xhtml
X-Git-Tag: make_still_working~549
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=7c3dc0455368fe74858226ab6cf3c19f68d0e2a7

corrected xhtml
---

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 87ca3917c..382f647f1 100644
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -222,6 +222,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:34:08 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index e1a4e7961..b5d4a797f 100644
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -258,6 +258,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:34:08 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html
index ad01b3644..cfcf7c77b 100644
--- 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">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:34:08 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 287810b55..1e1fa23b9 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -811,6 +811,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:34:08 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index fc3e24bc8..eb29584b5 100644
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -401,6 +401,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:34:08 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html
index e732b224b..6dd32de67 100644
--- a/helm/www/lambdadelta/ground_1.html
+++ b/helm/www/lambdadelta/ground_1.html
@@ -291,6 +291,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:34:08 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index e4ef243ae..1a9b9352f 100644
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -821,6 +821,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:34:08 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/home.html b/helm/www/lambdadelta/home.html
index 30ed25317..d28db2fab 100644
--- a/helm/www/lambdadelta/home.html
+++ b/helm/www/lambdadelta/home.html
@@ -283,6 +283,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:41 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:34:08 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index dabbb6d2c..eb42a5a58 100644
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -143,7 +143,7 @@
       +3% with optimized compilation, +5% without optimized compilation.
       [Svn revision: 13108] (<a href="http://lambdadelta.info/download/helena_0.8.3.tar.gz">archived source code</a>).
       <ul>
-          <li>
+          <li class="">
             <span class="emph gamma">2015-06.</span>
          The corrected specification of Landau's "Grundlagen der Analysis"
          is successfully validated in a λProlog implementation of λδ version 3.
@@ -164,29 +164,29 @@
       <a href="http://lambdadelta.info/documentation.html#ldJ3a">Documentation (J3a)</a>.
       [Svn revision: 13035] (<a href="http://lambdadelta.info/download/helena_0.8.2.tar.gz">archived source code</a>).
       <ul>
-          <li>
+          <li class="">
          The specification of Landau's "Grundlagen der Analysis"
          for <a href="http://coq.inria.fr/">Coq 8</a>:
          <a href="http://lambdadelta.info/download/grundlagen_2.v">grundlagen_2.v</a>
          (revised <span class="emph gamma">2015-02</span>).
       </li>
-          <li>
+          <li class="">
          The specification of Landau's "Grundlagen der Analysis"
          for <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>:
          <a href="http://lambdadelta.info/download/grundlagen_2.tar.bz2">grundlagen_2.tar.bz2</a>
          (revised <span class="emph gamma">2015-02</span>).
       </li>
-          <li>
+          <li class="">
          The corrected specification of Landau's "Grundlagen der Analysis":  
          <a href="http://lambdadelta.info/download/grundlagen_2.aut">grundlagen_2.aut</a>
          (revised <span class="emph gamma">2014-12</span>).
       </li>
-          <li>
+          <li class="">
             <span class="emph gamma">2015-02.</span>
          The translated specification of Landau's "Grundlagen der Analysis"
          is successfully validated in CC by <a href="http://coq.inria.fr/">Coq 8.4.3</a>.
       </li>
-          <li>
+          <li class="">
             <span class="emph gamma">2014-12.</span>
          The corrected specification of Landau's "Grundlagen der Analysis"
          is successfully validated in λδ version 3.
@@ -203,13 +203,13 @@
       increases of 22% with respect to version 0.8.0.
       [Svn revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived source code</a>).
       <ul>
-          <li>
+          <li class="">
          A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
          for editing ".hln" files (containing λδ textual syntax):
          <a href="http://lambdadelta.info/download/helena.sl">helena.sl</a>
          (revised <span class="emph alpha">2010-11</span>).
       </li>
-          <li>
+          <li class="">
             <span class="emph beta">2009-12.</span>
          Helena appears in F. Wiedijk's
          <a href="http://www.cs.ru.nl/%7Efreek/digimath/index.html#helena">
@@ -227,19 +227,19 @@
       <a href="http://lambdadelta.info/documentation.html#ldR2a">Documentation (R2a)</a>.
       [Svn revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived source code</a>).
       <ul>
-          <li>
+          <li class="">
          A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
          for editing ".aut" files
          (containing <a href="http://www.win.tue.nl/automath/">Automath</a> textual syntax):
          <a href="http://lambdadelta.info/download/automath.sl">automath.sl</a>
          (revised <span class="emph gamma">2008-07</span>).
       </li>
-          <li>
+          <li class="">
             <span class="emph beta">2009-09.</span>
          Jutting's specification of Landau's "Grundlagen der Analysis"
          enters λδ Digital Library.
       </li>
-          <li>
+          <li class="">
             <span class="emph beta">2009-06.</span>
          Jutting's specification of Landau's "Grundlagen der Analysis"
          is successfully processed, enabling sort inclusion.
@@ -302,6 +302,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:34:08 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 9a7841afe..80293df24 100644
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -143,7 +143,7 @@
         <span class="emph gamma">February 2015.</span>
         <a href="http://lambdadelta.info/implementation.html#v2">"Helena 0.8.2"</a> is updated.
       <ul>
-          <li>
+          <li class="">
          The translated specification of Landau's "Grundlagen der Analysis"
          is validated in CC by <a href="http://coq.inria.fr/">Coq 8.4.3</a>. 
       </li>
@@ -162,7 +162,7 @@
         <span class="emph gamma">December 2014.</span>
         <a href="http://lambdadelta.info/implementation.html#v2">"Helena 0.8.2"</a> is released.
       <ul>
-          <li>
+          <li class="">
          The corrected specification of Landau's "Grundlagen der Analysis"
          is validated in λδ version 3. 
       </li>
@@ -193,13 +193,13 @@
         <span class="emph alpha">December 2012.</span>
       The character "_" is removed from the denomination "lambda_delta":
       <ul>
-          <li>
+          <li class="">
          The denomination "\lambda\delta" is used in λδ-related texts.
       </li>
-          <li>
+          <li class="">
          The denomination "lambdadelta" is used in λδ-related identifiers.
       </li>
-          <li>
+          <li class="">
          Permanent λδ URL acquired:
          <a href="http://lambdadelta.info/">http://lambdadelta.info/</a>
          (pointing at this site).
@@ -212,15 +212,15 @@
         <span class="emph alpha">September 2011.</span>
       The denomination "lambda-delta" changes to "lambda_delta":
       <ul>
-          <li>
+          <li class="">
          The character "-" is reserved in λδ textual syntax
          (recognized by "Helena 0.8.1").            
       </li>
-          <li>
+          <li class="">
          Eventually, the occurrences of the character "-"
          will be replaced by "_" in all λδ-related identifiers.
       </li>
-          <li>
+          <li class="">
          In particular, this refactoring involves file names and path names.
       </li>
         </ul>
@@ -380,6 +380,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:41 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:34:08 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/osn.html b/helm/www/lambdadelta/osn.html
index e367a682d..db9208073 100644
--- a/helm/www/lambdadelta/osn.html
+++ b/helm/www/lambdadelta/osn.html
@@ -31,10 +31,9 @@
       In order to meet these design goals, OSN pursues the following features.
    </div>
     <ul xmlns:ld="http://lambdadelta.info/">
-      <span class="red-mark">
-        <li>
-          <span class="alpha">
-            <a href="https://en.wikipedia.org/wiki/S-expression">Symbolic expressions</a>
+      <li class="red-mark">
+        <span class="alpha">
+          <a href="https://en.wikipedia.org/wiki/S-expression">Symbolic expressions</a>
       based on widely accepted syntactical conventions
       provide for a <span class="emph ">lightweight</span> and <span class="emph ">generic</span> grammar,
       which is both <span class="emph ">easy for machines to process</span>,
@@ -49,12 +48,10 @@
       Apparently, these features fall outside the scope of OSN,
       which targets the data structures of <span class="emph ">formal languages</span>. 
    </span>
-        </li>
-      </span>
+      </li>
       <br />
-      <span class="blue-mark">
-        <li>
-          <span class="alpha">
+      <li class="blue-mark">
+        <span class="alpha">
       Optionally <a href="https://en.wikipedia.org/wiki/Namespace">qualified</a> symbolic expressions 
       allow OSN texts to mix data from different domains preserving their own semantics
       because name conflicts can be avoided.
@@ -62,20 +59,17 @@
       domain-specific OSN applications can work as expected even if
       data from different domains is added to the text they process.
    </span>
-        </li>
-      </span>
+      </li>
       <br />
-      <span class="green-mark">
-        <li>
-          <span class="alpha">
+      <li class="green-mark">
+        <span class="alpha">
       The <a href="https://en.wikipedia.org/wiki/ASCII">US-ASCII</a> character set,
       extended to <a href="http://www.utf-8.com/">UTF-8</a> in
       free-form text strings for the convenience of human readers,
       makes OSN documents <span class="emph ">easy to visualize and transport</span> over communication media.
       OSN design aims at supporting <span class="emph ">application-independent</span> standard encodings.
    </span>
-        </li>
-      </span>
+      </li>
     </ul>
     <div xmlns:ld="http://lambdadelta.info/" class="head2dx" id="grammar">Grammar <img class="icon37" alt="[butterfly]" title="\lambda\delta butterfly" src="http://lambdadelta.info/images/b6.png" />
     </div>
@@ -87,43 +81,43 @@
       and are available for extensions of OSN.
    </div>
     <ul xmlns:ld="http://lambdadelta.info/">
-      <li>
+      <li class="">
       This token can represent the identifiers and the numerical constants of most programming languages:
       <br />
         <span class="emph ebnf">symbol = 1 * symbol-char ; <br />symbol-char = '+' | '-' | '.' | '0' | ... | '9' | 'A' | ... | 'Z' | '_' | '`' | 'a' | ... | 'z' ; </span>
       </li>
       <br />
-      <li>
+      <li class="">
       This token contains free-form text with commonly accepted escape sequences:
       <br />
         <span class="emph ebnf">string = '"' , * ( string-char | "'" | '\' escape ) , '"' ; <br />string-char = ( #0 | ... | #10FFFF ) - ( #0 | ... | #1F | "'" | '\' | '"' | #7F ) ; <br />escape = 1 * space | '"' | "'" | '(' | ')' | '0' | '\' | 'a' | 'b' | 'e' | 'f' | 'n' | 'r' | 't' | ( 'u' , 4 * 4 hex ) | 'v' | ( 'x' , 2 * 2 hex ) ; <br />space = #9 | ... | #D | #20 ; <br />hex = '0' | ... | '9' | 'A' | ... | 'F' | 'a' | ... | 'f' ; </span>
       </li>
       <br />
-      <li>
+      <li class="">
       This token is a widely used alternative of the former token:
       <br />
         <span class="emph ebnf">string-alt = "'" , * ( string-char | '"' | '\' escape ) , "'" ; </span>
       </li>
       <br />
-      <li>
+      <li class="">
       This token separates the qualifiers of a symbolic expression:
       <br />
         <span class="emph ebnf">sep = ':' ; </span>
       </li>
       <br />
-      <li>
+      <li class="">
       This token starts a compound symbolic expression:
       <br />
         <span class="emph ebnf">open = '(' | '&lt;' | '[' | '{' ; </span>
       </li>
       <br />
-      <li>
+      <li class="">
       This token ends a compound symbolic expression:
       <br />
         <span class="emph ebnf">close = ')' | '&gt;' | ']' | '}' ; </span>
       </li>
       <br />
-      <li>
+      <li class="">
       This token is ignored and separates the other tokens:
       <br />
         <span class="emph ebnf">gap = space | ',' | ';' | '=' ; </span>
@@ -134,19 +128,19 @@
       Spaces of the form <span class="emph ebnf">1 * gap </span> can appear between any pair of tokens.
    </div>
     <ul xmlns:ld="http://lambdadelta.info/">
-      <li>
+      <li class="">
       An OSN text:
       <br />
         <span class="emph ebnf">text = * q-expr ; </span>
       </li>
       <br />
-      <li>
+      <li class="">
       A qualified symbolic expression:
       <br />
         <span class="emph ebnf">q-expr = * ( symbol , 1 * sep ) , expr ; </span>
       </li>
       <br />
-      <li>
+      <li class="">
       An unqualified symbolic expression:
       <br />
         <span class="emph ebnf">expr = symbol | string | string-alt | ( open , text , close ) ; </span>
@@ -193,6 +187,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:41 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:37:02 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index f93c67c62..fb8b6d6bd 100644
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -293,7 +293,7 @@
          Source scripts.
          <a href="http://lambdadelta.info/documentation.html#ldJ1a">Documentation (J1a)</a>.
          <ul>
-            <li>
+            <li class="">
               <span class="emph delta">2015 January 15.</span>
             17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
          </li>
@@ -310,28 +310,28 @@
       (revised <span class="emph delta">2011-09</span>).
       Static HTML pages generated by the <a href="http://helm.cs.unibo.it/">HELM</a> rendering engine.  
       <ul>
-          <li>
+          <li class="">
             <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
             Confluence of reduction</a>
          (Church-Rosser property).
       </li>
-          <li>
+          <li class="">
             <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">
             Correctness of types</a>.
       </li>
-          <li>
+          <li class="">
             <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">
             Uniqueness of types up to conversion</a>.
       </li>
-          <li>
+          <li class="">
             <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/pr3/ty3_sred_pr3.con.html">
             Subject reduction of the type assignment</a>.
       </li>
-          <li>
+          <li class="">
             <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/arity_props/ty3_sn3.con.html">
             Strong normalization of the typed terms</a>.
       </li>
-          <li>
+          <li class="">
             <a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">
             Decidability of the type inference problem</a>.
       </li>
@@ -378,6 +378,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:08:42 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Fri, 22 Jul 2016 19:34:08 +0200</div>
   </body>
 </html>
diff --git a/helm/www/lambdadelta/web/home/osn.ldw.xml b/helm/www/lambdadelta/web/home/osn.ldw.xml
index 1f5601058..54589fe20 100644
--- a/helm/www/lambdadelta/web/home/osn.ldw.xml
+++ b/helm/www/lambdadelta/web/home/osn.ldw.xml
@@ -13,7 +13,7 @@
       generic abstract syntax trees in the domain of formal languages.
       In order to meet these design goals, OSN pursues the following features.
    </body>
-   <list><style class="red-mark"><item><style class="alpha">
+   <list><item class="red-mark"><style class="alpha">
       <link to="https://en.wikipedia.org/wiki/S-expression">Symbolic expressions</link>
       based on widely accepted syntactical conventions
       provide for a <notice text="lightweight"/> and <notice text="generic"/> grammar,
@@ -28,24 +28,22 @@
       as well as the support for canonicalization.
       Apparently, these features fall outside the scope of OSN,
       which targets the data structures of <notice text="formal languages"/>. 
-   </style></item></style>
-   <newline/>
-   <style class="blue-mark"><item><style class="alpha">
+   </style></item><newline/>
+   <item class="blue-mark"><style class="alpha">
       Optionally <link to="https://en.wikipedia.org/wiki/Namespace">qualified</link> symbolic expressions 
       allow OSN texts to mix data from different domains preserving their own semantics
       because name conflicts can be avoided.
       As a consequence OSN documents are <notice text="easy to extend"/> in that
       domain-specific OSN applications can work as expected even if
       data from different domains is added to the text they process.
-   </style></item></style>
-   <newline/>
-   <style class="green-mark"><item><style class="alpha">
+   </style></item><newline/>
+   <item class="green-mark"><style class="alpha">
       The <link to="https://en.wikipedia.org/wiki/ASCII">US-ASCII</link> character set,
       extended to <link to="http://www.utf-8.com/">UTF-8</link> in
       free-form text strings for the convenience of human readers,
       makes OSN documents <notice text="easy to visualize and transport"/> over communication media.
       OSN design aims at supporting <notice text="application-independent"/> standard encodings.
-   </style></item></style></list>
+   </style></item></list>
 
    <section6 name="grammar">Grammar</section6>
 
diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl
index 56ab24894..b574a4125 100644
--- a/helm/www/lambdadelta/xslt/ld_web_root.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl
@@ -151,7 +151,7 @@
 </xsl:template>
 
 <xsl:template match="ld:item">
-   <li><xsl:apply-templates/></li>
+   <li class="{@class}"><xsl:apply-templates/></li>
 </xsl:template>
 
 <xsl:template match="ld:style">