Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
X400-Received: by mta relay.pipex.net in /PRMD=pipex/ADMD=cwmail/C=GB/; Relayed;
               Fri, 23 Apr 1993 15:17:46 +0100
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5 text (2));
               Relayed; Fri, 23 Apr 1993 15:16:18 +0100
Date: Fri, 23 Apr 1993 15:16:18 +0100
X400-Originator: R.B.Jones@win0109.wins.icl.co.uk
X400-Recipients: info-hol@ted.cs.uidaho.edu
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012600002543]
Original-Encoded-Information-Types: ia5 text (2),undefined (0)
X400-Content-Type: P2-1984 (2)
Content-Identifier: 2543
From: R.B.Jones@win0109.wins.icl.co.uk
Message-Id: <"2543*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@ted.cs.uidaho.edu
Subject: re: mk_thm


------------------------------ Start of body part 1

Of course mk_thm is very useful, it is much easier to prove
things with it.  But it really does undermine the LCF philosophy
and claims to integrity to make it so easy to take short cuts.
mk_thm can be coded safely if a theory is introduced with the
axiom "F" in it.  The use of a mk_thm coded in this way would be
preferable to the existing mk_thm because any theorems derived

------------------------------ Start of body part 2


using it would need to have the theory as an ancestor, while theories derived
without it need not have the axiom in context.  In this way the system would 
be keeping track of whether mk_thm might have been used.  (You would have to 
inhibit validation of tactics to get anywhere without it, since this uses 
mk_thm, but this wouldn't matter if you were reloading proofs which had 
already been debugged).

However, any user who cares about this can do these changes for himself (which 
ICL did when it was using Cambridge HOL for security applications).

Roger Jones
International Computers Limited

------------------------------ End of body part 2