src/HOL/Fun.ML
changeset 9993 c0f7fb6e538e
parent 9970 dfe4747c8318
child 10066 2f5686cf8c9a