src/ZF/Datatype.thy
changeset 74759 32e95d996acc
parent 74294 ee04dc00bf0a
child 78790 8f4424187193
equal deleted inserted replaced
74758:570eae6e36b0 74759:32e95d996acc