# HG changeset patch
# User wenzelm
# Date 1126644552 7200
# Node ID 923ef4a8c6729447c83a2e7798e7af77e392641f
# Parent 754b7fcff03e9a3aca3a37123629922c80f167cc
tuned;
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
nonIsar theories now, but these are likely to disappear soon.
+nonIsar 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 xsymbol for >=
is \. New transitivity rules have been added to HOL/Orderings.thy to
+is \. 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 "\"
@@ 335,7 +335,7 @@
* theory Finite_Set: changed the syntax for 'setsum', summation over
finite sets: "setsum (%x. e) A", which used to be "\x:A. e", is
now either "SUM x:A. e" or "\x \ A. e". The bound variable can
+now either "SUM x:A. e" or "\x \ 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 wallclock time that the outer shell wrapper produces.

+
* Pure: structure OrdList (cf. Pure/General/ord_list.ML) provides a
reasonably efficient lightweight implementation of sets as lists.