src/HOL/Sum.ML
changeset 7257 745cfc8871e2
parent 7254 fc7f95f293da
child 7293 959e060f4a2f