src/HOL/Tools/typecopy.ML
changeset 36017 7516568bebeb
parent 35994 9cc3df9a606e
child 36150 123f721c9a37