| changeset 20857 | 7f6f26d8349b |
| parent 20807 | bd3b60f9a343 |
| child 20919 | dab803075c62 |
--- a/NEWS Wed Oct 04 14:17:47 2006 +0200 +++ b/NEWS Wed Oct 04 14:25:47 2006 +0200 @@ -627,6 +627,11 @@ *** ML *** +* Pure/library: + +infixes ins ins_string ins_int have been abandoned in favour of insert. +INCOMPATIBILITY: rewrite "x ins(_...) xs" to "insert (op =) x xs" + * Pure/General/susp.ML: New module for delayed evaluations.