# HG changeset patch
# User wenzelm
# Date 1002135507 -7200
# Node ID 03c4a5c08a79cfded45c1d6d576f87be2137e97c
# Parent  e499dceca569b7a59b267aa2fad0547bc740ed9b
*** empty log message ***

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";