src/ZF/listfn.thy
changeset 13209 e62a6bd3f085
parent 124 858ab9a9b047