src/HOL/Tools/Function/measure_functions.ML
changeset 37493 2377d246a631
parent 37387 3581483cca6c
child 37678 0040bafffdef