manuel at pruvisto.org
Mon Aug 15 16:51:28 CEST 2022
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.
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.
> 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...
More information about the isabelle-dev