On Thursday, February 13, 2020 at 5:06:27 PM UTC+1, Norman Megill wrote: > > On Thursday, February 13, 2020 at 9:25:42 AM UTC-5, Benoit wrote: >> >> David: yes, ~bisymOLD and ~bi3antOLD should have both discouragement >> tags. I'm away from my main computer... can you add them ? >> >> Actually, most *OLD and *ALT should probably have both discouragement >> tags as well, it seems ? >> > > I think so. This can be checked by making sure all *OLD and *ALT labels > have both discouragements in the 'discouraged' file. There might be rare > exceptions for *ALT although I can't remember - e.g. we don't necessarily > want to prevent a shorter proof for a *ALT that occurs before the non-ALT. > I should look at each *ALT case with a missing discouragement. > > I think the *OLD theorems are no problem, they will be removed anyway sooner or later. But with the *ALT theorems we should be careful. E.g. ~nnindALT and ~nn0indALT have neither of the discouragement tags. Or ~ccat2s1fvwALT with "New usage is discouraged." only, which has a shorter proof than ~ccat2s1fvw (but occurs before the ALT-version!), but is requiring an additional definition. It would not harm (and would even be desirable) if the proof could be shortened further.
I would propose that a list of all *ALT theorems not having both discouragement tags is created and provided for review (preferably in a separate thread). -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2727fa99-94cb-4d98-b38d-fa08e44973bd%40googlegroups.com.
