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
