src/ZF/listfn.thy
changeset 9188 379b0c3f7c85
parent 124 858ab9a9b047