src/HOL/Real/Hyperreal/HyperDef.thy
changeset 10662 cf6be1804912
parent 10607 352f6f209775