Thanks both for the help, that is very kind. One problem I came across while tracking down which theorems used the ones in 18.1.7 is I came across several in mathboxes. For example ghomf1o <http://us.metamath.org/mpeuni/ghomf1o.html> relies on ghomid which is in 18.1.7.
My general question is how should theorems in mathboxes be handled if we are discussing removing 18.1.7? Do we need to replicate all theorems using the extensible structures in including all the ones in math boxes? What if they are odd theorems that other people aren't so interested in? Can we contact people and ask them to transfer them themselves? Is it ok to delete things from mathboxes without replacing them (I imagine this might be a problem for some people)? I feel this is a bit above my paygrade. 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? 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? In that vein could I ask for some help with the following pairs? I think I have found the right thing but I am not sure. Is ghsubablo <http://us.metamath.org/mpeuni/ghsubablo.html> covered by ghmabl <http://us.metamath.org/mpeuni/ghmabl.html> or is it to general? Is ghsubgo <http://us.metamath.org/mpeuni/ghsubgo.html> covered by ghmima <http://us.metamath.org/mpeuni/ghmima.html>? Is elghom <http://us.metamath.org/mpeuni/elghom.html>paired with isghm <http://us.metamath.org/mpeuni/isghm.html>? They use quite different symbols. For the rest <https://docs.google.com/spreadsheets/d/19Msa6Qib2oe1zA2QIDWKRjPQvq-08DlbuWVUADV4d04/edit?usp=sharing> I think I have all the pairs correct. -- 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/357681d5-6aa6-481f-979b-8b63228a690b%40googlegroups.com.
