NEWS: totalisation of ln
authorpaulson <lp15@cam.ac.uk>
Tue, 09 Jul 2024 11:23:50 +0100
changeset 80530 ae881e1480bb
parent 80529 e066cc867115
child 80531 c54a4c2db5b7
NEWS: totalisation of ln
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 ***