changeset 81753 | 908c3b7b80c1 |
parent 81746 | 8b4340d82248 |
child 81759 | 1b817e64af3c |
--- a/NEWS Wed Jan 08 15:49:52 2025 +0100 +++ b/NEWS Thu Jan 09 10:13:05 2025 +0100 @@ -297,7 +297,7 @@ * Transitional theory "HOL.Divides" moved to "HOL-Library.Divides" and supposed to be removed in a future release. Minor INCOMPATIBILITY. -Import "HOL-Library.Divides" and keep an eye qualified names with prefix +Import "HOL-Library.Divides" and keep an eye on qualified names with prefix "Divides" to ease transition. * The real-valued versions of ln, log, powr have been totalised by "ln 0