| changeset 35021 | c839a4c670c6 |
| parent 35009 | 5408e5207131 |
| child 35030 | f2f1e50bf65d |
--- a/NEWS Sun Feb 07 19:31:55 2010 +0100 +++ b/NEWS Sun Feb 07 19:33:34 2010 +0100 @@ -60,6 +60,10 @@ *** ML *** +* Renamed old-style Drule.standard to Drule.export_without_context, to +emphasize that this is in no way a standard operation. +INCOMPATIBILITY. + * Curried take and drop in library.ML; negative length is interpreted as infinity (as in chop). INCOMPATIBILITY.