src/HOL/Tools/typecopy.ML
changeset 33252 8bd2eb003b8f
parent 32378 89b19ab3b35c
child 33314 53d49370f7af
equal deleted inserted replaced
33251:4b13ab778b78 33252:8bd2eb003b8f