equal
deleted
inserted
replaced
596 |
596 |
597 * All constant names are now qualified. INCOMPATIBILITY. |
597 * All constant names are now qualified. INCOMPATIBILITY. |
598 |
598 |
599 |
599 |
600 *** ML *** |
600 *** ML *** |
|
601 |
|
602 * Renamed structure MetaSimplifier to Raw_Simplifier. Note that the |
|
603 main functionality is provided by structure Simplifier. |
601 |
604 |
602 * Syntax.pretty_priority (default 0) configures the required priority |
605 * Syntax.pretty_priority (default 0) configures the required priority |
603 of pretty-printed output and thus affects insertion of parentheses. |
606 of pretty-printed output and thus affects insertion of parentheses. |
604 |
607 |
605 * Syntax.default_root (default "any") configures the inner syntax |
608 * Syntax.default_root (default "any") configures the inner syntax |