Re: [mizar] Private DB

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

Hi Andrzej,

>I agree that for newbies it is disgusting. But in the case of
>advanced work creating the environment is nothing.

I agree a little bit.  This is certainly not the reason that
formalisation is so much work.

But still, I often find that something does not work exactly
the way it should (sometimes when I've already been working on
an article for quite some time), and then after a long search
it turns out that I miss some cluster from an article, which
already turns out to be mentioned in one of the other
directives in the environment!  With a simplified way to
import stuff that kind of confusion very probably wouldn't
have happened.

So, a question: does it ever happen that it is harmful to have
_too many_ articles mentioned in the "environ".  That the
solution to some problem is to _remove_ an article from the
registrations, say?  (If that would ever happen, I would tend
to say with Josef that it would be a problem with the library.)

Freek