src/HOL/Tools/Function/sum_tree.ML
changeset 55407 81f7e60755c3
parent 55393 ce5cebfaedda
child 55414 eab03e9cee8a