| changeset 79584 | 924e487288fb |
| parent 79575 | b21d8401f0ca |
| child 79599 | 2c18ac57e92e |
| child 79611 | 97612262718a |
--- 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.