On Wednesday, March 4, 2020 at 5:46:58 AM UTC-5, Jon P wrote: > > ... >
> I think I might narrow my efforts down a bit just to doing theorem pairing > (finding the new theorem which is the equivalent to the old). This is a > task that needs to be done for all of parts 18, 19 and 20 and is > non-controversial. I noticed some theorems, for example smgrpismgmOLD > <http://us.metamath.org/mpeuni/ghomf1o.html>, have in their description a > link to their new theorem. Is it ok if I start submitting pull requests > which add links to theorems for which I have found pairs? > Yes. > Is it ok to add OLD to the name, presumably that is not allowed if there > are any theorems that depend on it as it would break verification? > It won't break verification until the OLD is deleted. However, if all theorems using it are also OLD (and with an earlier obsolescence date), it will be fine. Indeed you may have to do that (i.e. rename theorems with usage to *OLD) once you start working back from endpoint theorems, since we don't actually delete them immediately but rename them to *OLD. Norm -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a7009e38-14d4-4ece-8fd1-635462b34625%40googlegroups.com.
