Return-Path: 
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from nsf.ac.uk by swan.cl.cam.ac.uk via JANET 
          with NIFTP to fgate (PP) id <891-0@swan.cl.cam.ac.uk>;
          Tue, 26 Mar 1991 23:04:41 +0000
Received: from edu.ucdavis.eecs.iris by sun2.nsfnet-relay.ac.uk 
          with SMTP inbound id <26638-0@sun2.nsfnet-relay.ac.uk>;
          Tue, 26 Mar 1991 23:02:42 +0000
Received: by iris.eecs.ucdavis.edu (5.57/UCD.EECS.4.0) id AA08473;
          Tue, 26 Mar 91 14:59:10 -0800
Received: from research.att.com by clover.eecs.ucdavis.edu (5.59/UCD.EECS.1.11) 
          id AA09285; Tue, 26 Mar 91 15:00:25 PST
Message-Id: <9103262300.AA09285@clover.eecs.ucdavis.edu>
From: elsa@com.att.research
Date: Tue, 26 Mar 91 17:58:53 EST
To: info-hol@edu.ucdavis.clover

In the next file send from me (elsa@research.att.com) is the is the
long-awaited, much delayed latex souce for the Proceedings of HOL3.  It
is moderately long, so I have taken the liberty of tar-compress-uuencoding
it.  To extract the latex source from the the next message you should:

1) Output the message, mail-header and all into a file named

			      HOL3.mail

2) Run the following shell command:

    (uudecode HOL3.mail; uncompress -c HOL3.tex.tar.Z | tar -xf -)


3) Check that you now have a latex file named HOL3.tex, and then
   remove the files HOL3.tex.tar.Z and HOL3.mail.

Now you should be able to run latex (twice) on this file and print out
the resulting dvi file.

With appologies for my tardiness,
				---Elsa L. Gunter