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