src/HOL/typedef.ML
changeset 4255 63ab0616900b
parent 4028 01745d56307d
child 4409 2af86fcb97d7