src/HOL/Hyperreal/HyperDef.thy
changeset 20343 e093a54bf25e
parent 20245 54db3583354f
child 20552 2c31dd358c21