update in web site and basic_2

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 1012526ed562d36ec7456eba8f51c98a8f2192f7..6206c24a1b928ae5757abbb18f1c928bf4a6cb18 100644 (file)
--- a/helm/www/lambdadelta/BTM.html
+++ b/helm/www/lambdadelta/BTM.html
@@ -223,6 +223,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 22 Feb 2014 12:36:18 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 24 Feb 2014 19:58:07 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 143dbad6e31baf3d9875ac4ee958f73cd2d682ed..6262941c8eca728fa9f32321bb27eb18c6d6e8c1 100644 (file)
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -6,8 +6,8 @@
     <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
     <meta http-equiv="Content-Style-Type" content="text/css" />
     <meta name="author" content="Ferruccio Guidi" />
-    <meta name="description" content="applications of lambdadelta version 2" />
-    <title>applications of lambdadelta version 2</title>
+    <meta name="description" content="applications of \lambda\delta version 2" />
+    <title>applications of \lambda\delta version 2</title>
     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
@@ -191,6 +191,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 22 Feb 2014 12:36:17 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 24 Feb 2014 19:58:07 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index 4f06fd3d0b1b495e4a17691e3d5c13fcc519486a..bbde8e1cf45d067ed3727363a9d833c9768bac5a 100644 (file)
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -6,8 +6,8 @@
     <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
     <meta http-equiv="Content-Style-Type" content="text/css" />
     <meta name="author" content="Ferruccio Guidi" />
-    <meta name="description" content="lambdadelta version 2" />
-    <title>lambdadelta version 2</title>
+    <meta name="description" content="\lambda\delta version 2" />
+    <title>\lambda\delta version 2</title>
     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
@@ -163,20 +163,20 @@
           <tr>
             <td class="snns component cyan">sizes</td>
             <td class="snns plane cyan">files</td>
-            <td class="snnn number cyan">328  </td>
+            <td class="snnn number cyan">329  </td>
             <td class="snns plane cyan">characters</td>
-            <td class="snnn number cyan">565577</td>
+            <td class="snnn number cyan">567347</td>
             <td class="snns plane cyan">nodes</td>
-            <td class="ssnn number cyan">1606912</td>
+            <td class="ssnn number cyan">1610281</td>
           </tr>
           <tr>
             <td class="snns component green">propositions</td>
             <td class="snns plane green">theorems</td>
             <td class="snnn number green">105</td>
             <td class="snns plane green">lemmas</td>
-            <td class="snnn number green">1109</td>
+            <td class="snnn number green">1114</td>
             <td class="snns plane green">total</td>
-            <td class="ssnn number green">1214</td>
+            <td class="ssnn number green">1219</td>
           </tr>
           <tr>
             <td class="snss component yellow">concepts</td>
@@ -541,7 +541,7 @@
             </td>
             <td class="snns file cyan">fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )</td>
             <td class="snnn file cyan">fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )</td>
-            <td class="snnn file cyan">fpbs_lift fpbs_aaa fpbs_fpns fpbs_fpbs</td>
+            <td class="snnn file cyan">fpbs_lift fpbs_aaa fpbs_fpns fpbs_fpbs fpbs_ext</td>
             <td class="ssnn file cyan">
               <br />
             </td>
@@ -1318,6 +1318,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 22 Feb 2014 12:36:18 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 24 Feb 2014 19:58:07 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 03e01a62d7ff12a5189e26bfca7b6253125e0ff2..ac460b90352cabda64166e0cb702f9ca1ca4aeef 100644 (file)
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -6,8 +6,8 @@
     <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
     <meta http-equiv="Content-Style-Type" content="text/css" />
     <meta name="author" content="Ferruccio Guidi" />
-    <meta name="description" content="lambdadelta version 2" />
-    <title>lambdadelta version 2</title>
+    <meta name="description" content="background for \lambda\delta version 2" />
+    <title>background for \lambda\delta version 2</title>
     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/ld_web.css" />
     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/lddl.css" />
     <link rel="stylesheet" type="text/css" href="http://lambdadelta.info/css/xhtbl.css" />
@@ -234,6 +234,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sat, 22 Feb 2014 12:36:18 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Mon, 24 Feb 2014 19:58:07 +0100</div>
 </body>
 </html>

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 75a81d02f1b46109f3ca07baf8dae94ee2fabe00..cb9b23247edeb484cfdd1f099750506ba2d81ebb 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -55,42 +55,42 @@
               paper (as it happens for most currently digitalized
               Mathematics).<br>
               <ol>
