diff -r e499dceca569 -r 03c4a5c08a79 NEWS
--- a/NEWS	Wed Oct 03 20:55:31 2001 +0200
+++ b/NEWS	Wed Oct 03 20:58:27 2001 +0200
@@ -27,6 +27,8 @@
 
 *** HOL ***
 
+* HOL: linorder_less_split superseded by linorder_cases;
+
 * HOL: added "The" definite description operator; move Hilbert's "Eps"
 to peripheral theory "Hilbert_Choice";
 
@@ -69,6 +71,8 @@
 * Classical reasoner: renamed addaltern to addafter, addSaltern to
 addSafter;
 
+* syntax: support non-oriented infixes;
+
 * print modes "type_brackets" and "no_type_brackets" control output of
 nested => (types); the default behavior is "brackets";