src/ZF/Datatype.thy
changeset 80567 b2c14b489e60
parent 78800 0b3700d31758
child 80636 4041e7c8059d