> > When I find myself writing three times the same 5 line proof, then I >> decide to extract a theorem, and almost certainly it could be used to >> shorten a dozen of my previous theorems, but it's hard to go back and >> find/rewrite them all. >> > It's not that hard: place your new theorem as early as possible in set.mm, and then run the script in the github repository "scripts/min.cmd". The file itself contains a comment explaining how to use it.
Benoît -- 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/801861ce-8370-4058-93d5-6ef89d745ec0n%40googlegroups.com.
