NEWS
changeset 6014 bfd4923b0957
parent 5973 040f6d2af50d
child 6028 1bfd52528bde
--- 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 ***