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