diff -r fcc7a78b7220 -r 0b088316b8a3 NEWS
--- a/NEWS	Thu Jan 02 12:14:51 2025 +0100
+++ b/NEWS	Thu Jan 02 12:49:39 2025 +0100
@@ -240,7 +240,9 @@
     This outputs a suggestion with instantiations of the facts using the
     "of" attribute (e.g. "assms(1)[of x]").
 
-* Theory "HOL-Library/Discrete" has been renamed "HOL-Library/Discrete_Functions"
+* Theory HOL-Library.Discrete has been renamed
+HOL-Library.Discrete_Functions
+
   Discrete.log -> floor_log
   Discrete.sqrt -> floor_sqrt
   Renamed lemmas accordingly (...log/sqrt... -> ...floor_log/sqrt...)
@@ -286,10 +288,9 @@
 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
-unconditional, with ln_mult_pos and ln_divide_pos introduced for legacy
-purposes.
+* 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 unconditional,
+with ln_mult_pos and ln_divide_pos introduced for legacy purposes.
 
 
 *** ML ***