src/HOL/Tools/Function/function_core.ML
changeset 33806 dfca0f0e6397
parent 33671 4b0f2599ed48
child 33766 c679f05600cd