src/HOL/Tools/typecopy.ML
changeset 37252 b79df37bbdc4
parent 36610 bafd82950e24
child 37469 1436d6f28f17