src/HOL/Typedef.thy
changeset 29609 a010aab5bed0
parent 29608 564ea783ace8
child 29797 08ef36ed2f8a