src/HOL/Typedef.thy
changeset 29795 c78806b621e1
parent 29608 564ea783ace8
child 29797 08ef36ed2f8a
equal deleted inserted replaced
29794:32d00a2a6f28 29795:c78806b621e1