src/ZF/Datatype.thy
changeset 12587 3f3d2ffb5df5
parent 12183 c10cea75dd56
child 13328 703de709a64b