src/HOL/Typedef.thy
changeset 29435 a5f84ac14609
parent 29056 dc08e3990c77
child 29608 564ea783ace8