BTW the way to make the replacement is by using the "/may_grow" option of minimize:
MM> prove dirkentg MM-PA> min ifbieq12d /may_grow Bytes refer to compressed proof size, steps to uncompressed length. Proof of "dirkeritg" remained at 23729 steps using "ifbieq12d". MM-PA> save new_proof /compressed MM-PA> exit Norm On Saturday, December 21, 2019 at 4:59:31 PM UTC-5, Alexander van der Vekens wrote: > > Hi Glauco, > no, I did not replace ifeq123d by ifbieq12d in any proof. Since the > theorems are not identical (they use different class variables), this is > not possible by a simple find&replace. But there is no urgency to replace > ifeq123d by ifbieq12d although ifeq123d is discouraged - the proofs using > ifeq123d are still valid. I marked feq123d as "discouraged" so that it > will/should not be used in additional proofs. > > Alexander > > > On Saturday, December 21, 2019 at 10:42:41 PM UTC+1, Glauco wrote: >> >> Hi Alexander, >> >> I didn't move ~ ifeq123d (because it is already available as ~ ifbieq12d >>> , so I marked ~ ifeq123d as "discouraged") >>> >> >> did you also replace all the references from ifeq123d to ifbieq12d (so >> that my theorems don't refer to a discouraged label, now?) >> >> Thanks >> Glauco >> >> >> >> > -- 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/9dbdb0c2-4fdb-4d96-978f-a1e75c99abf5%40googlegroups.com.
