src/HOL/Typedef.thy
changeset 27865 27a8ad9612a3
parent 27295 cfe5244301dd
child 28083 103d9282a946