src/HOL/Typedef.thy
changeset 27475 61b979a2c820
parent 27295 cfe5244301dd
child 28083 103d9282a946