I think that HOL/ex/Sum_of_Powers.thy should be moved to the AFP. It is a significant result: that the sum of the K-th powers of the first N positive integers is a polynomial in N. Using Bernoulli numbers and Bernoulli polynomials. This should not be hidden away in HOL-ex Larry