src/HOL/Tools/legacy_transfer.ML
changeset 67161 b762ed417ed9
parent 66795 420d0080545f
equal deleted inserted replaced
67160:f37bf261bdf6 67161:b762ed417ed9