| changeset 20348 | d59364649bcc |
| parent 20327 | 69a9d839dcc8 |
| child 20370 | 217aada4f795 |
--- a/NEWS Mon Aug 07 17:43:51 2006 +0200 +++ b/NEWS Tue Aug 08 08:18:59 2006 +0200 @@ -552,6 +552,11 @@ * Pure/library: +Semantically identical functions "equal_list" and "eq_list" have been +unified to "eq_list". + +* Pure/library: + val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd