src/HOL/Hyperreal/transfer.ML
changeset 22999 c1ce129e6f9c
parent 22846 fb79144af9a3
child 24039 273698405054
equal deleted inserted replaced
22998:97e1f9c2cc46 22999:c1ce129e6f9c