src/HOL/Typedef.thy
changeset 29686 4cd2874eb5ff
parent 29608 564ea783ace8
child 29797 08ef36ed2f8a