[isabelle-dev] NEWS: totalisation of ln

Lawrence Paulson lp15 at cam.ac.uk
Tue Jul 9 12:24:21 CEST 2024


* 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.

Larry



More information about the isabelle-dev mailing list