[mizar] Repetition of an attribute

[Boris Schminke <schminkeba@gmail.com>]

Dear All,
I've noticed that in the POLYALG1 article the definition of the mode
Algebra differs from the cluster registration just above it. Namely,
the attribute unital is repeated twice instead of two different
attributes: unital and scalar-unital. I think that this is a misprint
and it was meant because scalar-unital attribute is essential for an
algebra as a vector space. Moreover, I suppose that this mistake could
be easily made any other time when one have several attributes with
similar denoting symbols. I don't know who to address in such a
situation but I think that it might be useful to add a new error
message to checker ('attribute duplication' or something like this) to
avoid such mistakes in future. And of course, the error in the
POLYALG1 article should be corrected in the nearest revision of the
MML.
Yours,
Boris.