src/HOL/Hyperreal/HyperPow.thy
changeset 15251 bb6f072c8d10
parent 15229 1eb23f805c06
child 15360 300e09825d8b