--- a/NEWS Fri Dec 17 18:32:40 2010 +0100
+++ b/NEWS Fri Dec 17 18:38:33 2010 +0100
@@ -83,6 +83,13 @@
*** Pure ***
+* Command 'type_synonym' (with single argument) replaces somewhat
+outdated 'types', which is still available as legacy feature for some
+time.
+
+* Command 'nonterminal' (with 'and' separated list of arguments)
+replaces somewhat outdated 'nonterminals'. INCOMPATIBILITY.
+
* Command 'notepad' replaces former 'example_proof' for
experimentation in Isar without any result. INCOMPATIBILITY.
@@ -599,6 +606,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.