I forgot to mention that currently, the set.mm maintainers are actively renaming many well-known labels (e.g., ffvelrn has been renamed to ffvelcdm). To ensure that Yamma provides better suggestions, I recommend running the "Create Model" command. This step will be less critical once the relabeling project is complete, but for now, it can significantly enhance Yamma's accuracy.
-- 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 visit https://groups.google.com/d/msgid/metamath/a5122392-b4fa-47de-a61c-7314218a0633n%40googlegroups.com.
