# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1720520630 -3600
# Node ID ae881e1480bbd104e286cc212808c20ade7e7dc4
# Parent  e066cc867115b9c3a156e029c766b4d05011ef68
NEWS: totalisation of ln

diff -r e066cc867115 -r ae881e1480bb 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 ***