[isabelle-dev] NEWS (update)

[Makarius]

* Complete re-implementation of locales ...

- More flexible mechanisms to qualify names generated by locale 
expressions.  Qualifiers (prefixes) may be specified in locale 
expressions, and can be marked as mandatory (syntax: "name!:") or optional 
(syntax "name?:").  The default depends for plain "name:" depends on the 
situation where a locale expression is used: in commands 'locale' and 
'sublocale' prefixes are optional, in 'interpretation' and 'interpret' 
prefixes are mandatory.

This means users never need to specify either "!" or "?" in prefixes under 
normal circumstances.