src/HOL/Tools/legacy_transfer.ML
changeset 59692 03aa1b63af10
parent 59621 291934bac95e
child 60784 4f590c08fd5d