NEWS

--- a/NEWS	Thu Feb 06 16:44:50 2025 +0100
+++ b/NEWS	Thu Feb 06 16:21:00 2025 +0000
@@ -343,6 +343,8 @@
 * Theory "HOL-Library.Suc_Notation" provides compact notation for
 iterated Suc terms.
 
+* Theory "HOL.Nat": of_nat_diff is now a simprule, minor INCOMPATIBILITY.
+
 * Theory "HOL-Library.Adhoc_Overloading" has been moved to Pure. Minor
 INCOMPATIBILITY: need to adjust theory imports.