src/HOL/Hyperreal/NatStar.thy
changeset 20830 65ba80cae6df
parent 20740 5a103b43da5a
child 21404 eb85850d3eb7