NEWS

 are formally declared.  INCOMPATIBILITY.
 
 
 *** HOL ***
 
-* New testing tool "Mirabelle" for automated (proof) tools. Applies several
-tools and tactics like sledgehammer, metis, or quickcheck, to every proof step
-in a theory. To be used in batch mode via "isabelle mirabelle".
-
-* New proof method "sos" (sum of squares) for nonlinear real arithmetic
-(originally due to John Harison). It requires Library/Sum_Of_Squares.
-It is not a complete decision procedure but works well in practice
-on quantifier-free real arithmetic with +, -, *, ^, =, <= and <,
-i.e. boolean combinations of equalities and inequalities between
-polynomials. It makes use of external semidefinite programming solvers.
-For more information and examples see Library/Sum_Of_Squares.
-
-* Set.UNIV and Set.empty are mere abbreviations for top and bot.  INCOMPATIBILITY.
-
-* More convenient names for set intersection and union.  INCOMPATIBILITY:
-
+* New testing tool "Mirabelle" for automated (proof) tools. Applies
+several tools and tactics like sledgehammer, metis, or quickcheck, to
+every proof step in a theory. To be used in batch mode via the
+"mirabelle" utility.
+
+* New proof method "sos" (sum of squares) for nonlinear real
+arithmetic (originally due to John Harison). It requires
+Library/Sum_Of_Squares.  It is not a complete decision procedure but
+works well in practice on quantifier-free real arithmetic with +, -,
+*, ^, =, <= and <, i.e. boolean combinations of equalities and
+inequalities between polynomials. It makes use of external
+semidefinite programming solvers.  For more information and examples
+see src/HOL/Library/Sum_Of_Squares.
+
+* Set.UNIV and Set.empty are mere abbreviations for top and bot.
+INCOMPATIBILITY.
+
+* More convenient names for set intersection and union.
+INCOMPATIBILITY:
     Set.Int ~>  Set.inter
     Set.Un ~>   Set.union
 
 * Code generator attributes follow the usual underscore convention:
     code_unfold     replaces    code unfold
     code_post       replaces    code post
     etc.
   INCOMPATIBILITY.
-
-* New quickcheck implementation using new code generator.
 
 * New class "boolean_algebra".
 
 * Refinements to lattices classes:
   - added boolean_algebra type class

 * Power operations on relations and functions are now one dedicate
 constant compow with infix syntax "^^".  Power operations on
 multiplicative monoids retains syntax "^" and is now defined generic
 in class power.  INCOMPATIBILITY.
 
-* Relation composition "R O S" now has a "more standard" argument order,
-i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }".
+* Relation composition "R O S" now has a "more standard" argument
+order, i.e., "R O S = {(x,z). EX y. (x,y) : R & (y,z) : S }".
 INCOMPATIBILITY: Rewrite propositions with "S O R" --> "R O S". Proofs
-may occationally break, since the O_assoc rule was not rewritten like this.
-Fix using O_assoc[symmetric].
-The same applies to the curried version "R OO S".
-
-* GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm of finite and
-infinite sets. It is shown that they form a complete lattice.
+may occationally break, since the O_assoc rule was not rewritten like
+this.  Fix using O_assoc[symmetric].  The same applies to the curried
+version "R OO S".
+
+* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
+of finite and infinite sets. It is shown that they form a complete
+lattice.
 
 * ML antiquotation @{code_datatype} inserts definition of a datatype
 generated by the code generator; see Predicate.thy for an example.
 
 * New method "linarith" invokes existing linear arithmetic decision
 procedure only.
 
-* Implementation of quickcheck using generic code generator; default
-generators are provided for all suitable HOL types, records and
-datatypes.
+* New implementation of quickcheck uses generic code generator;
+default generators are provided for all suitable HOL types, records
+and datatypes.
 
 * Constants Set.Pow and Set.image now with authentic syntax;
 object-logic definitions Set.Pow_def and Set.image_def.
 INCOMPATIBILITY.
 

 with "_package", e.g.:
 
     DatatypePackage ~> Datatype
     InductivePackage ~> Inductive
 
-    etc.
-
 INCOMPATIBILITY.
 
 * NewNumberTheory: Jeremy Avigad's new version of part of
 NumberTheory.  If possible, use NewNumberTheory, not NumberTheory.
 
-* Simplified interfaces of datatype module.  INCOMPATIBILITY.
-
-* Abbreviation "arbitrary" of "undefined" has disappeared; use
-"undefined" directly.  INCOMPATIBILITY.
+* Discontinued abbreviation "arbitrary" of constant
+"undefined". INCOMPATIBILITY, use "undefined" directly.
 
 * New evaluator "approximate" approximates an real valued term using
 the same method as the approximation method.
 
 * Method "approximate" supports now arithmetic expressions as

 *** ML ***
 
 * PARALLEL_CHOICE and PARALLEL_GOALS provide basic support for
 parallel tactical reasoning.
 
-* Tactical FOCUS is similar to SUBPROOF, but allows the body tactic to
-introduce new subgoals and schematic variables.  FOCUS_PARAMS is
-similar, but focuses on the parameter prefix only, leaving subgoal
-premises unchanged.
+* Tacticals Subgoal.FOCUS, Subgoal.FOCUS_PREMS, Subgoal.FOCUS_PARAMS
+are similar to SUBPROOF, but are slightly more flexible: only the
+specified parts of the subgoal are imported into the context, and the
+body tactic may introduce new subgoals and schematic variables.
+
+* Old tactical METAHYPS, which does not observe the proof context, has
+been renamed to Old_Goals.METAHYPS and awaits deletion.  Use SUBPROOF
+or Subgoal.FOCUS etc.
 
 * Renamed functor TableFun to Table, and GraphFun to Graph.  (Since
 functors have their own ML name space there is no point to mark them
 separately.)  Minor INCOMPATIBILITY.