src/HOL/Hyperreal/HyperNat.thy
changeset 13049 ce180e5b7fa0
parent 11713 883d559b0b8c
child 13487 1291c6375c29