src/ZF/Datatype.thy
changeset 80316 82c20eaad94a
parent 78800 0b3700d31758
child 80636 4041e7c8059d