src/HOL/Hyperreal/HyperDef.thy
changeset 20830 65ba80cae6df
parent 20765 807c5f7dcb94
child 21210 c17fd2df4e9e