diff -r b8dead547d9e -r 4c7cba1f7ce9 NEWS
--- a/NEWS	Mon Mar 01 17:07:36 2010 +0100
+++ b/NEWS	Mon Mar 01 17:09:42 2010 +0100
@@ -51,6 +51,10 @@
 datatype constructors have been renamed from InfixName to Infix etc.
 Minor INCOMPATIBILITY.
 
+* Commands 'type_notation' and 'no_type_notation' declare type syntax
+within a local theory context, with explicit checking of the
+constructors involved (in contrast to the raw 'syntax' versions).
+
 
 *** HOL ***