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 <[email protected]>, 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.
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
