src/ZF/Datatype.thy
changeset 7145 c05373eebee3
parent 6070 032babd0120b
child 12175 5cf58a1799a7