src/HOL/Hyperreal/transfer.ML
changeset 21471 03a5ef1936c5
parent 20049 f48c4a3a34bc
child 21506 b2a673894ce5
equal deleted inserted replaced
21470:7c1b59ddcd56 21471:03a5ef1936c5