src/HOL/Hyperreal/HyperDef.thy
changeset 15150 c7af682b9ee5
parent 15140 322485b816ac
child 15169 2b5da07a0b89