--- a/NEWS Fri Mar 16 14:46:13 2012 +0100
+++ b/NEWS Fri Mar 16 18:20:12 2012 +0100
@@ -379,6 +379,10 @@
* Antiquotation @{keyword "name"} produces a parser for outer syntax
from a minor keyword introduced via theory header declaration.
+* Antiquotation @{command_spec "name"} produces the
+Outer_Syntax.command_spec from a major keyword introduced via theory
+header declaration; it can be passed to Outer_Syntax.command etc.
+
* Local_Theory.define no longer hard-wires default theorem name
"foo_def": definitional packages need to make this explicit, and may
choose to omit theorem bindings for definitions by using