src/HOL/Tools/Function/fun.ML
changeset 58836 4037bb00d08e
parent 58826 2ed2eaabe3df
child 59159 9312710451f5