From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 10 Aug 2014 18:42:56 +0000 (+0000)
Subject: - update in basic_2
X-Git-Tag: make_still_working~856
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=85155a59a3986914b005d7e7edd7351d8090e234

- update in basic_2
- minor update to the web site
---

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 30791b955..569e860f1 100644
--- 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: Thu, 07 Aug 2014 19:13:43 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 10 Aug 2014 20:37:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index 455542b95..bf8b58182 100644
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -191,6 +191,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 07 Aug 2014 19:13:43 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 10 Aug 2014 20:37:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index d8633e5ff..8726a8ae7 100644
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -60,18 +60,18 @@
             <td class="snns italic cyan">files</td>
             <td class="snnn right italic cyan">367</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">431848</td>
+            <td class="snnn right italic cyan">431944</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">1830463</td>
+            <td class="ssnn right italic cyan">1830639</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
             <td class="snnn right italic green">128</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">1303</td>
+            <td class="snnn right italic green">1304</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">1431</td>
+            <td class="ssnn right italic green">1432</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
@@ -85,6 +85,8 @@
         </tbody>
       </table>
     </div>
+
+   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="">Stage "B"</div>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="date">In progress.</span>
@@ -92,6 +94,8 @@
          for native type assignment.
    </li>
     </ul>
+
+   <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="">Stage "A": "Weakening the Applicability Condition"</div>
    <ul xmlns:ld="http://lambdadelta.info/">
       <li>
         <span class="date">2014 June 18.</span>
@@ -416,7 +420,7 @@
               <br />
             </td>
             <td class="snns top cyan">csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )</td>
-            <td class="snnn top cyan">csx_tstc_vector csx_aaa</td>
+            <td class="snnn top cyan">csx_tsts_vector csx_aaa</td>
             <td class="snnn top cyan">
               <br />
             </td>
@@ -534,7 +538,7 @@
               <br />
             </td>
             <td class="snns top cyan">cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )</td>
-            <td class="snnn top cyan">cpxs_tstc cpxs_tstc_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs</td>
+            <td class="snnn top cyan">cpxs_tsts cpxs_tsts_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs</td>
             <td class="snnn top cyan">
               <br />
             </td>
@@ -576,7 +580,7 @@
             <td class="nnns top capitalize italic cyan">
               <br />
             </td>
-            <td class="snns top italic cyan">local env. ref. for abstract candidates of reducibility</td>
+            <td class="snns top italic cyan">local env. ref. for generic reducibility</td>
             <td class="snns top cyan">lsubc ( ? ⊢ ? ⫃[?] ? )</td>
             <td class="snnn top cyan">lsubc_drop lsubc_drops lsubc_lsuba</td>
             <td class="snnn top cyan">
@@ -590,10 +594,10 @@
             <td class="nnns top capitalize italic cyan">
               <br />
             </td>
-            <td class="snns top italic cyan">support for abstract computation properties</td>
-            <td class="snns top cyan">acp</td>
-            <td class="snnn top cyan">acp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )</td>
-            <td class="snnn top cyan">acp_aaa</td>
+            <td class="snns top italic cyan">support for generic computation properties</td>
+            <td class="snns top cyan">gcp</td>
+            <td class="snnn top cyan">gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )</td>
+            <td class="snnn top cyan">gcp_aaa</td>
             <td class="ssnn top cyan">
               <br />
             </td>
@@ -1036,11 +1040,11 @@
             <td class="nnns top capitalize italic yellow">
               <br />
             </td>
-            <td class="snns top italic yellow">support for generic relocation</td>
-            <td class="snns top yellow">gr2 ( @⦃?,?⦄ ≡ ? )</td>
-            <td class="snnn top yellow">gr2_plus ( ? + ? )</td>
-            <td class="snnn top yellow">gr2_minus ( ? ▭ ? ≡ ? )</td>
-            <td class="ssnn top yellow">gr2_gr2</td>
+            <td class="snns top italic yellow">support for multiple relocation</td>
+            <td class="snns top yellow">mr2 ( @⦃?,?⦄ ≡ ? )</td>
+            <td class="snnn top yellow">mr2_plus ( ? + ? )</td>
+            <td class="snnn top yellow">mr2_minus ( ? ▭ ? ≡ ? )</td>
+            <td class="ssnn top yellow">mr2_mr2</td>
           </tr>
           <tr>
             <td class="snns top capitalize italic orange">substitution</td>
