# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1707307042 0
# Node ID 924e487288fb1070cc0d47491046597941c67cc4
# Parent  a521c241e946b28f52717a2d646fc15d0da04bdf
NEWS: corrected the definition of convexity of functions

diff -r a521c241e946 -r 924e487288fb NEWS
--- a/NEWS	Wed Feb 07 11:52:34 2024 +0000
+++ b/NEWS	Wed Feb 07 11:57:22 2024 +0000
@@ -25,6 +25,9 @@
   by Sledgehammer and should be used instead. For more information, see
   Sledgehammer's documentation relating to "preplay_timeout". INCOMPATIBILITY.
 
+* HOL-Analysis: corrected the definition of convex function (convex_on)
+  to require the underlying set to be convex. INCOMPATIBILITY.
+
 * Explicit type class for discrete_linear_ordered_semidom for integral
   semidomains with a discrete linear order.