Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Message-Id: <199601141544.RAA03952@tanichka.abo.fi>
To: info-hol@leopard.cs.byu.edu
Subject: Re: general renaming
In-Reply-To: Your message of "Fri, 12 Jan 1996 14:53:01 EET."
             <199601122153.AA175523581@jaguar.cs.byu.edu>
Date: Sun, 14 Jan 1996 17:44:12 +0200
From: John Harrison <jharriso@ra.abo.fi>


Paul writes:

| I need to rename (free) variables in theorems, eg,
|         |- a = b
| into
|         |- a = c
|
| Is there function in HOL88 which does this?  I can see
| how to write more own with a few functions, but I
| wanted to reuse if possible.

The INST function will probably do what you want. In the example you
cite one would do:

  INST ["c","b"] <theorem>

However it won't rename the same variable in assumptions; as far as
I know there's no function to do that directly, so you'd have to write
your own.

John.