src/HOL/Tools/typedef.ML
changeset 38638 94ed0f34aea2
parent 38388 94d5624dd1f7
child 38757 2b3e054ae6fc