src/ZF/func.thy
changeset 81773 5df6481f45f9
parent 81182 fc5066122e68