src/HOL/Sum.ML
changeset 10007 64bf7da1994a
parent 9311 ab5b24cbaa16