*** empty log message ***
authornipkow
Mon, 12 Aug 2002 17:59:57 +0200
changeset 13492 6aae8eb39a18
parent 13491 ddf6ae639f21
child 13493 5aa68c051725
*** empty log message ***
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;