Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
From: jimaf@leopard.cs.uidaho.edu (Jim Alves-Foss)
Message-Id: <9304192123.AA27507@leopard.cs.uidaho.edu>
Subject: Re: Worried about mk_tac and the philosophy of ML
To: chou@cs.ucla.edu
Date: Mon, 19 Apr 93 14:23:38 PDT
Cc: info-hol@ted.cs.uidaho.edu
In-Reply-To: <9304192101.AA27234@maui.cs.ucla.edu>; from "chou@cs.ucla.edu" at Apr 19, 93 2:01 pm
Mailer: Elm [revision: 66.33]

> 
> 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.
> 
Personally I create a NEW definition (I modify the name) and
then go on. I can also rerun proofs and definitions that used the
old definition to use the new one.

Phil Windley also suggests that you don't define things immediately
but instead just assume them. Once you are sure that things are correct
you can remove the "definitions" from the assumption list.

> I don't think there is anything that can prevent a _determined_
> unscrupulous user from doing unscrupulous things.
> 
> - Ching Tsun
>
True, BUT there shuold be a way of checking.

-Jim Alves-Foss