src/HOL/Tools/typedef.ML
changeset 62816 19387866eace
parent 62515 e73644de5db8
child 63003 bf5fcc65586b