src/HOL/ex/NatSum.thy
changeset 81364 84e4388f8ab1
parent 68224 1f7308050349