--- a/NEWS Tue Apr 17 22:35:48 2018 +0100
+++ b/NEWS Wed Apr 18 15:57:36 2018 +0100
@@ -209,6 +209,10 @@
choice operator. The dual of this property is also proved in
Hilbert_Choice.thy.
+* New syntax for the minimum/maximum of a function over a finite set:
+MIN x\<in>A. B and even MIN x. B (only useful for finite types), also
+MAX.
+
* Clarifed theorem names:
Min.antimono ~> Min.subset_imp
@@ -255,8 +259,9 @@
* HOL-Algebra: renamed (^) to [^]
-* Session HOL-Analysis: Moebius functions and the Riemann mapping
-theorem.
+* Session HOL-Analysis: Moebius functions, the Riemann mapping
+theorem, the Vitali covering theorem, change-of-variables results for
+integration and measures.
* Class linordered_semiring_1 covers zero_less_one also, ruling out
pathologic instances. Minor INCOMPATIBILITY.