# HG changeset patch
# User nipkow
# Date 974102037 -3600
# Node ID 96529827ff71d1319bf892d79f2e6f9bf58716b9
# Parent  a8d9a79ed95e6668ef1c5eea6179e3a71682029e
Removed > and >=

diff -r a8d9a79ed95e -r 96529827ff71 NEWS
--- 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);