Re: [mizar] Two articles are missing

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Hello,

On Thu, 17 Feb 2011, P.S.V.R wrote:

> By analyzing /usr/local/share/mizar/mml.vct via a script I wrote
>
> I found the following two sections, which are mentioned in mml.vct but its corresponding article does not exist in the /usr/local/share/mizar/mml/ directory
>
> AMI_7
> SCMNORM
>
> Seems like a bug in the current distribution.

No, this is not a bug. Looking at the mml.txt file (usually in the 
/usr/local/doc/mizar directory), one may find te following information 
about these two articles:

14.SCMNORM
   Normal Computers
    by Andrzej Trybulec
   Received March 3, 2008
   Has been removed on May 20, 2010

(...)

685. AMI_7
     Input and Output of Instructions
      by Artur Korni{\l}owicz
     Received May 8, 2001
     MML Identifier has been changed into AMISTD_4


The point is that the vocabulary names listed in the mml.vct file do not 
always correspond to Mizar articles, although normally authors of new 
submissions are required to name their vocabulary files in accordance with 
corresponding Mizar articles.

Best regards,

Adam Naumowicz

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================