src/HOL/Hyperreal/NatStar.thy
changeset 15175 b62f7b493360
parent 15169 2b5da07a0b89
child 15360 300e09825d8b
equal deleted inserted replaced
15174:fff9c761f89e 15175:b62f7b493360