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