Re: [mizar] Some bugs (or features)

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

On Mon, 12 Sep 2011, Boris Schminke wrote:

> Dear All,
> I've found some strange things. The first one happens when one try to
> [...]
> The second one is a typo in MEASURE2 article
> (http://mizar.org/version/current/html/measure2.html). In the title
> there is a mentioning of discrete categories but there are none of
> them in the article and the title at the FM page. I think that this
> mentioning should be deleted.
  Dear Boris,
  thank you for the information - this subtitle is already removed
and the corrected file will be distributed together with MML ver. 4.169.1133.
The problem is more general - during revisions parts of the text are 
transferred between articles and the original header may not reflect
the actual content of the file.
  Regards,
  Adam Grabowski
  Library Committee of the Association of Mizar Users