src/HOL/Sum.ML
changeset 4876 1c502a82bcde
parent 4830 bd73675adbed
child 4988 8f4dc836a2ea