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