NEWS

 
 * 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.
+important changes are listed below.  See the Tutorial on Locales 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

 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.
+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.  Old-style
+implicit 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.
+- When converting proof scripts, be sure to mandatory qualifiers in
+'interpretation' and 'interpret' should be retained by default, even
+if this is an INCOMPATIBILITY compared to former behaviour.
+Qualifiers in locale expressions range over a single locale instance
+only.
 
 * Command 'instance': attached definitions no longer accepted.
 INCOMPATIBILITY, use proper 'instantiation' target.
 
 * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.

 
 * New 'find_theorems' criterion "solves" matching theorems that
 directly solve the current goal.
 
 * Auto solve feature for main theorem statements (cf. option in Proof
-General Isabelle settings menu, enabled by default).  Whenever a new
+General Isabelle settings menu, disabled by default).  Whenever a new
 goal is stated, "find_theorems solves" is called; any theorems that
-could solve the lemma directly are listed underneath the goal.
+could solve the lemma directly are listed as part of the goal state.
 
 * Command 'find_consts' searches for constants based on type and name
 patterns, e.g.
 
     find_consts "_ => bool"
 
 By default, matching is against subtypes, but it may be restricted to
-the whole type. Searching by name is possible.  Multiple queries are
+the whole type.  Searching by name is possible.  Multiple queries are
 conjunctive and queries may be negated by prefixing them with a
 hyphen:
 
     find_consts strict: "_ => bool" name: "Int" -"int => int"