Thanks David. I think there is no hurry in updating the mm100 page (although your proposal sounds good). I would like to clean up some things first and I am away from my main computer this week. As for your remark about labeling, I am starting a new topic. It is true that it would be strange to mention "bj-findis" on the mm_100 page, since this looks like a temporary label.
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/9a2744a3-3a10-4bca-81e9-2291195b5b7d%40googlegroups.com.
