Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from iris.eecs.ucdavis.edu by swan.cl.cam.ac.uk with SMTP (PP)
          id <14502-0@swan.cl.cam.ac.uk>; Wed, 21 Aug 1991 19:23:23 +0100
Received: by iris.eecs.ucdavis.edu (5.57/UCD.EECS.7.0) id AA15106;
          Wed, 21 Aug 91 11:11:52 -0700
Received: from vax.nsfnet-relay.ac.uk by sun2.nsfnet-relay.ac.uk
          with SMTP inbound id <18188-2@sun2.nsfnet-relay.ac.uk>;
          Wed, 21 Aug 1991 17:40:47 +0100
Received: from ean-relay.ac.uk by vax.NSFnet-Relay.AC.UK via Ethernet with SMTP
          id ad12886; 21 Aug 91 17:29 BST
Received: from computer-lab.cambridge.ac.uk by Ean-Relay.AC.UK via Janet
          with NIFTP id aa07861; 21 Aug 91 18:26 BST
Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP)
          id <4954-0@swan.cl.cam.ac.uk>; Wed, 21 Aug 1991 16:17:35 +0100
To: garrel@com.oracorp.thorax
Cc: info-hol@edu.ucdavis.eecs.iris
Subject: Re: Alphabetic change of bound variables
In-Reply-To: Your message of Mon, 12 Aug 91 15:08:42 -0400. <9108121908.AA00817@thorax.oracorp.com>
Date: Wed, 21 Aug 91 16:17:17 +0100
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.072:21.07.91.15.18.06"@cl.cam.ac.uk>

The HOL inference rules that deal explicitly with alpha-equivalence are:

   ALPHA, ALPHA_CONV, GEN_ALPHA_CONV

Furthermore, many (most?) rules work "up to alpha-equivalence".  For
example modus ponens:

      |- P ==> Q    |- P'
    ----------------------   [if P' and P are alpha-equivalent]
            |- Q

Tom