src/ZF/func.thy
changeset 39190 a2775776be3f
parent 32960 69916a850301
child 41229 d797baa3d57c