On July 4, 2020 5:41:11 PM EDT, 'Stanislas Polu' via Metamath <[email protected]> wrote: >From an ML perspective, this is obviously desirable. We'd be glad to >help with that. Do you have a tentative set of theorems that would be >particularly interesting to "un-minimize"?
Some chained uses of simp instead of specialized therems like simp333 would be a start I think. To be honest, you might be best positioned to answer that question. Have you noticed any specializations that might eventually lead to never using general applications? I don't think we need to start with a large section. Just add a section with a few examples, and then people can propose additions as we go. --- David A.Wheeler -- 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/5B3FF018-13E8-4C17-944E-3842D2C608BF%40dwheeler.com.
