first article on lambdadelta version 3

diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html
index 1e6bf7d9c604b03ba6029aaae82485df2807b864..1883ffc4e87edff65f2420f8a8c03632e7340acb 100644 (file)
--- 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: Wed, 21 Jan 2015 17:13:08 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Feb 2015 19:13:36 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html
index a4ec380fb559768f450d6009d943c71f5a77c4d1..4a9d8c6953451b80ef2647b524fa9bf1b9c7bea3 100644 (file)
--- a/helm/www/lambdadelta/apps_2.html
+++ b/helm/www/lambdadelta/apps_2.html
@@ -152,29 +152,29 @@
           <tr>
             <td class="snns capitalize italic cyan">sizes</td>
             <td class="snns italic cyan">files</td>
-            <td class="snnn right italic cyan">14</td>
+            <td class="snnn right italic cyan">4</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">6787</td>
+            <td class="snnn right italic cyan">68581</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">10070</td>
+            <td class="ssnn right italic cyan">3637</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
             <td class="snns italic green">theorems</td>
             <td class="snnn right italic green">2</td>
             <td class="snns italic green">lemmas</td>
-            <td class="snnn right italic green">4</td>
+            <td class="snnn right italic green">1</td>
             <td class="snns italic green">total</td>
-            <td class="ssnn right italic green">6</td>
+            <td class="ssnn right italic green">3</td>
           </tr>
           <tr>
             <td class="snss capitalize italic yellow">concepts</td>
             <td class="snss italic yellow">declared</td>
-            <td class="snsn right italic yellow">6</td>
+            <td class="snsn right italic yellow">3</td>
             <td class="snss italic yellow">defined</td>
-            <td class="snsn right italic yellow">11</td>
+            <td class="snsn right italic yellow">9</td>
             <td class="snss italic yellow">total</td>
-            <td class="sssn right italic yellow">17</td>
+            <td class="sssn right italic yellow">12</td>
           </tr>
         </tbody>
       </table>
@@ -258,6 +258,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Feb 2015 19:13:36 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_1.html b/helm/www/lambdadelta/basic_1.html
index 0965840d7350a893b427334cea26c57b53ad1bf6..1a5a6c8f3e0c8315a9eb75bd29b3dcd05529146a 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">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Feb 2015 19:13:37 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html
index ca505d6478418a441ca2a055c673334f85ee63e0..af07faf971708044c1b61787a002c3d7460d2bd9 100644 (file)
--- a/helm/www/lambdadelta/basic_2.html
+++ b/helm/www/lambdadelta/basic_2.html
@@ -148,7 +148,7 @@
             <td class="snns italic cyan">characters</td>
             <td class="snnn right italic cyan">433402</td>
             <td class="snns italic cyan">nodes</td>
-            <td class="ssnn right italic cyan">1874778</td>
+            <td class="ssnn right italic cyan">1874774</td>
           </tr>
           <tr>
             <td class="snns capitalize italic green">propositions</td>
@@ -1384,6 +1384,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Feb 2015 19:13:36 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/documentation.html b/helm/www/lambdadelta/documentation.html
index ffa999aa230e6b4d30e76af2071122fe7629729a..2171f585557e72f048ac918426ada644ce21363f 100644 (file)
--- a/helm/www/lambdadelta/documentation.html
+++ b/helm/www/lambdadelta/documentation.html
@@ -112,6 +112,29 @@
       <a href="http://lambdadelta.info/download/lambdadelta.txt">lambdadelta.txt</a>
       (revised <span class="emph gamma">2014-10</span>).
    </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v3">
+      <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b8.png" /> λδ version 3 (proposed)</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      The main source of information is <span class="emph alpha">J4</span>.
+   </div>
+    <div xmlns:ld="http://lambdadelta.info/" class="text">
+      <table cellpadding="4" cellspacing="0">
+        <tbody>
+          <tr>
+            <td class="snns top" id="ldJ4">
+              <span class="emph alpha">J4.</span>
+            </td>
+            <td class="ssnn top">F. Guidi: <a href="http://lambdadelta.info/download/gda.pdf">A Verified Translation of Landau's "Grundlagen" from Automath into a Pure Type System, via λδ</a> (<span class="emph alpha">2015-02</span>). Submitted to JFR, Univerity of Bologna.</td>
+          </tr>
+          <tr>
+            <td class="nnss top" />
+            <td class="nssn top">
+              <br />
+            </td>
+          </tr>
+        </tbody>
+      </table>
+    </div>
     <div xmlns:ld="http://lambdadelta.info/" class="head3sn" id="v2">
       <img class="icon37" alt="[spacer]" title="lambdadelta butterfly" src="http://lambdadelta.info/images/b4.png" /> λδ version 2 (active)</div>
     <div xmlns:ld="http://lambdadelta.info/" class="text">
@@ -366,6 +389,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Feb 2015 19:13:35 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/download/gda.pdf b/helm/www/lambdadelta/download/gda.pdf
new file mode 100644 (file)
index 0000000..70ffdd3
Binary files /dev/null and b/helm/www/lambdadelta/download/gda.pdf differ

diff --git a/helm/www/lambdadelta/ground_1.html b/helm/www/lambdadelta/ground_1.html
index 7c788ec666585cdc94198416340d873d66cbb628..187b2b3c61378d0da59561b52c604cd7cf41a985 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">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Feb 2015 19:13:36 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html
index 17b7562e305eaad3830853aa26f4cd43b616eee0..0c631baac4f4bbceb701aff4be658d01f96359ce 100644 (file)
--- a/helm/www/lambdadelta/ground_2.html
+++ b/helm/www/lambdadelta/ground_2.html
@@ -134,7 +134,7 @@
             <td class="snns italic cyan">files</td>
             <td class="snnn right italic cyan">30</td>
             <td class="snns italic cyan">characters</td>
