Return-Path: 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:17 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA16060; Tue, 29 Jun 93 02:47:34 -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 AA16055; Tue, 29 Jun 93 02:47:29 -0700 Received: from puffin.cl.cam.ac.uk (user btg (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 29 Jun 1993 10:47:42 +0100 To: shaw@cs.ucdavis.edu (Rob Shaw) Cc: info-hol@ted.cs.uidaho.edu, Brian.Graham@cl.cam.ac.uk 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:47:37 +0100 From: Brian Graham Message-Id: <"swan.cl.cam.:177740:930629094746"@cl.cam.ac.uk> > 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? ABBREV_TAC does this, as well as making the substitution in all the assumptions as well. Look in: .../contrib/SECD/TACTICS/ABBREV_TAC.ml ------------------------------------------------------------------------------ Brian Graham | Tel: +44-223-334688 University of Cambridge | Fax: +44-223-334678 Computer Laboratory | Pembroke Street | Email: btg@cl.cam.ac.uk Cambridge, U.K. CB2 3QG |