src/ZF/listfn.thy
changeset 8766 1ef6e77e12ee
parent 124 858ab9a9b047