src/HOL/Hyperreal/Log.thy
changeset 24235 aea5c389a2f5
parent 21404 eb85850d3eb7