As I recently posted, I believe that all "Metamath 100" results (and thus all they depend on) should eventually move into the main body. After all, all Metamath 100 results are results that at least some others believe are important. I suspect the folks who already produced metamath 100 results would be the best situated for proposing where things go.
So: if you produced a metamath 100 result, but it's currently not in the main body, I would love to see your proposals to start moving their dependencies and the result itself into the main body. If there are many parts, I expect that mini case it would be easier to do it slowly in pieces. There is no rush. That said, I think it's important to keep working on getting more things moved from mathboxes into the main body. Tools like mmj2 only consider items in the main body for many automated steps, and in any case I think it's far more sensible to readers if major results are properly organized in the main body. --- 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/B5CE7EDA-E2C9-4C97-AF2F-1D2D6E249DED%40dwheeler.com.
