src/HOL/Hyperreal/HyperNat.thy
changeset 18960 9881ff995ff5
parent 17433 4cf2e7980529
child 19380 b808efaa5828