[isabelle-dev] NEWS (update)

Makarius makarius at sketis.net
Thu Mar 26 21:08:12 CET 2009

* 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.

More information about the isabelle-dev mailing list