NEWS
changeset 54049 566b769c3477
parent 54033 955c6549b3cb
child 54055 5bf55a713232
child 54305 d2def195bb6b
     1.1 --- a/NEWS	Wed Oct 02 23:05:36 2013 +0200
     1.2 +++ b/NEWS	Thu Oct 03 00:39:16 2013 +0200
     1.3 @@ -103,10 +103,11 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 -* Target-sensitive commands 'interpretation' and 'sublocale'.
     1.8 -Particularly, 'interpretation' now allows for non-persistent
     1.9 -interpretation within "context ... begin ... end" blocks.  See
    1.10 -"isar-ref" manual for details.
    1.11 +* Commands 'interpretation' and 'sublocale' are now target-sensitive.
    1.12 +In particular, 'interpretation' allows for non-persistent
    1.13 +interpretation within "context ... begin ... end" blocks offering a
    1.14 +light-weight alternative to 'sublocale'.  See "isar-ref" manual for
    1.15 +details.
    1.16  
    1.17  * Improved locales diagnostic command 'print_dependencies'.
    1.18