src/HOL/Hyperreal/transfer.ML
changeset 24325 5c29e8822f50
parent 24121 a93b0f4df838