src/HOL/Tools/typecopy.ML
changeset 33020 0908ed080ccf
parent 32378 89b19ab3b35c
child 33314 53d49370f7af