-                <li><a name="static"></a>F. Guidi: <a style="font-style: italic;" href="static/matita/lambdadelta/">lambdadelta</a>
+                <li><a name="static"></a>F. Guidi: <a style="font-style: italic;" href="http://lambdadelta.info/static/matita/lambdadelta/">lambdadelta</a>
                   (revised <span style="font-weight: bold;">2011-09</span>).
                   Formal
                   specification for <a href="http://matita.cs.unibo.it/">Matita</a> 0.5
                   (HTML pages generated
                   by the <a href="http://helm.cs.unibo.it/">HELM</a>
-                  rendering engine)<br>
+                  rendering engine)
                   Here are the most relevant theorems proved in the
                   formal specification:
                   <ul>
-                    <li><a href="static/matita/lambdadelta/Basic_1/pr3/pr3/pr3_confluence.con.html">Confluence
+                    <li><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><a href="static/matita/lambdadelta/Basic_1/ty3/props/ty3_correct.con.html">Correctness
+                    <li><a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_correct.con.html">Correctness
                         of
                         types</a>.</li>
-                    <li><a href="static/matita/lambdadelta/Basic_1/ty3/props/ty3_unique.con.html">Uniqueness
+                    <li><a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/props/ty3_unique.con.html">Uniqueness
                         of
                         types
                         up
                         to
                         conversion</a>.<br>
                     </li>
-                    <li><a href="static/matita/lambdadelta/Basic_1/ty3/pr3/ty3_sred_pr3.con.html">Subject
+                    <li><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><a href="static/matita/lambdadelta/Basic_1/ty3/arity_props/ty3_sn3.con.html">Strong
+                    <li><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><a href="static/matita/lambdadelta/Basic_1/ty3/dec/ty3_inference.con.html">Decidability
+                    <li><a href="http://lambdadelta.info/static/matita/lambdadelta/basic_1/ty3/dec/ty3_inference.con.html">Decidability
                         of
                         the
                         type
@@ -104,9 +104,10 @@
                   (revised <span style="font-weight: bold;">2011-09</span>).
                   Formal
                   specification for <a href="http://matita.cs.unibo.it/">Matita</a> 0.5 (<a href="http://helm.cs.unibo.it/">HELM</a> directory).<br>
-                  <br>
+                  <span style="font-weight: bold;">Currently, the HELM rendering engine is offline.</span><br>
+                 <br>
                 </li>
-                <li><a name="ldp1"></a>F. Guidi: <a href="download/lambdadelta_1.tar.gz"><span style="font-style: italic;">lambdadelta_1</span></a>
+                <li><a name="ldp1"></a>F. Guidi: <a href="http://lambdadelta.info/download/lambdadelta_1.tar.gz"><span style="font-style: italic;">lambdadelta_1</span></a>
                   (revised <span style="font-weight: bold;">2012-10</span>).
 Formal
                   specification for <span style="font-weight: bold;">Coq
@@ -131,13 +132,13 @@ Formal
               </ul>
               <ul>
                 <li><span style="font-weight: bold;">Access:</span> <a
-href="static/lddl/">static pages</a> (updated <span style="font-weight: bold;">2012-10</span>), <a href="download/lddl.tar.bz2">data set</a> (updated <span style="font-weight: bold;">2012-10</span>), <a href="http://lambdadelta.info/xml/">HELM server URL</a>
+href="http://lambdadelta.info/static/lddl/">static pages</a> (updated <span style="font-weight: bold;">2012-10</span>), <a href="http://lambdadelta.info/download/lddl.tar.bz2">data set</a> (updated <span style="font-weight: bold;">2012-10</span>), <a href="http://lambdadelta.info/xml/">HELM server URL</a>
                   (updated <span style="font-weight: bold;">2012-10</span>).</li>
               </ul>
               <ul>
-                <li><span style="font-weight: bold;">Examples:</span> <a href="static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
+                <li><span style="font-weight: bold;">Examples:</span> <a href="http://lambdadelta.info/static/lddl/brg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
                     definition
-                    "t234"</a> (in "basic_rg" λδ), <a href="static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
+                    "t234"</a> (in "basic_rg" λδ), <a href="http://lambdadelta.info/static/lddl/crg_si/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.html">Grundlagen's
                     definition
                     "t234"</a> (in "complete_rg" λδ).<br>
                 </li>
