src/HOL/Tools/Function/sum_tree.ML
changeset 37313 715d25555ca6
parent 36773 acb789f3936b
child 37387 3581483cca6c