# HG changeset patch
# User wenzelm
# Date 1730025964 -3600
# Node ID fb391ad09b3cf01dd58713534b094e77bab43d6f
# Parent  b98595f82a889d27397372537a3ea23437ce344d
tuned;

diff -r b98595f82a88 -r fb391ad09b3c NEWS
--- a/NEWS	Sun Oct 27 11:34:51 2024 +0100
+++ b/NEWS	Sun Oct 27 11:46:04 2024 +0100
@@ -168,10 +168,10 @@
       image_mset_diff_if_inj
       minus_add_mset_if_not_in_lhs[simp]
 
-* Transitional theory "Divides" moved to "HOL-Library.Divides" and
+* 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 on theorems prefixed with
-"Divides." to ease transition.
+Import "HOL-Library.Divides" and keep an eye qualified names with prefix
+"Divides" to ease transition.
 
 * The real-valued versions of ln, log, powr have been totalised by
 "ln(0) = x" and "ln(-x) = ln(x)". Many related theorems are now