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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
