src/HOL/Hyperreal/NatStar.thy
changeset 20574 a10885a269cb
parent 19765 dfe940911617
child 20732 275f9bd2ead9