src/HOL/ex/NatSum.thy
changeset 79596 1b3770369ee7
parent 68224 1f7308050349