src/ZF/Induct/Datatypes.thy
changeset 78395 c39819e3adc5
parent 76217 8655344f1cf6