src/ZF/Induct/ListN.thy
changeset 80323 5e5dcebd1ed8
parent 76987 4c275405faae