src/HOL/Hyperreal/HyperPow.thy
changeset 14100 804be4c4b642
parent 11713 883d559b0b8c
child 14348 744c868ee0b7