It already is in the AFP:
https://www.isa-afp.org/theories/bernoulli/#Bernoulli
If I recall correctly, I took Lukas's theory from HOL-ex, added a lot of
my own stuff, and put it in the AFP (with his permission and with him as
a co-author).
As for why I did not delete the version in HOL-ex, I cannot remember –
perhaps because it still is a small and self-contained derivation of
that result.
Manuel
On 15/08/2022 15:31, Lawrence Paulson wrote:
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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
