--- a/NEWS Thu Feb 26 15:42:35 2009 +0100
+++ b/NEWS Thu Feb 26 16:00:19 2009 +0100
@@ -6,6 +6,10 @@
*** General ***
+* The main reference manuals (isar-ref, implementation, system) have
+been updated and extended. Formally checked references as hyperlinks
+are now available in uniform manner.
+
* Simplified main Isabelle executables, with less surprises on
case-insensitive file-systems (such as Mac OS).
@@ -47,9 +51,6 @@
regular 4-core machine, if the initial heap space is made reasonably
large (cf. Poly/ML option -H). [Poly/ML 5.2.1 or later]
-* The Isabelle System Manual (system) has been updated, with formally
-checked references as hyperlinks.
-
* Generalized Isar history, with support for linear undo, direct state
addressing etc.
@@ -111,30 +112,32 @@
unify_trace_bound = 50 (formerly 25)
unify_search_bound = 60 (formerly 30)
-* Different bookkeeping for code equations:
- a) On theory merge, the last set of code equations for a particular constant
- is taken (in accordance with the policy applied by other parts of the
- code generator framework).
- b) Code equations stemming from explicit declarations (e.g. code attribute)
- gain priority over default code equations stemming from definition, primrec,
- fun etc.
- INCOMPATIBILITY.
-
-* Global versions of theorems stemming from classes do not carry
-a parameter prefix any longer. INCOMPATIBILITY.
+* Different bookkeeping for code equations (INCOMPATIBILITY):
+
+ a) On theory merge, the last set of code equations for a particular
+ constant is taken (in accordance with the policy applied by other
+ parts of the code generator framework).
+
+ b) Code equations stemming from explicit declarations (e.g. code
+ attribute) gain priority over default code equations stemming
+ from definition, primrec, fun etc.
+
+* Global versions of theorems stemming from classes do not carry a
+parameter prefix any longer. INCOMPATIBILITY.
* Dropped locale element "includes". This is a major INCOMPATIBILITY.
In existing theorem specifications replace the includes element by the
-respective context elements of the included locale, omitting those that
-are already present in the theorem specification. Multiple assume
-elements of a locale should be replaced by a single one involving the
-locale predicate. In the proof body, declarations (most notably
-theorems) may be regained by interpreting the respective locales in the
-proof context as required (command "interpret").
+respective context elements of the included locale, omitting those
+that are already present in the theorem specification. Multiple
+assume elements of a locale should be replaced by a single one
+involving the locale predicate. In the proof body, declarations (most
+notably theorems) may be regained by interpreting the respective
+locales in the proof context as required (command "interpret").
+
If using "includes" in replacement of a target solely because the
parameter types in the theorem are not as general as in the target,
-consider declaring a new locale with additional type constraints on the
-parameters (context element "constrains").
+consider declaring a new locale with additional type constraints on
+the parameters (context element "constrains").
* Dropped "locale (open)". INCOMPATIBILITY.
@@ -145,9 +148,9 @@
* 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.
+* 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
@@ -161,15 +164,15 @@
- 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.
+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
@@ -183,8 +186,8 @@
* The 'axiomatization' command now only works within a global theory
context. INCOMPATIBILITY.
-* New find_theorems criterion "solves" matching theorems that
-directly solve the current goal. Try "find_theorems solves".
+* New find_theorems criterion "solves" matching theorems that directly
+solve the current goal. Try "find_theorems solves".
* Added an auto solve option, which can be enabled through the
ProofGeneral Isabelle settings menu (disabled by default).
@@ -193,14 +196,15 @@
stated. Any theorems that could solve the lemma directly are listed
underneath the goal.
-* New command find_consts searches for constants based on type and name
-patterns, e.g.
+* New 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 conjunctive
-and queries may be negated by prefixing them with a hyphen:
+By default, matching is against subtypes, but it may be restricted to
+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"
@@ -312,7 +316,7 @@
process. New thread-based implementation also works on non-Unix
platforms (Cygwin). Provers are no longer hardwired, but defined
within the theory via plain ML wrapper functions. Basic Sledgehammer
-commands are covered in the isar-ref manual
+commands are covered in the isar-ref manual.
* Wrapper scripts for remote SystemOnTPTP service allows to use
sledgehammer without local ATP installation (Vampire etc.). See also
@@ -496,9 +500,8 @@
*** HOL-Algebra ***
* New locales for orders and lattices where the equivalence relation
- is not restricted to equality. INCOMPATIBILITY: all order and
- lattice locales use a record structure with field eq for the
- equivalence.
+is not restricted to equality. INCOMPATIBILITY: all order and lattice
+locales use a record structure with field eq for the equivalence.
* New theory of factorial domains.