src/HOL/Typedef.thy
changeset 27549 0525f5785155
parent 27295 cfe5244301dd
child 28083 103d9282a946