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, 29 Jun 1993 09:43:04 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA16018;
          Tue, 29 Jun 93 01:31:10 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from toadflax.cs.ucdavis.edu by ted.cs.uidaho.edu (16.6/1.34) 
          id AA16013; Tue, 29 Jun 93 01:31:06 -0700
Received: by toadflax.cs.ucdavis.edu (4.1/UCD.CS.2.3) id AA01632;
          Tue, 29 Jun 93 01:31:32 PDT
Date: Tue, 29 Jun 93 01:31:32 PDT
From: shaw@cs.ucdavis.edu (Rob Shaw)
Message-Id: <9306290831.AA01632@toadflax.cs.ucdavis.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: not quite SPEC_TAC


Hello,

This one should be pretty simple. Suppose that I have a goal which contains
many similar subterms, say "f(g(x))". I want to replace all the "f(g(x))"
with "y" (some completely free name), and also gain the assumption that
[" y = f(g(x)) "]. SPEC_TAC does the substitution, but doesn't give me the
assumption. How do I get both?

Thanx!

Rob