src/ZF/func.ML
changeset 798 31ec33d96231
parent 760 f0200e91b272
child 824 120fc7e857ba