src/HOL/Tools/Function/size.ML
changeset 39459 7753083c00e6
parent 38348 cf7b2121ad9d
child 39557 fe5722fce758