src/HOL/Hyperreal/transfer.ML
changeset 17740 fc385ce6187d
parent 17432 835647238122
child 17956 369e2af8ee45