Stream: General

Topic: Logarithms


view this post on Zulip Wolfgang Jeltsch (Nov 28 2021 at 21:08):

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