Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! lusk@mcs.anl.gov) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Sat, 18 Jun 1994 15:13:26 +0100
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