src/HOL/Tools/legacy_transfer.ML
changeset 47356 19fb95255ec9
parent 47324 ed2bad9b7c6a
child 47455 26315a545e26
equal deleted inserted replaced
47355:3d9d98e0f1a4 47356:19fb95255ec9