src/HOL/Hyperreal/HyperPow.thy
changeset 20830 65ba80cae6df
parent 20730 da903f59e9ba
child 21256 47195501ecf7