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 <[email protected]> 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 <[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
