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