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