src/ZF/Induct/ListN.thy
changeset 78395 c39819e3adc5
parent 76987 4c275405faae