src/HOL/Typedef.thy
changeset 29183 f1648e009dc1
parent 29056 dc08e3990c77
child 29608 564ea783ace8