--- a/NEWS Thu Mar 15 22:21:28 2012 +0100
+++ b/NEWS Thu Mar 15 23:06:22 2012 +0100
@@ -10,6 +10,7 @@
- markup for bound variables
- markup for types of term variables (e.g. displayed as tooltips)
+ - support for user-defined Isar commands within the running session
* Updated and extended reference manuals ("isar-ref" and
"implementation"); reduced remaining material in old "ref" manual.
@@ -371,6 +372,9 @@
*** 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.