X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fwww%2Flambdadelta%2Fimplementation.html;h=cb9b23247edeb484cfdd1f099750506ba2d81ebb;hb=47293eadb6240cdfa50cc9571aeddcc85b229b51;hp=75a81d02f1b46109f3ca07baf8dae94ee2fabe00;hpb=a255d83ebcb9b700a6f30cbcd109d223fc0d98cb;p=helm.git

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 75a81d02f..cb9b23247 100644
--- 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>