On November 26, 2020 11:09:53 AM PST, Norman Megill wrote:
>df-tru has been nothing but trouble, and sometimes I rue the day it
>escaped
>from a mathbox. :)
Haha yeah it has been, hasn't it?
I suspect we're pretty much stuck with it, especially in iset.mm, because
The current web page generation algorithm looks for the next "$a |-" using
the syntax. If its label starts with "ax-" the syntax is called "primitive"
on the web page. I'll have to add an exception for the case of wal, which
I'll try to do in the next release of metamath.exe.
df-tru has been
