]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambdadelta/web/home/specification.ldw.xml
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
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 556549c393d00f5190ddc0d40f9f3c4440c27379..c58b253a82f0fd6a6cabe3f58105f4ed55d87914 100644 (file)
--- a/helm/www/lambdadelta/web/home/specification.ldw.xml
+++ b/helm/www/lambdadelta/web/home/specification.ldw.xml
@@ -3,27 +3,27 @@
 <page xmlns="http://lambdadelta.info/"
       description = "\lambda\delta home page"
       title = "\lambda\delta home page"
 <page xmlns="http://lambdadelta.info/"
       description = "\lambda\delta home page"
       title = "\lambda\delta home page"
-      head = "The Formal System λδ (\lambda\delta)"
+      logo = "crux"
+      head = "The Formal Systems of the λδ (\lambda\delta) Family"
 >
    <sitemap name="sitemap"/>
 
 >
    <sitemap name="sitemap"/>
 
-   <section5 name="specifications">Computer-checked formal specifications</section5>
+   <section15 name="specifications">Computer-checked formal specifications</section15>
    <body>
    <body>
-      λδ is developed as a machine-checked digital specification.
-      It comes in several versions listed in the next table,
-      which includes the major milestones.
+      The systems of the λδ family are developed as machine-checked digital specifications,
+      and are listed in the next table, which includes the major milestones.
    </body>
    <body>
       The life cycle of a specification consists of four periods.
    </body>
    <body>
       The life cycle of a specification consists of four periods.
-      <notice class="alpha" notice="Alpha:"/>
+      <notice class="alpha" text="Alpha:"/>
       the definitions are designed and the major propositions are proved,
       then the calculus is announced with a presentation.
       the definitions are designed and the major propositions are proved,
       then the calculus is announced with a presentation.
-      <notice class="beta" notice="Beta:"/>
+      <notice class="beta" text="Beta:"/>
       major changes and additions may occur before the calculus is released on paper.
       major changes and additions may occur before the calculus is released on paper.
-      <notice class="gamma" notice="Gamma:"/>
+      <notice class="gamma" text="Gamma:"/>
       subsequent improvements occur until the specification is completed or superseded,
       while major changes and additions are announced and reported on paper.
       subsequent improvements occur until the specification is completed or superseded,
       while major changes and additions are announced and reported on paper.
-      <notice class="delta" notice="Delta:"/>
+      <notice class="delta" text="Delta:"/>
       after its conclusion, the specification is modified just for maintenance. 
    </body>
    <table name="versions"/>
       after its conclusion, the specification is modified just for maintenance. 
    </body>
    <table name="versions"/>
@@ -31,23 +31,31 @@
    <body>
      Informational pages on the specifications are provided.
    </body>
    <body>
      Informational pages on the specifications are provided.
    </body>
