[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