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