corrected
authorhaftmann
Thu, 09 Jan 2025 10:13:05 +0100
changeset 81753 908c3b7b80c1
parent 81752 a1743b71092e
child 81754 e7a77c795cf9
child 81755 1609254b74c5
corrected
NEWS
--- 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