New locales.

--- a/NEWS	Tue Dec 30 11:10:01 2008 +0100
+++ b/NEWS	Tue Dec 30 16:50:46 2008 +0100
@@ -130,7 +130,7 @@
 consider declaring a new locale with additional type constraints on the
 parameters (context element "constrains").
 
-* Dropped "locale (open)".  INCOMPATBILITY.
+* Dropped "locale (open)".  INCOMPATIBILITY.
 
 * Interpretation commands no longer attempt to simplify goal.
 INCOMPATIBILITY: in rare situations the generated goal differs.  Use
@@ -139,6 +139,36 @@
 * Interpretation commands no longer accept interpretation attributes.
 INCOMPATBILITY.
 
+* 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.
+
 * Command 'instance': attached definitions no longer accepted.
 INCOMPATIBILITY, use proper 'instantiation' target.