src/ZF/listfn.thy
changeset 2944 283e31f6a4be
parent 124 858ab9a9b047