src/HOL/Hyperreal/HyperDef.thy
changeset 20467 210b326a03c9
parent 20245 54db3583354f
child 20552 2c31dd358c21