Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Mon, 19 Apr 1993 22:30:25 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14551;
          Mon, 19 Apr 93 14:01:57 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA14546;
          Mon, 19 Apr 93 14:01:52 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA27234;
          Mon, 19 Apr 93 14:01:14 -0700
Message-Id: <9304192101.AA27234@maui.cs.ucla.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Re: Worried about mk_tac and the philosophy of ML
Date: Mon, 19 Apr 93 14:01:10 PDT
From: chou@cs.ucla.edu

Tom Melham wrote:

> Note that we *could* get rid of mk_thm in HOL88

But I don't think we should.  One use of mk_thm: if you find one
of your definitions should be changed but it will take 20 minutes
to load everything back from ML source files, what do you do?
Well, you use mk_thm to create the modified version of the
definition and proceed.  Of course, I'm supposing that you know
what you are doing and haven't used the original definition in
any essential way.

I don't think there is anything that can prevent a _determined_
unscrupulous user from doing unscrupulous things.

- Ching Tsun