src/HOL/Hyperreal/HyperNat.thy
changeset 17907 c20e4bddcb11
parent 17433 4cf2e7980529
child 19380 b808efaa5828