> On Fri, 1 Nov 2019 20:17:56 -0400, Mario Carneiro <[email protected]> wrote: > On Fri, Nov 1, 2019 at 5:00 PM Norman Megill <[email protected]> wrote:
These are useful tips. I've tried to add a summary of these tips to mmnatded.raw.html in this pull request: https://github.com/metamath/set.mm/pull/1236 There is no label sumeq2dva ; I presume esumeq12dva was intended (if not, please let me know). --- 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/E1iQwtl-00015C-Ef%40rmmprod07.runbox.
