src/HOL/Tools/typecopy.ML
changeset 33354 1f70087cdef5
parent 33314 53d49370f7af
child 33522 737589bb9bb8
equal deleted inserted replaced
33353:17d9c977f928 33354:1f70087cdef5