src/HOL/Tools/Function/measure_functions.ML
changeset 31816 ffaf6dd53045
parent 31775 2b04504fcb69
child 31902 862ae16a799d