src/ZF/Datatype.thy
changeset 8913 0bc13d5e60b8
parent 6070 032babd0120b
child 12175 5cf58a1799a7