src/HOL/ex/NatSum.ML
changeset 3564 f886dbd91ee5
parent 3269 eca2a3634acd
child 3648 bc2c363371ee