src/HOL/Sum.ML
changeset 4987 257aeccdefc3
parent 4830 bd73675adbed
child 4988 8f4dc836a2ea