Re: [mizar] Private DB

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

Hi Josef,

>I quite fear that e.g.
>
>extends JORDAN, OSAFREE;
>notations SCMRING4;
>
>will be even more cryptic to the users than the current
>"rococo", unless the overloading "behaves well".

You have a point there.  Still, I think that even if it's not
perfect, it will be at least much better.  So why not have
this until something even more better comes along?

>and automatically add it all to the "theorems" directive.
>
>And again, problem is that you may also need to add some "constructor" 
>directives for that

So this third proposal was meant to be independent of the
other two.  It _just_ was meant to not have to add stuff to
the theorems line all the time.  So the way I imagine you
would use a system in which the theorems line takes care of
itself, is that you use it _exactly_ like you use the system
today... only you don't have to write the theorems line.

You seem to want to take many improvement steps together, and
then you complain that it will become a mess.  I say: just
take one clear easy step, even when it doesn't get you
_really_ where you want to be.  And then at least it be a
little better.

Freek