Re: [mizar] Repetition of an attribute

[Adam Grabowski <adam@math.uwb.edu.pl>]

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