Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Sat, 17 Apr 1993 12:52:42 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA08604;
          Sat, 17 Apr 93 04:44:58 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA08599;
          Sat, 17 Apr 93 04:44:52 -0700
Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Sat, 17 Apr 1993 12:44:40 +0100
To: val@com.netcom (Dewey Val Schorre)
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: Worried about mk_tac and the philosophy of ML
In-Reply-To: Your message of Fri, 16 Apr 93 18:41:27 -0700. <9304170141.AA24517@netcom2.netcom.com>
Date: Sat, 17 Apr 93 12:44:35 +0100
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.997:17.04.93.11.44.43"@cl.cam.ac.uk>


> Could not some unscrupulous person post a large HOL file alleging to 
> prove Fermat's Last theorem, but really containing a mk_thm imbedded 

> How can we be sure that nothing like this has happened in our HOL 
> libraries?

Well, I fgrep for mk_thm (and new_axiom) anything put into the
built-in library.  

Note that we *could* get rid of mk_thm in HOL88 --- Proofpower doesn't
have it, nor does HOL90 (I think).  So there's really no need to give
it all up as a bad job and use lisp instead.

Tom