src/HOL/Sum.ML
changeset 11025 a70b796d9af8
parent 9311 ab5b24cbaa16