Thanks, Norm, for these hints - it could have been expected that the discussion about labels is not new...
Your approach, which I like very much, goes in a similar direction as my suggestion adding titels/names to the theorems, see https://groups.google.com/d/msg/metamath/XPYuatviNV0/C86R2MSqDQAJ. Of course, your approach is more systematic - having advantages (e.g. consistency,verifiability) and disadvantages (e.g. readability for humans, can become very long, especially if fully expanded - for example elfzom1p1elfzo -> "element_finite set of sequential integers_minus_1_plus_1_element_finite set of sequential integers) compared with my suggestion. I wonder, however, where/how the acronym keys are placed. In principle, the three variants of my post mentioned above could be used: 1. First "sentence" of a comment, e.g. $( 3_eq_tr_4_d A deduction from three chained equalities. ... 2. Special parenthetical, e.g. $( (acronym 3_eq_tr_4_d) A deduction from three chained equalities. ... 3. Additional information comment, e.g. $( $j acronym 3_eq_tr_4_d $) $( A deduction from three chained equalities. ... Finally, it is also my opinion not to change the labels, but to use the acronyms in the html pages, either as tooltips (only) or in the pages themselves, as proposed in my post mentioned above: Such an [acronym (maybe fully expanded)] could be used in the HTML outputs, > both in the overview (new column "Title" or "Name" between columns "Label" > and "Description") and for a single theorem (in a new line "Title: ..." > between "Theorem <label>" and "Description: ....") and in the proofs (new > column "Title" or "Name" or "Theorem" between columns "Ref" and > "Expression"). > Alexander -- 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/0d9d245e-fbf9-42c2-8046-6830a6b74f7b%40googlegroups.com.
