src/HOL/Tools/Function/size.ML
changeset 39915 ecf97cf3d248
parent 39557 fe5722fce758
child 40627 becf5d5187cc