src/HOL/Tools/Function/size.ML
changeset 36130 9a672f7d488d
parent 35756 cfde251d03a5
child 36610 bafd82950e24