# HG changeset patch
# User nipkow
# Date 1101984295 -3600
# Node ID bb2dd95c8c5e0040ff37b95d683373fef910283e
# Parent  300e09825d8b64d6d1bd5d7ef08122339efbfd61
*** empty log message ***

diff -r 300e09825d8b -r bb2dd95c8c5e NEWS
--- a/NEWS	Thu Dec 02 11:42:01 2004 +0100
+++ b/NEWS	Thu Dec 02 11:44:55 2004 +0100
@@ -192,7 +192,9 @@
   Moreover, the mathematically important symbolic identifier
   \<epsilon> becomes available as variable, constant etc.
 
-* HOL: "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x"
+* HOL: "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
+  Similarly for all quantifiers: "ALL x > y" etc.
+  The x-symbol for >= is \<ge>.
 
 * HOL/SetInterval: The syntax for open intervals has changed: