interpretation/interpret: prefixes are mandatory by default;
misc tuning and updates;

--- a/NEWS	Thu Mar 26 19:00:29 2009 +0100
+++ b/NEWS	Thu Mar 26 19:24:21 2009 +0100
@@ -139,8 +139,8 @@
 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
@@ -154,19 +154,23 @@
 
 - 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.
@@ -180,9 +184,9 @@
 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.
@@ -190,7 +194,7 @@
     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: