src/HOL/Tools/Function/function_common.ML
changeset 50705 0e943b33d907
parent 49979 4de92b4aa74a
child 52383 71df93ff010d