Thanks. I'll take care of adding the discouragement tags. I just wanted agreement that it is the correct thing to do.
Norm On Saturday, February 22, 2020 at 8:30:30 PM UTC-5, Benoit wrote: > > I think that the *ALT and *OLD theorems appearing in the list (and those I > quoted earlier in this thread) can be given both discouragement tags. This > will take care of most of "my" cases (and others). I can do it if Norm > wants. As for the other minimizations of theorems of the form bj-* in this > list, it's better to add a proof modif discouragement tag. I can also do > it if Norm prefers. > > Benoît > -- 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/e6e6ea29-f67d-424e-9722-22dee254cb9f%40googlegroups.com.
