Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 15 Jun 1993 21:57:41 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA12144;
          Tue, 15 Jun 93 13:48:07 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from Moby.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA12139;
          Tue, 15 Jun 93 13:48:01 -0700
Received: by makaha.cs.ucla.edu (Sendmail 5.61a+YP/2.27) id AA10755;
          Tue, 15 Jun 93 13:48:20 -0700
Date: Tue, 15 Jun 93 13:48:20 -0700
From: toal@cs.ucla.edu (Ray Toal)
Message-Id: <9306152048.AA10755@makaha.cs.ucla.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: A simple question


Hi,

The following question seems simple, but I'm missing something obvious
(I think).  I'd like to extend EXISTS_TAC to instantiate a particular
bound variable, for example

     ?x1 ... xn. t
========================    NEW_EXISTS_TAC xi u
?x1..x(i-1)x(i+1)..xn. t[u/xi]

Usually I use REDUCE or REPEATED_SMART_EXISTS_TAC to do big-step
simplifications of existentially quantified goals, but sometimes
a more delicate tactic is desired.  I think the solution has
something to do with working one's way into the "list" of
bound vars with RAND_CONV o ABS_CONV but I'm stuck.  Any solution
would be much appreciated.

Thanks

Ray Toal