# HG changeset patch
# User paulson
# Date 912764406 -3600
# Node ID bfd4923b0957a9c55efb614052f04fe0d32dfa9f
# Parent  6da9ae6d40f5cbe7d6c849a0d45bfa937cac928b
locales

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 ***