src/HOL/Typedef.thy
changeset 37979 0f21ebea4a73
parent 37863 7f113caabcf4
child 38393 7c045c03598f