Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 20 May 1993 11:41:54 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA00060; Thu, 20 May 93 03:30:42 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA00054; Thu, 20 May 93 03:30:33 -0700 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 20 May 1993 11:30:18 +0100 To: shaw@cs.ucdavis.edu (Rob Shaw) Cc: info-hol@ted.cs.uidaho.edu, Tom.Melham@cl.cam.ac.uk Subject: Re: new_open_axiom ?? In-Reply-To: Your message of "Wed, 19 May 93 20:39:30 PDT." <9305200339.AA02696@toadflax.cs.ucdavis.edu> Date: Thu, 20 May 93 11:30:13 +0100 From: Tom Melham Message-Id: <"swan.cl.cam.:039070:930520103023"@cl.cam.ac.uk> > What is new_open_axiom? It's not in our version 2.0 manuals, and I can't > seem to find it in any of the standard .th files. The HOL88 version 2.01 REFERENCE entry is: new_open_axiom : ((string # term) -> thm) SYNOPSIS This function is for internal use only and is to be deleted from a future version of the system. It should not be used. Actually, in HOL88 this function is part of the "interface" to the underlying code taken from LCF. In HOL90, it appears to name a function that asserts an axiom without closing it up by generalizing free variables. Tom