changeset 13492 | 6aae8eb39a18 |
parent 13478 | 9cfbcb9acfef |
child 13500 | 2222c7a0e8bb |
--- 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;