- some renaming according to the written version of basic_2

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / web / apps_2.ldw.xml
diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml

index f13d943f893367f9983885a841e0c15cc900f8e9..e4499a294b2793272e787a5f56417a7adc97c3de 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml
@@ -10,32 +10,30 @@
           applications of λδ version 2.
           In particular it contains the components below.
     </body>
-   <news date="MLTT1.">
-         Martin-Löf's Type Theory with one universe
-         using λδ as theory of expressions.
-   </news>
-   <news date="Functional.">
-         The validation algorithm for λδ as implemented in
-         <rlink to="implementation.html#helena">Helena 0.8</rlink>.
-   </news>
+   <topitem name="MLTT1">
+      <notice class="alpha" notice="MLTT1."/>
+      Martin-Löf's Type Theory with one universe
+      using λδ as theory of expressions.
+   </topitem>
+   <topitem name="functional">
+      <notice class="alpha" notice="Functional."/>
+      The validation algorithm for λδ as implemented in
+      <rlink to="implementation.html#helena">Helena 0.8</rlink>.
+   </topitem>
  
     <section>Summary of the Specification</section>
     <body>Here is a numerical acount of the specification's contents
           and its timeline.
-         Nodes are counted according to the "intrinsinc complexity measure"
-         [F. Guidi: "Procedural Representation of CIC Proof Terms"
-         Journal of Automated Reasoning 44(1-2), Springer (February 2010),
-         pp. 53-78].
     </body>
     <table name="apps_2_sum"/>
-   <news date="2012 February 24.">
+   <news class="alpha" date="2012 February 24.">
           The Applications directory is started.
     </news>
-   <news date="2011 December 20.">
+   <news class="alpha" date="2011 December 20.">
           The Functional component is started
           inside the specification of λδ version 2.
     </news>
-   <news date="2011 December 12.">
+   <news class="alpha" date="2011 December 12.">
           The MLTT1 component is started.
     </news>
  
@@ -48,9 +46,5 @@
     </body>
     <table name="apps_2_src"/>
  
-   <section>Physical Structure of the Specification</section>
-   <body>The source files are grouped in directories,
-         one for each component.
-   </body>
     <footer/>
  </page>