src/ZF/Datatype.thy
changeset 79919 65e0682cca63
parent 78800 0b3700d31758
child 80636 4041e7c8059d