NEWS
 changeset 17495 ddb14cbec6a2 parent 17457 5b9538fc6d67 child 17519 9c10585a238c
```     1.1 --- a/NEWS	Tue Sep 20 00:16:29 2005 +0200
1.2 +++ b/NEWS	Tue Sep 20 08:20:22 2005 +0200
1.3 @@ -710,6 +710,16 @@
1.4    x |> f                f #> g
1.5    (x, y) |-> f          f #-> g
1.6
1.7 +* Pure/library.ML: introduced/changed precedence of infix operators:
1.8 +
1.9 +  infix 1 |> |-> ||> ||>> |>> |>>> #> #->;
1.10 +  infix 2 ?;
1.11 +  infix 3 o oo ooo oooo;
1.12 +  infix 4 ~~ upto downto;
1.13 +
1.14 +Maybe INCOMPATIBILITY when any of those is used in conjunction with other
1.15 +infix operators.
1.16 +
1.17  * Pure/library.ML: natural list combinators fold, fold_rev, and
1.18  fold_map support linear functional transformations and nesting.  For
1.19  example:
1.20 @@ -736,17 +746,14 @@
1.21
1.22  * Pure/General: structure AList (cf. Pure/General/alist.ML) provides
1.23  basic operations for association lists, following natural argument
1.24 -order.  The old functions may be expressed as follows:
1.25 +order; ; moreover the explicit equality predicate passed here avoids
1.26 +potentially expensive polymorphic runtime equality checks.
1.27 +The old functions may be expressed as follows:
1.28
1.29    assoc = uncurry (AList.lookup (op =))
1.30    assocs = these oo AList.lookup (op =)
1.31    overwrite = uncurry (AList.update (op =)) o swap
1.32
1.33 -* Pure/General: structure AList (cf. Pure/General/alist.ML) provides
1.34 -basic operations for association lists, following natural argument
1.35 -order; moreover the explicit equality predicate passed here avoids
1.36 -potentially expensive polymorphic runtime equality checks.
1.37 -
1.38  * Pure/General: structure OrdList (cf. Pure/General/ord_list.ML)
1.39  provides a reasonably efficient light-weight implementation of sets as
1.40  lists.
```