src/HOL/ex/NatSum.ML
changeset 3362 0b268cff9344
parent 3269 eca2a3634acd
child 3648 bc2c363371ee