-   <topitem>
-      <notice class="alpha" notice="Notice on displayed numerical acounts:"/>
+   <topitem name="notice1">
+      <notice class="alpha" text="Notice on displayed numerical acounts:"/>
       nodes are counted according to the "intrinsic complexity measure"
       [F. Guidi: "Procedural Representation of CIC Proof Terms"
       Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
    </topitem>
       nodes are counted according to the "intrinsic complexity measure"
       [F. Guidi: "Procedural Representation of CIC Proof Terms"
       Journal of Automated Reasoning 44(1-2), Springer (February 2010), pp. 53-78].       
    </topitem>
-   <topitem>
-      <notice class="alpha" notice="Notice on displayed logical structures:"/>
+   <topitem name="notice2">
+      <notice class="alpha" text="Notice on displayed logical structures:"/>
       from the logical standpoint, the source scripts are grouped in "planes"
       and these are grouped in "components";
       the notation for the relations or functions
       introduced in each script, is shown in parentheses (? are placeholders).
    </topitem>
 
       from the logical standpoint, the source scripts are grouped in "planes"
       and these are grouped in "components";
       the notation for the relations or functions
       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 =========================================================== -->
 
 <!-- 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:
    <body>
       The formal specification of λδ version 2
       is available in the following formats:
@@ -55,15 +63,16 @@
 
    <topitem name="source2">
       <body>
 
    <topitem name="source2">
       <body>
-         <rlink to="download/lambdadelta_2.tar.gz">lambdadelta_2 for Matita 0.99.2</rlink>
-         (revised <notice class="gamma" notice="2014-10"/>).
-         Source scripts.
+         <rlink to="download/lambdadelta_2A1.tar.gz">lambdadelta_2A1 for Matita 0.99.2</rlink>
+         (revised <notice class="gamma" text="2014-10"/>).
+         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.
       </body>
       <body>
       </body>
       <body>
          The scripts are grouped in directories, first by part, then by component.
       </body>
       <body>
-         <notice class="alpha" notice="Notice:"/>
+         <notice class="alpha" text="Notice:"/>
          the scripts are checked by the latest version of Matita from
          <link to="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</link>
          at path &lt;trunk/matita/&gt;.
          the scripts are checked by the latest version of Matita from
          <link to="http://matita.cs.unibo.it/download.shtml">HELM Subversion repository</link>
          at path &lt;trunk/matita/&gt;.
@@ -72,14 +81,15 @@
 
    <body>
       Informational pages on the parts of the specification:
 
    <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 =========================================================== -->
 
    </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:
    <body>
       The formal specification of λδ version 1
       is available in the following formats:
@@ -88,10 +98,11 @@
    <topitem name="source1">
       <body>
          <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
    <topitem name="source1">
       <body>
          <rlink to="download/lambdadelta_1.tar.gz">lambdadelta_1 for Coq 7.3.1</rlink>
-         (revised <notice class="delta" notice="2015-01"/>).
+         (revised <notice class="delta" text="2015-09"/>).
          Source scripts.
          Source scripts.
+         <rlink to="html/documentation.html#ldJ1a">Documentation (J1a)</rlink>.
          <list><item>
          <list><item>
-            <notice class="delta" notice="2015 January 15."/>
+            <notice class="delta" text="2015 January 15."/>
             17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
          </item></list>
       </body>      
             17 new lemmas and former lemma "eq_nat_dec" renamed as "nat_dec_neg".
          </item></list>
       </body>      
@@ -102,7 +113,7 @@
 
    <topitem name="static1">
       <rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</rlink>
 
    <topitem name="static1">
       <rlink to="static/matita/lambdadelta/">lambdadelta_1 for Matita 0.5</rlink>
-      (revised <notice class="delta" notice="2011-09"/>).
+      (revised <notice class="delta" text="2011-09"/>).
       Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.  
       <list><item>
          <rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
       Static HTML pages generated by the <link to="http://helm.cs.unibo.it/">HELM</link> rendering engine.  
       <list><item>
          <rlink to="static/matita/lambdadelta/basic_1/pr3/pr3/pr3_confluence.con.html">
@@ -129,15 +140,15 @@
    <topitem name="dynamic1">
       <link to="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
          lambdadelta_1 for Matita 0.5</link>
    <topitem name="dynamic1">
       <link to="http://mowgli.cs.unibo.it:58080/apply?keys=RT&amp;xmluri=http://helm.cs.unibo.it/helm//html/folder/index.html&amp;prop.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.thencoding=UTF-8&amp;prop.encoding=UTF-8&amp;prop.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=UTF-8&amp;param.media-type=text/html&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;profile=default&amp;param.profile=default&amp;param.CICURI=theory:/matita/lambdadelta/">
          lambdadelta_1 for Matita 0.5</link>
-      (revised <notice class="delta" notice="2011-09"/>).
+      (revised <notice class="delta" text="2011-09"/>).
       <link to="http://helm.cs.unibo.it/">HELM</link> directory.
       <link to="http://helm.cs.unibo.it/">HELM</link> directory.
-      <notice class="alpha" notice="Notice: the HELM rendering engine is offline."/>
+      <notice class="alpha" text="Notice: the HELM rendering engine is offline."/>
    </topitem>
 
    <body>
       Informational pages on the parts of the specification:
    </topitem>
 
    <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/>
    </body>
 
    <footer/>
Unnamed repository; edit this file 'description' to name the repository.