src/ZF/func.thy
changeset 82145 5b8639cb0d11
parent 81182 fc5066122e68