Thanks David. I looked at the corresponding MPE webpage (http://us2.metamath.org/mpeuni/mmtheorems21.html) and the following, and indeed aevALT ax16nfALT dral1ALT dveeq2ALT sbequ8ALT equsb3ALT should have the "(Proof modification is discouraged.)" tag. They already, and correctly, have the "(New usage is discouraged.)" tag.
This is probably due to Wolf and I moving around a few theorems (mainly Wolf reducing dependencies and moving theorems earlier, and me insisting to keep as *ALT versions shorter proofs using more axioms). This phenomenon is concentrated in this part of set.mm. 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/4faa7255-fb0a-4615-af96-efe00e891cbf%40googlegroups.com.
