NEWS
changeset 47822 aae5566d6756
parent 47798 e7ea35b41e2d
child 47827 9ff441f295c2
     1.1 --- a/NEWS	Thu Mar 15 19:02:34 2012 +0100
     1.2 +++ b/NEWS	Thu Mar 15 19:48:19 2012 +0100
     1.3 @@ -371,6 +371,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Antiquotation @{keyword "name"} produces a parser for outer syntax
     1.8 +from a minor keyword introduced via theory header declaration.
     1.9 +
    1.10  * Local_Theory.define no longer hard-wires default theorem name
    1.11  "foo_def": definitional packages need to make this explicit, and may
    1.12  choose to omit theorem bindings for definitions by using