src/HOL/Hyperreal/HyperNat.thy
changeset 22143 cf58486ca11b
parent 21865 55cc354fd2d9
child 23431 25ca91279a9b