[isabelle-dev] NEWS

[ballarin at mailbroy.informatik.tu-muenchen.de]

* Complete re-implementation of locales.  INCOMPATIBILITY.
The most important changes are listed below.  See documentation
(forthcoming) and tutorial (also forthcoming) for details.

- In locale expressions, instantiation replaces renaming.  Parameters
must be declared in a for clause.  To aid compatibility with previous
parameter inheritance, in locale declarations, parameters that are not
'touched' (instantiation position "_" or omitted) are implicitly added
with their syntax at the beginning of the for clause.

- Syntax from abbreviations and definitions in locales is available in
locale expressions and context elements.  The latter is particularly
useful in locale declarations.

- More flexible mechanisms to qualify names generated by locale
expressions.  Qualifiers (prefixes) may be specified in locale
expressions.  Available are normal qualifiers (syntax "name:") and strict
qualifiers (syntax "name!:").  The latter must occur in name references
and are useful to avoid accidental hiding of names, the former are
optional.  Qualifiers derived from the parameter names of a locale are no
longer generated.

- "sublocale l < e" replaces "interpretation l < e".  The instantiation
clause in "interpretation" and "interpret" (square brackets) is no
longer available.  Use locale expressions.

- When converting proof scripts, be sure to replace qualifiers in
"interpretation" and "interpret" by strict qualifiers.  Qualifiers in
locale expressions range over a single locale instance only.