NEWS

--- a/NEWS	Wed Dec 01 18:11:50 2004 +0100
+++ b/NEWS	Wed Dec 01 18:17:01 2004 +0100
@@ -192,6 +192,8 @@
   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/SetInterval: The syntax for open intervals has changed:
 
   Old         New