NEWS
changeset 41494 e1fce873b814
parent 41327 a0d9258e2091
child 41495 d797baa3d57c
     1.1 --- a/NEWS	Fri Dec 17 16:25:21 2010 +0100
     1.2 +++ b/NEWS	Fri Dec 17 17:08:56 2010 +0100
     1.3 @@ -599,6 +599,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Renamed structure MetaSimplifier to Raw_Simplifier.  Note that the
     1.8 +main functionality is provided by structure Simplifier.
     1.9 +
    1.10  * Syntax.pretty_priority (default 0) configures the required priority
    1.11  of pretty-printed output and thus affects insertion of parentheses.
    1.12