Re: [mizar] Private DB

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

Hi Josef,

>I do not know what exactly you oppose, since I do not know
>what exactly I propose ;-)

Well, you propose changing how "notations" select the meaning
of a give notation, and I do not think that that is one of the
aspects of Mizar that really needs to be changed at the
moment.  I don't see the problem with it.

So there are other things in Mizar that I would much rather
see changed first.  (My own pet peeves: having a directive
that gives you all the other directives for an article at
once; have "then" be allowed after "consider"; and to be
allowed to have empty types.  This last one is the only
non-trivial of the three, but really it's the thing that I
yearn for most.  In fact this obligatory non-emptyness of
types has stopped me from seriously working with Mizar for
some time now.  I regularly start doing something with Mizar,
hit this problem again, and turn away in disgust.)

>See mml.lar in the Mizar distro (hidden and tarski have to be
>prepended).

Ah, thanks for pointing this out.  (From now on I'll
painstakingly try to put all my directives in mml.lar order :-))

>>for all the directives _but_ notations the order is irrelevant?
>
>I am not sure about the "definitions" directive.

Ah yes, that's another one.

Freek