To check that both tags are provided for *OLD statements is OK. I would feel not comfortable, however, if all ALT theorems/definitions must have both tags. "(New usage is discouraged.)" would be OK, but not "(Proof modification is discouraged.)". I think we have two meanings of ALT: alternate proofs or alternate definitions/variants of theorems. For the first case "(Proof modification is discouraged.)" makes sense, but not for the second case: here I would like to have shorter proofs (found automatically) if possible. A solution could be to provide two separate suffixes: ALTP for "alternate proof", ALT for "alternate definitions/variants of theorems".
-- 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/2e1f06c1-7147-4398-811b-629ab9975712%40googlegroups.com.
