src/HOL/Hyperreal/HyperDef.thy
changeset 21824 153fad1e7318
parent 21810 b2d23672b003
child 21855 74909ecaf20a