NEWS

--- a/NEWS	Mon Jul 08 22:28:02 2024 +0100
+++ b/NEWS	Tue Jul 09 11:23:50 2024 +0100
@@ -47,6 +47,10 @@
 "HOL-Library.Divides" and keep an eye on theorems prefixed with "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.
 
 *** System ***