"Claim" has been added in metamath.exe version 0.182. I didn't add "Case" because it seemed to me that it would almost always be accompanied by another keyword, and in "Theorem 1.1 Case 2" it would cause the theorem number to be omitted. But I'm willing to reconsider that. (The algorithm scans backwards from the [author] tag until a keyword is found.)
On Sunday, April 5, 2020 at 2:09:21 PM UTC-4, David A. Wheeler wrote: > > On Sun, 5 Apr 2020 08:10:56 -0700 (PDT), Norman Megill wrote: > > That's a good idea. Give me about a week to release a new version with > > this keyword. If you think of any others that would be useful let me > know. > > I agree. Let's make sure we update the "conventions" section to match. > The current list of keywords is always given by "help write bibliography". It might be better if the conventions reference the help command rather than duplicating the list, otherwise there is a risk of it getting out of sync. I am also wondering if it might be better to specify the list in the $t comment (the one with the htmldefs) in set.mm rather than having it hard-coded in metamath.exe. Any opinions? > > Norm: Please let us know if you add anything else, some tools (like my vim > extension) > will need to tweaked. How would this be affected if we put the list into the $t comment? Norm -- 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/243e067c-7fc3-468d-8a82-7dcd02b39e88%40googlegroups.com.
