NEWS
changeset 29253 3c6cd80a4854
parent 29197 6d4cb27ed19c
child 29398 89813bbf0f3e
     1.1 --- a/NEWS	Tue Dec 30 11:10:01 2008 +0100
     1.2 +++ b/NEWS	Tue Dec 30 16:50:46 2008 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4  consider declaring a new locale with additional type constraints on the
     1.5  parameters (context element "constrains").
     1.6  
     1.7 -* Dropped "locale (open)".  INCOMPATBILITY.
     1.8 +* Dropped "locale (open)".  INCOMPATIBILITY.
     1.9  
    1.10  * Interpretation commands no longer attempt to simplify goal.
    1.11  INCOMPATIBILITY: in rare situations the generated goal differs.  Use
    1.12 @@ -139,6 +139,36 @@
    1.13  * Interpretation commands no longer accept interpretation attributes.
    1.14  INCOMPATBILITY.
    1.15  
    1.16 +* Complete re-implementation of locales.  INCOMPATIBILITY.
    1.17 +The most important changes are listed below.  See documentation
    1.18 +(forthcoming) and tutorial (also forthcoming) for details.
    1.19 +
    1.20 +- In locale expressions, instantiation replaces renaming.  Parameters
    1.21 +must be declared in a for clause.  To aid compatibility with previous
    1.22 +parameter inheritance, in locale declarations, parameters that are not
    1.23 +'touched' (instantiation position "_" or omitted) are implicitly added
    1.24 +with their syntax at the beginning of the for clause.
    1.25 +
    1.26 +- Syntax from abbreviations and definitions in locales is available in
    1.27 +locale expressions and context elements.  The latter is particularly
    1.28 +useful in locale declarations.
    1.29 +
    1.30 +- More flexible mechanisms to qualify names generated by locale
    1.31 +expressions.  Qualifiers (prefixes) may be specified in locale
    1.32 +expressions.  Available are normal qualifiers (syntax "name:") and strict
    1.33 +qualifiers (syntax "name!:").  The latter must occur in name references
    1.34 +and are useful to avoid accidental hiding of names, the former are
    1.35 +optional.  Qualifiers derived from the parameter names of a locale are no
    1.36 +longer generated.
    1.37 +
    1.38 +- "sublocale l < e" replaces "interpretation l < e".  The instantiation
    1.39 +clause in "interpretation" and "interpret" (square brackets) is no
    1.40 +longer available.  Use locale expressions.
    1.41 +
    1.42 +- When converting proof scripts, be sure to replace qualifiers in
    1.43 +"interpretation" and "interpret" by strict qualifiers.  Qualifiers in
    1.44 +locale expressions range over a single locale instance only.
    1.45 +
    1.46  * Command 'instance': attached definitions no longer accepted.
    1.47  INCOMPATIBILITY, use proper 'instantiation' target.
    1.48