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