src/HOL/Tools/Function/sum_tree.ML
changeset 37388 793618618f78
parent 37387 3581483cca6c
child 37678 0040bafffdef