Re: [mizar] Private DB

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

Hi Josef,

>I think that one simplified directive like "import all the topology stuff" 
>would at least simplify starting a Mizar article on advanced topics. The 
>practice today is first to think "what article is closest to my topic", 
>and then to copy its environment. If someone new does the mistake of 
>trying to understand the black magic behind environmental directives, he 
>is probably lost as a Mizar author forever. The old directives could 
>remain for fine-tuning if needed.

Ah!  Why not have a directive "copy", that gives you
everything that is in the environment of an existing
article?  Then later you could extend that by adding
"traditional" directives after it.

Or wouldn't that work well, as you only would be able to
extend the notations at the end?

Freek