| changeset 46948 | aae5566d6756 |
| parent 46916 | e7ea35b41e2d |
| child 46956 | 9ff441f295c2 |
--- a/NEWS Thu Mar 15 19:02:34 2012 +0100 +++ b/NEWS Thu Mar 15 19:48:19 2012 +0100 @@ -371,6 +371,9 @@ *** ML *** +* Antiquotation @{keyword "name"} produces a parser for outer syntax +from a minor keyword introduced via theory header declaration. + * 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