src/HOL/Hyperreal/HyperPow.thy
changeset 20700 7e3450c10c2d
parent 20541 f614c619b1e1
child 20730 da903f59e9ba