src/HOL/typedef.ML
changeset 4862 613ce4cc303f
parent 4409 2af86fcb97d7