NEWS
changeset 46959 cdc791910460
parent 46956 9ff441f295c2
child 46961 5c6955f487e5
child 46965 0c8fb96cce73
--- a/NEWS	Fri Mar 16 13:05:30 2012 +0100
+++ b/NEWS	Fri Mar 16 14:42:11 2012 +0100
@@ -41,6 +41,10 @@
 "syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref
 manual.  Minor INCOMPATIBILITY.
 
+* Forward declaration of outer syntax keywords within the theory
+header -- minor INCOMPATIBILITY for user-defined commands.  Allow new
+commands to be used in the same theory where defined.
+
 
 *** Pure ***
 
@@ -372,9 +376,6 @@
 
 *** ML ***
 
-* Outer syntax keywords for user-defined Isar commands need to be
-defined explicitly in the theory header.  Minor INCOMPATIBILITY.
-
 * Antiquotation @{keyword "name"} produces a parser for outer syntax
 from a minor keyword introduced via theory header declaration.