*** empty log message ***
authornipkow
Wed, 01 Dec 2004 18:17:01 +0100
changeset 15356 cfd08f5e0bdd
parent 15355 0de05d104060
child 15357 96698f16e3d9
*** empty log message ***
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