src/HOL/Sum.ML
changeset 10379 93630e0c5ae9
parent 9311 ab5b24cbaa16