[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Private DB

On Sun, Sep 17, 2006 at 10:22:02PM +0200, Josef Urban wrote:
> 
> 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.

I was under the impression the the Encyclopaedia of Mathematics in Mizar
has been aiming, at least in part, at this goal.

-- 
Piotr Rudnicki        CompSci, University of Alberta, Edmonton, Canada
                      http://web.cs.ualberta.ca/~piotr