diff -r 8ac6d4902b56 -r 43abdba4da5c NEWS --- 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 --