I propose that dummylink & idi be marked with "(New usage is discouraged.)".
As noted in the text, they should normally never appear in a completed proof. Marking them this way will prevent them from being automatically used, and I think that's usually what is wanted. The normal mmj2 invocation has special case stuff to avoid its invocation, but that was created before we had the marking "(New usage is discouraged.)". Of course, someone can specifically *force* its use, but then it will noticed as such. I noticed this while trying to update the mmj2 tutorial. Does that seem reasonable? --- David A. Wheeler -- 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/E1iqmbZ-00085g-9o%40rmmprod07.runbox.
