1.1 --- a/NEWS	Wed Oct 10 17:31:56 2007 +0200
     1.2 +++ b/NEWS	Wed Oct 10 17:31:58 2007 +0200
     1.3 @@ -371,8 +371,10 @@
     1.4  
     1.5  * Isar/locales: 'notation' provides a robust interface to the 'syntax'
     1.6  primitive that also works in a locale context (both for constants and
     1.7 -fixed variables).  Type declaration and internal syntactic
     1.8 -representation of given constants retrieved from the context.
     1.9 +fixed variables). Type declaration and internal syntactic representation
    1.10 +of given constants retrieved from the context. Likewise, the
    1.11 +'no_notation' command allows to remove given syntax annotations from the
    1.12 +current context.
    1.13  
    1.14  * Isar/locales: new derived specification elements 'axiomatization',
    1.15  'definition', 'abbreviation', which support type-inference, admit