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