diff -r 11e7ee2ca77f -r e1fce873b814 NEWS --- a/NEWS Fri Dec 17 16:25:21 2010 +0100 +++ b/NEWS Fri Dec 17 17:08:56 2010 +0100 @@ -599,6 +599,9 @@ *** ML *** +* Renamed structure MetaSimplifier to Raw_Simplifier. Note that the +main functionality is provided by structure Simplifier. + * Syntax.pretty_priority (default 0) configures the required priority of pretty-printed output and thus affects insertion of parentheses.