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

Re: [mizar] A quote

Freek:

On Thu, Jan 15, 2004 at 08:22:08PM +0100, Freek Wiedijk wrote:

> I think I agree with this.  With properly automated
> computations you can throw away all of the AXIOMS and [X]REAL_*
> and XCMPLX_* series of articles.  I _hate_ searching through
> those articles for lemmas that I know are there, but that I
> can't find.

Searching these articles drives me nuts at times yet I do not see how
you plan to eliminate them.  Could you elaborate please?

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