NEWS

 
 New in this Isabelle version
 ----------------------------
 
 *** 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).
 
   - The main Isabelle tool wrapper is now called "isabelle" instead of

 
 * Proofs of fully specified statements are run in parallel on
 multi-core systems.  A speedup factor of 2-3 can be expected on a
 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.
 
 * Recovered hiding of consts, which was accidentally broken in

 * Changed defaults for unify configuration options:
 
   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.
 
 * Interpretation commands no longer attempt to simplify goal.
 INCOMPATIBILITY: in rare situations the generated goal differs.  Use
 methods intro_locales and unfold_locales to clarify.
 
 * 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
 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.
-
-- "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
 locale expressions range over a single locale instance only.
 

 * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
 
 * 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).
  
 When enabled, find_theorems solves is called whenever a new lemma is
 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"
 
 
 *** Document preparation ***

 * Generic ATP manager for Sledgehammer, based on ML threads instead of
 Posix processes.  Avoids potentially expensive forking of the ML
 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
 ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
 variable.  Other provers may be included via suitable ML wrappers, see

 
 
 *** 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.
 
 * Units_l_inv and Units_r_inv are now simprules by default.
 INCOMPATIBILITY.  Simplifier proof that require deletion of l_inv