src/HOL/ex/NatSum.thy
changeset 82734 89347c0cc6a3
parent 68224 1f7308050349