From lusk Sat Jun 18 09:10:25 1994
Received: from linus.mitre.org (linus.mitre.org [129.83.10.1]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id JAA11902 for <qed@mcs.anl.gov>; Sat, 18 Jun 1994 09:10:03 -0500
Received: from localhost (localhost [127.0.0.1]) by linus.mitre.org (8.6.7/RCF-6S) with ESMTP id KAA19441 for <qed@mcs.anl.gov>; Sat, 18 Jun 1994 10:10:01 -0400
Message-Id: <199406181410.KAA19441@linus.mitre.org>
To: qed@mcs.anl.gov
Subject: Re: Examples 
In-reply-to: Your message of "Fri, 17 Jun 1994 22:31:07 MDT."
             <94Jun17.223123-0600.18656-1@scapa.cs.ualberta.ca> 
Date: Sat, 18 Jun 1994 10:09:59 -0400
From: "F. Javier Thayer" <jt@linus.mitre.org>


>> Could you suggest something?

   I'm not sure what the question is, but I assume you want me to
suggest something that is possible to do from the existing Mizar
library of theorems. Wouldn't a development of the first few chapters
of Dieudonne's book "Foundations of Modern Analysis be" a
possibility?

   I also think Victor Yodaiken's suggestion of "Concrete Mathematics"
is an ambitious, but in my opinion feasible project using any of the
currently existing theorem checkers/provers. THAT would be real eye
catcher don't you think?


Javier Thayer