On Tuesday, February 25, 2020 at 7:00:48 PM UTC+1, Norman Megill wrote: > > Since there were no other replies, unfortunately I just updated set.mm > with both discouragements on every ALT because of the problems they were > creating. I suppose I could revert and do the analysis all over, but I > want to get the minimizations applied soon without unwanted side effects. > How many of your theorems does this affect? > Sorry, I was on a journey over the weekend... But don't worry, there are some ALT definitions/theorems in my mathbox about magmas/semigroups and graphs which are affected. For these, I can take care by myself. So if we use ALT for alternate proofs only (in the future), we could use Alt for "alternate definitions/variants of theorems". Then we can check the tags for *ALT theorems, and will have no checks for *Alt theorems.
-- 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/c2235e70-b964-488c-8ce1-09ff69d162bb%40googlegroups.com.
