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