--- 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: