Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <04753-0@swan.cl.cam.ac.uk>; Fri, 28 Feb 1992 16:41:34 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02464;
          Fri, 28 Feb 92 08:17:32 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from scylla.oracorp.com by ted.cs.uidaho.edu (16.6/1.34) id AA02361;
          Fri, 28 Feb 92 08:17:20 -0800
Received: from sparta.oracorp.com by oracorp.com (4.1/2.1-ORA Corporation)
          id AA24235; Fri, 28 Feb 92 11:18:41 EST
Date: Fri, 28 Feb 92 11:18:40 EST
From: shb@com.oracorp
Received: by sparta.oracorp.com (4.1/1.3-ORA Corporation) id AA02689;
          Fri, 28 Feb 92 11:18:40 EST
Message-Id: <9202281618.AA02689@sparta.oracorp.com>
To: info-hol@edu.uidaho.cs.ted
Subject: Partial instantiation

Can someone give me a convenient way of partially instantiating
universally-quantified conclusions?  For x, y, z, t nums I'd like to be
able to go, say, from !x y z t. f(x,y,z,t) to !x y t. f(x,y,3,t).
SPECL doesn't seem to be able to do it, and I'd like to avoid having to
use combinations of SPEC and GEN.

Also, to those of you I promised the sorting utility, it's coming, it's
coming.  We're a small company, we've never given away software before,
and the manager who wants to choose appropriate copyright/disclaimer
statements has more important things to worry about at the moment.  At
least once the policy is set the problem won't arise again.

Steve Brackin
ORA Corporation
Ithaca, NY