src/HOL/Typedef.thy
changeset 25231 1aa9c8f022d0
parent 24269 4b2aac7669b3
child 25535 4975b7529a14