Re: [mizar] Was it meant to be that way?

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

On Mon, 26 Jan 2004, Piotr Rudnicki wrote:

> Nice piece of advice.  But it was someone else that wrote the
> definition and I only tried to use it.  I could have even heard about
> the default yet I needed an hour to sort it out.  This is a small trap.

The definitional theorems are small traps, especially if the definiens 
consists of several cases. Looking them up with mmlquery takes
considerably less than one hour :-).

Josef