src/HOL/Tools/typedef.ML
changeset 62722 f5ee068b96a6
parent 62515 e73644de5db8
child 63003 bf5fcc65586b