# HG changeset patch
# User nipkow
# Date 1029167997 -7200
# Node ID 6aae8eb39a184f49deeb0cce275f08aa5573259d
# Parent  ddf6ae639f21bde0efcd075ae2bb0411dc671d9e
*** empty log message ***

diff -r ddf6ae639f21 -r 6aae8eb39a18 NEWS
--- a/NEWS	Mon Aug 12 17:48:19 2002 +0200
+++ b/NEWS	Mon Aug 12 17:59:57 2002 +0200
@@ -1,4 +1,3 @@
-
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
@@ -35,6 +34,9 @@
 * 'typedef' command has new option "open" to suppress the set
 definition;
 
+* Functions Min and Max on finite sets have been introduced.
+  (theory Finite_Set)
+
 * attribute [symmetric] now works for relations as well; it turns
 (x,y) : R^-1 into (y,x) : R, and vice versa;