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 ? Thanks, Benoît On Thursday, February 13, 2020 at 9:13:39 AM UTC+1, David Starner wrote: > > "bisymOLD" says "Obsolete theorem as of 27-May-2019." Unfortunately, > it's not marked as discouraged, and bj-bisym is now changing to be a > copy of it. Not a stop-the-world issue--a bug in set.mm, not > metamath--but bj-bisym should probably manually not be changed and > bisymOLD be marked as discouraged, unless other things start to depend > on bisymOLD. > > -- > Kie ekzistas vivo, ekzistas espero. > -- 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/60ecf266-6f3c-4c38-a2b3-0d2351a17df6%40googlegroups.com.
