src/HOL/Typedef.thy
changeset 29214 76c7fc5ba849
parent 29056 dc08e3990c77
child 29608 564ea783ace8