diff -r 896896a867e6 -r 5408e5207131 NEWS
--- a/NEWS	Sat Feb 06 08:42:37 2010 +0100
+++ b/NEWS	Sat Feb 06 14:39:33 2010 +0100
@@ -6,16 +6,16 @@
 
 *** Pure ***
 
-* Code generator: details of internal data cache have no impact on
-the user space functionality any longer.
+* Code generator: details of internal data cache have no impact on the
+user space functionality any longer.
 
 
 *** HOL ***
 
-* new theory Algebras.thy contains generic algebraic structures and
+* New theory Algebras contains generic algebraic structures and
 generic algebraic operations.  INCOMPATIBILTY: constants zero, one,
-plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and less
-have been moved from HOL.thy to Algebras.thy.
+plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and
+less have been moved from HOL.thy to Algebras.thy.
 
 * HOLogic.strip_psplit: types are returned in syntactic order, similar
 to other strip and tuple operations.  INCOMPATIBILITY.
@@ -24,24 +24,24 @@
 replaced by new-style primrec, especially in theory List.  The corresponding
 constants now have authentic syntax.  INCOMPATIBILITY.
 
-* Reorganized theory Multiset.thy: less duplication, less historical
+* Reorganized theory Multiset: less duplication, less historical
 organization of sections, conversion from associations lists to
 multisets, rudimentary code generation.  Use insert_DiffM2 [symmetric]
 instead of elem_imp_eq_diff_union, if needed.  INCOMPATIBILITY.
 
-* Reorganized theory Sum_Type.thy; Inl and Inr now have
-authentic syntax.  INCOMPATIBILITY.
+* Reorganized theory Sum_Type; Inl and Inr now have authentic syntax.
+INCOMPATIBILITY.
 
 * Code generation: ML and OCaml code is decorated with signatures.
 
-* Complete_Lattice.thy: lemmas top_def and bot_def have been replaced
-by the more convenient lemmas Inf_empty and Sup_empty.  Dropped lemmas
-Inf_insert_simp and Sup_insert_simp, which are subsumed by Inf_insert
-and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace former Inf_Univ
-and Sup_Univ.  Lemmas inf_top_right and sup_bot_right subsume inf_top
-and sup_bot respectively.  INCOMPATIBILITY.
-
-* Finite_Set.thy and List.thy: some lemmas have been generalized from
+* Theory Complete_Lattice: lemmas top_def and bot_def have been
+replaced by the more convenient lemmas Inf_empty and Sup_empty.
+Dropped lemmas Inf_insert_simp and Sup_insert_simp, which are subsumed
+by Inf_insert and Sup_insert.  Lemmas Inf_UNIV and Sup_UNIV replace
+former Inf_Univ and Sup_Univ.  Lemmas inf_top_right and sup_bot_right
+subsume inf_top and sup_bot respectively.  INCOMPATIBILITY.
+
+* Theory Finite_Set and List: some lemmas have been generalized from
 sets to lattices:
 
   fun_left_comm_idem_inter      ~> fun_left_comm_idem_inf
@@ -55,7 +55,8 @@
   INTER_fold_inter              ~> INFI_fold_inf
   UNION_fold_union              ~> SUPR_fold_sup
 
-* Added transpose to List.thy.
+* Theory List: added transpose.
+
 
 *** ML ***