src/ZF/func.thy
changeset 39128 93a7365fb4ee
parent 32960 69916a850301
child 41229 d797baa3d57c