src/HOL/Tools/legacy_transfer.ML
changeset 67543 e8b2d85e4a8b
parent 66795 420d0080545f
equal deleted inserted replaced
67542:7afca3218b65 67543:e8b2d85e4a8b