src/HOL/Tools/typecopy.ML
changeset 33354 1f70087cdef5
parent 33314 53d49370f7af
child 33522 737589bb9bb8