Here my opinion on the topics discussed by Péter and Mario: * I agree with Mario that stars should not be allowed after or within labels, at least if they are used with ~ to auto-link them. By the way, I also cannot find ~ el2v* and ~ el3v* in the latest version of set.mm. * ` $p |- ( A e. V -> ` should not be allowed because $e and $p are not tokens. Wouldn't $p ` |- ( A e. V -> ` be sufficient? * quoted strings longer than a line can be split up. See, for example, ~ numclwwlk7. I think this is a sufficiently good solution.
-- 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/4ca268b3-f13d-4922-be5b-6a4e1748e11cn%40googlegroups.com.
