NEWS
changeset 67999 1b05f74f2e5f
parent 67993 271e2d84e7a3
child 68003 9b89d831dc80
child 68072 493b818e8e10
     1.1 --- a/NEWS	Tue Apr 17 22:35:48 2018 +0100
     1.2 +++ b/NEWS	Wed Apr 18 15:57:36 2018 +0100
     1.3 @@ -209,6 +209,10 @@
     1.4  choice operator. The dual of this property is also proved in 
     1.5  Hilbert_Choice.thy.
     1.6  
     1.7 +* New syntax for the minimum/maximum of a function over a finite set:
     1.8 +MIN x\<in>A. B  and even  MIN x. B (only useful for finite types), also
     1.9 +MAX.
    1.10 +
    1.11  * Clarifed theorem names:
    1.12  
    1.13    Min.antimono ~> Min.subset_imp
    1.14 @@ -255,8 +259,9 @@
    1.15  
    1.16  * HOL-Algebra: renamed (^) to [^]
    1.17  
    1.18 -* Session HOL-Analysis: Moebius functions and the Riemann mapping
    1.19 -theorem.
    1.20 +* Session HOL-Analysis: Moebius functions, the Riemann mapping
    1.21 +theorem, the Vitali covering theorem, change-of-variables results for
    1.22 +integration and measures.
    1.23  
    1.24  * Class linordered_semiring_1 covers zero_less_one also, ruling out
    1.25  pathologic instances. Minor INCOMPATIBILITY.