src/ZF/func.thy
changeset 81812 232ccd03d9af
parent 81182 fc5066122e68