Removed > and >=

--- a/NEWS	Mon Nov 13 08:53:21 2000 +0100
+++ b/NEWS	Mon Nov 13 08:53:57 2000 +0100
@@ -60,9 +60,6 @@
 
 * added overloaded operations "inverse" and "divide" (infix "/");
 
-* >, >= and \<ge> can now be used for input; they are immediately replaced
-  by the converse symbol, eg "x > y" by "y < x".
-
 * HOL/typedef: simplified package, provide more useful rules (see also
 HOL/subset.thy);