@benoit and @alexander - Thank you for your comments. Go ahead and import > semigroup (assuming no one else objects). Hopefully, though, I've > communicated my point that we don't want this to lead to flurry of shallow > definitions that people must learn, just to address a perceived difficulty > in understanding the df-* statements (that are technical definitions not > always meant to be read directly by humans). > >
I think you have taken the right decision. Your contributors will be grateful. -- FL -- 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/751ddf1b-388e-49ce-a32c-ec09d8fdaecd%40googlegroups.com.
