src/HOL/Hyperreal/HLog.thy
changeset 20700 7e3450c10c2d
parent 19765 dfe940911617
child 21404 eb85850d3eb7