src/HOL/Hyperreal/HyperNat.thy
changeset 14898 a25550451b51
parent 14738 83f1a514dcb4
child 15053 405be2b48f5b