@@ -1188,9 +1192,9 @@
             <td class="nnns top capitalize italic red">
               <br />
             </td>
-            <td class="snns top italic red">same top term constructor</td>
-            <td class="snns top red">tstc ( ? ≂ ? )</td>
-            <td class="snnn top red">tstc_tstc tstc_vector</td>
+            <td class="snns top italic red">same top term structure</td>
+            <td class="snns top red">tsts ( ? ≂ ? )</td>
+            <td class="snnn top red">tsts_tsts tsts_vector</td>
             <td class="snnn top red">
               <br />
             </td>
@@ -1320,6 +1324,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 07 Aug 2014 19:13:43 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 10 Aug 2014 20:37:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index 9dcf6aaf2..bc3db1d98 100644
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -333,6 +333,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 07 Aug 2014 19:13:43 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 10 Aug 2014 20:37:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 463a398fe..e1d8597a9 100644
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -234,6 +234,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 07 Aug 2014 19:13:43 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 10 Aug 2014 20:37:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 450f6a6ba..280cf254b 100644
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -107,7 +107,7 @@
             <td class="snnn top orange">
               <a href="http://matita.cs.unibo.it/">Matita 0.99.2</a>
             </td>
-            <td class="snnn top orange">"a"</td>
+            <td class="snnn top orange">"A"</td>
             <td class="snnn top orange">April 2011</td>
             <td class="snnn top orange">July 2014</td>
             <td class="snnn top orange">Planned in 2014</td>
@@ -266,6 +266,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 07 Aug 2014 19:13:43 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 10 Aug 2014 20:37:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index 944beb7ba..58aef1be4 100644
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -135,6 +135,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 07 Aug 2014 19:13:43 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 10 Aug 2014 20:37:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index 76152d9c5..83ffc3a4d 100644
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -303,6 +303,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 07 Aug 2014 19:13:43 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 10 Aug 2014 20:37:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html
index 90e8326b3..225072623 100644
--- a/helm/www/lambdadelta/version_1.html
+++ b/helm/www/lambdadelta/version_1.html
@@ -167,6 +167,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 07 Aug 2014 19:13:43 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 10 Aug 2014 20:37:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html
index bbd38fe2f..1b2d8119c 100644
--- a/helm/www/lambdadelta/version_2.html
+++ b/helm/www/lambdadelta/version_2.html
@@ -131,6 +131,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Thu, 07 Aug 2014 19:13:43 +0200</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Sun, 10 Aug 2014 20:37:31 +0200</div>
 </body>
 </html>
diff --git a/helm/www/lambdadelta/web/home/versions.tbl b/helm/www/lambdadelta/web/home/versions.tbl
index e8bb5117b..5c4112e16 100644
--- a/helm/www/lambdadelta/web/home/versions.tbl
+++ b/helm/www/lambdadelta/web/home/versions.tbl
@@ -7,7 +7,7 @@ table {
       ] 
    class "orange" 
       [ @@("version_2" "Version 2") "\"basic_2\"" @("http://matita.cs.unibo.it/" "Matita 0.99.2")
-        "\"a\"" "April 2011" "July 2014" "Planned in 2014" "Not planned yet"
+        "\"A\"" "April 2011" "July 2014" "Planned in 2014" "Not planned yet"
       ] 
    class "red"
       [ @@("version_1" "Version 1") "\"basic_1\"" @("http://coq.inria.fr/" "Coq 7.3.1")
diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl
index d0024b8dc..014d2e65e 100644
--- a/helm/www/lambdadelta/xslt/ld_web_root.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl
@@ -62,6 +62,12 @@
    </div>
 </xsl:template>
 
+<xsl:template match="ld:subsection">
+   <div class="head3sn" id="{@name}">
+      <xsl:apply-templates/>
+   </div>
+</xsl:template>
+
 <xsl:template match="ld:body">
    <div class="text">
       <xsl:apply-templates/>