-            <td class="snnn right italic cyan">46649</td>
+            <td class="snnn right italic cyan">68581</td>
             <td class="snns italic cyan">nodes</td>
             <td class="ssnn right italic cyan">62380</td>
           </tr>
@@ -328,6 +328,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Feb 2015 19:13:36 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/images/b8.png b/helm/www/lambdadelta/images/b8.png
new file mode 100644 (file)
index 0000000..d2638f8
Binary files /dev/null and b/helm/www/lambdadelta/images/b8.png differ

diff --git a/helm/www/lambdadelta/implementation.html b/helm/www/lambdadelta/implementation.html
index 82dcacfd5db933f2ca7bbc10168ec928ea5d6ca2..d9285e579bf23ff7d715dc657195eb0e362b001b 100644 (file)
--- a/helm/www/lambdadelta/implementation.html
+++ b/helm/www/lambdadelta/implementation.html
@@ -255,6 +255,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Feb 2015 19:13:36 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html
index afc6f7d8a9401fed265a5822e96ff71d51d91381..2fd519a642b46899c6f2aa8ef70bb213912ca1ea 100644 (file)
--- a/helm/www/lambdadelta/index.html
+++ b/helm/www/lambdadelta/index.html
@@ -202,6 +202,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Feb 2015 19:13:35 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html
index a1dfcd5903c13ad7d314762f4b0c3d8ba3956282..bfaf3b9c998dcd1b9ce78ac81cddfeb19eb71555 100644 (file)
--- a/helm/www/lambdadelta/news.html
+++ b/helm/www/lambdadelta/news.html
@@ -335,6 +335,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Feb 2015 19:13:35 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/specification.html b/helm/www/lambdadelta/specification.html
index 464ace8317f729f85f2ccbb357a0b4bcbc4bb887..29fe9706633871c8005a9d38d9a2720aa5c12852 100644 (file)
--- a/helm/www/lambdadelta/specification.html
+++ b/helm/www/lambdadelta/specification.html
@@ -328,6 +328,6 @@
     <div xmlns:ld="http://lambdadelta.info/" class="spacer">
       <br />
     </div>
-    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 21 Jan 2015 17:13:08 +0100</div>
+    <div xmlns:ld="http://lambdadelta.info/" class="spacer">Last update: Wed, 18 Feb 2015 19:13:36 +0100</div>
   </body>
 </html>

diff --git a/helm/www/lambdadelta/web/home/documentation.ldw.xml b/helm/www/lambdadelta/web/home/documentation.ldw.xml
index 01bda01915daf4b9a036baa1c1d2bdb520239b21..a51f64307e740bf753974dde89a84b41d80f7cd8 100644 (file)
--- a/helm/www/lambdadelta/web/home/documentation.ldw.xml
+++ b/helm/www/lambdadelta/web/home/documentation.ldw.xml
@@ -16,6 +16,12 @@
       <rlink to="download/lambdadelta.txt">lambdadelta.txt</rlink>
       (revised <notice class="gamma" notice="2014-10"/>).
    </body>
+
+   <subsection name="v3"><version3-icon/>λδ version 3 (proposed)</subsection>
+   <body>
+      The main source of information is <notice class="alpha" notice="J4"/>.
+   </body>
+   <table name="documentation_3"/>
    
    <subsection name="v2"><version2-icon/>λδ version 2 (active)</subsection>
    <body>

diff --git a/helm/www/lambdadelta/web/home/documentation_3.tbl b/helm/www/lambdadelta/web/home/documentation_3.tbl
new file mode 100644 (file)
index 0000000..ec291e0
--- /dev/null
+++ b/helm/www/lambdadelta/web/home/documentation_3.tbl
@@ -0,0 +1,14 @@
+name "documentation_3"
+
+table {
+   [ { name "ldJ4" "<span class=\"emph alpha\">J4.</span>" "" } {
+     "F. Guidi:" +
+     @@("download/gda.pdf"
+     "A Verified Translation of Landau's \"Grundlagen\" from Automath into a Pure Type System, via λδ") +
+     "(<span class=\"emph alpha\">2015-02</span>)." +
+     "Submitted to JFR, Univerity of Bologna."
+     * }
+   ]
+}
+
+class "top" [ * ]

diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl
index 8c2c3ad3949300b3ed505f761ceb3b7520a99bb9..f47a9a942db1bce60225da54343946d1ee47bb3a 100644 (file)
--- a/helm/www/lambdadelta/xslt/ld_web_root.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl
@@ -52,6 +52,16 @@
    </div>
 </xsl:template>
 
+<xsl:template match="ld:section8">
+   <div class="head2dx" id="{@name}">
+      <xsl:apply-templates/>
+      <xsl:call-template name="sp"/>
+      <xsl:call-template name="butterfly">
+         <xsl:with-param name="name" select="8"/>
+      </xsl:call-template>
+   </div>
+</xsl:template>
+
 <xsl:template match="ld:section9">
    <div class="head2dx" id="{@name}">
       <xsl:apply-templates/>
@@ -124,6 +134,13 @@
    <span class="emph {@class}"><xsl:value-of select="@notice"/></span>
 </xsl:template>
 
+<xsl:template match="ld:version3-icon">
+   <xsl:call-template name="butterfly">
+      <xsl:with-param name="name" select="8"/>
+   </xsl:call-template>
+   <xsl:call-template name="sp"/>
+</xsl:template>
+
 <xsl:template match="ld:version2-icon">
    <xsl:call-template name="butterfly">
       <xsl:with-param name="name" select="4"/>