Re: [mizar] Maintenance

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Sun, 3 Nov 2002, Andrzej Trybulec wrote:

> The life will be a bit easier, if we assign proper subjects to messages,
> and try to avoid messages devoted to two different topics. I appreciate
> the valuable contribution of Josef on 'Global choice', but why the
> subject is 'structures'?
> Similarly the last messages related to 'Lexical integrity' are marked
> just 'Puzzle', that is justified only in the case of the first message,
> maybe.

That's what the "refactoring" feature of TWiki is about :-), but TWiki has
died silently, probably. 
As for the structures, my first message was rather on structures, and 
until your reply on 8 Oct, th discussion too. Then you wrote:

> Date: Tue, 08 Oct 2002 23:05:12 +0900
> From: Andrzej Trybulec <trybulec@cs.shinshu-u.ac.jp>
> Reply-To: mizar-forum@mizar.uwb.edu.pl
> To: mizar-forum@mizar.uwb.edu.pl
> Subject: Re: [mizar] structures
>
> Josef Urban wrote:
> 
> > Hi,
> >
> > Discussion about the usage of global choice in the Mizar type system 
> has
> > been revived recently. I believe we should discuss these things
> > publicly, so I resend here some thoughts about the structures in 
> Mizar.
> 
> Josef is right, only he wrote about structures, not about the Global 
> Choice.
> Let me remind what it is about. Actually I wrote few years ago about it. 
> On the Mizar Digest. Maybe a bit more that few, we were still on BITNET.
>
> .....


Regards,
Josef