On 2/13/20 9:25 AM EST, Benoit wrote [in the "Full 'minimize' run on set.mm" thread]: > > Actually, most *OLD and *ALT should probably have both discouragement > tags as well, it seems ? > > Thanks, > Benoît
*ALT theorems in the full job logs (not just the suspicious proof size decreases that I posted) are creating unnecessary manual cleanup effort to get things to a point where I can run the final minimization. To avoid this problem in the future, I am wondering if it would be acceptable to make Benoit's suggestion mandatory and to have 'verify markup' check for it. Does anyone see any problem in requiring *OLD and *ALT to have both discouragement tags ["(New usage is discouraged.)", "(Proof modification is discouraged.)"] always? Is there ever any reason for not having these tags? (If in some special case an *ALT could benefit from 'minimize' or a proof revision, we can always use '/override' on a custom basis for that purpose.) 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/b4207575-a46f-4bf9-b24d-413aa6906478%40googlegroups.com.
