src/HOL/Hyperreal/NatStar.ML
changeset 10784 27e4d90b35b5
parent 10778 2c6605049646
child 10797 028d22926a41