src/HOL/Tools/legacy_transfer.ML
changeset 60597 2da9b632069b
parent 59621 291934bac95e
child 60784 4f590c08fd5d