Received: from leopard.cs.byu.edu (leopard.cs.byu.edu [128.187.2.182]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id WAA00107; Mon, 15 Jan 1996 22:38:39 +0200
Received: by leopard.cs.byu.edu
	(1.37.109.15/16.2) id AA146685498; Mon, 15 Jan 1996 12:51:38 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Received: from uu3.psi.com by leopard.cs.byu.edu with SMTP
	(1.37.109.15/16.2) id AA146625495; Mon, 15 Jan 1996 12:51:35 -0700
Received: from cayuga.grammatech.com by uu3.psi.com (5.65b/4.0.940727-PSI/PSINet) via UUCP;
        id AA12798 for ; Mon, 15 Jan 96 14:43:52 -0500
Received: from skaneateles.grammatech.com ([206.233.219.4]) by grammatech.com (4.1/SMI-4.1)
	id AA02115; Mon, 15 Jan 96 14:25:34 EST
Date: Mon, 15 Jan 96 14:25:34 EST
From: paul@grammatech.com (Paul Anderson)
Message-Id: <9601151925.AA02115@grammatech.com>
To: info-hol@leopard.cs.byu.edu
Subject:  general renaming


[ I'm writing from a friend's account - please return email to
drs1004@cl.cam.ac.uk ]

Hi Paul,

Elsa has a function to instantiate variables both in the conclusion and
the assumptions.  It's in the "utils" library in hol90.  I think she
calls it STRONG_INST.

Cheers,
Don

P.S. I don't know if you need this behaviour, but I thought I'd mention
it anyway.  The behaviour is kind of useful for developing abstract
theories.