diff -r bc5d582d6cfe -r cc85eaab20f6 NEWS
--- a/NEWS	Thu Feb 28 15:54:37 2008 +0100
+++ b/NEWS	Thu Feb 28 15:55:04 2008 +0100
@@ -29,56 +29,62 @@
 instance operations together with an instantiation proof.
 Type-checking phase allows to refer to class operations uniformly.
 See HOL/Complex/Complex.thy for an Isar example and
-HOL/Library/Eval.thy for an ML example.  Supersedes previous
-experimental versions.
+HOL/Library/Eval.thy for an ML example.
 
 
 *** HOL ***
 
-* Theory Int: The representation of numerals has changed.  The infix operator
-BIT and the bit datatype with constructors B0 and B1 have disappeared.
-INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in place of "x BIT bit.B0"
-and "y BIT bit.B1", respectively.  Theorems involving BIT, B0, or B1 have been
-renamed with "Bit0" or "Bit1" accordingly.
-
-* Theory Nat: definition of <= and < on natural numbers no longer depend
-on well-founded relations.  INCOMPATIBILITY.  Definitions le_def and less_def
-have disappeared.  Consider lemmas not_less [symmetric, where ?'a = nat]
-and less_eq [symmetric] instead.
-
-* Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin (whose purpose 
-mainly is for various fold_set functionals) have been abandoned in favour of
-the existing algebraic classes ab_semigroup_mult, comm_monoid_mult,
-ab_semigroup_idem_mult, lower_semilattice (resp. upper_semilattice) and linorder.
+* Theory Int: The representation of numerals has changed.  The infix
+operator BIT and the bit datatype with constructors B0 and B1 have
+disappeared.  INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in
+place of "x BIT bit.B0" and "y BIT bit.B1", respectively.  Theorems
+involving BIT, B0, or B1 have been renamed with "Bit0" or "Bit1"
+accordingly.
+
+* Theory Nat: definition of <= and < on natural numbers no longer
+depend on well-founded relations.  INCOMPATIBILITY.  Definitions
+le_def and less_def have disappeared.  Consider lemmas not_less
+[symmetric, where ?'a = nat] and less_eq [symmetric] instead.
+
+* Theory Finite_Set: locales ACf, ACe, ACIf, ACIfSL and ACIfSLlin
+(whose purpose mainly is for various fold_set functionals) have been
+abandoned in favour of the existing algebraic classes
+ab_semigroup_mult, comm_monoid_mult, ab_semigroup_idem_mult,
+lower_semilattice (resp. upper_semilattice) and linorder.
 INCOMPATIBILITY.
 
-* Theorem Inductive.lfp_ordinal_induct generalized to complete lattices.  The
-form set-specific version is available as Inductive.lfp_ordinal_induct_set.
+* Theory Transitive_Closure: induct and cases rules now declare proper
+case_names ("base" and "step").  INCOMPATIBILITY.
+
+* Theorem Inductive.lfp_ordinal_induct generalized to complete
+lattices.  The form set-specific version is available as
+Inductive.lfp_ordinal_induct_set.
 
 * Theorems "power.simps" renamed to "power_int.simps".
 
-* New class semiring_div provides basic abstract properties of semirings
+* Class semiring_div provides basic abstract properties of semirings
 with division and modulo operations.  Subsumes former class dvd_mod.
 
-* Merged theories IntDef, Numeral and IntArith into unified theory Int.
+* Merged theories IntDef, Numeral and IntArith into unified theory
+Int.  INCOMPATIBILITY.
+
+* Theory Library/Code_Index: type "index" now represents natural
+numbers rather than integers.  INCOMPATIBILITY.
+
+* New class "uminus" with operation "uminus" (split of from class
+"minus" which now only has operation "minus", binary).
 INCOMPATIBILITY.
 
-* Theory Library/Code_Index: type "index" now represents natural numbers rather
-than integers.  INCOMPATIBILITY.
-
-* New class "uminus" with operation "uminus" (split of from class "minus"
-which now only has operation "minus", binary).  INCOMPATIBILITY.
-
 * New primrec package.  Specification syntax conforms in style to
-definition/function/....  No separate induction rule is provided.
-The "primrec" command distinguishes old-style and new-style specifications
+definition/function/....  No separate induction rule is provided.  The
+"primrec" command distinguishes old-style and new-style specifications
 by syntax.  The former primrec package is now named OldPrimrecPackage.
 When adjusting theories, beware: constants stemming for new-style
 primrec specifications have authentic syntax.
 
 * Library/Multiset: {#a, b, c#} abbreviates {#a#} + {#b#} + {#c#}.
 
-* Library/ListSpace: new theory of arithmetic vector operations.
+* Library/ListVector: new theory of arithmetic vector operations.
 
 * Constants "card", "internal_split", "option_map" now with authentic
 syntax.  INCOMPATIBILITY.
@@ -90,7 +96,7 @@
 Sup_set_def, le_def, less_def, option_map_def now with object
 equality.  INCOMPATIBILITY.
 
-* New method "induction_scheme" derives user-specified induction rules
+* Method "induction_scheme" derives user-specified induction rules
 from wellfounded induction and completeness of patterns. This factors
 out some operations that are done internally by the function package
 and makes them available separately. See "HOL/ex/Induction_Scheme.thy"