src/HOL/Tools/typedef.ML
changeset 60651 1049f3724ac0
parent 59936 b8ffc3dc9e24
child 61103 8ed21464e260