src/HOL/Hyperreal/NatStar.thy
changeset 21145 87a03f9b7db2
parent 20740 5a103b43da5a
child 21404 eb85850d3eb7