src/HOL/Tools/legacy_transfer.ML
changeset 67403 90fe8c635ba0
parent 66795 420d0080545f
equal deleted inserted replaced
67402:b71431a2051e 67403:90fe8c635ba0