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 11:04:12 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA16053;
          Tue, 29 Jun 93 02:43:29 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA16048;
          Tue, 29 Jun 93 02:43:24 -0700
Received: from albatross.cl.cam.ac.uk (user sk (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Tue, 29 Jun 1993 10:43:39 +0100
To: shaw@cs.ucdavis.edu (Rob Shaw)
Cc: info-hol@ted.cs.uidaho.edu
Subject: Re: not quite SPEC_TAC
In-Reply-To: Your message of "Tue, 29 Jun 93 01:31:32 PDT." <9306290831.AA01632@toadflax.cs.ucdavis.edu>
Date: Tue, 29 Jun 93 10:43:31 +0100
From: Sara Kalvala <Sara.Kalvala@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:177310:930629094343"@cl.cam.ac.uk>



Hi Rob,

> 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)) "].

Check out the file abbrev_tac.ml in the contrib/btg-tactics directory.


							- Sara