--- a/CONTRIBUTORS Fri Jul 15 15:44:22 2005 +0200
+++ b/CONTRIBUTORS Fri Jul 15 15:45:04 2005 +0200
@@ -1,3 +1,7 @@
+
+* July 2005: Florian Haftmann, TUM
+ Some combinators for linear functional transformations in ML:
+ |-> #-> fold_yield etc.
* May 2005: Rafal Kolanski, NICTA
Substantially improved retrieval of facts from theory/proof context.
--- a/NEWS Fri Jul 15 15:44:22 2005 +0200
+++ b/NEWS Fri Jul 15 15:45:04 2005 +0200
@@ -420,7 +420,7 @@
* 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.
+add_frees, add_vars etc. 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