src/HOL/Hyperreal/HyperNat.thy
changeset 13207 0d07e49dc9a5
parent 11713 883d559b0b8c
child 13487 1291c6375c29