diff -r 37f47ea6fed1 -r 351fc2f8493d NEWS --- 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.