* Pure/library.ML: several combinators for linear functional transformations;
* Pure/library.ML: canonical list combinators fold, fold_rev, and fold_yield;
* Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, fold_types;

--- a/NEWS	Fri Jul 15 15:35:28 2005 +0200
+++ b/NEWS	Fri Jul 15 15:44:11 2005 +0200
@@ -378,13 +378,13 @@
 The functions the, if_none, is_some, is_none have been adapted
 accordingly, while Option.map replaces apsome.
 
-* The exception LIST has been given up in favour of the standard
-exceptions Empty and Subscript, as well as Library.UnequalLengths.
-Function like Library.hd and Library.tl are superceded by the standard
-hd and tl functions etc.
-
-A number of basic functions are now no longer exported to the ML
-toplevel, as they are variants of standard functions.  The following
+* Pure/library.ML: the exception LIST has been given up in favour of
+the standard exceptions Empty and Subscript, as well as
+Library.UnequalLengths.  Function like Library.hd and Library.tl are
+superceded by the standard hd and tl functions etc.
+
+A number of basic list functions are no longer exported to the ML
+toplevel, as they are variants of predefined functions.  The following
 suggests how one can translate existing code:
 
     rev_append xs ys = List.revAppend (xs, ys)
@@ -393,9 +393,35 @@
     flat xss = List.concat xss
     seq fs = List.app fs
     partition P xs = List.partition P xs
-    filter P xs = List.filter P xs
     mapfilter f xs = List.mapPartial f xs
 
+* Pure/library.ML: several combinators for linear functional
+transformations, notably reverse application and composition:
+
+  x |> f		f #> g
+  (x, y) |-> f		f #-> g
+
+* Pure/library.ML: canonical list combinators fold, fold_rev, and
+fold_yield support linear functional transformations and nesting.  For
+example:
+
+  fold f [x1, ..., xN] y =
+    y |> f x1 |> ... |> f xN
+
+  (fold o fold) f [xs1, ..., xsN] y =
+    y |> fold f xs1 |> ... |> fold f xsN
+
+  fold f [x1, ..., xN] =
+    f x1 #> ... #> f xN
+
+  (fold o fold) f [xs1, ..., xsN] =
+    fold f xs1 #> ... #> fold f xsN
+
+* Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types,
+fold_types traverse types/terms from left to right, observing
+canonical argument order.  Supercedes previous foldl_XXX versions,
+add_frees, add_vars have been adapted as well: INCOMPATIBILITY.
+
 * Pure: output via the Isabelle channels of writeln/warning/error
 etc. is now passed through Output.output, with a hook for arbitrary
 transformations depending on the print_mode (cf. Output.add_mode --