src/HOL/Hyperreal/HyperNat.thy
changeset 11718 92706a69dacc
parent 11713 883d559b0b8c
child 13487 1291c6375c29