diff -r 9d2de9b6e7f4 -r 8f15fbce549f NEWS
--- a/NEWS	Fri Nov 10 16:26:44 2000 +0100
+++ b/NEWS	Fri Nov 10 16:31:28 2000 +0100
@@ -57,6 +57,9 @@
 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
 
+* >, >= 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);