src/ZF/func.thy
changeset 78021 ce6e3bc34343
parent 76217 8655344f1cf6
child 80754 701912f5645a