src/ZF/Datatype.thy
changeset 80180 e83b1489f4f2
parent 78800 0b3700d31758
child 80636 4041e7c8059d