src/ZF/listfn.thy
changeset 8434 5e4bba59bfaa
parent 124 858ab9a9b047