src/HOL/Tools/typecopy.ML
changeset 38531 a11a1e4e0403
parent 38528 bbaaaf6f1cbe