# HG changeset patch
# User nipkow
# Date 959065698 -7200
# Node ID f4599af94b834ac471da16729dfd069cf5eb8d87
# Parent  c434283b4cfa71339d5b9001cdd1d6272175011d
SetInterval

diff -r c434283b4cfa -r f4599af94b83 NEWS
--- 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,