author wenzelm Tue, 13 Sep 2005 22:49:12 +0200 changeset 17371 923ef4a8c672 parent 17370 754b7fcff03e child 17372 d73f67e90a95
tuned;
 NEWS file | annotate | diff | comparison | revisions
```--- 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.
```