src/HOL/Hyperreal/HyperDef.thy
changeset 20192 956cd30ef3be
parent 19931 fb32b43e7f80
child 20245 54db3583354f