syntactic components detached from basic_2 become static_2

[helm.git] / helm / www / lambdadelta / web / home / specification.ldw.xml
diff --git a/helm/www/lambdadelta/web/home/specification.ldw.xml b/helm/www/lambdadelta/web/home/specification.ldw.xml

index a489b47a8f2ca93d61cea3d4d4a52ea84d1cbb91..c58b253a82f0fd6a6cabe3f58105f4ed55d87914 100644 (file)
--- a/helm/www/lambdadelta/web/home/specification.ldw.xml
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -3,6 +3,7 @@
  <page xmlns="http://lambdadelta.info/"
        description = "\lambda\delta home page"
        title = "\lambda\delta home page"
+      logo = "crux"
        head = "The Formal Systems of the λδ (\lambda\delta) Family"
  >
     <sitemap name="sitemap"/>
@@ -44,9 +45,17 @@
        introduced in each script, is shown in parentheses (? are placeholders).
     </topitem>
  
+<!-- VERSION 3 =========================================================== -->
+
+   <subsection name="v3"><img logo="ld3"/>λδ version 3 (proposed)</subsection>
+   <body>
+      The formal specification of λδ version 3
+      is forthcoming.
+   </body>
+
  <!-- VERSION 2 =========================================================== -->
  
-   <subsection name="v2"><version2-icon/>λδ version 2 (active)</subsection>
+   <subsection name="v2"><img logo="ld2"/>λδ version 2 (active)</subsection>
     <body>
        The formal specification of λδ version 2
        is available in the following formats:
@@ -56,8 +65,8 @@
        <body>
           <rlink to="download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</rlink>
           (revised <notice class="gamma" text="2014-10"/>).
-         Source scripts.
-         <rlink to="documentation.html#ldR2c">Documentation (R2c)</rlink>.
+         Source scripts [Svn revision: 12964].
+         <rlink to="html/documentation.html#ldR2c">Documentation (R2c)</rlink>.
        </body>
        <body>
           The scripts are grouped in directories, first by part, then by component.
@@ -72,14 +81,15 @@
  
     <body>
        Informational pages on the parts of the specification:
-      <rlink to="ground_2.html">Background</rlink>,
-      <rlink to="basic_2.html">Core</rlink>,
-      <rlink to="apps_2.html">Applications</rlink>.
+      <rlink to="html/ground_2.html">Background</rlink>,
+      <rlink to="html/static_2.html">Syntax</rlink>,
+      <rlink to="html/basic_2.html">Core</rlink>,
+      <rlink to="html/apps_2.html">Applications</rlink>.
     </body>
  
  <!-- VERSION 1 =========================================================== -->
  
-   <subsection name="v1"><version1-icon/>λδ version 1 (superseded)</subsection>
+   <subsection name="v1"><img logo="ld1"/>λδ version 1 (superseded)</subsection>
     <body>
        The formal specification of λδ version 1
        is available in the following formats:
@@ -90,7 +100,7 @@
           <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
           (revised <notice class="delta" text="2015-09"/>).
           Source scripts.
-         <rlink to="documentation.html#ldJ1a">Documentation (J1a)</rlink>.
+         <rlink to="html/documentation.html#ldJ1a">Documentation (J1a)</rlink>.
           <list><item>
              <notice class="delta" text="2015 January 15."/>
              17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
@@ -137,8 +147,8 @@
  
     <body>
        Informational pages on the parts of the specification:
-      <rlink to="ground_1.html">Background</rlink>,
-      <rlink to="basic_1.html">Core</rlink>.
+      <rlink to="html/ground_1.html">Background</rlink>,
+      <rlink to="html/basic_1.html">Core</rlink>.
     </body>
  
     <footer/>