src/HOL/Tools/Function/function_common.ML
changeset 46377 dce6c3a460a9
parent 46042 ab32a87ba01a
child 46496 b8920f3fd259