NEWS

   The symbol \<some> is displayed as the alternative epsilon of LaTeX
   and x-symbol; use option '-m epsilon' to get it actually printed.
   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:
 
   Old         New
   {..n(}   -> {..<n}