src/HOL/Tools/Function/function.ML
changeset 39915 ecf97cf3d248
parent 39754 150f831ce4a3
child 40076 6f012a209dac