[isabelle-dev] Sum_of_powers

[Manuel Eberl]

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