src/HOL/Tools/Function/fun.ML
changeset 58839 ccda99401bc8
parent 58826 2ed2eaabe3df
child 59159 9312710451f5