- basic_2: induction for preservation results now uses supclosure

[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 d8206ed982e239c5ef674bd7fefaaba3f5ed4e2d..1c4a0bef5072bbecc79b820015ae008ec76cf0d7 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
@@ -33,6 +33,11 @@
          Extended context-sensitive strong normalization
          for simply typed terms.
    </news>
+   <news date="2013 April 16.">
+         Reaxiomatized substitution and reduction 
+         commute with respect to subclosure
+         (anniversary milestone).
+   </news>
    <news date="2013 March 16.">
          Mutual recursive preservation of stratified native validity
         for hyper computation on closures.