src/HOL/Hyperreal/transfer.ML
changeset 20720 4358cd94a449
parent 20049 f48c4a3a34bc
child 21506 b2a673894ce5