src/HOL/Tools/Function/function.ML
changeset 39978 11bfb7e7cc86
parent 39754 150f831ce4a3
child 40076 6f012a209dac