diff -r c966a1aab860 -r 03d2a2d0ee4a NEWS
--- a/NEWS	Thu Apr 29 17:29:53 2010 +0200
+++ b/NEWS	Thu Apr 29 17:47:53 2010 +0200
@@ -64,6 +64,11 @@
 
 * Type constructors admit general mixfix syntax, not just infix.
 
+* Concrete syntax may be attached to local entities without a proof
+body, too.  This works via regular mixfix annotations for 'fix',
+'def', 'obtain' etc. or via the explicit 'write' command, which is
+similar to the 'notation' command in theory specifications.
+
 * Use of cumulative prems via "!" in some proof methods has been
 discontinued (legacy feature).
 
@@ -7004,3 +7009,5 @@
 types;
 
 :mode=text:wrap=hard:maxLineLen=72:
+
+ LocalWords:  def