src/HOL/Hyperreal/HyperPow.thy
changeset 21594 2859c94d67d4
parent 21404 eb85850d3eb7
child 21848 b35faf14a89f