src/HOL/Hyperreal/Log.thy
changeset 25322 e2eac0c30ff5
parent 21404 eb85850d3eb7