NEWS

--- a/NEWS	Fri Oct 12 21:22:35 2012 +0200
+++ b/NEWS	Fri Oct 12 21:39:58 2012 +0200
@@ -62,6 +62,13 @@
 
 *** HOL ***
 
+* Simplified 'typedef' specifications: historical options for implicit
+set definition and alternative name have been discontinued.  The
+former behavior of "typedef (open) t = A" is now the default, but
+written just "typedef t = A".  INCOMPATIBILITY, need to adapt theories
+accordingly.
+
+
 * Theory "Library/Multiset":
 
   - Renamed constants