src/HOL/Tools/legacy_transfer.ML
changeset 56366 0362c3bb4d02
parent 51717 9e7d1c139569
child 58824 d480d1d7c544
equal deleted inserted replaced
56365:713f9b9a7e51 56366:0362c3bb4d02