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