- new extendedd beta-reductum involving native type annotation

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2.ldw.xml

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
index 1c4a0bef5072bbecc79b820015ae008ec76cf0d7..b2cadf0d28d42d383f7858061959bb851f030c97 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
@@ -26,11 +26,14 @@
          for native type assignment.
    </news>
    <news date="In progress.">
-         Closure of extended context-sensitive computation
+         Closure of context-sensitive extended computation
          for native validity.
    </news>
    <news date="In progress.">
-         Extended context-sensitive strong normalization
+         Reaxiomatized β-reductum as in extended β-reduction
+   </news>
+   <news date="2013 July 20.">
+         Context-sensitive extended strong normalization
          for simply typed terms.
    </news>
    <news date="2013 April 16.">
@@ -40,13 +43,13 @@
    </news>
    <news date="2013 March 16.">
          Mutual recursive preservation of stratified native validity
-        for hyper computation on closures.
+         for hyper computation on closures.
    </news>
    <news date="2012 October 16.">
          Confluence for context-free parallel reduction on closures.
    </news>
    <news date="2012 July 26.">
-         Term binders polarized to control ζ reduction.
+         Term binders polarized to control ζ-reduction.
    </news>
    <news date="2012 April 16.">
          Context-sensitive subject equivalence