src/HOL/Tools/Function/function_common.ML
changeset 60987 ea00d17eba3b
parent 60682 5a6cd2560549
child 61112 e966c311e9a7