diff -r 6da9ae6d40f5 -r bfd4923b0957 NEWS
--- a/NEWS	Thu Dec 03 14:10:04 1998 +0100
+++ b/NEWS	Fri Dec 04 10:40:06 1998 +0100
@@ -9,6 +9,9 @@
 
 * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement
 
+*** General ***
+
+* in locales, the "assumes" and "defines" parts may be omitted if empty;
 
 *** Internal programming interfaces ***