What logarithm functions are provided by standard sessions like HOL
, HOL-Library
, and HOL-Analysis
? There’s log
, but I can’t even get ln
.
And, more generally, how could I find this out myself? Search by browsing through https://isabelle.in.tum.de/library/HOL/index.html
needs quite some good guessing to be efficient, and automated search with https://search.isabelle.in.tum.de/
shows 920 hits when entering log
.
Last updated: Jul 15 2022 at 23:21 UTC