Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <06688-0@swan.cl.cam.ac.uk>; Sun, 12 Jan 1992 01:49:23 +0000
Received: by ted.cs.uidaho.edu.cs.uidaho.edu (16.6/1.34) id AA20306;
          Sat, 11 Jan 92 17:39:03 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from corton.inria.fr by ted.cs.uidaho.edu.cs.uidaho.edu (16.6/1.34)
          id AA20302; Sat, 11 Jan 92 17:38:56 -0800
Received: from margaux.inria.fr by corton.inria.fr (5.65c8d/91.12.15)
          via Fnet-EUnet id AA24849; Sun, 12 Jan 1992 02:40:55 +0100 (MET)
Original-Received: from
                   localhost.inria.fr by margaux.inria.fr, Sun, 12 Jan 92
                   02:37:15 +0100
PP-warning: Illegal Received field on preceding line
Message-Id: <9201120137.AA05187@margaux.inria.fr>
To: info-hol@edu.uidaho.cs.ted
Subject: Bound Variables
Date: Sun, 12 Jan 92 02:37:12 N
From: murthy@fr.inria.margaux


How are bound variables represented in terms in HOL?  I mean, in the
actual, physical representation of lambda(x.b), are occurrences of "x"
in "b" a string, or a number?

Thanks,
--chet--