src/HOL/Hyperreal/transfer.ML
changeset 22172 e7d6cb237b5e
parent 21708 45e7491bea47
child 22739 d12a9d75eee6
equal deleted inserted replaced
22171:58f554f51f0d 22172:e7d6cb237b5e