@@ -176,7 +177,7 @@ href="static/lddl/">static pages</a> (updated <span style="font-weight: bold;">2
                     der
                     Analysis</span>" increases of 22% with respect to
                   version 0.8.0. [Svn
-                  revision: 11032] (<a href="download/helena_0.8.1.tar.gz">archived
+                  revision: 11032] (<a href="http://lambdadelta.info/download/helena_0.8.1.tar.gz">archived
                     source code</a>)
                   <ul>
                     <li><span style="font-weight: bold;">2009-12.</span>
@@ -197,7 +198,7 @@ computer
                   importation from <a href="http://www.win.tue.nl/automath/">Automath</a>
                   and exportation to <a href="http://www.w3.org/XML/">XML</a>.
                   [Svn
-                  revision: 10304] (<a href="download/helena_0.8.0.tar.gz">archived
+                  revision: 10304] (<a href="http://lambdadelta.info/download/helena_0.8.0.tar.gz">archived
                     source code</a>)<br>
                   <ul>
                     <li><span style="font-weight: bold;">2009-09.</span>
@@ -216,21 +217,21 @@ computer
               <h3 style="text-align: right;">Other resources <img style="width: 37px; height: 37px;" alt="[Butterfly]" title="Butterfly" src="images/b4.png"></h3>
               <ul>
                 <li><a name="bibtex"></a>A
-                  BibTeX database of λδ documentation: <a href="download/lambdadelta.bib"><span style="font-style: italic;">lambdadelta.bib</span></a>,
-                  <a style="font-style: italic;" href="download/lambdadelta.txt">lambdadelta.txt</a>
+                  BibTeX database of λδ documentation: <a href="http://lambdadelta.info/download/lambdadelta.bib"><span style="font-style: italic;">lambdadelta.bib</span></a>,
+                  <a style="font-style: italic;" href="http://lambdadelta.info/download/lambdadelta.txt">lambdadelta.txt</a>
                   (revised <span style="font-weight: bold;">2012-10</span>).</li>
               </ul>
               <ul>
                 <li>A <a href="http://www.jedsoft.org/jed/">Jed mode</a>
                   for
-                  editing ".hln" files (containing λδ textual syntax): <a style="font-style: italic;" href="download/helena.sl">helena.sl</a>
+                  editing ".hln" files (containing λδ textual syntax): <a style="font-style: italic;" href="http://lambdadelta.info/download/helena.sl">helena.sl</a>
                   (revised <span style="font-weight: bold;">2010-11</span>).</li>
               </ul>
               <ul>
                 <li>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 style="font-style: italic;" href="download/automath.sl">automath.sl</a>
+                  textual syntax): <a style="font-style: italic;" href="http://lambdadelta.info/download/automath.sl">automath.sl</a>
                   (revised <span style="font-weight: bold;">2008-07</span>).</li>
               </ul>
               <ul>
@@ -247,7 +248,7 @@ computer
           Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"></a> <a href="http://www.anybrowser.org/campaign/"><img alt="[Use Any
           Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"></a> <img style="width: 88px; height: 31px;" alt="[PNG Used Here]" title="PNG Used Here" src="images/PNGnow2.png"><br>
       <br>
-      Last update 2012-12-02 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+      Last update 2014-02-22 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
         Guidi</a><br>
     </div>
   

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 62e31753bd6040f68e34993f50db81b7756ddbd8..07e98c6a926e9ec182be6d56c1ff5853404fd173 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -92,7 +92,7 @@ includes the major milestones:<br>
             </td>
             <td style="vertical-align: top; background-color: rgb(255, 223, 191);">planned
 in
-2013<br>
+2014<br>
             </td>
             <td style="vertical-align: top; background-color: rgb(255, 223, 191);">not
 planned yet<br>
@@ -138,7 +138,7 @@ Options" entry → "General" tab → "Fonts" button.</span><br>
 <br>
 <a href="http://validator.w3.org/check?uri=referer"><img alt="[Valid HTML 4.01 Transitional]" title="Valid HTML 4.01 Transitional" src="http://www.w3.org/Icons/valid-html401" style="border: 0px solid ; width: 88px; height: 31px;"></a> <a href="http://www.anybrowser.org/campaign/"><img alt="[Use Any Browser Here]" title="Use Any Browser Here" src="images/globe_trans.png" style="border: 0px solid ; width: 147px; height: 42px;"></a> <img style="width: 88px; height: 31px;" alt="[PNG Used Here]" title="PNG Used Here" src="images/PNGnow2.png"><br>
 <br>
-Last update 2012-12-02 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
+Last update 2014-02-24 by <a href="http://www.cs.unibo.it/%7Efguidi/">Ferruccio
 Guidi</a><br>
 </div>