src/HOL/Tools/Function/sum_tree.ML
changeset 37225 32c5251f78cd
parent 36773 acb789f3936b
child 37387 3581483cca6c