Re: vocabularies

Dear Freek,

we may glue a vocabulary into the article, which one?

There is no clear idea what it is the vocabulary of the article. There 
are two possibilities:

1. historical: the symbols originally invented by the author of an article:
 What it means that somebody invented such symbols as '+' , 'even' or 
'Function' ?
Maybe in the case of such (mode) symbols as  'DnT' or  'N_Sub_set_fam' I 
would like to know who is the guy. :-)

2. pragmatical: the first ( in the order of processing - given on 
MML.LAR) article in which the symbol is used.
It is true, that the names of vocabularies are (mostly) the same as the 
names of articles. It is the result of a revision,
proposed by Piotr Rudnicki.  We put the symbol on a vocabulary with the 
same name as the name of the article in which it was first used.
I was  very suspicious, but Piotr convinced me that it will be helpful 
and he was right.

It is not stable: e.g.
'sequence' is on the vocabulary NORMSP_1 (335)
first used in  NAT_1 (62)
'non-zero' - on the vocabulary ANPROJ_1 (320)
first used in STRUCT_0 (275) and not used in ANPROJ_1 at all!

The number in parentheses is the place of the article on MML.LAR.

I cannot imagine how we could maintain MML with the vocabularies glued 
in the articles.

Regards,
Andrzej

Freek Wiedijk wrote:

>I think I would like the articles to have three parts:
>
>	environ
>	  ...
>	vocabulary
>	  ...
>	begin
>	  ...
>
>So there wouldn't change too much, but there would be
>just one file that one would need to work on, and one
>"name space" that would be shared for naming both articles
>and vocabularies.
>
>For instance we would have (random example):
>
>  :: Some Basic Properties of Sets
>  ::  by Czes{\l}aw Byli\'nski
>  ::
>  :: Received February 1, 1989
>  :: Copyright (c) 1990 Association of Mizar Users
>
>  environ
>
>   vocabularies BOOLE, TARSKI, INCPROJ;
>   notations TARSKI, XBOOLE_0, ENUMSET1;
>   constructors TARSKI, XBOOLE_0, ENUMSET1;
>   registrations XBOOLE_0;
>   definitions TARSKI, XBOOLE_0;
>   theorems TARSKI, XBOOLE_0, ENUMSET1, XBOOLE_1;
>   schemes XBOOLE_0;
>
>  vocabulary
>
>    Rare_c=-comparable
>
>  begin
>
>  reserve v,x,x1,x2,y,y1,y2,z,A,B,X,X1,X2,X3,X4,Y,Y1,Y2,Z,N,M for set;
>
>  registration
>    let x, y be set;
>  [etc. etc.]
>
>I think it would be much better this way.
>
>Freek
>
>  
>