Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 20 Jan 1994 04:45:06 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA12745;
          Wed, 19 Jan 1994 20:44:37 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA12737;
          Wed, 19 Jan 1994 20:44:27 -0700
Received: from panther.cs.byu.edu by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA17876;
          Wed, 19 Jan 1994 19:41:16 -0800
Received: from localhost by panther.cs.byu.edu with SMTP (1.37.109.8/16.2) 
          id AA10250; Wed, 19 Jan 1994 20:41:43 -0700
To: info-hol@cs.uidaho.edu
Subject: X_EXISTS_TAC
Date: Wed, 19 Jan 1994 20:41:43 -0700
From: Phil Windley <windley@leopard.cs.byu.edu>
Message-ID: <"swan.cl.cam.:141450:940120044614"@cl.cam.ac.uk>


Does anyone have a tactic that behaves like EXISTS_TAC but allows you to
pick which existentially quantified variable to provide a witness for?  For
example, suppose I have:

g
"? w x y z . t[w,x,y,z]";;

e(
X_EXISTS_TAC "y" "witness"
);;

would yield

"? w x z . t[w,x,witness,z]"

Of course, a conversion that proves permuting the variables doesn't change
the meaning would be as good.

--phil--