src/HOL/Hyperreal/NatStar.thy
changeset 20667 953b68f4a9f3
parent 19765 dfe940911617
child 20732 275f9bd2ead9