diff -r 754b7fcff03e -r 923ef4a8c672 NEWS
--- a/NEWS	Tue Sep 13 22:21:06 2005 +0200
+++ b/NEWS	Tue Sep 13 22:49:12 2005 +0200
@@ -19,7 +19,7 @@
 
 will disappear in the next release.  Use isatool fixheaders to convert
 existing theory files.  Note that there is no change in ancient
-non-Isar theories now, but these are likely to disappear soon.
+non-Isar theories now, but these will disappear soon.
 
 * Theory loader: parent theories can now also be referred to via
 relative and absolute paths.
@@ -311,7 +311,7 @@
 
 * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
 Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=
-is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to 
+is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to
 support corresponding Isar calculations.
 
 * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>"
@@ -335,7 +335,7 @@
 
 * theory Finite_Set: changed the syntax for 'setsum', summation over
 finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is
-now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can 
+now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can
 be a tuple pattern.
 
 Some new syntax forms are available:
@@ -414,8 +414,8 @@
 (INCOMPATIBILITY):
 
   abs_eq             now named abs_of_nonneg
-  abs_of_ge_0        now named abs_of_nonneg 
-  abs_minus_eq       now named abs_of_nonpos  
+  abs_of_ge_0        now named abs_of_nonneg
+  abs_minus_eq       now named abs_of_nonpos
   imp_abs_id         now named abs_of_nonneg
   imp_abs_neg_id     now named abs_of_nonpos
   mult_pos           now named mult_pos_pos
@@ -506,8 +506,8 @@
 * Pure/library.ML: several combinators for linear functional
 transformations, notably reverse application and composition:
 
-  x |> f		f #> g
-  (x, y) |-> f		f #-> g
+  x |> f                f #> g
+  (x, y) |-> f          f #-> g
 
 * Pure/library.ML: canonical list combinators fold, fold_rev, and
 fold_map support linear functional transformations and nesting.  For
@@ -559,7 +559,7 @@
 * Isar session: The initial use of ROOT.ML is now always timed,
 i.e. the log will show the actual process times, in contrast to the
 elapsed wall-clock time that the outer shell wrapper produces.
- 
+
 * Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a
 reasonably efficient light-weight implementation of sets as lists.