"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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAMZ%3Dzj7ww62T8%2BnWz%2BjY%3D2%3D4aEBSiNVaEeNv6TEs7Ljt-G3G0A%40mail.gmail.com.