[isabelle-dev] Sum_of_powers

[Tobias Nipkow]

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 
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-ex
>>
>> Larry
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220815/bb11f363/attachment.bin>