src/HOL/Hyperreal/transfer.ML
changeset 21404 eb85850d3eb7
parent 20049 f48c4a3a34bc
child 21506 b2a673894ce5