[isabelle-dev] Sum_of_powers

[Lawrence Paulson]

I think it should be deleted. It’s confusing to have two copies of the same material, and I even wasted time trying to move the preliminaries out of there; perhaps they should be deleted as well.

Larry
On 15 Aug 2022, 14:54 +0100, Manuel Eberl <manuel at pruvisto.org>, wrote:

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220815/b8d2b0a4/attachment.htm>