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