src/ZF/func.thy
changeset 79060 9f2040e5e2d6
parent 76217 8655344f1cf6
child 80754 701912f5645a