src/HOL/Tools/legacy_transfer.ML
changeset 59977 ad2d1cd53877
parent 59621 291934bac95e
child 60784 4f590c08fd5d