src/HOL/Typedef.thy
changeset 27885 76b51cd0a37c
parent 27295 cfe5244301dd
child 28083 103d9282a946