[isabelle-dev] Sum_of_powers

[Lukas Bulwahn]

Manuel, Larry, please simply delete the duplicate version. I assume
Manuel kept it because the Top 100 theorems list might refer to that
statement in that theory, but if that reference breaks, we can and
should just fix that and not keep this duplicate.

Lukas

On Mon, Aug 15, 2022 at 4:51 PM Manuel Eberl <manuel at pruvisto.org> wrote:
>
> No objections in principle, but as always, deleting it may break existing citations. We could leave it in and replace its content with just a link to the AFP entry. Or just delete it and not care about external references. I don't have any strong feelings about this – perhaps Lukas will comment on this as well.
>
> Manuel
>
>
> On 15/08/2022 16:41, Lawrence Paulson wrote:
>
> 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.