SetInterval

--- a/NEWS	Tue May 23 07:32:24 2000 +0200
+++ b/NEWS	Tue May 23 09:08:18 2000 +0200
@@ -161,6 +161,9 @@
 individually as well, resulting in a separate list of theorems for
 each equation;
 
+* HOL: new (overloaded) notation for the set of elements below/above some
+element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval.
+
 * HOL: theorems impI, allI, ballI bound as "strip";
 
 * theory Sexp now in HOL/Induct examples (used to be part of main HOL,