src/ZF/Datatype.thy
changeset 74510 21a20b990724
parent 74294 ee04dc00bf0a
child 78790 8f4424187193