Interesting. This is presumably a consequence of the recent (ish) change to the definition of the true constant and is also found at http://us.metamath.org/mpeuni/wal.html
Because this message is generated programmatically, the fix probably isn't as simple as one might think. So I guess I'll leave this to "Norm, others". On November 26, 2020 2:28:42 AM PST, Marnix Klooster <[email protected]> wrote: >Hello Norm, others, > >A quick bug report. I just noted that >http://us.metamath.org/ileuni/wal.html >incorrectly says "See definition df-tru ><http://us.metamath.org/ileuni/df-tru.html> 1245 for more information." > It >should probably instead say, "This syntax is primitive. The first axiom >using it is ...", like http://us.metamath.org/ileuni/wex.html says. > >Thanks. > >-Marnix >-- >Marnix Klooster >[email protected] > >-- >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/CAF7V2P-SZ%3DGMDZNu8Z3kgHZoK5hitSyZ%2BPKk_%2Bo0m5SDAO6s1A%40mail.gmail.com. -- 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/52843E85-2E6A-49D4-8A6E-EAFE8D365835%40panix.com.
