src/HOL/ex/NatSum.thy
changeset 80317 be2e772e0adf
parent 68224 1f7308050349