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/b8a73a3e-9a6c-4355-b391-4e5f80e51f4b%40googlegroups.com.
