NEWS
changeset 61606 6d5213bd9709
parent 61604 bb20f11dd842
child 61614 34978e1b234f
     1.1 --- a/NEWS	Mon Nov 09 15:48:17 2015 +0100
     1.2 +++ b/NEWS	Mon Nov 09 21:04:49 2015 +0100
     1.3 @@ -276,12 +276,13 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 -* Qualifiers in locale expressions default to mandatory ('!')
     1.8 -regardless of the command.  Previously, for 'locale' and 'sublocale'
     1.9 -the default was optional ('?').  INCOMPATIBILITY
    1.10 +* Qualifiers in locale expressions default to mandatory ('!') regardless
    1.11 +of the command. Previously, for 'locale' and 'sublocale' the default was
    1.12 +optional ('?'). The old synatx '!' has been discontinued.
    1.13 +INCOMPATIBILITY, remove '!' and add '?' as required.
    1.14  
    1.15  * Keyword 'rewrites' identifies rewrite morphisms in interpretation
    1.16 -commands.  Previously, the keyword was 'where'.  INCOMPATIBILITY
    1.17 +commands.  Previously, the keyword was 'where'.  INCOMPATIBILITY.
    1.18  
    1.19  * Command 'print_definitions' prints dependencies of definitional
    1.20  specifications. This functionality used to be part of 'print_theory'.
    1.21 @@ -501,7 +502,12 @@
    1.22  
    1.23  * Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
    1.24  
    1.25 -* Library/Omega_Words_Fun: Infinite words modeled as functions nat => 'a.
    1.26 +* Library/Omega_Words_Fun: Infinite words modeled as functions nat =>
    1.27 +'a.
    1.28 +
    1.29 +* HOL-Statespace: command 'statespace' uses mandatory qualifier for
    1.30 +import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
    1.31 +remove '!' and add '?' as required.
    1.32  
    1.33  
    1.34  *** ML ***