src/HOL/Tools/typecopy.ML
changeset 31834 b7f1e86d9f04
parent 31735 a00292a5587d
child 32378 89b19ab3b35c