src/HOL/Tools/Function/sum_tree.ML
changeset 80729 dff10bb4ebdb
parent 69593 3dda49e08b9d
child 82967 73af47bc277c
equal deleted inserted replaced
80728:bb292fc53f82 80729:dff10bb4ebdb