src/ZF/Inductive.thy
changeset 74510 21a20b990724
parent 74296 abc878973216
child 76213 e44d86131648