Re: Repetition of an attribute

Adam Grabowski <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <Pine.GSO.4.61.1008300256220.27310@math>
On Sun, 29 Aug 2010, Boris Schminke wrote:

> 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
> <...>
> avoid such mistakes in future. And of course, the error in the
> POLYALG1 article should be corrected in the nearest revision of the
> MML.
   Dear Boris,
   thank you for pointing this out - it was a result of splitting
the attribute VectSp-like into more elementary ones, and it is
of course a misprint done during this revision; luckily the mode itself
is seldom used as most of the work is done by attributes, so the proofs
remain correct. This will be corrected soon.
   Regards,
   Adam Grabowski
   Library Committee of the Association of Mizar Users
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.