Re: [mizar] vocabullaries

[Freek Wiedijk <freek@cs.ru.nl>]

Dear Andrzej,

>>Of course _I_ always want the vocabulary files to be part
>>of the articles.
>
>Are you really serious about it?

Yes!  Completely serious.

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