src/ZF/listfn.thy
changeset 13807 a28a8fbc76d4
parent 124 858ab9a9b047