| changeset 41228 | e1fce873b814 |
| parent 41079 | a0d9258e2091 |
| child 41229 | d797baa3d57c |
--- 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.