Re: [mizar] Private DB

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

Hi Josef,

>The only ambiguity is whether "copy FOO" should only import
>the environment declarations of FOO, or also the theorems,
>clusters, etc. introduced in FOO (btw., the "vocabularies"
>directive is already now pretty inconsistent with the rest of
>directives in this sense). So perhaps "needs", "import", or
>"include" could be less ambiguous (hopefully being understood
>as including FOO as well)?

Maybe "extends"?

Yes, I agree that whatever you call it, it should include the
stuff in the article itself too.

>I sincerely hate this sensitivity of "notations" (and
>"definitions") to the ordering of directives. In my opinion,
>something is wrong with the article, if such tweaking is
>needed.

I don't know: redefinitions are often used to make the typing
of operations more specific, and those redefinitions have to
come after the original definition too.  That's a matter of
ordering on the notations as well, I think?  So it's not just
a matter of choosing non-ambiguous notation.

>One thing is to allow overloaded notation for various parts
>of mathematics, but other thing is to manage the readability
>of that overloading. In my opinion Mizar has gone too far in
>allowing unreadable overloading. It should force authors to
>introduce and use nonambiguous synonyms when clash of
>notation occurs.

I don't know about this, I very much like the freedom that
Mizar gives you to re-use notation all the way you want, I
would hate it if that would be restricted in some way.

Freek