--- 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.