src/HOL/ex/NatSum.thy
changeset 78851 db37cae970a6
parent 68224 1f7308050349