On 15/08/2022 15:53, Manuel Eberl wrote:
It already is in the AFP: https://www.isa-afp.org/theories/bernoulli/#BernoulliIf 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.
It doesn't look much more self-contained than https://www.isa-afp.org/theories/bernoulli/#Bernoulli
Thus I am also in favour of deletiom. The NEWS entry can point to the AFP entry. Tobias
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-exLarry _______________________________________________ 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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
