src/HOL/Hyperreal/transfer.ML
changeset 21776 e65109e168f3
parent 21708 45e7491bea47
child 22739 d12a9d75eee6