src/HOL/Hyperreal/HyperNat.thy
changeset 24851 4e304aac841a
parent 23431 25ca91279a9b
child 25112 98824cc791c0