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

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Mon, Jan 26, 2004 at 09:49:48PM +0100, Josef Urban wrote:
> 
> 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 :-).

That thought crossed my mind, however, I was not connected to the
Internet at the time.  Maybe mmlquery should be distributed as a
standalone utility.  Several GBs are no sweat these days.

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