src/HOL/Hyperreal/HyperDef.thy
changeset 19988 05f940b9ef15
parent 19931 fb32b43e7f80
child 20245 54db3583354f