Hi David! You=E2=80=99re right! Then the integral of the exponential function (df-ef) shall be in a theorem c= alled itgef.
And =E2=80=9Cexp=E2=80=9D alone could name both x^A and A^x, so I believe =E2= =80=9Citgmon=E2=80=9D (for monomial) would be a better choice, but then it w= ould be nice to document it, since it does not correspond to any df- definit= ion! BR, _ Thierry _ Thierry > Le 13 juin 2019 =C3=A0 01:15, David A. Wheeler <[email protected]> a =C3= =A9crit : >=20 >> On Thu, 13 Jun 2019 00:45:47 +0800, Thierry Arnoux <[email protected]= t> wrote: >> The table in the "convention" lists /some commonly used/ abbreviations. >>=20 >> Shall we try to make it as exhaustive as possible so that it becomes a >> /reference/, which can be used when one wants to find an existing >> theorem, or name a new one? >=20 > If we made an exhaustive table then it'd have to include all the "df-..." e= ntries. > Ignoring mathboxes, that would require 779 definitions, only a few of > which are there now (counted with grep 'df-.*$a' ,set.mm | wc -l). >=20 > That's a pretty big table. > I think the shorter table is easier to deal with, so I don't think we > should eliminate the short table. >=20 > If you want an exhaustive table, > we could create a script to automatically generate > an exhaustive table by combining the short table and the "df-... $a" defin= itions. > We could run that once & edit by hand, or just rerun the script > to keep generating the full table. An exhaustive table produced from a > script is more likely to actually stay correct, once it's correct :-). >=20 > --- David A. Wheeler >=20 > --=20 > 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 e= mail to [email protected]. > To view this discussion on the web visit https://groups.google.com/d/msgid= /metamath/E1hb6qL-0005Yf-6C%40rmmprod07.runbox. -- 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/F3DDE375-C625-4FEF-BB48-EC0A69568DE7%40gmx.net.
