src/HOL/Tools/transfer.ML
changeset 48922 6f3ccfa7818d
parent 48066 c6783c9b87bf
child 49625 06cf80661e7a
equal deleted inserted replaced
48921:5d8d409b897e 48922:6f3ccfa7818d