src/HOL/Hyperreal/Log.thy
changeset 14898 a25550451b51
parent 14430 5cb24165a2e1
child 15053 405be2b48f5b