nipkow at in.tum.de
Mon Aug 15 18:03:43 CEST 2022
On 15/08/2022 15:53, Manuel Eberl wrote:
> 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.
It doesn't look much more self-contained than
Thus I am also in favour of deletiom. The NEWS entry can point to the AFP entry.
> 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
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev