src/HOL/Tools/legacy_transfer.ML
changeset 60451 1f2b29f78439
parent 59621 291934bac95e
child 60784 4f590c08fd5d
equal deleted inserted replaced
60450:b54b913dfa6a 60451:1f2b29f78439